let n be Nat; :: thesis: ( 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 ) :: thesis: ( 2 divides (digits n,10) . 0 implies 2 divides n )

proof

A3: len (digits n,10) >= 1 by Th7;
assume A4: 2 divides n ; :: thesis: 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 ; :: thesis: 2 divides (digits n,10) . 0

then A9: 0 in dom (digits n,10) by NAT_1:45;
A10: 2 divides Sum d by A4, A7, Th8;
len d = 1 by A5, A8;
then d = <%(d . 0 )%> by AFINSQ_1:38;
then Sum d = d . 0 by AFINSQ_2:65
.= ((digits n,10) . 0 ) * (10 |^ 0 ) by A5, A6, A9 ;
then 2 divides ((digits n,10) . 0 ) * 1 by A10, NEWTON:9;
hence 2 divides (digits n,10) . 0 ; :: thesis: verum

end;

suppose A11: len (digits n,10) > 1 ; :: thesis: 2 divides (digits n,10) . 0

then reconsider k = (len (digits n,10)) - 1 as Element of NAT by NAT_1:21;
defpred S₁[ Nat, set ] means $2 = d . ($1 + 1);

A12: now

let l be Nat; :: thesis: ( l in dom <%(d . 0 )%> implies d . l = <%(d . 0 )%> . l )
assume l in dom <%(d . 0 )%> ; :: thesis: d . l = <%(d . 0 )%> . l
then l in 1 by AFINSQ_1:def 5;
then l < 1 by NAT_1:45;
then l = 0 by NAT_1:14;
hence d . l = <%(d . 0 )%> . l by AFINSQ_1:38; :: thesis: verum

end;

A13: for u being Nat st u in k holds
ex x being Element of NAT st S₁[u,x] ;
consider d9 being XFinSequence of NAT such that
A14: ( dom d9 = k & ( for x being Nat st x in k holds
S₁[x,d9 . x] ) ) from STIRL2_1:sch 5(A13);

now

let i be Nat; :: thesis: ( i in dom d9 implies 2 divides d9 . i )
assume A15: i in dom d9 ; :: thesis: 2 divides d9 . i
then i < k by A14, NAT_1:45;
then i + 1 < k + 1 by XREAL_1:10;
then A16: i + 1 in dom d by A5, NAT_1:45;
d9 . i = d . (i + 1) by A14, A15
.= ((digits n,10) . (i + 1)) * (10 |^ (i + 1)) by A6, A16
.= ((digits n,10) . (i + 1)) * ((10 |^ i) * 10) by NEWTON:11
.= 2 * ((((digits n,10) . (i + 1)) * (10 |^ i)) * 5) ;
hence 2 divides d9 . i by NAT_D:def 3; :: thesis: verum

end;

then 2 divides Sum d9 by Th5;
then A17: (Sum d9) mod 2 = 0 by PEPIN:6;

A18: now

let l be Nat; :: thesis: ( l in dom d9 implies d . ((len <%(d . 0 )%>) + l) = d9 . l )
A19: (len <%(d . 0 )%>) + l = l + 1 by AFINSQ_1:38;
assume l in dom d9 ; :: thesis: d . ((len <%(d . 0 )%>) + l) = d9 . l
hence d . ((len <%(d . 0 )%>) + l) = d9 . l by A14, A19; :: thesis: verum

end;

dom d = k + 1 by A5
.= (len <%(d . 0 )%>) + (len d9) by A14, AFINSQ_1:36 ;
then d = <%(d . 0 )%> ^ d9 by A12, A18, AFINSQ_1:def 4;
then Sum d = (Sum <%(d . 0 )%>) + (Sum d9) by AFINSQ_2:67;
then n = (Sum <%(d . 0 )%>) + (Sum d9) by A7, Th8;
then n = (d . 0 ) + (Sum d9) by AFINSQ_2:65;
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, NAT_1:45;
then 2 divides ((digits n,10) . 0 ) * (10 |^ 0 ) by A5, A6, A20;
then 2 divides ((digits n,10) . 0 ) * 1 by NEWTON:9;
hence 2 divides (digits n,10) . 0 ; :: thesis: verum

end;

end;

end;

assume A21: 2 divides (digits n,10) . 0 ; :: thesis: 2 divides n

now

let i be Nat; :: thesis: ( i in dom d implies 2 divides d . b₁ )
assume A22: i in dom d ; :: thesis: 2 divides d . b₁

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: 2 divides d . b₁

then d . i = ((digits n,10) . 0 ) * (10 |^ 0 ) by A1, A22
.= ((digits n,10) . 0 ) * 1 by NEWTON:9 ;
hence 2 divides d . i by A21; :: thesis: verum

end;

suppose i > 0 ; :: thesis: 2 divides d . b₁

then consider j being Nat such that
A23: j + 1 = i by NAT_1:6;
d . i = ((digits n,10) . i) * (10 |^ (j + 1)) by A1, A22, A23
.= ((digits n,10) . i) * ((10 |^ j) * 10) by NEWTON:11
.= 2 * ((((digits n,10) . i) * (10 |^ j)) * 5) ;
hence 2 divides d . i by NAT_D:def 3; :: thesis: verum

end;

end;

end;

then 2 divides value (digits n,10),10 by A2, Th5;
hence 2 divides n by Th8; :: thesis: verum