let n be Nat; :: thesis: ( 100 divides n iff ( (digits (n,10)) . 0 = 0 & (digits (n,10)) . 1 = 0 ) )
thus ( 100 divides n implies ( (digits (n,10)) . 0 = 0 & (digits (n,10)) . 1 = 0 ) ) :: thesis: ( (digits (n,10)) . 0 = 0 & (digits (n,10)) . 1 = 0 implies 100 divides n )

proof

assume A1: 100 divides n ; :: thesis: ( (digits (n,10)) . 0 = 0 & (digits (n,10)) . 1 = 0 )
100 = 10 * 10 ;
then 10 divides 100 by INT_1:def 3;
then 10 divides n by A1, INT_2:9;
hence A2: (digits (n,10)) . 0 = 0 by NUMERAL1:7; :: thesis: (digits (n,10)) . 1 = 0

per cases ( not 1 in dom (digits (n,10)) or 1 in dom (digits (n,10)) ) ;

suppose not 1 in dom (digits (n,10)) ; :: thesis: (digits (n,10)) . 1 = 0

hence (digits (n,10)) . 1 = 0 by FUNCT_1:def 2; :: thesis: verum

end;

suppose A3: 1 in dom (digits (n,10)) ; :: thesis: (digits (n,10)) . 1 = 0

dom <%0%> = 1 by AFINSQ_1:def 4;
then digits (n,10) <> <%0%> by A3;
then A4: n <> 0 by NUMERAL1:def 2;
set s = mid ((digits (n,10)),2,(len (digits (n,10))));
10 * 10 divides (10 * (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10))) + 0 by NUMERAL2:19, A2, A1;
then 10 divides value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10) by GROUP_22:1;
then A5: (digits ((value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)),10)) . 0 = 0 by NUMERAL1:7;
A6: 1 < len (digits (n,10)) by A3, AFINSQ_1:86;
2 -' 1 = 2 - 1 by XREAL_0:def 2;
then A7: mid ((digits (n,10)),2,(len (digits (n,10)))) = (digits (n,10)) /^ 1 ;
then A8: len (mid ((digits (n,10)),2,(len (digits (n,10))))) = (len (digits (n,10))) - 1 by A6, AFINSQ_2:7;
then A9: len (mid ((digits (n,10)),2,(len (digits (n,10))))) > 1 - 1 by A6, XREAL_1:9;
then 0 < len (mid ((digits (n,10)),2,(len (digits (n,10))))) ;
then reconsider ls1 = (len (mid ((digits (n,10)),2,(len (digits (n,10)))))) - 1 as Nat by NAT_1:20;
ls1 + 1 = (len (digits (n,10))) - 1 by A8;
then ls1 + 1 < (len (digits (n,10))) - 0 by XREAL_1:15;
then (mid ((digits (n,10)),2,(len (digits (n,10))))) . ((len (mid ((digits (n,10)),2,(len (digits (n,10)))))) - 1) = (digits (n,10)) . ((len (digits (n,10))) - 1) by A8, A7, AFINSQ_2:8;
then A10: (mid ((digits (n,10)),2,(len (digits (n,10))))) . ((len (mid ((digits (n,10)),2,(len (digits (n,10)))))) - 1) <> 0 by A4, NUMERAL1:def 2;
for i being Nat st i in dom (mid ((digits (n,10)),2,(len (digits (n,10))))) holds
(mid ((digits (n,10)),2,(len (digits (n,10))))) . i < 10

proof

let i be Nat; :: thesis: ( i in dom (mid ((digits (n,10)),2,(len (digits (n,10))))) implies (mid ((digits (n,10)),2,(len (digits (n,10))))) . i < 10 )
assume i in dom (mid ((digits (n,10)),2,(len (digits (n,10))))) ; :: thesis: (mid ((digits (n,10)),2,(len (digits (n,10))))) . i < 10
then A11: (mid ((digits (n,10)),2,(len (digits (n,10))))) . i in rng (mid ((digits (n,10)),2,(len (digits (n,10))))) by FUNCT_1:3;
rng (mid ((digits (n,10)),2,(len (digits (n,10))))) c= rng (digits (n,10)) by AFINSQ_2:9;
then (mid ((digits (n,10)),2,(len (digits (n,10))))) . i in rng (digits (n,10)) by A11;
then consider o being object such that
A12: ( o in dom (digits (n,10)) & (mid ((digits (n,10)),2,(len (digits (n,10))))) . i = (digits (n,10)) . o ) by FUNCT_1:def 3;
reconsider o = o as Nat by A12;
thus (mid ((digits (n,10)),2,(len (digits (n,10))))) . i < 10 by A4, A12, NUMERAL1:def 2; :: thesis: verum

end;

then A13: digits ((value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)),10) = mid ((digits (n,10)),2,(len (digits (n,10)))) by A9, A10, Th5;
(digits (n,10)) . (0 + 1) = (mid ((digits (n,10)),2,(len (digits (n,10))))) . 0 by A6, A7, AFINSQ_2:8;
hence (digits (n,10)) . 1 = 0 by A5, A13; :: thesis: verum

end;

end;

end;

assume A14: ( (digits (n,10)) . 0 = 0 & (digits (n,10)) . 1 = 0 ) ; :: thesis: 100 divides n
consider d9 being XFinSequence of NAT such that
A15: ( dom d9 = dom (digits (n,10)) & ( for i being Nat st i in dom d9 holds
d9 . i = ((digits (n,10)) . i) * (10 |^ i) ) & value ((digits (n,10)),10) = Sum d9 ) by NUMERAL1:def 1;

now :: thesis: for i being Nat st i in dom d9 holds
100 divides d9 . i

let i be Nat; :: thesis: ( i in dom d9 implies 100 divides d9 . b₁ )
assume A16: i in dom d9 ; :: thesis: 100 divides d9 . b₁

per cases ( i < 2 or i >= 2 ) ;

suppose i < 2 ; :: thesis: 100 divides d9 . b₁

then ( i = 0 or i = 1 ) by NAT_1:23;
then ( d9 . i = ((digits (n,10)) . 0) * (10 |^ 0) or d9 . i = ((digits (n,10)) . 1) * (10 |^ 1) ) by A16, A15;
hence 100 divides d9 . i by A14, INT_2:12; :: thesis: verum

end;

suppose i >= 2 ; :: thesis: 100 divides d9 . b₁

then reconsider j = i - 2 as Nat by NAT_1:21;
d9 . i = ((digits (n,10)) . i) * (10 |^ (j + 2)) by A15, A16
.= ((digits (n,10)) . i) * ((10 |^ j) * (10 |^ 2)) by NEWTON:8
.= ((digits (n,10)) . i) * ((10 |^ j) * (10 * 10)) by POLYEQ_5:1
.= (((digits (n,10)) . i) * (10 |^ j)) * 100 ;
hence 100 divides d9 . i by INT_1:def 3; :: thesis: verum

end;

end;

end;

then 100 divides Sum d9 by NUMERAL2:16;
then 100 divides value ((digits (n,10)),10) by A15;
hence 100 divides n by NUMERAL1:5; :: thesis: verum