let
i
be non
zero
Integer
;
:: thesis:
tan
is
PI
*
i
periodic
i
in
INT
by
INT_1:def 2
;
then
consider
k
being
Nat
such that
A1
: (
i
=
k
or
i
=

k
)
by
INT_1:def 1
;
per
cases
(
i
=
k
or
i
=

k
)
by
A1
;
suppose
i
=
k
;
:: thesis:
tan
is
PI
*
i
periodic
then
ex
m
being
Nat
st
i
=
m
+
1
by
NAT_1:6
;
hence
tan
is
PI
*
i
periodic
by
Lm12
;
:: thesis:
verum
end;
suppose
A2
:
i
=

k
;
:: thesis:
tan
is
PI
*
i
periodic
then
consider
m
being
Nat
such that
A3
:

i
=
m
+
1
by
NAT_1:6
;
tan
is
PI
*
(
m
+
1
)
periodic
by
Lm12
;
then
tan
is

(
PI
*
(
m
+
1
)
)
periodic
by
Th14
;
hence
tan
is
PI
*
i
periodic
by
A2
,
A3
;
:: thesis:
verum
end;
end;