let n0 be non zero Nat; :: thesis: Sum (Euler_phi | (NatDivisors n0)) = n0
( dom Euler_phi = NAT & rng Euler_phi c= REAL ) by FUNCT_2:def 1;
then reconsider EU9 = Euler_phi as sequence of REAL by FUNCT_2:2;
set X = Seg n0;
defpred S₁[ set , set ] means $2 = { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & $1 in NatDivisors n0 & h = $1 & i gcd n0 = n0 / h ) } ;
A1: dom Euler_phi = NAT by FUNCT_2:def 1;
A2: for k being Nat st k in Seg n0 holds
ex x being Element of bool (Seg n0) st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg n0 implies ex x being Element of bool (Seg n0) st S₁[k,x] )
set X9 = { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & k in NatDivisors n0 & h = k & i gcd n0 = n0 / h ) } ;
for x being object st x in { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & k in NatDivisors n0 & h = k & i gcd n0 = n0 / h ) } holds
x in Seg n0

proof

let x be object ; :: thesis: ( x in { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & k in NatDivisors n0 & h = k & i gcd n0 = n0 / h ) } implies x in Seg n0 )
assume x in { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & k in NatDivisors n0 & h = k & i gcd n0 = n0 / h ) } ; :: thesis: x in Seg n0
then ex i being Element of NAT st
( i = x & ex h being Nat st
( i in Seg n0 & k in NatDivisors n0 & h = k & i gcd n0 = n0 / h ) ) ;
hence x in Seg n0 ; :: thesis: verum

end;

then reconsider X9 = { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & k in NatDivisors n0 & h = k & i gcd n0 = n0 / h ) } as Element of bool (Seg n0) by TARSKI:def 3;
assume k in Seg n0 ; :: thesis: ex x being Element of bool (Seg n0) st S₁[k,x]
take X9 ; :: thesis: S₁[k,X9]
thus S₁[k,X9] ; :: thesis: verum

end;

consider fp being FinSequence of bool (Seg n0) such that
A3: ( dom fp = Seg n0 & ( for k being Nat st k in Seg n0 holds
S₁[k,fp . k] ) ) from FINSEQ_1:sch 5(A2);
A4: NatDivisors n0 c= Seg n0 by MOEBIUS1:40;
then A5: rng (Sgm (NatDivisors n0)) c= dom fp by A3, FINSEQ_1:def 14;
then A6: rng (Sgm (NatDivisors n0)) c= dom (Card fp) by CARD_3:def 2;
then reconsider f1 = (Card fp) * (Sgm (NatDivisors n0)) as FinSequence of NAT by Th9;
A7: NatDivisors n0 c= dom fp by A3, MOEBIUS1:40;
A8: dom ((Card fp) * (Sgm (NatDivisors n0))) = dom (Sgm (NatDivisors n0)) by A6, RELAT_1:27
.= dom (Euler_phi * (Sgm (NatDivisors n0))) by A5, A1, RELAT_1:27, XBOOLE_1:1 ;
for k being Element of NAT st k in dom ((Card fp) * (Sgm (NatDivisors n0))) holds
((Card fp) * (Sgm (NatDivisors n0))) . k = (Euler_phi * (Sgm (NatDivisors n0))) . k

proof

let k be Element of NAT ; :: thesis: ( k in dom ((Card fp) * (Sgm (NatDivisors n0))) implies ((Card fp) * (Sgm (NatDivisors n0))) . k = (Euler_phi * (Sgm (NatDivisors n0))) . k )
set k9 = (Sgm (NatDivisors n0)) . k;
set Y = { l where l is Element of NAT : ( (Sgm (NatDivisors n0)) . k,l are_coprime & l >= 1 & l <= (Sgm (NatDivisors n0)) . k ) } ;
set Z = { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } ;
deffunc H₁( Nat) -> set = ($1 * n0) / ((Sgm (NatDivisors n0)) . k);
A9: for x being object st x in { l where l is Element of NAT : ( (Sgm (NatDivisors n0)) . k,l are_coprime & l >= 1 & l <= (Sgm (NatDivisors n0)) . k ) } holds
x in NAT

proof

let x be object ; :: thesis: ( x in { l where l is Element of NAT : ( (Sgm (NatDivisors n0)) . k,l are_coprime & l >= 1 & l <= (Sgm (NatDivisors n0)) . k ) } implies x in NAT )
assume x in { l where l is Element of NAT : ( (Sgm (NatDivisors n0)) . k,l are_coprime & l >= 1 & l <= (Sgm (NatDivisors n0)) . k ) } ; :: thesis: x in NAT
then ex l being Element of NAT st
( x = l & (Sgm (NatDivisors n0)) . k,l are_coprime & l >= 1 & l <= (Sgm (NatDivisors n0)) . k ) ;
hence x in NAT ; :: thesis: verum

end;

assume A10: k in dom ((Card fp) * (Sgm (NatDivisors n0))) ; :: thesis: ((Card fp) * (Sgm (NatDivisors n0))) . k = (Euler_phi * (Sgm (NatDivisors n0))) . k
then k in dom (Sgm (NatDivisors n0)) by FUNCT_1:11;
then (Sgm (NatDivisors n0)) . k in rng (Sgm (NatDivisors n0)) by FUNCT_1:3;
then A11: (Sgm (NatDivisors n0)) . k in NatDivisors n0 by FINSEQ_1:def 14;
then A12: 1 <= (Sgm (NatDivisors n0)) . k by A3, A7, FINSEQ_1:1;
(Sgm (NatDivisors n0)) . k,1 are_coprime by WSIERP_1:9;
then 1 in { l where l is Element of NAT : ( (Sgm (NatDivisors n0)) . k,l are_coprime & l >= 1 & l <= (Sgm (NatDivisors n0)) . k ) } by A12;
then reconsider Y = { l where l is Element of NAT : ( (Sgm (NatDivisors n0)) . k,l are_coprime & l >= 1 & l <= (Sgm (NatDivisors n0)) . k ) } as non empty Subset of NAT by A9, TARSKI:def 3;
consider f being Function such that
A13: ( dom f = Y & ( for d being Element of Y holds f . d = H₁(d) ) ) from FUNCT_1:sch 4();
for y being object holds
( y in rng f iff y in { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } )

proof

let y be object ; :: thesis: ( y in rng f iff y in { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } )

hereby :: thesis: ( y in { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } implies y in rng f )

assume y in rng f ; :: thesis: y in { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) }
then consider x being object such that
A14: x in dom f and
A15: y = f . x by FUNCT_1:def 3;
reconsider x = x as Element of Y by A13, A14;
A16: 0 < (Sgm (NatDivisors n0)) . k by A11;
(Sgm (NatDivisors n0)) . k divides n0 by A11, MOEBIUS1:39;
then consider j being Nat such that
A17: n0 = ((Sgm (NatDivisors n0)) . k) * j by NAT_D:def 3;
y = H₁(x) by A13, A15
.= x * (n0 / ((Sgm (NatDivisors n0)) . k)) by XCMPLX_1:74 ;
then A18: y = x * (j / (((Sgm (NatDivisors n0)) . k) / ((Sgm (NatDivisors n0)) . k))) by A17, XCMPLX_1:77
.= x * (j / 1) by A16, XCMPLX_1:60
.= x * j ;
then reconsider i = y as Element of NAT by ORDINAL1:def 12;
x in Y ;
then consider l being Element of NAT such that
A19: x = l and
A20: (Sgm (NatDivisors n0)) . k,l are_coprime and
A21: l >= 1 and
A22: l <= (Sgm (NatDivisors n0)) . k ;
A23: x * j <= ((Sgm (NatDivisors n0)) . k) * j by A19, A22, XREAL_1:64;
j <> 0 by A17;
then j + 1 > 0 + 1 by XREAL_1:6;
then 1 <= j by NAT_1:13;
then 1 * 1 <= x * j by A19, A21, XREAL_1:66;
then A24: i in Seg n0 by A17, A18, A23;
A25: ((Sgm (NatDivisors n0)) . k) gcd l = 1 by A20, INT_2:def 3;
n0 / ((Sgm (NatDivisors n0)) . k) = j / (((Sgm (NatDivisors n0)) . k) / ((Sgm (NatDivisors n0)) . k)) by A17, XCMPLX_1:77
.= j / 1 by A16, XCMPLX_1:60 ;
then i gcd n0 = n0 / ((Sgm (NatDivisors n0)) . k) by A19, A17, A18, A25, EULER_1:5;
hence y in { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } by A11, A24; :: thesis: verum

end;

assume y in { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } ; :: thesis: y in rng f
then consider i being Element of NAT such that
A26: i = y and
A27: ex h being Nat st
( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) ;
i gcd n0 divides i by INT_2:def 2;
then consider x being Nat such that
A28: i = (i gcd n0) * x by NAT_D:def 3;
A29: y = (x * n0) / ((Sgm (NatDivisors n0)) . k) by A26, A27, A28, XCMPLX_1:74;
reconsider x = x as Element of NAT by ORDINAL1:def 12;
A30: (Sgm (NatDivisors n0)) . k <> 0 by A27;
A31: ((Sgm (NatDivisors n0)) . k) * (i gcd n0) = n0 / (((Sgm (NatDivisors n0)) . k) / ((Sgm (NatDivisors n0)) . k)) by A27, XCMPLX_1:81
.= n0 / 1 by A30, XCMPLX_1:60 ;
then A32: (Sgm (NatDivisors n0)) . k,x are_coprime by A27, A28, EULER_1:6;
x <> 0 by A27, A28, FINSEQ_1:1;
then x + 1 > 0 + 1 by XREAL_1:6;
then A33: x >= 1 by NAT_1:13;
i <= n0 by A27, FINSEQ_1:1;
then x <= (Sgm (NatDivisors n0)) . k by A27, A28, A31, XREAL_1:68;
then x in dom f by A13, A32, A33;
then reconsider x = x as Element of Y by A13;
y = f . x by A13, A29;
hence y in rng f by A13, FUNCT_1:def 3; :: thesis: verum

end;

then A34: rng f = { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } by TARSKI:2;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume x1 in dom f ; :: thesis: ( not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
then reconsider x19 = x1 as Element of Y by A13;
assume x2 in dom f ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
then reconsider x29 = x2 as Element of Y by A13;
assume A35: f . x1 = f . x2 ; :: thesis: x1 = x2
A36: H₁(x19) = f . x19 by A13
.= H₁(x29) by A13, A35 ;
x19 * (n0 / ((Sgm (NatDivisors n0)) . k)) = (x19 * n0) / ((Sgm (NatDivisors n0)) . k) by XCMPLX_1:74
.= x29 * (n0 / ((Sgm (NatDivisors n0)) . k)) by A36, XCMPLX_1:74 ;
hence x1 = x2 by A12, XCMPLX_1:5; :: thesis: verum

end;

then f is one-to-one by FUNCT_1:def 4;
then A37: Y, { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } are_equipotent by A13, A34, WELLORD2:def 4;
fp . ((Sgm (NatDivisors n0)) . k) = { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } by A3, A7, A11;
then card (fp . ((Sgm (NatDivisors n0)) . k)) = card Y by A37, CARD_1:5;
then (Card fp) . ((Sgm (NatDivisors n0)) . k) = Euler ((Sgm (NatDivisors n0)) . k) by A7, A11, CARD_3:def 2;
then A38: (Card fp) . ((Sgm (NatDivisors n0)) . k) = Euler_phi . ((Sgm (NatDivisors n0)) . k) by Def7;
((Card fp) * (Sgm (NatDivisors n0))) . k = (Card fp) . ((Sgm (NatDivisors n0)) . k) by A10, FUNCT_1:12;
hence ((Card fp) * (Sgm (NatDivisors n0))) . k = (Euler_phi * (Sgm (NatDivisors n0))) . k by A8, A10, A38, FUNCT_1:12; :: thesis: verum

end;

then A39: (Card fp) * (Sgm (NatDivisors n0)) = Euler_phi * (Sgm (NatDivisors n0)) by A8, PARTFUN1:5;
set k = len fp;
A40: Func_Seq (Euler_phi,(Sgm (NatDivisors n0))) = Euler_phi * (Sgm (NatDivisors n0)) by BHSP_5:def 4
.= Func_Seq (EU9,(Sgm (NatDivisors n0))) by BHSP_5:def 4 ;
A41: for x being object holds
( x in NatDivisors n0 iff ( x in Seg n0 & not x in (Card fp) " {0} ) )

proof

reconsider y = 0 as Element of NAT ;
let x be object ; :: thesis: ( x in NatDivisors n0 iff ( x in Seg n0 & not x in (Card fp) " {0} ) )
A42: y in {0} by TARSKI:def 1;

hereby :: thesis: ( x in Seg n0 & not x in (Card fp) " {0} implies x in NatDivisors n0 )

assume A43: x in NatDivisors n0 ; :: thesis: ( x in Seg n0 & not x in (Card fp) " {0} )
then reconsider k = x as Element of NAT ;
thus x in Seg n0 by A4, A43; :: thesis: not x in (Card fp) " {0}
assume x in (Card fp) " {0} ; :: thesis: contradiction
then consider y being object such that
A44: ( [x,y] in Card fp & y in {0} ) by RELAT_1:def 14;
( y = 0 & y = (Card fp) . x ) by A44, FUNCT_1:1, TARSKI:def 1;
then card (fp . x) = {} by A3, A4, A43, CARD_3:def 2;
then A45: fp . x = {} ;
k divides n0 by A43, MOEBIUS1:39;
then consider i being Nat such that
A46: n0 = k * i by NAT_D:def 3;
i <> 0 by A46;
then 0 + 1 < i + 1 by XREAL_1:6;
then A47: 1 <= i by NAT_1:13;
A48: i divides n0 by A46, NAT_D:def 3;
then i <= n0 by NAT_D:7;
then A49: i in Seg n0 by A47;
A50: k <> 0 by A46;
n0 = k * (i gcd n0) by A46, A48, NEWTON:49;
then n0 / k = (i gcd n0) * (k / k) by XCMPLX_1:74
.= (i gcd n0) * 1 by A50, XCMPLX_1:60 ;
then i in { i9 where i9 is Element of NAT : ex h being Nat st
( i9 in Seg n0 & k in NatDivisors n0 & h = k & i9 gcd n0 = n0 / h ) } by A43, A49;
hence contradiction by A3, A4, A43, A45; :: thesis: verum

end;

assume A51: x in Seg n0 ; :: thesis: ( x in (Card fp) " {0} or x in NatDivisors n0 )
then reconsider k = x as Element of NAT ;
A52: fp . k = { i9 where i9 is Element of NAT : ex h being Nat st
( i9 in Seg n0 & k in NatDivisors n0 & h = k & i9 gcd n0 = n0 / h ) } by A3, A51;
assume A53: not x in (Card fp) " {0} ; :: thesis: x in NatDivisors n0
assume A54: not x in NatDivisors n0 ; :: thesis: contradiction
fp . k = {}

proof

assume fp . k <> {} ; :: thesis: contradiction
then consider x9 being object such that
A55: x9 in fp . k by XBOOLE_0:def 1;
ex i being Element of NAT st
( x9 = i & ex h being Nat st
( i in Seg n0 & k in NatDivisors n0 & h = k & i gcd n0 = n0 / h ) ) by A52, A55;
hence contradiction by A54; :: thesis: verum

end;

then A56: y = (Card fp) . x by A3, A51, CARD_1:27, CARD_3:def 2;
x in dom (Card fp) by A3, A51, CARD_3:def 2;
then [k,y] in Card fp by A56, FUNCT_1:1;
hence contradiction by A53, A42, RELSET_1:30; :: thesis: verum

end;

reconsider f29 = Card fp as FinSequence of REAL by Th13;
reconsider f19 = f1 as FinSequence of REAL by Th13;
Seg n0 = dom (Card fp) by A3, CARD_3:def 2;
then f19 = f29 - {0} by A41, XBOOLE_0:def 5;
then A58: Sum f19 = Sum f29 by Th12;
A59: for d, e being Nat st d in dom fp & e in dom fp & d <> e holds
fp . d misses fp . e

proof

let d, e be Nat; :: thesis: ( d in dom fp & e in dom fp & d <> e implies fp . d misses fp . e )
assume d in dom fp ; :: thesis: ( not e in dom fp or not d <> e or fp . d misses fp . e )
then A60: fp . d = { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & d in NatDivisors n0 & h = d & i gcd n0 = n0 / h ) } by A3;
assume e in dom fp ; :: thesis: ( not d <> e or fp . d misses fp . e )
then A61: fp . e = { i where i is Element of NAT : ex h being Nat st
( i in Seg n0 & e in NatDivisors n0 & h = e & i gcd n0 = n0 / h ) } by A3;
assume A62: d <> e ; :: thesis: fp . d misses fp . e
assume not fp . d misses fp . e ; :: thesis: contradiction
then (fp . d) /\ (fp . e) <> {} by XBOOLE_0:def 7;
then consider x being object such that
A63: x in (fp . d) /\ (fp . e) by XBOOLE_0:def 1;
x in fp . d by A63, XBOOLE_0:def 4;
then A64: ex i1 being Element of NAT st
( x = i1 & ex h being Nat st
( i1 in Seg n0 & d in NatDivisors n0 & h = d & i1 gcd n0 = n0 / h ) ) by A60;
x in fp . e by A63, XBOOLE_0:def 4;
then ex i2 being Element of NAT st
( x = i2 & ex h being Nat st
( i2 in Seg n0 & e in NatDivisors n0 & h = e & i2 gcd n0 = n0 / h ) ) by A61;
then d = n0 / (n0 / e) by A64, XCMPLX_1:52;
hence contradiction by A62, XCMPLX_1:52; :: thesis: verum

end;

A65: for x being object holds
( x in union (rng fp) iff x in Seg n0 )

proof

let x be object ; :: thesis: ( x in union (rng fp) iff x in Seg n0 )
thus ( x in union (rng fp) implies x in Seg n0 ) ; :: thesis: ( x in Seg n0 implies x in union (rng fp) )
assume A66: x in Seg n0 ; :: thesis: x in union (rng fp)
then reconsider i = x as Nat ;
i gcd n0 divides n0 by NAT_D:def 5;
then consider h being Nat such that
A67: n0 = (i gcd n0) * h by NAT_D:def 3;
A68: 0 < h by A67;
then 0 + 1 < h + 1 by XREAL_1:6;
then A69: 1 <= h by NAT_1:13;
A70: h divides n0 by A67, NAT_D:def 3;
then A71: h in NatDivisors n0 by A68;
set Y = fp . h;
A72: h <> 0 by A67;
h <= n0 by A70, NAT_D:7;
then A73: h in dom fp by A3, A69;
then A74: fp . h in rng fp by FUNCT_1:3;
A75: fp . h = { i9 where i9 is Element of NAT : ex h9 being Nat st
( i9 in Seg n0 & h in NatDivisors n0 & h9 = h & i9 gcd n0 = n0 / h9 ) } by A3, A73;
n0 / h = (i gcd n0) * (h / h) by A67, XCMPLX_1:74
.= (i gcd n0) * 1 by A72, XCMPLX_1:60 ;
then x in fp . h by A66, A71, A75;
hence x in union (rng fp) by A74, TARSKI:def 4; :: thesis: verum

end;

card (union (rng fp)) = Sum (Card fp) by A59, INT_5:48;
then A76: card (Seg n0) = Sum (Card fp) by A65, TARSKI:2;
card (Seg n0) = card n0 by FINSEQ_1:55;
then n0 = Sum (Card fp) by A76;
then Sum (Func_Seq (Euler_phi,(Sgm (NatDivisors n0)))) = n0 by A58, A39, BHSP_5:def 4;
hence Sum (Euler_phi | (NatDivisors n0)) = n0 by A40, Th24; :: thesis: verum