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_{1}[ 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_{1}[k,x]

A3: ( dom fp = Seg n0 & ( for k being Nat st k in Seg n0 holds

S_{1}[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 13;

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

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} ) )

reconsider f19 = f1 as FinSequence of REAL by Th13;

A57: NatDivisors n0 c= Seg n0 by MOEBIUS1:40;

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

( x in union (rng fp) iff x in Seg n0 )

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, A57, Th24; :: thesis: verum

( 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

( 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

proof

consider fp being FinSequence of bool (Seg n0) such that
let k be Nat; :: thesis: ( k in Seg n0 implies ex x being Element of bool (Seg n0) st S_{1}[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

( 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_{1}[k,x]

take X9 ; :: thesis: S_{1}[k,X9]

thus S_{1}[k,X9]
; :: thesis: verum

end;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

then reconsider X9 = { i where i is Element of NAT : ex h being Nat st
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;( 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

( 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

take X9 ; :: thesis: S

thus S

A3: ( dom fp = Seg n0 & ( for k being Nat st k in Seg n0 holds

S

A4: NatDivisors n0 c= Seg n0 by MOEBIUS1:40;

then A5: rng (Sgm (NatDivisors n0)) c= dom fp by A3, FINSEQ_1:def 13;

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

then A39:
(Card fp) * (Sgm (NatDivisors n0)) = Euler_phi * (Sgm (NatDivisors n0))
by A8, PARTFUN1:5;
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_{1}( 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

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 A4, FINSEQ_1:def 13;

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_{1}(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 ) } )

( 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

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;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

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

assume A10:
k in dom ((Card fp) * (Sgm (NatDivisors n0)))
; :: thesis: ((Card fp) * (Sgm (NatDivisors n0))) . k = (Euler_phi * (Sgm (NatDivisors n0))) . k
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 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

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 A4, FINSEQ_1:def 13;

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

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

then A34:
rng f = { i where i is Element of NAT : ex h being Nat st
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 ) } )

( 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;( 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 { 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_{1}(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;( 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 * (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

( 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

( 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

then
f is one-to-one
by FUNCT_1:def 4;
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_{1}(x19) =
f . x19
by A13

.= H_{1}(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;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

.= H

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

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

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 f29 = Card fp as FinSequence of REAL by Th13;
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;

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 = {}

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;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 A51:
x in Seg n0
; :: thesis: ( x in (Card fp) " {0} or 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;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

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

then A56:
y = (Card fp) . x
by A3, A51, CARD_1:27, CARD_3:def 2;
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 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

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

reconsider f19 = f1 as FinSequence of REAL by Th13;

A57: NatDivisors n0 c= Seg n0 by MOEBIUS1:40;

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

A65:
for x being object holds
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;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

( x in union (rng fp) iff x in Seg n0 )

proof

card (union (rng fp)) = Sum (Card fp)
by A59, INT_5:48;
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, MOEBIUS1:39;

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;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, MOEBIUS1:39;

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

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, A57, Th24; :: thesis: verum