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 ) )