let a, b be non empty 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 A1: 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
defpred S₁[ Element of NAT ] means for a, b being non empty 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;
A2: S₁[ 0 ]

proof

let a, b be non empty 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 A3: 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

assume A4: 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
A5: support (pfexp b) = {} by A3;
support (pfexp a) = {}

proof

assume support (pfexp a) <> {} ; :: thesis: contradiction
then consider x being set such that
A6: x in support (pfexp a) by XBOOLE_0:def 1;
reconsider x = x as Prime by A6, NAT_3:34;
reconsider x = x as prime Element of NAT by ORDINAL1:def 13;
(pfexp a) . x <> 0 by A6, POLYNOM1:def 7;
then x |-count a <> 0 by NAT_3:def 8;
then x |-count b > 0 by A4;
then (pfexp b) . x <> 0 by NAT_3:def 8;
hence contradiction by A5, POLYNOM1:def 7; :: thesis: verum

end;

then A7: a = 1 by NAT_3:52;
set d = 1;
take 1 ; :: thesis: b = a * 1
thus b = a * 1 by A5, A7, 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;

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

proof

let a be non empty Nat; :: thesis: for x being Prime holds a div (x |^ (x |-count a)) is non empty Nat
let x be Prime; :: thesis: a div (x |^ (x |-count a)) is non empty Nat
assume A9: a div (x |^ (x |-count a)) is not non empty Nat ; :: thesis: contradiction

per cases ( x |-count a = 0 or x |-count a <> 0 ) ;

suppose x |-count a = 0 ; :: thesis: contradiction

then A10: x |^ (x |-count a) = 1 by NEWTON:9;
thus contradiction by A9, A10, NAT_2:6; :: thesis: verum

end;

suppose x |-count a <> 0 ; :: thesis: contradiction

then A11: ( x > 1 & x |-count a > 0 ) by INT_2:def 5;
set xca = x |^ (x |-count a);
A12: ex t being Nat st
( a = ((x |^ (x |-count a)) * 0 ) + t & t < x |^ (x |-count a) ) by A9, NAT_D:def 1;
x |^ (x |-count a) divides a by A11, NAT_3:def 7;
hence contradiction by A12, NAT_D:7; :: thesis: verum

end;

end;

end;

A13: for n1, n2 being non empty Nat st n1 divides n2 holds
(n2 div n1) * n1 = n2

proof

let n1, n2 be non empty 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;

A14: for b, b1 being non empty 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 empty 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 A15: 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 )
assume A16: b1 = b div (x |^ (x |-count b)) ; :: thesis: ( not x in support (pfexp b) or card (support (pfexp b1)) = n )
assume A17: x in support (pfexp b) ; :: thesis: card (support (pfexp b1)) = n
set xcb = x |-count b;
A18: x > 1 by INT_2:def 5;
then x |^ (x |-count b) divides b by NAT_3:def 7;
then A19: b = b1 * (x |^ (x |-count b)) by A13, A16;
(pfexp b) . x <> 0 by A17, POLYNOM1:def 7;
then A20: x |-count b <> 0 by NAT_3:def 8;
reconsider b1 = b1 as Element of NAT by ORDINAL1:def 13;
A21: b1,x are_relative_prime

proof

assume not b1,x are_relative_prime ; :: 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
A22: b1 = x * c by NAT_D:def 3;
A23: ( x |^ (x |-count b) divides b & not x |^ ((x |-count b) + 1) divides b ) by A18, NAT_3:def 7;
then b = (x * c) * (x |^ (x |-count b)) by A13, A16, A22
.= c * ((x |^ (x |-count b)) * x)
.= c * (x |^ ((x |-count b) + 1)) by NEWTON:11 ;
hence contradiction by A23, NAT_D:def 3; :: thesis: verum

end;

reconsider b1 = b1 as non empty Nat ;
card (support (pfexp ((x |^ (x |-count b)) * b1))) = (card (support (pfexp (x |^ (x |-count b))))) + (card (support (pfexp b1))) by A21, EULER_2:32, NAT_3:47;
then n + 1 = (card {x}) + (card (support (pfexp b1))) by A15, A19, A20, NAT_3:42;
then n + 1 = 1 + (card (support (pfexp b1))) by CARD_2:60;
hence card (support (pfexp b1)) = n ; :: thesis: verum

end;

A24: for a, a1, b, b1 being non empty 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 empty 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 A25: 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 )
assume A26: 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 A27: 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 A28: p is prime ; :: thesis: p |-count a1 <= p |-count b1
then A29: p > 1 by INT_2:def 5;
set xca = x |-count a;
set xcb = x |-count b;
A30: x > 1 by INT_2:def 5;
then x |^ (x |-count a) divides a by NAT_3:def 7;
then A31: p |-count a1 = (p |-count a) -' (p |-count (x |^ (x |-count a))) by A26, A28, NAT_3:31;
x |^ (x |-count b) divides b by A30, NAT_3:def 7;
then A32: p |-count b1 = (p |-count b) -' (p |-count (x |^ (x |-count b))) by A27, A28, 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 A29, NAT_3:25;
hence p |-count a1 <= p |-count b1 by A31, NAT_2:10; :: thesis: verum

end;

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

p |-count (x |^ (x |-count a)) = (x |-count a) * (p |-count x) by A28, NAT_3:32
.= (x |-count a) * 0 by A29, A33, NAT_3:24
.= 0 ;
then A34: p |-count a1 = (p |-count a) - 0 by A31, XREAL_1:235
.= p |-count a ;
p |-count (x |^ (x |-count b)) = (x |-count b) * (p |-count x) by A28, NAT_3:32
.= (x |-count b) * 0 by A29, A33, NAT_3:24
.= 0 ;
then p |-count b1 = (p |-count b) - 0 by A32, XREAL_1:235
.= p |-count b ;
hence p |-count a1 <= p |-count b1 by A25, A28, A34; :: thesis: verum

end;

end;

end;

A35: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A36: S₁[n] ; :: thesis: S₁[n + 1]
for a, b being non empty 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 empty 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 A37: 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 )
assume A38: 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
support (pfexp b) <> {} by A37;
then consider x being set such that
A39: x in support (pfexp b) by XBOOLE_0:def 1;
reconsider x = x as Prime by A39, NAT_3:34;
A40: x in NAT by ORDINAL1:def 13;
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 empty Nat by A8;
A41: card (support (pfexp b1)) = n by A14, A37, A39;
for p being Element of NAT st p is prime holds
p |-count a1 <= p |-count b1 by A24, A38;
then consider d being Element of NAT such that
A42: b1 = a1 * d by A36, A41;
set xcb = x |-count b;
set xca = x |-count a;
A43: (x |-count b) - (x |-count a) = (x |-count b) -' (x |-count a) by A38, A40, XREAL_1:235;
x <> 1 by INT_2:def 5;
then A44: ( x |^ (x |-count b) divides b & x |^ (x |-count a) divides a ) by NAT_3:def 7;
then A45: b = (d * (a div (x |^ (x |-count a)))) * (x |^ ((x |-count a) + ((x |-count b) -' (x |-count a)))) by A13, A42, A43
.= (d * (a div (x |^ (x |-count a)))) * ((x |^ (x |-count a)) * (x |^ ((x |-count b) -' (x |-count a)))) by NEWTON:13
.= (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 A13, A44
.= a * (d * (x |^ ((x |-count b) -' (x |-count a)))) ;
reconsider e = d * (x |^ ((x |-count b) -' (x |-count a))) as Element of NAT by ORDINAL1:def 13;
take e ; :: thesis: b = a * e
thus b = a * e by A45; :: thesis: verum

end;

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

end;

A46: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A35);
ex n1 being Element of NAT st n1 = card (support (pfexp b)) ;
hence ex c being Element of NAT st b = a * c by A1, A46; :: thesis: verum