let n be Nat; ( 2 divides n iff 2 divides (digits (n,10)) . 0 )
consider d being XFinSequence of NAT such that
dom d = dom (digits (n,10))
and
A1:
for i being Nat st i in dom d holds
d . i = ((digits (n,10)) . i) * (10 |^ i)
and
A2:
value ((digits (n,10)),10) = Sum d
by Def1;
thus
( 2 divides n implies 2 divides (digits (n,10)) . 0 )
( 2 divides (digits (n,10)) . 0 implies 2 divides n )proof
A3:
len (digits (n,10)) >= 1
by Th4;
assume A4:
2
divides n
;
2 divides (digits (n,10)) . 0
consider d being
XFinSequence of
NAT such that A5:
dom d = dom (digits (n,10))
and A6:
for
i being
Nat st
i in dom d holds
d . i = ((digits (n,10)) . i) * (10 |^ i)
and A7:
value (
(digits (n,10)),10)
= Sum d
by Def1;
per cases
( len (digits (n,10)) = 1 or len (digits (n,10)) > 1 )
by A3, XXREAL_0:1;
suppose A8:
len (digits (n,10)) = 1
;
2 divides (digits (n,10)) . 0then A9:
0 in dom (digits (n,10))
by AFINSQ_1:86;
A10:
2
divides Sum d
by A4, A7, Th5;
len d = 1
by A5, A8;
then
d = <%(d . 0)%>
by AFINSQ_1:34;
then Sum d =
d . 0
by AFINSQ_2:53
.=
((digits (n,10)) . 0) * (10 |^ 0)
by A5, A6, A9
;
then
2
divides ((digits (n,10)) . 0) * 1
by A10, NEWTON:4;
hence
2
divides (digits (n,10)) . 0
;
verum end; suppose A11:
len (digits (n,10)) > 1
;
2 divides (digits (n,10)) . 0then reconsider k =
(len (digits (n,10))) - 1 as
Element of
NAT by NAT_1:21;
defpred S1[
Nat,
set ]
means $2
= d . ($1 + 1);
A13:
for
u being
Nat st
u in Segm k holds
ex
x being
Element of
NAT st
S1[
u,
x]
;
consider d9 being
XFinSequence of
NAT such that A14:
(
dom d9 = Segm k & ( for
x being
Nat st
x in Segm k holds
S1[
x,
d9 . x] ) )
from STIRL2_1:sch 5(A13);
then
2
divides Sum d9
by Th2;
then A17:
(Sum d9) mod 2
= 0
by PEPIN:6;
dom d =
k + 1
by A5
.=
(len <%(d . 0)%>) + (len d9)
by A14, AFINSQ_1:33
;
then
d = <%(d . 0)%> ^ d9
by A12, A18, AFINSQ_1:def 3;
then
Sum d = (Sum <%(d . 0)%>) + (Sum d9)
by AFINSQ_2:55;
then
n = (Sum <%(d . 0)%>) + (Sum d9)
by A7, Th5;
then
n = (d . 0) + (Sum d9)
by AFINSQ_2:53;
then
((d . 0) + (Sum d9)) mod 2
= 0
by A4, PEPIN:6;
then
(d . 0) mod 2
= 0
by A17, NAT_D:17;
then A20:
2
divides d . 0
by PEPIN:6;
0 in dom (digits (n,10))
by A11, AFINSQ_1:86;
then
2
divides ((digits (n,10)) . 0) * (10 |^ 0)
by A5, A6, A20;
then
2
divides ((digits (n,10)) . 0) * 1
by NEWTON:4;
hence
2
divides (digits (n,10)) . 0
;
verum end; end;
end;
assume A21:
2 divides (digits (n,10)) . 0
; 2 divides n
then
2 divides value ((digits (n,10)),10)
by A2, Th2;
hence
2 divides n
by Th5; verum