let n, m be Element of NAT ; :: thesis: for r being Real
for X being finite set st X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[p,m] ) } & r >= 0 holds
card X <= [\r/]
defpred S₁[ Nat] means for n, m being Element of NAT
for r being Real
for X being finite set st X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[p,m] ) } & r >= 0 & $1 = [\r/] holds
card X <= [\r/];
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: for m being Element of NAT
for r being Real
for X being finite set st X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[p,m] ) } & r >= 0 & n + 1 = [\r/] holds
card X <= [\r/]

let m be Element of NAT ; :: thesis: for r being Real
for X being finite set st X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[p,m] ) } & r >= 0 & n + 1 = [\r/] holds
card b₅ <= [\b₄/]
let r be Real; :: thesis: for X being finite set st X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[p,m] ) } & r >= 0 & n + 1 = [\r/] holds
card b₄ <= [\b₃/]
let X be finite set ; :: thesis: ( X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[p,m] ) } & r >= 0 & n + 1 = [\r/] implies card b₃ <= [\b₂/] )
set r1 = r - 1;
set X1 = { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } ;
set X2 = { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } ;
A3: 0 + n <= 1 + n by XREAL_1:6;
assume A4: X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[p,m] ) } ; :: thesis: ( r >= 0 & n + 1 = [\r/] implies card b₃ <= [\b₂/] )

now :: thesis: for x being object st x in { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } \/ { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } holds
x in X

let x be object ; :: thesis: ( x in { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } \/ { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } implies b₁ in X )
assume A5: x in { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } \/ { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } ; :: thesis: b₁ in X

per cases ( x in { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } or x in { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } ) by A5, XBOOLE_0:def 3;

suppose x in { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } ; :: thesis: b₁ in X

then consider p being prime Element of NAT such that
A6: F₁(p,m) = x and
A7: p <= r - 1 and
A8: P₁[p,m] ;
(- 1) + r <= 0 + r by XREAL_1:6;
then p <= r by A7, XXREAL_0:2;
hence x in X by A4, A6, A8; :: thesis: verum

end;

suppose x in { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } ; :: thesis: b₁ in X

then ex p being prime Element of NAT st
( F₁(p,m) = x & r - 1 < p & p <= r & P₁[p,m] ) ;
hence x in X by A4; :: thesis: verum

end;

end;

end;

then A9: { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } \/ { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } c= X ;
assume r >= 0 ; :: thesis: ( n + 1 = [\r/] implies card b₃ <= [\b₂/] )

now :: thesis: for x being object st x in X holds
x in { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } \/ { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) }

let x be object ; :: thesis: ( x in X implies x in { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } \/ { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } )
assume x in X ; :: thesis: x in { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } \/ { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) }
then consider p being prime Element of NAT such that
A10: ( F₁(p,m) = x & p <= r & P₁[p,m] ) by A4;
( ( F₁(p,m) = x & p <= r - 1 & P₁[p,m] ) or ( F₁(p,m) = x & r - 1 < p & p <= r & P₁[p,m] ) ) by A10;
then ( x in { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } or x in { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } ) ;
hence x in { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } \/ { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } by XBOOLE_0:def 3; :: thesis: verum

end;

then X c= { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } \/ { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } ;
then A11: X = { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } \/ { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } by A9, XBOOLE_0:def 10;
then reconsider X1 = { F₁(p,m) where p is prime Element of NAT : ( p <= r - 1 & P₁[p,m] ) } as finite set by FINSET_1:1, XBOOLE_1:7;
assume A12: n + 1 = [\r/] ; :: thesis: card b₃ <= [\b₂/]
then A13: n = [\r/] + (- 1)
.= [\(r + (- 1))/] by INT_1:28
.= [\(r - 1)/] ;
then A14: r - 1 >= 0 by INT_1:def 6;
then A15: card X1 <= [\(r - 1)/] by A2, A13;

per cases ( for x being object holds not x in { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } or ex x being set st x in { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } ) ;

suppose for x being object holds not x in { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } ; :: thesis: card b₃ <= [\b₂/]

then { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } = {} by XBOOLE_0:def 1;
hence card X <= [\r/] by A12, A13, A11, A15, A3, XXREAL_0:2; :: thesis: verum

end;

suppose A16: ex x being set st x in { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } ; :: thesis: card b₃ <= [\b₂/]

then consider x being set such that
A17: x in { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } ;

A18: now :: thesis: not { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } <> {x}

assume { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } <> {x} ; :: thesis: contradiction
then consider y being object such that
A19: y in { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } and
A20: y <> x by A16, ZFMISC_1:35;
consider p1 being prime Element of NAT such that
A21: F₁(p1,m) = x and
A22: ( r - 1 < p1 & p1 <= r ) and
P₁[p1,m] by A17;
A23: p1 = [\r/] by A22, INT_1:def 6;
ex p2 being prime Element of NAT st
( F₁(p2,m) = y & r - 1 < p2 & p2 <= r & P₁[p2,m] ) by A19;
hence contradiction by A20, A21, A23, INT_1:def 6; :: thesis: verum

end;

per cases ( not x in X1 or x in X1 ) ;

suppose not x in X1 ; :: thesis: card b₃ <= [\b₂/]

then card X = (card X1) + 1 by A11, A18, CARD_2:41;
hence card X <= [\r/] by A12, A13, A15, XREAL_1:6; :: thesis: verum

end;

suppose x in X1 ; :: thesis: card b₃ <= [\b₂/]

then { F₁(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P₁[p,m] ) } c= X1 by A18, ZFMISC_1:31;
then card X <= n by A2, A13, A14, A11, XBOOLE_1:12;
hence card X <= [\r/] by A12, A3, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

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

end;

A24: S₁[ 0 ]

proof

let n, m be Element of NAT ; :: thesis: for r being Real
for X being finite set st X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[p,m] ) } & r >= 0 & 0 = [\r/] holds
card X <= [\r/]
let r be Real; :: thesis: for X being finite set st X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[p,m] ) } & r >= 0 & 0 = [\r/] holds
card X <= [\r/]
let X be finite set ; :: thesis: ( X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[p,m] ) } & r >= 0 & 0 = [\r/] implies card X <= [\r/] )
assume A25: X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[p,m] ) } ; :: thesis: ( not r >= 0 or not 0 = [\r/] or card X <= [\r/] )
assume r >= 0 ; :: thesis: ( not 0 = [\r/] or card X <= [\r/] )
assume A26: 0 = [\r/] ; :: thesis: card X <= [\r/]
then r - 1 < 0 by INT_1:def 6;
then A27: (r - 1) + 1 < 0 + 1 by XREAL_1:6;

now :: thesis: for x being object holds not x in X

let x be object ; :: thesis: not x in X
assume x in X ; :: thesis: contradiction
then consider p being prime Element of NAT such that
F₁(p,m) = x and
A28: p <= r and
P₁[p,m] by A25;
p < 1 by A27, A28, XXREAL_0:2;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

hence card X <= [\r/] by A26, CARD_1:27, XBOOLE_0:def 1; :: thesis: verum

end;

A29: for n being Nat holds S₁[n] from NAT_1:sch 2(A24, A1);
let r be Real; :: thesis: for X being finite set st X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[p,m] ) } & r >= 0 holds
card X <= [\r/]
let X be finite set ; :: thesis: ( X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[p,m] ) } & r >= 0 implies card X <= [\r/] )
assume that
A30: X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[p,m] ) } and
A31: r >= 0 ; :: thesis: card X <= [\r/]
[\r/] is Element of NAT by A31, INT_1:53;
hence card X <= [\r/] by A29, A30, A31; :: thesis: verum