let s be Nat; :: thesis: ex n being Nat st
( Sum (digits (n,10)) = s & s divides n )

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

suppose A1: s = 0 ; :: thesis: ex n being Nat st
( Sum (digits (n,10)) = s & s divides n )

take n = 0 ; :: thesis: ( Sum (digits (n,10)) = s & s divides n )
digits (n,10) = <%0%> by NUMERAL1:def 2;
hence Sum (digits (n,10)) = s by A1, AFINSQ_2:53; :: thesis: s divides n
thus s divides n by A1; :: thesis: verum

end;

suppose A2: s > 0 ; :: thesis: ex n being Nat st
( Sum (digits (n,10)) = s & s divides n )

set a = 2 |-count s;
set b = 5 |-count s;
A3: ( 2 |^ (2 |-count s) divides s & 5 |^ (5 |-count s) divides s ) by A2, NAT_3:def 7;
A4: 2 |^ (2 |-count s),5 |^ (5 |-count s) are_coprime by WSIERP_1:11, EULER_1:2, PEPIN:59;
then consider t being Nat such that
A5: s = ((2 |^ (2 |-count s)) * (5 |^ (5 |-count s))) * t by NAT_D:def 3, A3, PEPIN:4;
A6: t divides s by A5;
A7: t <> 0 by A5, A2;
then A8: Euler t <> 0 ;
deffunc H₁() -> set = (s * (Euler t)) + 1;
defpred S₁[ Nat, object ] means ( ( ex l being Nat st
( 1 <= l & l <= s & $1 = l * (Euler t) ) & $2 = 1 ) or ( ( for l being Nat holds
( not 1 <= l or not l <= s or not $1 = l * (Euler t) ) ) & $2 = 0 ) );
A9: for k being Nat st k in H₁() holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in H₁() implies ex x being object st S₁[k,x] )
assume k in H₁() ; :: thesis: ex x being object st S₁[k,x]

per cases ( ex l being Nat st
( 1 <= l & l <= s & k = l * (Euler t) ) or for l being Nat holds
( not 1 <= l or not l <= s or not k = l * (Euler t) ) ) ;

suppose A10: ex l being Nat st
( 1 <= l & l <= s & k = l * (Euler t) ) ; :: thesis: ex x being object st S₁[k,x]

take x = 1; :: thesis: S₁[k,x]
thus S₁[k,x] by A10; :: thesis: verum

end;

suppose A11: for l being Nat holds
( not 1 <= l or not l <= s or not k = l * (Euler t) ) ; :: thesis: ex x being object st S₁[k,x]

take x = 0 ; :: thesis: S₁[k,x]
thus S₁[k,x] by A11; :: thesis: verum

end;

end;

end;

consider d being XFinSequence such that
A12: ( dom d = H₁() & ( for k being Nat st k in H₁() holds
S₁[k,d . k] ) ) from AFINSQ_1:sch 1(A9);
rng d c= NAT

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in rng d or o in NAT )
assume o in rng d ; :: thesis: o in NAT
then consider k being object such that
A13: ( k in dom d & o = d . k ) by FUNCT_1:def 3;
reconsider k = k as Nat by A13;

per cases ( ex l being Nat st
( 1 <= l & l <= s & k = l * (Euler t) ) or for l being Nat holds
( not 1 <= l or not l <= s or not k = l * (Euler t) ) ) ;

suppose ex l being Nat st
( 1 <= l & l <= s & k = l * (Euler t) ) ; :: thesis: o in NAT

then d . k = 1 by A13, A12;
hence o in NAT by A13; :: thesis: verum

end;

suppose for l being Nat holds
( not 1 <= l or not l <= s or not k = l * (Euler t) ) ; :: thesis: o in NAT

then d . k = 0 by A13, A12;
hence o in NAT by A13; :: thesis: verum

end;

end;

end;

then reconsider d = d as XFinSequence of NAT by RELAT_1:def 19;
A14: s >= 0 + 1 by A2, NAT_1:13;
then 1 * (Euler t) < (s * (Euler t)) + 1 by NAT_1:13, XREAL_1:64;
then A15: 1 * (Euler t) in Segm H₁() by NAT_1:44;
then A16: d . (1 * (Euler t)) = 1 by A14, A12;
set o = value (d,10);
consider e being XFinSequence of NAT such that
A17: ( dom e = dom d & ( for i being Nat st i in dom e holds
e . i = (d . i) * (10 |^ i) ) & value (d,10) = Sum e ) by NUMERAL1:def 1;
e . (Euler t) = 1 * (10 |^ (Euler t)) by A17, A12, A15, A16;
then A18: value (d,10) > 0 by A17, A12, A15, AFINSQ_2:61;
take n = (10 |^ ((2 |-count s) + (5 |-count s))) * (value (d,10)); :: thesis: ( Sum (digits (n,10)) = s & s divides n )
s * (Euler t) < (s * (Euler t)) + 1 by NAT_1:13;
then s * (Euler t) in Segm H₁() by NAT_1:44;
then A19: d . ((len d) - 1) <> 0 by A12, A14;

now :: thesis: for i being Nat st i in dom d holds
d . i < 10

let i be Nat; :: thesis: ( i in dom d implies d . b₁ < 10 )
assume i in dom d ; :: thesis: d . b₁ < 10

per cases then ( ( ex l being Nat st
( 1 <= l & l <= s & i = l * (Euler t) ) & d . i = 1 ) or ( ( for l being Nat holds
( not 1 <= l or not l <= s or not i = l * (Euler t) ) ) & d . i = 0 ) ) by A12;

suppose ( ex l being Nat st
( 1 <= l & l <= s & i = l * (Euler t) ) & d . i = 1 ) ; :: thesis: d . b₁ < 10

hence d . i < 10 ; :: thesis: verum

end;

suppose ( ( for l being Nat holds
( not 1 <= l or not l <= s or not i = l * (Euler t) ) ) & d . i = 0 ) ; :: thesis: d . b₁ < 10

hence d . i < 10 ; :: thesis: verum

end;

end;

end;

then A20: digits ((value (d,10)),10) = d by NUMBER11:5, A12, A19;
rng d c= {0,1}

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in rng d or o in {0,1} )
assume o in rng d ; :: thesis: o in {0,1}
then consider k being object such that
A21: ( k in dom d & o = d . k ) by FUNCT_1:def 3;
reconsider k = k as Nat by A21;

per cases ( ex l being Nat st
( 1 <= l & l <= s & k = l * (Euler t) ) or for l being Nat holds
( not 1 <= l or not l <= s or not k = l * (Euler t) ) ) ;

suppose ex l being Nat st
( 1 <= l & l <= s & k = l * (Euler t) ) ; :: thesis: o in {0,1}

then d . k = 1 by A21, A12;
hence o in {0,1} by A21, TARSKI:def 2; :: thesis: verum

end;

suppose for l being Nat holds
( not 1 <= l or not l <= s or not k = l * (Euler t) ) ; :: thesis: o in {0,1}

then d . k = 0 by A21, A12;
hence o in {0,1} by A21, TARSKI:def 2; :: thesis: verum

end;

end;

end;

then A22: Sum d = 1 * (card (d " {1})) by AFINSQ_2:68;
deffunc H₂( Nat) -> set = ($1 + 1) * (Euler t);
consider f being XFinSequence such that
A23: ( len f = s & ( for k being Nat st k in s holds
f . k = H₂(k) ) ) from AFINSQ_1:sch 2();
A24: rng f = d " {1}

proof

thus rng f c= d " {1} :: according to XBOOLE_0:def 10 :: thesis: d " {1} c= rng f

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in rng f or o in d " {1} )
assume o in rng f ; :: thesis: o in d " {1}
then consider u being object such that
A25: ( u in dom f & o = f . u ) by FUNCT_1:def 3;
reconsider u = u as Nat by A25;
A26: 0 + 1 <= u + 1 by XREAL_1:6;
u in Segm s by A25, A23;
then u < s by NAT_1:44;
then A27: u + 1 <= s by NAT_1:13;
then (u + 1) * (Euler t) < H₁() by NAT_1:13, XREAL_1:64;
then A28: (u + 1) * (Euler t) in Segm H₁() by NAT_1:44;
then d . ((u + 1) * (Euler t)) = 1 by A26, A27, A12;
then d . ((u + 1) * (Euler t)) in {1} by TARSKI:def 1;
then (u + 1) * (Euler t) in d " {1} by A12, A28, FUNCT_1:def 7;
hence o in d " {1} by A23, A25; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in d " {1} or o in rng f )
assume o in d " {1} ; :: thesis: o in rng f
then ( o in dom d & d . o in {1} ) by FUNCT_1:def 7;
then consider l being Nat such that
A29: ( 1 <= l & l <= s & o = l * (Euler t) ) by A12;
A30: (l -' 1) + 1 = (l - 1) + 1 by A29, XREAL_1:233;
then l -' 1 < s by A29, NAT_1:13;
then A31: l -' 1 in Segm s by NAT_1:44;
then o = f . (l -' 1) by A29, A23, A30;
hence o in rng f by A23, A31, FUNCT_1:3; :: thesis: verum

end;

f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume A32: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then reconsider X1 = x1, X2 = x2 as Nat ;
( f . X1 = (X1 + 1) * (Euler t) & f . X2 = (X2 + 1) * (Euler t) ) by A32, A23;
then X1 + 1 = X2 + 1 by XCMPLX_1:5, A8, A32;
hence x1 = x2 ; :: thesis: verum

end;

then s,d " {1} are_equipotent by A23, A24, WELLORD2:def 4;
then A33: card s = card (d " {1}) by CARD_1:5;
digits (n,10) = (((2 |-count s) + (5 |-count s)) --> 0) ^ (digits ((value (d,10)),10)) by Th55, A18;
hence Sum (digits (n,10)) = (Sum (((2 |-count s) + (5 |-count s)) --> 0)) + (Sum (digits ((value (d,10)),10))) by AFINSQ_2:55
.= (((2 |-count s) + (5 |-count s)) * 0) + s by AFINSQ_2:58, A20, A22, A33
.= s ;
:: thesis: s divides n
10 = 5 * 2 ;
then A34: 2 |^ (2 |-count s) divides 10 |^ (2 |-count s) by NEWTON02:15, INT_1:def 3;
(2 |-count s) + 0 <= (2 |-count s) + (5 |-count s) by XREAL_1:7;
then 10 |^ (2 |-count s) divides 10 |^ ((2 |-count s) + (5 |-count s)) by NEWTON:89;
then A35: 2 |^ (2 |-count s) divides 10 |^ ((2 |-count s) + (5 |-count s)) by A34, INT_2:9;
10 = 5 * 2 ;
then A36: 5 |^ (5 |-count s) divides 10 |^ (5 |-count s) by NEWTON02:15, INT_1:def 3;
0 + (5 |-count s) <= (2 |-count s) + (5 |-count s) by XREAL_1:7;
then 10 |^ (5 |-count s) divides 10 |^ ((2 |-count s) + (5 |-count s)) by NEWTON:89;
then 5 |^ (5 |-count s) divides 10 |^ ((2 |-count s) + (5 |-count s)) by A36, INT_2:9;
then A37: (2 |^ (2 |-count s)) * (5 |^ (5 |-count s)) divides 10 |^ ((2 |-count s) + (5 |-count s)) by A35, A4, PEPIN:4;
t divides value (d,10)

proof

per cases ( t = 0 or t = 1 or t >= 1 + 1 ) by NAT_1:23;

suppose t = 0 ; :: thesis: t divides value (d,10)

hence t divides value (d,10) by A5, A2; :: thesis: verum

end;

suppose t = 1 ; :: thesis: t divides value (d,10)

hence t divides value (d,10) by NAT_D:6; :: thesis: verum

end;

suppose t >= 1 + 1 ; :: thesis: t divides value (d,10)

then A38: t > 1 by NAT_1:13;
A39: 2,t are_coprime

proof

assume not 2,t are_coprime ; :: thesis: contradiction
then A40: 2 gcd t <> 1 ;
( 2 gcd t divides 2 & 2 gcd t divides t ) by INT_2:21;
then 2 divides t by A40, INT_2:28;
then consider t2 being Nat such that
A41: t = 2 * t2 by NAT_D:def 3;
s = (((2 |^ (2 |-count s)) * 2) * (5 |^ (5 |-count s))) * t2 by A5, A41
.= ((2 |^ ((2 |-count s) + 1)) * (5 |^ (5 |-count s))) * t2 by NEWTON:6
.= (2 |^ ((2 |-count s) + 1)) * ((5 |^ (5 |-count s)) * t2) ;
then 2 |^ ((2 |-count s) + 1) divides s ;
hence contradiction by A2, NAT_3:def 7; :: thesis: verum

end;

5,t are_coprime

proof

assume not 5,t are_coprime ; :: thesis: contradiction
then A42: 5 gcd t <> 1 ;
( 5 gcd t divides 5 & 5 gcd t divides t ) by INT_2:21;
then 5 divides t by A42, PEPIN:59;
then consider t5 being Nat such that
A43: t = 5 * t5 by NAT_D:def 3;
s = (((5 |^ (5 |-count s)) * 5) * (2 |^ (2 |-count s))) * t5 by A5, A43
.= ((5 |^ ((5 |-count s) + 1)) * (2 |^ (2 |-count s))) * t5 by NEWTON:6
.= (5 |^ ((5 |-count s) + 1)) * ((2 |^ (2 |-count s)) * t5) ;
then 5 |^ ((5 |-count s) + 1) divides s ;
hence contradiction by A2, NAT_3:def 7; :: thesis: verum

end;

then A44: 2 * 5,t are_coprime by INT_2:26, A39;

now :: thesis: for i being Nat st i in dom e holds
d . i = (e . i) mod t

let i be Nat; :: thesis: ( i in dom e implies d . b₁ = (e . b₁) mod t )
assume A45: i in dom e ; :: thesis: d . b₁ = (e . b₁) mod t

per cases ( ex l being Nat st
( 1 <= l & l <= s & i = l * (Euler t) ) or for l being Nat holds
( not 1 <= l or not l <= s or not i = l * (Euler t) ) ) ;

suppose ex l being Nat st
( 1 <= l & l <= s & i = l * (Euler t) ) ; :: thesis: d . b₁ = (e . b₁) mod t

then consider l being Nat such that
A46: ( 1 <= l & l <= s & i = l * (Euler t) ) ;
d . i = 1 by A45, A12, A17, A46;
then e . i = 1 * (10 |^ (l * (Euler t))) by A46, A17, A45
.= (10 |^ (Euler t)) |^ l by NEWTON:9 ;
then (e . i) mod t = (((10 |^ (Euler t)) mod t) |^ l) mod t by EULER_2:22
.= (1 |^ l) mod t by A44, A38, EULER_2:18
.= 1 by A38, NAT_D:14 ;
hence d . i = (e . i) mod t by A45, A12, A17, A46; :: thesis: verum

end;

suppose A47: for l being Nat holds
( not 1 <= l or not l <= s or not i = l * (Euler t) ) ; :: thesis: d . b₁ = (e . b₁) mod t

then d . i = 0 by A45, A12, A17;
then e . i = 0 * (10 |^ i) by A17, A45;
hence d . i = (e . i) mod t by A47, A45, A12, A17; :: thesis: verum

end;

end;

end;

then (Sum e) mod t = s mod t by A22, A33, NUMERAL2:17, A17
.= 0 by A6 ;
hence t divides value (d,10) by A17, A7, PEPIN:6; :: thesis: verum

end;

end;

end;

hence s divides n by NAT_3:1, A37, A5; :: thesis: verum

end;

end;