defpred S₁[ Nat] means for p being Prime holds
( ( p |-count (Product (primesFinS $1)) = 1 implies primeindex p < $1 ) & ( primeindex p < $1 implies p |-count (Product (primesFinS $1)) = 1 ) & ( p |-count (Product (primesFinS $1)) = 0 implies primeindex p >= $1 ) & ( primeindex p >= $1 implies p |-count (Product (primesFinS $1)) = 0 ) );
A1: S₁[ 0 ]

proof

let p be Prime; :: thesis: ( ( p |-count (Product (primesFinS 0)) = 1 implies primeindex p < 0 ) & ( primeindex p < 0 implies p |-count (Product (primesFinS 0)) = 1 ) & ( p |-count (Product (primesFinS 0)) = 0 implies primeindex p >= 0 ) & ( primeindex p >= 0 implies p |-count (Product (primesFinS 0)) = 0 ) )
A2: Product (primesFinS 0) = 1 by RVSUM_1:94;
p > 1 by INT_2:def 4;
then p |-count (Product (primesFinS 0)) = 0 by A2, NAT_3:21;
hence ( ( p |-count (Product (primesFinS 0)) = 1 implies primeindex p < 0 ) & ( primeindex p < 0 implies p |-count (Product (primesFinS 0)) = 1 ) & ( p |-count (Product (primesFinS 0)) = 0 implies primeindex p >= 0 ) & ( primeindex p >= 0 implies p |-count (Product (primesFinS 0)) = 0 ) ) ; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let p be Prime; :: thesis: ( ( p |-count (Product (primesFinS (n + 1))) = 1 implies primeindex p < n + 1 ) & ( primeindex p < n + 1 implies p |-count (Product (primesFinS (n + 1))) = 1 ) & ( p |-count (Product (primesFinS (n + 1))) = 0 implies primeindex p >= n + 1 ) & ( primeindex p >= n + 1 implies p |-count (Product (primesFinS (n + 1))) = 0 ) )
A5: Product (primesFinS (n + 1)) = (Product (primesFinS n)) * (primenumber n) by Th25;
A6: p |-count (Product (primesFinS (n + 1))) = (p |-count (Product (primesFinS n))) + (p |-count (primenumber n)) by A5, NAT_3:28;
A7: n in NAT by ORDINAL1:def 12;
A8: p > 1 by INT_2:def 4;
thus ( p |-count (Product (primesFinS (n + 1))) = 1 iff primeindex p < n + 1 ) :: thesis: ( p |-count (Product (primesFinS (n + 1))) = 0 iff primeindex p >= n + 1 )

proof

thus ( p |-count (Product (primesFinS (n + 1))) = 1 implies primeindex p < n + 1 ) :: thesis: ( primeindex p < n + 1 implies p |-count (Product (primesFinS (n + 1))) = 1 )

proof

assume p |-count (Product (primesFinS (n + 1))) = 1 ; :: thesis: primeindex p < n + 1
then A9: (p |-count (Product (primesFinS n))) + (p |-count (primenumber n)) = 1 by A6;

per cases ( p = primenumber n or p <> primenumber n ) ;

suppose p = primenumber n ; :: thesis: primeindex p < n + 1

then primeindex p = n by A7, NUMBER10:def 4;
hence primeindex p < n + 1 by NAT_1:13; :: thesis: verum

end;

suppose p <> primenumber n ; :: thesis: primeindex p < n + 1

then p |-count (primenumber n) = 0 by A8, NAT_3:24;
then p |-count (Product (primesFinS n)) = 1 by A9;
then primeindex p < n by A4;
hence primeindex p < n + 1 by NAT_1:13; :: thesis: verum

end;

end;

end;

assume primeindex p < n + 1 ; :: thesis: p |-count (Product (primesFinS (n + 1))) = 1
then primeindex p <= n by NAT_1:13;

per cases then ( primeindex p = n or primeindex p < n ) by XXREAL_0:1;

suppose A10: primeindex p = n ; :: thesis: p |-count (Product (primesFinS (n + 1))) = 1

then primenumber n = p by NUMBER10:def 4;
then A11: p |-count (primenumber n) = 1 by A8, NAT_3:22;
p |-count (Product (primesFinS n)) = 0 by A10, A4;
hence p |-count (Product (primesFinS (n + 1))) = 1 by A6, A11; :: thesis: verum

end;

suppose A12: primeindex p < n ; :: thesis: p |-count (Product (primesFinS (n + 1))) = 1

then p < primenumber n by NUMBER13:12;
then A13: p |-count (primenumber n) = 0 by A8, NAT_3:24;
p |-count (Product (primesFinS n)) = 1 by A12, A4;
hence p |-count (Product (primesFinS (n + 1))) = 1 by A6, A13; :: thesis: verum

end;

end;

end;

thus ( p |-count (Product (primesFinS (n + 1))) = 0 implies primeindex p >= n + 1 ) :: thesis: ( primeindex p >= n + 1 implies p |-count (Product (primesFinS (n + 1))) = 0 )

proof

assume p |-count (Product (primesFinS (n + 1))) = 0 ; :: thesis: primeindex p >= n + 1
then (p |-count (Product (primesFinS n))) + (p |-count (primenumber n)) = 0 by A6;
then ( p |-count (Product (primesFinS n)) = 0 & p |-count (primenumber n) = 0 ) ;
then ( primeindex p >= n & primenumber n <> p ) by A4, A8, NAT_3:22;
then ( primeindex p >= n & primeindex p <> n ) by NUMBER10:def 4;
then primeindex p > n by XXREAL_0:1;
hence primeindex p >= n + 1 by NAT_1:13; :: thesis: verum

end;

assume A14: primeindex p >= n + 1 ; :: thesis: p |-count (Product (primesFinS (n + 1))) = 0
then primeindex p >= n by NAT_1:13;
then A15: p |-count (Product (primesFinS n)) = 0 by A4;
A16: p >= primenumber (n + 1) by A14, NUMBER13:12;
n < n + 1 by NAT_1:13;
then primenumber (n + 1) > primenumber n by MOEBIUS2:21;
then p > primenumber n by A16, XXREAL_0:2;
then p |-count (primenumber n) = 0 by A8, NAT_3:24;
then p |-count (Product (primesFinS (n + 1))) = 0 by A6, A15;
hence p |-count (Product (primesFinS (n + 1))) = 0 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
hence for p being Prime
for k being Nat holds
( ( p |-count (Product (primesFinS k)) = 1 implies primeindex p < k ) & ( primeindex p < k implies p |-count (Product (primesFinS k)) = 1 ) & ( p |-count (Product (primesFinS k)) = 0 implies primeindex p >= k ) & ( primeindex p >= k implies p |-count (Product (primesFinS k)) = 0 ) ) ; :: thesis: verum