Metamath Proof Explorer

Theorem bposlem4

Description: Lemma for bpos . (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Hypotheses bpos.1 
|- ( ph -> N e. ( ZZ>= ` 5 ) )
bpos.2 
|- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
bpos.3 
|- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )
bpos.4 
|- K = ( |_ ` ( ( 2 x. N ) / 3 ) )
bpos.5 
|- M = ( |_ ` ( sqrt ` ( 2 x. N ) ) )
Assertion bposlem4 
|- ( ph -> M e. ( 3 ... K ) )

Proof

Step Hyp Ref Expression
1 bpos.1 
 |-  ( ph -> N e. ( ZZ>= ` 5 ) )
2 bpos.2 
 |-  ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
3 bpos.3 
 |-  F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )
4 bpos.4 
 |-  K = ( |_ ` ( ( 2 x. N ) / 3 ) )
5 bpos.5 
 |-  M = ( |_ ` ( sqrt ` ( 2 x. N ) ) )
6 2nn 
 |-  2 e. NN
7 5nn 
 |-  5 e. NN
8 eluznn 
 |-  ( ( 5 e. NN /\ N e. ( ZZ>= ` 5 ) ) -> N e. NN )
9 7 1 8 sylancr 
 |-  ( ph -> N e. NN )
10 nnmulcl 
 |-  ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
11 6 9 10 sylancr 
 |-  ( ph -> ( 2 x. N ) e. NN )
12 11 nnred 
 |-  ( ph -> ( 2 x. N ) e. RR )
13 11 nnrpd 
 |-  ( ph -> ( 2 x. N ) e. RR+ )
14 13 rpge0d 
 |-  ( ph -> 0 <_ ( 2 x. N ) )
15 12 14 resqrtcld 
 |-  ( ph -> ( sqrt ` ( 2 x. N ) ) e. RR )
16 15 flcld 
 |-  ( ph -> ( |_ ` ( sqrt ` ( 2 x. N ) ) ) e. ZZ )
17 sqrt9 
 |-  ( sqrt ` 9 ) = 3
18 9re 
 |-  9 e. RR
19 18 a1i 
 |-  ( ph -> 9 e. RR )
20 10re 
 |-  ; 1 0 e. RR
21 20 a1i 
 |-  ( ph -> ; 1 0 e. RR )
22 lep1 
 |-  ( 9 e. RR -> 9 <_ ( 9 + 1 ) )
23 18 22 ax-mp 
 |-  9 <_ ( 9 + 1 )
24 9p1e10 
 |-  ( 9 + 1 ) = ; 1 0
25 23 24 breqtri 
 |-  9 <_ ; 1 0
26 25 a1i 
 |-  ( ph -> 9 <_ ; 1 0 )
27 5cn 
 |-  5 e. CC
28 2cn 
 |-  2 e. CC
29 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
30 27 28 29 mulcomli 
 |-  ( 2 x. 5 ) = ; 1 0
31 eluzle 
 |-  ( N e. ( ZZ>= ` 5 ) -> 5 <_ N )
32 1 31 syl 
 |-  ( ph -> 5 <_ N )
33 9 nnred 
 |-  ( ph -> N e. RR )
34 5re 
 |-  5 e. RR
35 2re 
 |-  2 e. RR
36 2pos 
 |-  0 < 2
37 35 36 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
38 lemul2 
 |-  ( ( 5 e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 5 <_ N <-> ( 2 x. 5 ) <_ ( 2 x. N ) ) )
39 34 37 38 mp3an13 
 |-  ( N e. RR -> ( 5 <_ N <-> ( 2 x. 5 ) <_ ( 2 x. N ) ) )
40 33 39 syl 
 |-  ( ph -> ( 5 <_ N <-> ( 2 x. 5 ) <_ ( 2 x. N ) ) )
41 32 40 mpbid 
 |-  ( ph -> ( 2 x. 5 ) <_ ( 2 x. N ) )
42 30 41 eqbrtrrid 
 |-  ( ph -> ; 1 0 <_ ( 2 x. N ) )
43 19 21 12 26 42 letrd 
 |-  ( ph -> 9 <_ ( 2 x. N ) )
44 0re 
 |-  0 e. RR
45 9pos 
 |-  0 < 9
46 44 18 45 ltleii 
 |-  0 <_ 9
47 18 46 pm3.2i 
 |-  ( 9 e. RR /\ 0 <_ 9 )
48 13 rprege0d 
 |-  ( ph -> ( ( 2 x. N ) e. RR /\ 0 <_ ( 2 x. N ) ) )
49 sqrtle 
 |-  ( ( ( 9 e. RR /\ 0 <_ 9 ) /\ ( ( 2 x. N ) e. RR /\ 0 <_ ( 2 x. N ) ) ) -> ( 9 <_ ( 2 x. N ) <-> ( sqrt ` 9 ) <_ ( sqrt ` ( 2 x. N ) ) ) )
50 47 48 49 sylancr 
 |-  ( ph -> ( 9 <_ ( 2 x. N ) <-> ( sqrt ` 9 ) <_ ( sqrt ` ( 2 x. N ) ) ) )
51 43 50 mpbid 
 |-  ( ph -> ( sqrt ` 9 ) <_ ( sqrt ` ( 2 x. N ) ) )
52 17 51 eqbrtrrid 
 |-  ( ph -> 3 <_ ( sqrt ` ( 2 x. N ) ) )
53 3z 
 |-  3 e. ZZ
54 flge 
 |-  ( ( ( sqrt ` ( 2 x. N ) ) e. RR /\ 3 e. ZZ ) -> ( 3 <_ ( sqrt ` ( 2 x. N ) ) <-> 3 <_ ( |_ ` ( sqrt ` ( 2 x. N ) ) ) ) )
55 15 53 54 sylancl 
 |-  ( ph -> ( 3 <_ ( sqrt ` ( 2 x. N ) ) <-> 3 <_ ( |_ ` ( sqrt ` ( 2 x. N ) ) ) ) )
56 52 55 mpbid 
 |-  ( ph -> 3 <_ ( |_ ` ( sqrt ` ( 2 x. N ) ) ) )
57 53 eluz1i 
 |-  ( ( |_ ` ( sqrt ` ( 2 x. N ) ) ) e. ( ZZ>= ` 3 ) <-> ( ( |_ ` ( sqrt ` ( 2 x. N ) ) ) e. ZZ /\ 3 <_ ( |_ ` ( sqrt ` ( 2 x. N ) ) ) ) )
58 16 56 57 sylanbrc 
 |-  ( ph -> ( |_ ` ( sqrt ` ( 2 x. N ) ) ) e. ( ZZ>= ` 3 ) )
59 3nn 
 |-  3 e. NN
60 nndivre 
 |-  ( ( ( 2 x. N ) e. RR /\ 3 e. NN ) -> ( ( 2 x. N ) / 3 ) e. RR )
61 12 59 60 sylancl 
 |-  ( ph -> ( ( 2 x. N ) / 3 ) e. RR )
62 3re 
 |-  3 e. RR
63 62 a1i 
 |-  ( ph -> 3 e. RR )
64 13 sqrtgt0d 
 |-  ( ph -> 0 < ( sqrt ` ( 2 x. N ) ) )
65 lemul2 
 |-  ( ( 3 e. RR /\ ( sqrt ` ( 2 x. N ) ) e. RR /\ ( ( sqrt ` ( 2 x. N ) ) e. RR /\ 0 < ( sqrt ` ( 2 x. N ) ) ) ) -> ( 3 <_ ( sqrt ` ( 2 x. N ) ) <-> ( ( sqrt ` ( 2 x. N ) ) x. 3 ) <_ ( ( sqrt ` ( 2 x. N ) ) x. ( sqrt ` ( 2 x. N ) ) ) ) )
66 63 15 15 64 65 syl112anc 
 |-  ( ph -> ( 3 <_ ( sqrt ` ( 2 x. N ) ) <-> ( ( sqrt ` ( 2 x. N ) ) x. 3 ) <_ ( ( sqrt ` ( 2 x. N ) ) x. ( sqrt ` ( 2 x. N ) ) ) ) )
67 52 66 mpbid 
 |-  ( ph -> ( ( sqrt ` ( 2 x. N ) ) x. 3 ) <_ ( ( sqrt ` ( 2 x. N ) ) x. ( sqrt ` ( 2 x. N ) ) ) )
68 remsqsqrt 
 |-  ( ( ( 2 x. N ) e. RR /\ 0 <_ ( 2 x. N ) ) -> ( ( sqrt ` ( 2 x. N ) ) x. ( sqrt ` ( 2 x. N ) ) ) = ( 2 x. N ) )
69 12 14 68 syl2anc 
 |-  ( ph -> ( ( sqrt ` ( 2 x. N ) ) x. ( sqrt ` ( 2 x. N ) ) ) = ( 2 x. N ) )
70 67 69 breqtrd 
 |-  ( ph -> ( ( sqrt ` ( 2 x. N ) ) x. 3 ) <_ ( 2 x. N ) )
71 3pos 
 |-  0 < 3
72 62 71 pm3.2i 
 |-  ( 3 e. RR /\ 0 < 3 )
73 72 a1i 
 |-  ( ph -> ( 3 e. RR /\ 0 < 3 ) )
74 lemuldiv 
 |-  ( ( ( sqrt ` ( 2 x. N ) ) e. RR /\ ( 2 x. N ) e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( ( ( sqrt ` ( 2 x. N ) ) x. 3 ) <_ ( 2 x. N ) <-> ( sqrt ` ( 2 x. N ) ) <_ ( ( 2 x. N ) / 3 ) ) )
75 15 12 73 74 syl3anc 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) x. 3 ) <_ ( 2 x. N ) <-> ( sqrt ` ( 2 x. N ) ) <_ ( ( 2 x. N ) / 3 ) ) )
76 70 75 mpbid 
 |-  ( ph -> ( sqrt ` ( 2 x. N ) ) <_ ( ( 2 x. N ) / 3 ) )
77 flword2 
 |-  ( ( ( sqrt ` ( 2 x. N ) ) e. RR /\ ( ( 2 x. N ) / 3 ) e. RR /\ ( sqrt ` ( 2 x. N ) ) <_ ( ( 2 x. N ) / 3 ) ) -> ( |_ ` ( ( 2 x. N ) / 3 ) ) e. ( ZZ>= ` ( |_ ` ( sqrt ` ( 2 x. N ) ) ) ) )
78 15 61 76 77 syl3anc 
 |-  ( ph -> ( |_ ` ( ( 2 x. N ) / 3 ) ) e. ( ZZ>= ` ( |_ ` ( sqrt ` ( 2 x. N ) ) ) ) )
79 elfzuzb 
 |-  ( ( |_ ` ( sqrt ` ( 2 x. N ) ) ) e. ( 3 ... ( |_ ` ( ( 2 x. N ) / 3 ) ) ) <-> ( ( |_ ` ( sqrt ` ( 2 x. N ) ) ) e. ( ZZ>= ` 3 ) /\ ( |_ ` ( ( 2 x. N ) / 3 ) ) e. ( ZZ>= ` ( |_ ` ( sqrt ` ( 2 x. N ) ) ) ) ) )
80 58 78 79 sylanbrc 
 |-  ( ph -> ( |_ ` ( sqrt ` ( 2 x. N ) ) ) e. ( 3 ... ( |_ ` ( ( 2 x. N ) / 3 ) ) ) )
81 4 oveq2i 
 |-  ( 3 ... K ) = ( 3 ... ( |_ ` ( ( 2 x. N ) / 3 ) ) )
82 80 5 81 3eltr4g 
 |-  ( ph -> M e. ( 3 ... K ) )