Metamath Proof Explorer

Theorem bpos1lem

Description: Lemma for bpos1 . (Contributed by Mario Carneiro, 12-Mar-2014)

Ref Expression
Hypotheses bpos1.1 
|- ( E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) -> ph )
bpos1.2 
|- ( N e. ( ZZ>= ` P ) -> ph )
bpos1.3 
|- P e. Prime
bpos1.4 
|- A e. NN0
bpos1.5 
|- ( A x. 2 ) = B
bpos1.6 
|- A < P
bpos1.7 
|- ( P < B \/ P = B )
Assertion bpos1lem 
|- ( N e. ( ZZ>= ` A ) -> ph )

Proof

Step Hyp Ref Expression
1 bpos1.1 
 |-  ( E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) -> ph )
2 bpos1.2 
 |-  ( N e. ( ZZ>= ` P ) -> ph )
3 bpos1.3 
 |-  P e. Prime
4 bpos1.4 
 |-  A e. NN0
5 bpos1.5 
 |-  ( A x. 2 ) = B
6 bpos1.6 
 |-  A < P
7 bpos1.7 
 |-  ( P < B \/ P = B )
8 prmnn 
 |-  ( P e. Prime -> P e. NN )
9 3 8 ax-mp 
 |-  P e. NN
10 9 nnzi 
 |-  P e. ZZ
11 eluzelz 
 |-  ( N e. ( ZZ>= ` A ) -> N e. ZZ )
12 eluz 
 |-  ( ( P e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` P ) <-> P <_ N ) )
13 10 11 12 sylancr 
 |-  ( N e. ( ZZ>= ` A ) -> ( N e. ( ZZ>= ` P ) <-> P <_ N ) )
14 13 2 biimtrrdi 
 |-  ( N e. ( ZZ>= ` A ) -> ( P <_ N -> ph ) )
15 9 nnrei 
 |-  P e. RR
16 15 a1i 
 |-  ( N e. ( ZZ>= ` A ) -> P e. RR )
17 4 nn0rei 
 |-  A e. RR
18 2re 
 |-  2 e. RR
19 17 18 remulcli 
 |-  ( A x. 2 ) e. RR
20 5 19 eqeltrri 
 |-  B e. RR
21 20 a1i 
 |-  ( N e. ( ZZ>= ` A ) -> B e. RR )
22 eluzelre 
 |-  ( N e. ( ZZ>= ` A ) -> N e. RR )
23 remulcl 
 |-  ( ( 2 e. RR /\ N e. RR ) -> ( 2 x. N ) e. RR )
24 18 22 23 sylancr 
 |-  ( N e. ( ZZ>= ` A ) -> ( 2 x. N ) e. RR )
25 15 20 leloei 
 |-  ( P <_ B <-> ( P < B \/ P = B ) )
26 7 25 mpbir 
 |-  P <_ B
27 26 a1i 
 |-  ( N e. ( ZZ>= ` A ) -> P <_ B )
28 4 nn0cni 
 |-  A e. CC
29 2cn 
 |-  2 e. CC
30 28 29 5 mulcomli 
 |-  ( 2 x. A ) = B
31 eluzle 
 |-  ( N e. ( ZZ>= ` A ) -> A <_ N )
32 2pos 
 |-  0 < 2
33 18 32 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
34 lemul2 
 |-  ( ( A e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( A <_ N <-> ( 2 x. A ) <_ ( 2 x. N ) ) )
35 17 33 34 mp3an13 
 |-  ( N e. RR -> ( A <_ N <-> ( 2 x. A ) <_ ( 2 x. N ) ) )
36 22 35 syl 
 |-  ( N e. ( ZZ>= ` A ) -> ( A <_ N <-> ( 2 x. A ) <_ ( 2 x. N ) ) )
37 31 36 mpbid 
 |-  ( N e. ( ZZ>= ` A ) -> ( 2 x. A ) <_ ( 2 x. N ) )
38 30 37 eqbrtrrid 
 |-  ( N e. ( ZZ>= ` A ) -> B <_ ( 2 x. N ) )
39 16 21 24 27 38 letrd 
 |-  ( N e. ( ZZ>= ` A ) -> P <_ ( 2 x. N ) )
40 39 anim2i 
 |-  ( ( N < P /\ N e. ( ZZ>= ` A ) ) -> ( N < P /\ P <_ ( 2 x. N ) ) )
41 breq2 
 |-  ( p = P -> ( N < p <-> N < P ) )
42 breq1 
 |-  ( p = P -> ( p <_ ( 2 x. N ) <-> P <_ ( 2 x. N ) ) )
43 41 42 anbi12d 
 |-  ( p = P -> ( ( N < p /\ p <_ ( 2 x. N ) ) <-> ( N < P /\ P <_ ( 2 x. N ) ) ) )
44 43 rspcev 
 |-  ( ( P e. Prime /\ ( N < P /\ P <_ ( 2 x. N ) ) ) -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
45 3 40 44 sylancr 
 |-  ( ( N < P /\ N e. ( ZZ>= ` A ) ) -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
46 45 1 syl 
 |-  ( ( N < P /\ N e. ( ZZ>= ` A ) ) -> ph )
47 46 expcom 
 |-  ( N e. ( ZZ>= ` A ) -> ( N < P -> ph ) )
48 lelttric 
 |-  ( ( P e. RR /\ N e. RR ) -> ( P <_ N \/ N < P ) )
49 15 22 48 sylancr 
 |-  ( N e. ( ZZ>= ` A ) -> ( P <_ N \/ N < P ) )
50 14 47 49 mpjaod 
 |-  ( N e. ( ZZ>= ` A ) -> ph )