defpred S1[ Element of NAT ] means for n, m being Element of NAT
for r being Real
for X being finite set st X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[p,m] ) } & r >= 0 & $1 = [\r/] holds
card X <= [\r/];
A1: S1[ 0 ]
proof
let n, m be Element of NAT ; :: thesis: for r being Real
for X being finite set st X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[p,m] ) } & r >= 0 & 0 = [\r/] holds
card X <= [\r/]
let r be Real; :: thesis: for X being finite set st X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[p,m] ) } & r >= 0 & 0 = [\r/] holds
card X <= [\r/]
let X be finite set ; :: thesis: ( X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[p,m] ) } & r >= 0 & 0 = [\r/] implies card X <= [\r/] )
assume A2: X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[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 A3: 0 = [\r/] ; :: thesis: card X <= [\r/]
then r - 1 < 0 by INT_1:def 4;
then A4: (r - 1) + 1 < 0 + 1 by XREAL_1:8;
now
let x be set ; :: thesis: not x in X
assume x in X ; :: thesis: contradiction
then consider p being prime Element of NAT such that
A5: ( F1(p,m) = x & p <= r & P1[p,m] ) by A2;
p < 1 by A4, A5, XXREAL_0:2;
hence contradiction by INT_2:def 5; :: thesis: verum
end;
hence card X <= [\r/] by A3, CARD_1:47, XBOOLE_0:def 1; :: thesis: verum
end;
A6: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; :: thesis: S1[n + 1]
now
let m be Element of NAT ; :: thesis: for r being Real
for X being finite set st X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[p,m] ) } & r >= 0 & n + 1 = [\r/] holds
card b5 <= [\b4/]
let r be Real; :: thesis: for X being finite set st X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[p,m] ) } & r >= 0 & n + 1 = [\r/] holds
card b4 <= [\b3/]
let X be finite set ; :: thesis: ( X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[p,m] ) } & r >= 0 & n + 1 = [\r/] implies card b3 <= [\b2/] )
assume A8: X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[p,m] ) } ; :: thesis: ( r >= 0 & n + 1 = [\r/] implies card b3 <= [\b2/] )
assume r >= 0 ; :: thesis: ( n + 1 = [\r/] implies card b3 <= [\b2/] )
assume A9: n + 1 = [\r/] ; :: thesis: card b3 <= [\b2/]
set r1 = r - 1;
A10: n = [\r/] + (- 1) by A9
.= [\(r + (- 1))/] by INT_1:51
.= [\(r - 1)/] ;
then A11: r - 1 >= 0 by INT_1:def 4;
set X1 = { F1(p,m) where p is prime Element of NAT : ( p <= r - 1 & P1[p,m] ) } ;
set X2 = { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } ;
now
let x be set ; :: thesis: ( x in X implies x in { F1(p,m) where p is prime Element of NAT : ( p <= r - 1 & P1[p,m] ) } \/ { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } )
assume x in X ; :: thesis: x in { F1(p,m) where p is prime Element of NAT : ( p <= r - 1 & P1[p,m] ) } \/ { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) }
then consider p being prime Element of NAT such that
A12: ( F1(p,m) = x & p <= r & P1[p,m] ) by A8;
( ( F1(p,m) = x & p <= r - 1 & P1[p,m] ) or ( F1(p,m) = x & r - 1 < p & p <= r & P1[p,m] ) ) by A12;
then ( x in { F1(p,m) where p is prime Element of NAT : ( p <= r - 1 & P1[p,m] ) } or x in { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } ) ;
hence x in { F1(p,m) where p is prime Element of NAT : ( p <= r - 1 & P1[p,m] ) } \/ { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } by XBOOLE_0:def 3; :: thesis: verum
end;
then A13: X c= { F1(p,m) where p is prime Element of NAT : ( p <= r - 1 & P1[p,m] ) } \/ { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } by TARSKI:def 3;
now
let x be set ; :: thesis: ( x in { F1(p,m) where p is prime Element of NAT : ( p <= r - 1 & P1[p,m] ) } \/ { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } implies b1 in X )
assume A14: x in { F1(p,m) where p is prime Element of NAT : ( p <= r - 1 & P1[p,m] ) } \/ { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } ; :: thesis: b1 in X
per cases ( x in { F1(p,m) where p is prime Element of NAT : ( p <= r - 1 & P1[p,m] ) } or x in { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } ) by A14, XBOOLE_0:def 3;
suppose x in { F1(p,m) where p is prime Element of NAT : ( p <= r - 1 & P1[p,m] ) } ; :: thesis: b1 in X
then consider p being prime Element of NAT such that
A15: ( F1(p,m) = x & p <= r - 1 & P1[p,m] ) ;
(- 1) + r <= 0 + r by XREAL_1:8;
then ( F1(p,m) = x & p <= r & P1[p,m] ) by A15, XXREAL_0:2;
hence x in X by A8; :: thesis: verum
end;
suppose x in { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } ; :: thesis: b1 in X
then ex p being prime Element of NAT st
( F1(p,m) = x & r - 1 < p & p <= r & P1[p,m] ) ;
hence x in X by A8; :: thesis: verum
end;
end;
end;
then { F1(p,m) where p is prime Element of NAT : ( p <= r - 1 & P1[p,m] ) } \/ { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } c= X by TARSKI:def 3;
then A16: X = { F1(p,m) where p is prime Element of NAT : ( p <= r - 1 & P1[p,m] ) } \/ { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } by A13, XBOOLE_0:def 10;
then reconsider X1 = { F1(p,m) where p is prime Element of NAT : ( p <= r - 1 & P1[p,m] ) } as finite set by FINSET_1:13, XBOOLE_1:7;
A17: card X1 <= [\(r - 1)/] by A7, A10, A11;
A18: 0 + n <= 1 + n by XREAL_1:8;
per cases ( for x being set holds not x in { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } or ex x being set st x in { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } ) ;
suppose for x being set holds not x in { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } ; :: thesis: card b3 <= [\b2/]
then { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } = {} by XBOOLE_0:def 1;
hence card X <= [\r/] by A9, A10, A16, A17, A18, XXREAL_0:2; :: thesis: verum
end;
suppose A19: ex x being set st x in { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } ; :: thesis: card b3 <= [\b2/]
then consider x being set such that
A20: x in { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } ;
A21: now
assume { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } <> {x} ; :: thesis: contradiction
then consider y being set such that
A22: ( y in { F1(p,m) where p is prime Element of NAT : ( r - 1 < p & p <= r & P1[p,m] ) } & y <> x ) by A19, ZFMISC_1:41;
consider p1 being prime Element of NAT such that
A23: ( F1(p1,m) = x & r - 1 < p1 & p1 <= r & P1[p1,m] ) by A20;
consider p2 being prime Element of NAT such that
A24: ( F1(p2,m) = y & r - 1 < p2 & p2 <= r & P1[p2,m] ) by A22;
p1 = [\r/] by A23, INT_1:def 4;
hence contradiction by A22, A23, A24, INT_1:def 4; :: thesis: verum
end;
end;
end;
end;
hence S1[n + 1] ; :: thesis: verum
end;
A25: for n being Element of NAT holds S1[n] from NAT_1:sch 1(A1, A6);
 let n, m be Element of NAT ; :: thesis: for r being Real
for X being finite set st X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[p,m] ) } & r >= 0 holds
card X <= [\r/]
let r be Real; :: thesis: for X being finite set st X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[p,m] ) } & r >= 0 holds
card X <= [\r/]
let X be finite set ; :: thesis: ( X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[p,m] ) } & r >= 0 implies card X <= [\r/] )
assume A26: ( X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[p,m] ) } & r >= 0 ) ; :: thesis: card X <= [\r/]
then [\r/] is Element of NAT by INT_1:80;
hence card X <= [\r/] by A25, A26; :: thesis: verum