A1: for a, a1, b, b1 being non zero Nat
for x being Prime st ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) & a1 = a div (x |^ (x |-count a)) & b1 = b div (x |^ (x |-count b)) holds
for p being Element of NAT st p is prime holds
p |-count a1 <= p |-count b1

proof

let a, a1, b, b1 be non zero Nat; :: thesis: for x being Prime st ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) & a1 = a div (x |^ (x |-count a)) & b1 = b div (x |^ (x |-count b)) holds
for p being Element of NAT st p is prime holds
p |-count a1 <= p |-count b1
let x be Prime; :: thesis: ( ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) & a1 = a div (x |^ (x |-count a)) & b1 = b div (x |^ (x |-count b)) implies for p being Element of NAT st p is prime holds
p |-count a1 <= p |-count b1 )
assume A2: for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ; :: thesis: ( not a1 = a div (x |^ (x |-count a)) or not b1 = b div (x |^ (x |-count b)) or for p being Element of NAT st p is prime holds
p |-count a1 <= p |-count b1 )
set xcb = x |-count b;
set xca = x |-count a;
assume A3: a1 = a div (x |^ (x |-count a)) ; :: thesis: ( not b1 = b div (x |^ (x |-count b)) or for p being Element of NAT st p is prime holds
p |-count a1 <= p |-count b1 )
assume A4: b1 = b div (x |^ (x |-count b)) ; :: thesis: for p being Element of NAT st p is prime holds
p |-count a1 <= p |-count b1
let p be Element of NAT ; :: thesis: ( p is prime implies p |-count a1 <= p |-count b1 )
assume A5: p is prime ; :: thesis: p |-count a1 <= p |-count b1
then A6: p > 1 by INT_2:def 4;
A7: x > 1 by INT_2:def 4;
then x |^ (x |-count a) divides a by NAT_3:def 7;
then A8: p |-count a1 = (p |-count a) -' (p |-count (x |^ (x |-count a))) by A3, A5, NAT_3:31;
x |^ (x |-count b) divides b by A7, NAT_3:def 7;
then A9: p |-count b1 = (p |-count b) -' (p |-count (x |^ (x |-count b))) by A4, A5, NAT_3:31;

per cases ( x = p or x <> p ) ;

suppose x = p ; :: thesis: p |-count a1 <= p |-count b1

then p |-count (x |^ (x |-count a)) = p |-count a by A6, NAT_3:25;
hence p |-count a1 <= p |-count b1 by A8, NAT_2:8; :: thesis: verum

end;

suppose A10: x <> p ; :: thesis: p |-count a1 <= p |-count b1

p |-count (x |^ (x |-count b)) = (x |-count b) * (p |-count x) by A5, NAT_3:32
.= (x |-count b) * 0 by A6, A10, NAT_3:24
.= 0 ;
then A11: p |-count b1 = (p |-count b) - 0 by A9, XREAL_1:233
.= p |-count b ;
p |-count (x |^ (x |-count a)) = (x |-count a) * (p |-count x) by A5, NAT_3:32
.= (x |-count a) * 0 by A6, A10, NAT_3:24
.= 0 ;
then p |-count a1 = (p |-count a) - 0 by A8, XREAL_1:233
.= p |-count a ;
hence p |-count a1 <= p |-count b1 by A2, A5, A11; :: thesis: verum

end;

end;

end;

A12: for a being non zero Nat
for x being Prime holds a div (x |^ (x |-count a)) is non zero Nat

proof

let a be non zero Nat; :: thesis: for x being Prime holds a div (x |^ (x |-count a)) is non zero Nat
let x be Prime; :: thesis: a div (x |^ (x |-count a)) is non zero Nat
assume A13: a div (x |^ (x |-count a)) is not non zero Nat ; :: thesis: contradiction
set xca = x |^ (x |-count a);
x > 1 by INT_2:def 4;
then A14: x |^ (x |-count a) divides a by NAT_3:def 7;
ex t being Nat st
( a = ((x |^ (x |-count a)) * 0) + t & t < x |^ (x |-count a) ) by A13, NAT_D:def 1;
hence contradiction by A14, NAT_D:7; :: thesis: verum

end;

defpred S₁[ Nat] means for a, b being non zero Nat st card (support (pfexp b)) = $1 & ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) holds
ex c being Element of NAT st b = a * c;
let a, b be non zero Nat; :: thesis: ( ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) implies ex c being Element of NAT st b = a * c )
assume A15: for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ; :: thesis: ex c being Element of NAT st b = a * c
A16: ex n1 being Element of NAT st n1 = card (support (pfexp b)) ;
A17: for n1, n2 being non zero Nat st n1 divides n2 holds
(n2 div n1) * n1 = n2

proof

let n1, n2 be non zero Nat; :: thesis: ( n1 divides n2 implies (n2 div n1) * n1 = n2 )
assume n1 divides n2 ; :: thesis: (n2 div n1) * n1 = n2
then ex a being Nat st n2 = n1 * a by NAT_D:def 3;
hence (n2 div n1) * n1 = n2 by NAT_D:18; :: thesis: verum

end;

A18: for b, b1 being non zero Nat
for x being Prime
for n being Element of NAT st card (support (pfexp b)) = n + 1 & b1 = b div (x |^ (x |-count b)) & x in support (pfexp b) holds
card (support (pfexp b1)) = n

proof

let b, b1 be non zero Nat; :: thesis: for x being Prime
for n being Element of NAT st card (support (pfexp b)) = n + 1 & b1 = b div (x |^ (x |-count b)) & x in support (pfexp b) holds
card (support (pfexp b1)) = n
let x be Prime; :: thesis: for n being Element of NAT st card (support (pfexp b)) = n + 1 & b1 = b div (x |^ (x |-count b)) & x in support (pfexp b) holds
card (support (pfexp b1)) = n
let n be Element of NAT ; :: thesis: ( card (support (pfexp b)) = n + 1 & b1 = b div (x |^ (x |-count b)) & x in support (pfexp b) implies card (support (pfexp b1)) = n )
assume A19: card (support (pfexp b)) = n + 1 ; :: thesis: ( not b1 = b div (x |^ (x |-count b)) or not x in support (pfexp b) or card (support (pfexp b1)) = n )
set xcb = x |-count b;
assume A20: b1 = b div (x |^ (x |-count b)) ; :: thesis: ( not x in support (pfexp b) or card (support (pfexp b1)) = n )
A21: x > 1 by INT_2:def 4;
then x |^ (x |-count b) divides b by NAT_3:def 7;
then A22: b = b1 * (x |^ (x |-count b)) by A17, A20;
reconsider b1 = b1 as Element of NAT by ORDINAL1:def 12;
A23: b1,x are_coprime

proof

assume not b1,x are_coprime ; :: thesis: contradiction
then b1 gcd x = x by PEPIN:2;
then x divides b1 by NAT_D:def 5;
then consider c being Nat such that
A24: b1 = x * c by NAT_D:def 3;
A25: not x |^ ((x |-count b) + 1) divides b by A21, NAT_3:def 7;
x |^ (x |-count b) divides b by A21, NAT_3:def 7;
then b = (x * c) * (x |^ (x |-count b)) by A17, A20, A24
.= c * ((x |^ (x |-count b)) * x)
.= c * (x |^ ((x |-count b) + 1)) by NEWTON:6 ;
hence contradiction by A25, NAT_D:def 3; :: thesis: verum

end;

assume x in support (pfexp b) ; :: thesis: card (support (pfexp b1)) = n
then (pfexp b) . x <> 0 by PRE_POLY:def 7;
then A26: x |-count b <> 0 by NAT_3:def 8;
reconsider b1 = b1 as non zero Nat ;
card (support (pfexp ((x |^ (x |-count b)) * b1))) = (card (support (pfexp (x |^ (x |-count b))))) + (card (support (pfexp b1))) by A23, EULER_2:17, NAT_3:47;
then n + 1 = (card {x}) + (card (support (pfexp b1))) by A19, A22, A26, NAT_3:42;
then n + 1 = 1 + (card (support (pfexp b1))) by CARD_2:42;
hence card (support (pfexp b1)) = n ; :: thesis: verum

end;

A27: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A28: S₁[n] ; :: thesis: S₁[n + 1]
for a, b being non zero Nat st card (support (pfexp b)) = n + 1 & ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) holds
ex c being Element of NAT st b = a * c

proof

let a, b be non zero Nat; :: thesis: ( card (support (pfexp b)) = n + 1 & ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) implies ex c being Element of NAT st b = a * c )
assume A29: card (support (pfexp b)) = n + 1 ; :: thesis: ( ex p being Element of NAT st
( p is prime & not p |-count a <= p |-count b ) or ex c being Element of NAT st b = a * c )
then support (pfexp b) <> {} ;
then consider x being object such that
A30: x in support (pfexp b) ;
reconsider x = x as Prime by A30, NAT_3:34;
set a1 = a div (x |^ (x |-count a));
set b1 = b div (x |^ (x |-count b));
reconsider a1 = a div (x |^ (x |-count a)), b1 = b div (x |^ (x |-count b)) as non zero Nat by A12;
assume A31: for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ; :: thesis: ex c being Element of NAT st b = a * c
then A32: for p being Element of NAT st p is prime holds
p |-count a1 <= p |-count b1 by A1;
set xca = x |-count a;
set xcb = x |-count b;
x in NAT by ORDINAL1:def 12;
then A33: (x |-count b) - (x |-count a) = (x |-count b) -' (x |-count a) by A31, XREAL_1:233;
n in NAT by ORDINAL1:def 12;
then card (support (pfexp b1)) = n by A18, A29, A30;
then consider d being Element of NAT such that
A34: b1 = a1 * d by A28, A32;
reconsider e = d * (x |^ ((x |-count b) -' (x |-count a))) as Element of NAT by ORDINAL1:def 12;
take e ; :: thesis: b = a * e
A35: x <> 1 by INT_2:def 4;
then A36: x |^ (x |-count a) divides a by NAT_3:def 7;
x |^ (x |-count b) divides b by A35, NAT_3:def 7;
then b = (d * (a div (x |^ (x |-count a)))) * (x |^ ((x |-count a) + ((x |-count b) -' (x |-count a)))) by A17, A34, A33
.= (d * (a div (x |^ (x |-count a)))) * ((x |^ (x |-count a)) * (x |^ ((x |-count b) -' (x |-count a)))) by NEWTON:8
.= (d * ((a div (x |^ (x |-count a))) * (x |^ (x |-count a)))) * (x |^ ((x |-count b) -' (x |-count a)))
.= (d * a) * (x |^ ((x |-count b) -' (x |-count a))) by A17, A36
.= a * (d * (x |^ ((x |-count b) -' (x |-count a)))) ;
hence b = a * e ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A37: S₁[ 0 ]

proof

let a, b be non zero Nat; :: thesis: ( card (support (pfexp b)) = 0 & ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) implies ex c being Element of NAT st b = a * c )
assume A38: card (support (pfexp b)) = 0 ; :: thesis: ( ex p being Element of NAT st
( p is prime & not p |-count a <= p |-count b ) or ex c being Element of NAT st b = a * c )
( ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) implies ex c being Element of NAT st b = a * c )

proof

set d = 1;
assume A39: for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ; :: thesis: ex c being Element of NAT st b = a * c
take 1 ; :: thesis: b = a * 1
A40: support (pfexp b) = {} by A38;
support (pfexp a) = {}

proof

assume support (pfexp a) <> {} ; :: thesis: contradiction
then consider x being object such that
A41: x in support (pfexp a) ;
reconsider x = x as Prime by A41, NAT_3:34;
reconsider x = x as prime Element of NAT by ORDINAL1:def 12;
(pfexp a) . x <> 0 by A41, PRE_POLY:def 7;
then x |-count a <> 0 by NAT_3:def 8;
then x |-count b > 0 by A39;
then (pfexp b) . x <> 0 by NAT_3:def 8;
hence contradiction by A40, PRE_POLY:def 7; :: thesis: verum

end;

then a = 1 by NAT_3:52;
hence b = a * 1 by A40, NAT_3:52; :: thesis: verum

end;

hence ( ex p being Element of NAT st
( p is prime & not p |-count a <= p |-count b ) or ex c being Element of NAT st b = a * c ) ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A37, A27);
hence ex c being Element of NAT st b = a * c by A15, A16; :: thesis: verum