let m be Nat; :: thesis: for p being Prime st m >= 1 holds
Euler (p |^ m) = (p |^ m) - (p |^ (m -' 1))
let p be Prime; :: thesis: ( m >= 1 implies Euler (p |^ m) = (p |^ m) - (p |^ (m -' 1)) )
assume A1: m >= 1 ; :: thesis: Euler (p |^ m) = (p |^ m) - (p |^ (m -' 1))
set X = { k where k is Element of NAT : ( p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) } ;
set X1 = { k where k is Element of NAT : ( not p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) } ;
set X2 = { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) } ;
set X3 = { k where k is Element of NAT : ( p divides k & k >= 1 & k <= p |^ m ) } ;
reconsider w = p |^ (m -' 1) as Element of NAT by ORDINAL1:def 12;
A2: { k where k is Element of NAT : ( not p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) } = { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) }

proof

thus { k where k is Element of NAT : ( not p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) } c= { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) } :: according to XBOOLE_0:def 10 :: thesis: { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) } c= { k where k is Element of NAT : ( not p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { k where k is Element of NAT : ( not p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) } or a in { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) } )
assume a in { k where k is Element of NAT : ( not p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) } ; :: thesis: a in { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) }
then consider b being Element of NAT such that
A3: ( b = a & not p |^ m,b are_coprime & b >= 1 & b <= p |^ m ) ;
not p,b are_coprime by A3, WSIERP_1:10;
hence a in { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) } by A3; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) } or a in { k where k is Element of NAT : ( not p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) } )
assume a in { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) } ; :: thesis: a in { k where k is Element of NAT : ( not p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) }
then consider k being Element of NAT such that
A4: ( k = a & not p,k are_coprime & k >= 1 & k <= p |^ m ) ;
p gcd k = p by A4, PEPIN:2;
then A5: p divides k by NAT_D:def 5;
p |^ 1 divides p |^ m by A1, NEWTON:89;
then A6: p divides p |^ m ;

now :: thesis: not p |^ m,k are_coprime

assume p |^ m,k are_coprime ; :: thesis: contradiction
then p = 1 by A5, A6, PYTHTRIP:def 1;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

hence a in { k where k is Element of NAT : ( not p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) } by A4; :: thesis: verum

end;

A7: { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) } = { k where k is Element of NAT : ( p divides k & k >= 1 & k <= p |^ m ) }

proof

thus { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) } c= { k where k is Element of NAT : ( p divides k & k >= 1 & k <= p |^ m ) } :: according to XBOOLE_0:def 10 :: thesis: { k where k is Element of NAT : ( p divides k & k >= 1 & k <= p |^ m ) } c= { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) } or x in { k where k is Element of NAT : ( p divides k & k >= 1 & k <= p |^ m ) } )
assume x in { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) } ; :: thesis: x in { k where k is Element of NAT : ( p divides k & k >= 1 & k <= p |^ m ) }
then consider k being Element of NAT such that
A8: ( x = k & not p,k are_coprime & k >= 1 & k <= p |^ m ) ;
p gcd k = p by A8, PEPIN:2;
then p divides k by NAT_D:def 5;
hence x in { k where k is Element of NAT : ( p divides k & k >= 1 & k <= p |^ m ) } by A8; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( p divides k & k >= 1 & k <= p |^ m ) } or x in { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) } )
assume x in { k where k is Element of NAT : ( p divides k & k >= 1 & k <= p |^ m ) } ; :: thesis: x in { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) }
then consider k being Element of NAT such that
A9: ( x = k & p divides k & k >= 1 & k <= p |^ m ) ;
p gcd k = p by A9, NEWTON:49;
then p gcd k > 1 by INT_2:def 4;
then not p,k are_coprime by INT_2:def 3;
hence x in { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) } by A9; :: thesis: verum

end;

{ k where k is Element of NAT : ( p divides k & k >= 1 & k <= p |^ m ) } c= Seg (p |^ m)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( p divides k & k >= 1 & k <= p |^ m ) } or x in Seg (p |^ m) )
assume x in { k where k is Element of NAT : ( p divides k & k >= 1 & k <= p |^ m ) } ; :: thesis: x in Seg (p |^ m)
then ex k being Element of NAT st
( k = x & p divides k & k >= 1 & k <= p |^ m ) ;
hence x in Seg (p |^ m) ; :: thesis: verum

end;

then reconsider X1 = { k where k is Element of NAT : ( not p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) } , X2 = { k where k is Element of NAT : ( not p,k are_coprime & k >= 1 & k <= p |^ m ) } , X3 = { k where k is Element of NAT : ( p divides k & k >= 1 & k <= p |^ m ) } as finite Subset of NAT by A2, A7, XBOOLE_1:1;
deffunc H₁( Nat) -> set = $1 * p;
consider f being FinSequence such that
A10: ( len f = w & ( for d being Nat st d in dom f holds
f . d = H₁(d) ) ) from FINSEQ_1:sch 2();
A11: rng f = X3

proof

thus rng f c= X3 :: according to XBOOLE_0:def 10 :: thesis: X3 c= rng f

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in X3 )
assume a in rng f ; :: thesis: a in X3
then consider s being Nat such that
A12: ( s in dom f & f . s = a ) by FINSEQ_2:10;
A13: a = s * p by A12, A10;
then reconsider a = a as Element of NAT by ORDINAL1:def 12;
A14: p divides a by A13, NAT_D:def 3;
s in Seg w by A12, A10, FINSEQ_1:def 3;
then A15: ( s >= 1 & s <= w ) by FINSEQ_1:1;
p > 1 by INT_2:def 4;
then A16: s * p >= 1 * 1 by A15, XREAL_1:66;
s * p <= w * p by A15, XREAL_1:66;
then A17: s * p <= p |^ ((m -' 1) + 1) by NEWTON:6;
p |^ ((m -' 1) + 1) = p |^ ((m + 1) -' 1) by A1, NAT_D:38
.= p |^ m by NAT_D:34 ;
hence a in X3 by A13, A14, A16, A17; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X3 or a in rng f )
assume a in X3 ; :: thesis: a in rng f
then consider k being Element of NAT such that
A18: ( a = k & p divides k & k >= 1 & k <= p |^ m ) ;
consider t being Nat such that
A19: k = p * t by A18, NAT_D:def 3;
t <> 0 by A19, A18;
then A20: t >= 1 by NAT_1:14;
p |^ m = p |^ ((m + 1) -' 1) by NAT_D:34
.= p |^ ((m -' 1) + 1) by A1, NAT_D:38
.= (p |^ (m -' 1)) * p by NEWTON:6 ;
then (p * t) / p <= ((p |^ (m -' 1)) * p) / p by XREAL_1:72, A18, A19;
then t <= (w * p) / p by XCMPLX_1:89;
then t <= w by XCMPLX_1:89;
then t in Seg w by A20;
then A21: t in dom f by A10, FINSEQ_1:def 3;
f . t = t * p by A21, A10;
hence a in rng f by A18, A19, A21, FUNCT_1:3; :: thesis: verum

end;

for a, b being object st a in dom f & b in dom f & f . a = f . b holds
a = b

proof

let a, b be object ; :: thesis: ( a in dom f & b in dom f & f . a = f . b implies a = b )
assume A22: ( a in dom f & b in dom f & f . a = f . b ) ; :: thesis: a = b
then reconsider a = a, b = b as Element of NAT ;
( f . a = a * p & f . b = b * p ) by A22, A10;
hence a = b by A22, XCMPLX_1:5; :: thesis: verum

end;

then f is one-to-one by FUNCT_1:def 4;
then A23: w = card X1 by A2, A7, A10, A11, FINSEQ_4:62;
A24: X1 c= Seg (p |^ m)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X1 or x in Seg (p |^ m) )
assume x in X1 ; :: thesis: x in Seg (p |^ m)
then consider k being Element of NAT such that
A25: ( x = k & not p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) ;
thus x in Seg (p |^ m) by A25; :: thesis: verum

end;

A26: { k where k is Element of NAT : ( p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) } c= Seg (p |^ m)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) } or x in Seg (p |^ m) )
assume x in { k where k is Element of NAT : ( p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) } ; :: thesis: x in Seg (p |^ m)
then consider k being Element of NAT such that
A27: ( x = k & p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) ;
thus x in Seg (p |^ m) by A27; :: thesis: verum

end;

then A28: X1 \/ { k where k is Element of NAT : ( p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) } c= Seg (p |^ m) by A24, XBOOLE_1:8;
reconsider X = { k where k is Element of NAT : ( p |^ m,k are_coprime & k >= 1 & k <= p |^ m ) } as finite Subset of NAT by A26, XBOOLE_1:1;
Seg (p |^ m) c= X1 \/ X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg (p |^ m) or x in X1 \/ X )
assume A29: x in Seg (p |^ m) ; :: thesis: x in X1 \/ X
then reconsider x = x as Element of NAT ;
A30: ( x >= 1 & x <= p |^ m ) by A29, FINSEQ_1:1;

per cases ( p |^ m,x are_coprime or not p |^ m,x are_coprime ) ;

suppose p |^ m,x are_coprime ; :: thesis: x in X1 \/ X

then x in X by A30;
hence x in X1 \/ X by XBOOLE_0:def 3; :: thesis: verum

end;

suppose not p |^ m,x are_coprime ; :: thesis: x in X1 \/ X

then x in X1 by A30;
hence x in X1 \/ X by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then A31: X1 \/ X = Seg (p |^ m) by A28;
for x being object holds not x in X1 /\ X

proof

given x being object such that A32: x in X1 /\ X ; :: thesis: contradiction
A33: ( x in X1 & x in X ) by A32, XBOOLE_0:def 4;
then consider k1 being Element of NAT such that
A34: ( x = k1 & not p |^ m,k1 are_coprime & k1 >= 1 & k1 <= p |^ m ) ;
consider k2 being Element of NAT such that
A35: ( x = k2 & p |^ m,k2 are_coprime & k2 >= 1 & k2 <= p |^ m ) by A33;
thus contradiction by A34, A35; :: thesis: verum

end;

then X1 /\ X = {} by XBOOLE_0:def 1;
then X1 misses X ;
then (card X1) + (card X) = card (Seg (p |^ m)) by A31, CARD_2:40;
then w + (card X) = p |^ m by A23, FINSEQ_1:57;
hence Euler (p |^ m) = (p |^ m) - (p |^ (m -' 1)) ; :: thesis: verum