This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chtub

Description: An upper bound on the Chebyshev function. (Contributed by Mario Carneiro, 13-Mar-2014) (Revised 22-Sep-2014.)

Ref Expression
Assertion chtub 
|- ( ( N e. RR /\ 2 < N ) -> ( theta ` N ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 1lt2 
 |-  1 < 2
3 rplogcl 
 |-  ( ( 2 e. RR /\ 1 < 2 ) -> ( log ` 2 ) e. RR+ )
4 1 2 3 mp2an 
 |-  ( log ` 2 ) e. RR+
5 elrp 
 |-  ( ( log ` 2 ) e. RR+ <-> ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) )
6 4 5 mpbi 
 |-  ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) )
7 6 simpli 
 |-  ( log ` 2 ) e. RR
8 7 recni 
 |-  ( log ` 2 ) e. CC
9 8 mulridi 
 |-  ( ( log ` 2 ) x. 1 ) = ( log ` 2 )
10 cht2 
 |-  ( theta ` 2 ) = ( log ` 2 )
11 9 10 eqtr4i 
 |-  ( ( log ` 2 ) x. 1 ) = ( theta ` 2 )
12 fveq2 
 |-  ( ( |_ ` N ) = 2 -> ( theta ` ( |_ ` N ) ) = ( theta ` 2 ) )
13 11 12 eqtr4id 
 |-  ( ( |_ ` N ) = 2 -> ( ( log ` 2 ) x. 1 ) = ( theta ` ( |_ ` N ) ) )
14 chtfl 
 |-  ( N e. RR -> ( theta ` ( |_ ` N ) ) = ( theta ` N ) )
15 14 adantr 
 |-  ( ( N e. RR /\ 2 < N ) -> ( theta ` ( |_ ` N ) ) = ( theta ` N ) )
16 13 15 sylan9eqr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( ( log ` 2 ) x. 1 ) = ( theta ` N ) )
17 2t2e4 
 |-  ( 2 x. 2 ) = 4
18 df-4 
 |-  4 = ( 3 + 1 )
19 17 18 eqtri 
 |-  ( 2 x. 2 ) = ( 3 + 1 )
20 simplr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> 2 < N )
21 simpl 
 |-  ( ( N e. RR /\ 2 < N ) -> N e. RR )
22 2pos 
 |-  0 < 2
23 1 22 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
24 23 a1i 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( 2 e. RR /\ 0 < 2 ) )
25 ltmul2 
 |-  ( ( 2 e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 2 < N <-> ( 2 x. 2 ) < ( 2 x. N ) ) )
26 1 21 24 25 mp3an2ani 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( 2 < N <-> ( 2 x. 2 ) < ( 2 x. N ) ) )
27 20 26 mpbid 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( 2 x. 2 ) < ( 2 x. N ) )
28 19 27 eqbrtrrid 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( 3 + 1 ) < ( 2 x. N ) )
29 3re 
 |-  3 e. RR
30 29 a1i 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> 3 e. RR )
31 1red 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> 1 e. RR )
32 remulcl 
 |-  ( ( 2 e. RR /\ N e. RR ) -> ( 2 x. N ) e. RR )
33 1 21 32 sylancr 
 |-  ( ( N e. RR /\ 2 < N ) -> ( 2 x. N ) e. RR )
34 33 adantr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( 2 x. N ) e. RR )
35 30 31 34 ltaddsub2d 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( ( 3 + 1 ) < ( 2 x. N ) <-> 1 < ( ( 2 x. N ) - 3 ) ) )
36 28 35 mpbid 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> 1 < ( ( 2 x. N ) - 3 ) )
37 resubcl 
 |-  ( ( ( 2 x. N ) e. RR /\ 3 e. RR ) -> ( ( 2 x. N ) - 3 ) e. RR )
38 33 29 37 sylancl 
 |-  ( ( N e. RR /\ 2 < N ) -> ( ( 2 x. N ) - 3 ) e. RR )
39 38 adantr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( ( 2 x. N ) - 3 ) e. RR )
40 6 a1i 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) )
41 ltmul2 
 |-  ( ( 1 e. RR /\ ( ( 2 x. N ) - 3 ) e. RR /\ ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) ) -> ( 1 < ( ( 2 x. N ) - 3 ) <-> ( ( log ` 2 ) x. 1 ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) ) )
42 31 39 40 41 syl3anc 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( 1 < ( ( 2 x. N ) - 3 ) <-> ( ( log ` 2 ) x. 1 ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) ) )
43 36 42 mpbid 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( ( log ` 2 ) x. 1 ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )
44 16 43 eqbrtrrd 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( theta ` N ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )
45 chtcl 
 |-  ( N e. RR -> ( theta ` N ) e. RR )
46 45 ad2antrr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( theta ` N ) e. RR )
47 reflcl 
 |-  ( N e. RR -> ( |_ ` N ) e. RR )
48 47 ad2antrr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( |_ ` N ) e. RR )
49 remulcl 
 |-  ( ( 2 e. RR /\ ( |_ ` N ) e. RR ) -> ( 2 x. ( |_ ` N ) ) e. RR )
50 1 48 49 sylancr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( 2 x. ( |_ ` N ) ) e. RR )
51 resubcl 
 |-  ( ( ( 2 x. ( |_ ` N ) ) e. RR /\ 3 e. RR ) -> ( ( 2 x. ( |_ ` N ) ) - 3 ) e. RR )
52 50 29 51 sylancl 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( 2 x. ( |_ ` N ) ) - 3 ) e. RR )
53 remulcl 
 |-  ( ( ( log ` 2 ) e. RR /\ ( ( 2 x. ( |_ ` N ) ) - 3 ) e. RR ) -> ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) e. RR )
54 7 52 53 sylancr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) e. RR )
55 38 adantr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( 2 x. N ) - 3 ) e. RR )
56 remulcl 
 |-  ( ( ( log ` 2 ) e. RR /\ ( ( 2 x. N ) - 3 ) e. RR ) -> ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) e. RR )
57 7 55 56 sylancr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) e. RR )
58 15 adantr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( theta ` ( |_ ` N ) ) = ( theta ` N ) )
59 simpr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) )
60 df-3 
 |-  3 = ( 2 + 1 )
61 60 fveq2i 
 |-  ( ZZ>= ` 3 ) = ( ZZ>= ` ( 2 + 1 ) )
62 59 61 eleqtrrdi 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( |_ ` N ) e. ( ZZ>= ` 3 ) )
63 fveq2 
 |-  ( k = ( |_ ` N ) -> ( theta ` k ) = ( theta ` ( |_ ` N ) ) )
64 oveq2 
 |-  ( k = ( |_ ` N ) -> ( 2 x. k ) = ( 2 x. ( |_ ` N ) ) )
65 64 oveq1d 
 |-  ( k = ( |_ ` N ) -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. ( |_ ` N ) ) - 3 ) )
66 65 oveq2d 
 |-  ( k = ( |_ ` N ) -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) )
67 63 66 breq12d 
 |-  ( k = ( |_ ` N ) -> ( ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> ( theta ` ( |_ ` N ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) ) )
68 oveq2 
 |-  ( x = 3 -> ( 3 ... x ) = ( 3 ... 3 ) )
69 68 raleqdv 
 |-  ( x = 3 -> ( A. k e. ( 3 ... x ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> A. k e. ( 3 ... 3 ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
70 oveq2 
 |-  ( x = n -> ( 3 ... x ) = ( 3 ... n ) )
71 70 raleqdv 
 |-  ( x = n -> ( A. k e. ( 3 ... x ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
72 oveq2 
 |-  ( x = ( n + 1 ) -> ( 3 ... x ) = ( 3 ... ( n + 1 ) ) )
73 72 raleqdv 
 |-  ( x = ( n + 1 ) -> ( A. k e. ( 3 ... x ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> A. k e. ( 3 ... ( n + 1 ) ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
74 oveq2 
 |-  ( x = ( |_ ` N ) -> ( 3 ... x ) = ( 3 ... ( |_ ` N ) ) )
75 74 raleqdv 
 |-  ( x = ( |_ ` N ) -> ( A. k e. ( 3 ... x ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> A. k e. ( 3 ... ( |_ ` N ) ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
76 6lt8 
 |-  6 < 8
77 6re 
 |-  6 e. RR
78 6pos 
 |-  0 < 6
79 77 78 elrpii 
 |-  6 e. RR+
80 8re 
 |-  8 e. RR
81 8pos 
 |-  0 < 8
82 80 81 elrpii 
 |-  8 e. RR+
83 logltb 
 |-  ( ( 6 e. RR+ /\ 8 e. RR+ ) -> ( 6 < 8 <-> ( log ` 6 ) < ( log ` 8 ) ) )
84 79 82 83 mp2an 
 |-  ( 6 < 8 <-> ( log ` 6 ) < ( log ` 8 ) )
85 76 84 mpbi 
 |-  ( log ` 6 ) < ( log ` 8 )
86 85 a1i 
 |-  ( k e. ( 3 ... 3 ) -> ( log ` 6 ) < ( log ` 8 ) )
87 elfz1eq 
 |-  ( k e. ( 3 ... 3 ) -> k = 3 )
88 87 fveq2d 
 |-  ( k e. ( 3 ... 3 ) -> ( theta ` k ) = ( theta ` 3 ) )
89 cht3 
 |-  ( theta ` 3 ) = ( log ` 6 )
90 88 89 eqtrdi 
 |-  ( k e. ( 3 ... 3 ) -> ( theta ` k ) = ( log ` 6 ) )
91 87 oveq2d 
 |-  ( k e. ( 3 ... 3 ) -> ( 2 x. k ) = ( 2 x. 3 ) )
92 91 oveq1d 
 |-  ( k e. ( 3 ... 3 ) -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. 3 ) - 3 ) )
93 3cn 
 |-  3 e. CC
94 93 2timesi 
 |-  ( 2 x. 3 ) = ( 3 + 3 )
95 93 93 94 mvrraddi 
 |-  ( ( 2 x. 3 ) - 3 ) = 3
96 92 95 eqtrdi 
 |-  ( k e. ( 3 ... 3 ) -> ( ( 2 x. k ) - 3 ) = 3 )
97 96 oveq2d 
 |-  ( k e. ( 3 ... 3 ) -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( ( log ` 2 ) x. 3 ) )
98 2rp 
 |-  2 e. RR+
99 relogcl 
 |-  ( 2 e. RR+ -> ( log ` 2 ) e. RR )
100 98 99 ax-mp 
 |-  ( log ` 2 ) e. RR
101 100 recni 
 |-  ( log ` 2 ) e. CC
102 101 93 mulcomi 
 |-  ( ( log ` 2 ) x. 3 ) = ( 3 x. ( log ` 2 ) )
103 3z 
 |-  3 e. ZZ
104 relogexp 
 |-  ( ( 2 e. RR+ /\ 3 e. ZZ ) -> ( log ` ( 2 ^ 3 ) ) = ( 3 x. ( log ` 2 ) ) )
105 98 103 104 mp2an 
 |-  ( log ` ( 2 ^ 3 ) ) = ( 3 x. ( log ` 2 ) )
106 102 105 eqtr4i 
 |-  ( ( log ` 2 ) x. 3 ) = ( log ` ( 2 ^ 3 ) )
107 cu2 
 |-  ( 2 ^ 3 ) = 8
108 107 fveq2i 
 |-  ( log ` ( 2 ^ 3 ) ) = ( log ` 8 )
109 106 108 eqtri 
 |-  ( ( log ` 2 ) x. 3 ) = ( log ` 8 )
110 97 109 eqtrdi 
 |-  ( k e. ( 3 ... 3 ) -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( log ` 8 ) )
111 86 90 110 3brtr4d 
 |-  ( k e. ( 3 ... 3 ) -> ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) )
112 111 rgen 
 |-  A. k e. ( 3 ... 3 ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) )
113 df-2 
 |-  2 = ( 1 + 1 )
114 2div2e1 
 |-  ( 2 / 2 ) = 1
115 eluzle 
 |-  ( n e. ( ZZ>= ` 3 ) -> 3 <_ n )
116 60 115 eqbrtrrid 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 2 + 1 ) <_ n )
117 2z 
 |-  2 e. ZZ
118 eluzelz 
 |-  ( n e. ( ZZ>= ` 3 ) -> n e. ZZ )
119 zltp1le 
 |-  ( ( 2 e. ZZ /\ n e. ZZ ) -> ( 2 < n <-> ( 2 + 1 ) <_ n ) )
120 117 118 119 sylancr 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 2 < n <-> ( 2 + 1 ) <_ n ) )
121 116 120 mpbird 
 |-  ( n e. ( ZZ>= ` 3 ) -> 2 < n )
122 eluzelre 
 |-  ( n e. ( ZZ>= ` 3 ) -> n e. RR )
123 ltdiv1 
 |-  ( ( 2 e. RR /\ n e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 2 < n <-> ( 2 / 2 ) < ( n / 2 ) ) )
124 1 23 123 mp3an13 
 |-  ( n e. RR -> ( 2 < n <-> ( 2 / 2 ) < ( n / 2 ) ) )
125 122 124 syl 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 2 < n <-> ( 2 / 2 ) < ( n / 2 ) ) )
126 121 125 mpbid 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 2 / 2 ) < ( n / 2 ) )
127 114 126 eqbrtrrid 
 |-  ( n e. ( ZZ>= ` 3 ) -> 1 < ( n / 2 ) )
128 122 rehalfcld 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( n / 2 ) e. RR )
129 1re 
 |-  1 e. RR
130 ltadd1 
 |-  ( ( 1 e. RR /\ ( n / 2 ) e. RR /\ 1 e. RR ) -> ( 1 < ( n / 2 ) <-> ( 1 + 1 ) < ( ( n / 2 ) + 1 ) ) )
131 129 129 130 mp3an13 
 |-  ( ( n / 2 ) e. RR -> ( 1 < ( n / 2 ) <-> ( 1 + 1 ) < ( ( n / 2 ) + 1 ) ) )
132 128 131 syl 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 1 < ( n / 2 ) <-> ( 1 + 1 ) < ( ( n / 2 ) + 1 ) ) )
133 127 132 mpbid 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 1 + 1 ) < ( ( n / 2 ) + 1 ) )
134 113 133 eqbrtrid 
 |-  ( n e. ( ZZ>= ` 3 ) -> 2 < ( ( n / 2 ) + 1 ) )
135 134 adantr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> 2 < ( ( n / 2 ) + 1 ) )
136 peano2z 
 |-  ( ( n / 2 ) e. ZZ -> ( ( n / 2 ) + 1 ) e. ZZ )
137 136 adantl 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n / 2 ) + 1 ) e. ZZ )
138 zltp1le 
 |-  ( ( 2 e. ZZ /\ ( ( n / 2 ) + 1 ) e. ZZ ) -> ( 2 < ( ( n / 2 ) + 1 ) <-> ( 2 + 1 ) <_ ( ( n / 2 ) + 1 ) ) )
139 117 137 138 sylancr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 < ( ( n / 2 ) + 1 ) <-> ( 2 + 1 ) <_ ( ( n / 2 ) + 1 ) ) )
140 135 139 mpbid 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 + 1 ) <_ ( ( n / 2 ) + 1 ) )
141 60 140 eqbrtrid 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> 3 <_ ( ( n / 2 ) + 1 ) )
142 1red 
 |-  ( n e. ( ZZ>= ` 3 ) -> 1 e. RR )
143 ltle 
 |-  ( ( 1 e. RR /\ ( n / 2 ) e. RR ) -> ( 1 < ( n / 2 ) -> 1 <_ ( n / 2 ) ) )
144 129 128 143 sylancr 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 1 < ( n / 2 ) -> 1 <_ ( n / 2 ) ) )
145 127 144 mpd 
 |-  ( n e. ( ZZ>= ` 3 ) -> 1 <_ ( n / 2 ) )
146 142 128 128 145 leadd2dd 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( n / 2 ) + 1 ) <_ ( ( n / 2 ) + ( n / 2 ) ) )
147 122 recnd 
 |-  ( n e. ( ZZ>= ` 3 ) -> n e. CC )
148 147 2halvesd 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( n / 2 ) + ( n / 2 ) ) = n )
149 146 148 breqtrd 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( n / 2 ) + 1 ) <_ n )
150 149 adantr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n / 2 ) + 1 ) <_ n )
151 elfz 
 |-  ( ( ( ( n / 2 ) + 1 ) e. ZZ /\ 3 e. ZZ /\ n e. ZZ ) -> ( ( ( n / 2 ) + 1 ) e. ( 3 ... n ) <-> ( 3 <_ ( ( n / 2 ) + 1 ) /\ ( ( n / 2 ) + 1 ) <_ n ) ) )
152 103 151 mp3an2 
 |-  ( ( ( ( n / 2 ) + 1 ) e. ZZ /\ n e. ZZ ) -> ( ( ( n / 2 ) + 1 ) e. ( 3 ... n ) <-> ( 3 <_ ( ( n / 2 ) + 1 ) /\ ( ( n / 2 ) + 1 ) <_ n ) ) )
153 136 118 152 syl2anr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( ( n / 2 ) + 1 ) e. ( 3 ... n ) <-> ( 3 <_ ( ( n / 2 ) + 1 ) /\ ( ( n / 2 ) + 1 ) <_ n ) ) )
154 141 150 153 mpbir2and 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n / 2 ) + 1 ) e. ( 3 ... n ) )
155 fveq2 
 |-  ( k = ( ( n / 2 ) + 1 ) -> ( theta ` k ) = ( theta ` ( ( n / 2 ) + 1 ) ) )
156 oveq2 
 |-  ( k = ( ( n / 2 ) + 1 ) -> ( 2 x. k ) = ( 2 x. ( ( n / 2 ) + 1 ) ) )
157 156 oveq1d 
 |-  ( k = ( ( n / 2 ) + 1 ) -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) )
158 157 oveq2d 
 |-  ( k = ( ( n / 2 ) + 1 ) -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) )
159 155 158 breq12d 
 |-  ( k = ( ( n / 2 ) + 1 ) -> ( ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) ) )
160 159 rspcv 
 |-  ( ( ( n / 2 ) + 1 ) e. ( 3 ... n ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) ) )
161 154 160 syl 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) ) )
162 128 recnd 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( n / 2 ) e. CC )
163 162 adantr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( n / 2 ) e. CC )
164 2cn 
 |-  2 e. CC
165 ax-1cn 
 |-  1 e. CC
166 adddi 
 |-  ( ( 2 e. CC /\ ( n / 2 ) e. CC /\ 1 e. CC ) -> ( 2 x. ( ( n / 2 ) + 1 ) ) = ( ( 2 x. ( n / 2 ) ) + ( 2 x. 1 ) ) )
167 164 165 166 mp3an13 
 |-  ( ( n / 2 ) e. CC -> ( 2 x. ( ( n / 2 ) + 1 ) ) = ( ( 2 x. ( n / 2 ) ) + ( 2 x. 1 ) ) )
168 163 167 syl 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. ( ( n / 2 ) + 1 ) ) = ( ( 2 x. ( n / 2 ) ) + ( 2 x. 1 ) ) )
169 147 adantr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> n e. CC )
170 2ne0 
 |-  2 =/= 0
171 divcan2 
 |-  ( ( n e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( 2 x. ( n / 2 ) ) = n )
172 164 170 171 mp3an23 
 |-  ( n e. CC -> ( 2 x. ( n / 2 ) ) = n )
173 169 172 syl 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. ( n / 2 ) ) = n )
174 164 mulridi 
 |-  ( 2 x. 1 ) = 2
175 174 a1i 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. 1 ) = 2 )
176 173 175 oveq12d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( n / 2 ) ) + ( 2 x. 1 ) ) = ( n + 2 ) )
177 168 176 eqtrd 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. ( ( n / 2 ) + 1 ) ) = ( n + 2 ) )
178 177 oveq1d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) = ( ( n + 2 ) - 3 ) )
179 subsub3 
 |-  ( ( n e. CC /\ 3 e. CC /\ 2 e. CC ) -> ( n - ( 3 - 2 ) ) = ( ( n + 2 ) - 3 ) )
180 93 164 179 mp3an23 
 |-  ( n e. CC -> ( n - ( 3 - 2 ) ) = ( ( n + 2 ) - 3 ) )
181 169 180 syl 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( n - ( 3 - 2 ) ) = ( ( n + 2 ) - 3 ) )
182 2p1e3 
 |-  ( 2 + 1 ) = 3
183 93 164 165 182 subaddrii 
 |-  ( 3 - 2 ) = 1
184 183 oveq2i 
 |-  ( n - ( 3 - 2 ) ) = ( n - 1 )
185 181 184 eqtr3di 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n + 2 ) - 3 ) = ( n - 1 ) )
186 178 185 eqtrd 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) = ( n - 1 ) )
187 186 oveq2d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) = ( ( log ` 2 ) x. ( n - 1 ) ) )
188 187 breq2d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) <-> ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( n - 1 ) ) ) )
189 137 zred 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n / 2 ) + 1 ) e. RR )
190 chtcl 
 |-  ( ( ( n / 2 ) + 1 ) e. RR -> ( theta ` ( ( n / 2 ) + 1 ) ) e. RR )
191 189 190 syl 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( theta ` ( ( n / 2 ) + 1 ) ) e. RR )
192 122 adantr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> n e. RR )
193 peano2rem 
 |-  ( n e. RR -> ( n - 1 ) e. RR )
194 192 193 syl 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( n - 1 ) e. RR )
195 remulcl 
 |-  ( ( ( log ` 2 ) e. RR /\ ( n - 1 ) e. RR ) -> ( ( log ` 2 ) x. ( n - 1 ) ) e. RR )
196 100 194 195 sylancr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 2 ) x. ( n - 1 ) ) e. RR )
197 remulcl 
 |-  ( ( ( log ` 2 ) e. RR /\ n e. RR ) -> ( ( log ` 2 ) x. n ) e. RR )
198 100 192 197 sylancr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 2 ) x. n ) e. RR )
199 191 196 198 ltadd1d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( n - 1 ) ) <-> ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) < ( ( ( log ` 2 ) x. ( n - 1 ) ) + ( ( log ` 2 ) x. n ) ) ) )
200 101 a1i 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( log ` 2 ) e. CC )
201 194 recnd 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( n - 1 ) e. CC )
202 200 201 169 adddid 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 2 ) x. ( ( n - 1 ) + n ) ) = ( ( ( log ` 2 ) x. ( n - 1 ) ) + ( ( log ` 2 ) x. n ) ) )
203 adddi 
 |-  ( ( 2 e. CC /\ n e. CC /\ 1 e. CC ) -> ( 2 x. ( n + 1 ) ) = ( ( 2 x. n ) + ( 2 x. 1 ) ) )
204 164 165 203 mp3an13 
 |-  ( n e. CC -> ( 2 x. ( n + 1 ) ) = ( ( 2 x. n ) + ( 2 x. 1 ) ) )
205 169 204 syl 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. ( n + 1 ) ) = ( ( 2 x. n ) + ( 2 x. 1 ) ) )
206 174 oveq2i 
 |-  ( ( 2 x. n ) + ( 2 x. 1 ) ) = ( ( 2 x. n ) + 2 )
207 205 206 eqtrdi 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. ( n + 1 ) ) = ( ( 2 x. n ) + 2 ) )
208 207 oveq1d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( n + 1 ) ) - 3 ) = ( ( ( 2 x. n ) + 2 ) - 3 ) )
209 zmulcl 
 |-  ( ( 2 e. ZZ /\ n e. ZZ ) -> ( 2 x. n ) e. ZZ )
210 117 118 209 sylancr 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 2 x. n ) e. ZZ )
211 210 zcnd 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 2 x. n ) e. CC )
212 211 adantr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. n ) e. CC )
213 subsub3 
 |-  ( ( ( 2 x. n ) e. CC /\ 3 e. CC /\ 2 e. CC ) -> ( ( 2 x. n ) - ( 3 - 2 ) ) = ( ( ( 2 x. n ) + 2 ) - 3 ) )
214 93 164 213 mp3an23 
 |-  ( ( 2 x. n ) e. CC -> ( ( 2 x. n ) - ( 3 - 2 ) ) = ( ( ( 2 x. n ) + 2 ) - 3 ) )
215 212 214 syl 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. n ) - ( 3 - 2 ) ) = ( ( ( 2 x. n ) + 2 ) - 3 ) )
216 183 oveq2i 
 |-  ( ( 2 x. n ) - ( 3 - 2 ) ) = ( ( 2 x. n ) - 1 )
217 169 2timesd 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. n ) = ( n + n ) )
218 217 oveq1d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. n ) - 1 ) = ( ( n + n ) - 1 ) )
219 165 a1i 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> 1 e. CC )
220 169 169 219 addsubd 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n + n ) - 1 ) = ( ( n - 1 ) + n ) )
221 218 220 eqtrd 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. n ) - 1 ) = ( ( n - 1 ) + n ) )
222 216 221 eqtrid 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. n ) - ( 3 - 2 ) ) = ( ( n - 1 ) + n ) )
223 208 215 222 3eqtr2rd 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n - 1 ) + n ) = ( ( 2 x. ( n + 1 ) ) - 3 ) )
224 223 oveq2d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 2 ) x. ( ( n - 1 ) + n ) ) = ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) )
225 202 224 eqtr3d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( ( log ` 2 ) x. ( n - 1 ) ) + ( ( log ` 2 ) x. n ) ) = ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) )
226 225 breq2d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) < ( ( ( log ` 2 ) x. ( n - 1 ) ) + ( ( log ` 2 ) x. n ) ) <-> ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
227 188 199 226 3bitrd 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) <-> ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
228 3nn 
 |-  3 e. NN
229 elfzuz 
 |-  ( ( ( n / 2 ) + 1 ) e. ( 3 ... n ) -> ( ( n / 2 ) + 1 ) e. ( ZZ>= ` 3 ) )
230 154 229 syl 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n / 2 ) + 1 ) e. ( ZZ>= ` 3 ) )
231 eluznn 
 |-  ( ( 3 e. NN /\ ( ( n / 2 ) + 1 ) e. ( ZZ>= ` 3 ) ) -> ( ( n / 2 ) + 1 ) e. NN )
232 228 230 231 sylancr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n / 2 ) + 1 ) e. NN )
233 chtublem 
 |-  ( ( ( n / 2 ) + 1 ) e. NN -> ( theta ` ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 1 ) ) <_ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 4 ) x. ( ( ( n / 2 ) + 1 ) - 1 ) ) ) )
234 232 233 syl 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( theta ` ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 1 ) ) <_ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 4 ) x. ( ( ( n / 2 ) + 1 ) - 1 ) ) ) )
235 177 oveq1d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 1 ) = ( ( n + 2 ) - 1 ) )
236 addsubass 
 |-  ( ( n e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( n + 2 ) - 1 ) = ( n + ( 2 - 1 ) ) )
237 164 165 236 mp3an23 
 |-  ( n e. CC -> ( ( n + 2 ) - 1 ) = ( n + ( 2 - 1 ) ) )
238 169 237 syl 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n + 2 ) - 1 ) = ( n + ( 2 - 1 ) ) )
239 2m1e1 
 |-  ( 2 - 1 ) = 1
240 239 oveq2i 
 |-  ( n + ( 2 - 1 ) ) = ( n + 1 )
241 238 240 eqtrdi 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n + 2 ) - 1 ) = ( n + 1 ) )
242 235 241 eqtrd 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 1 ) = ( n + 1 ) )
243 242 fveq2d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( theta ` ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 1 ) ) = ( theta ` ( n + 1 ) ) )
244 pncan 
 |-  ( ( ( n / 2 ) e. CC /\ 1 e. CC ) -> ( ( ( n / 2 ) + 1 ) - 1 ) = ( n / 2 ) )
245 163 165 244 sylancl 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( ( n / 2 ) + 1 ) - 1 ) = ( n / 2 ) )
246 245 oveq2d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 4 ) x. ( ( ( n / 2 ) + 1 ) - 1 ) ) = ( ( log ` 4 ) x. ( n / 2 ) ) )
247 relogexp 
 |-  ( ( 2 e. RR+ /\ 2 e. ZZ ) -> ( log ` ( 2 ^ 2 ) ) = ( 2 x. ( log ` 2 ) ) )
248 98 117 247 mp2an 
 |-  ( log ` ( 2 ^ 2 ) ) = ( 2 x. ( log ` 2 ) )
249 sq2 
 |-  ( 2 ^ 2 ) = 4
250 249 fveq2i 
 |-  ( log ` ( 2 ^ 2 ) ) = ( log ` 4 )
251 164 101 mulcomi 
 |-  ( 2 x. ( log ` 2 ) ) = ( ( log ` 2 ) x. 2 )
252 248 250 251 3eqtr3i 
 |-  ( log ` 4 ) = ( ( log ` 2 ) x. 2 )
253 252 oveq1i 
 |-  ( ( log ` 4 ) x. ( n / 2 ) ) = ( ( ( log ` 2 ) x. 2 ) x. ( n / 2 ) )
254 164 a1i 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> 2 e. CC )
255 200 254 163 mulassd 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( ( log ` 2 ) x. 2 ) x. ( n / 2 ) ) = ( ( log ` 2 ) x. ( 2 x. ( n / 2 ) ) ) )
256 253 255 eqtrid 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 4 ) x. ( n / 2 ) ) = ( ( log ` 2 ) x. ( 2 x. ( n / 2 ) ) ) )
257 173 oveq2d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 2 ) x. ( 2 x. ( n / 2 ) ) ) = ( ( log ` 2 ) x. n ) )
258 246 256 257 3eqtrd 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 4 ) x. ( ( ( n / 2 ) + 1 ) - 1 ) ) = ( ( log ` 2 ) x. n ) )
259 258 oveq2d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 4 ) x. ( ( ( n / 2 ) + 1 ) - 1 ) ) ) = ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) )
260 234 243 259 3brtr3d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( theta ` ( n + 1 ) ) <_ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) )
261 peano2uz 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( n + 1 ) e. ( ZZ>= ` 3 ) )
262 eluzelz 
 |-  ( ( n + 1 ) e. ( ZZ>= ` 3 ) -> ( n + 1 ) e. ZZ )
263 261 262 syl 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( n + 1 ) e. ZZ )
264 263 zred 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( n + 1 ) e. RR )
265 264 adantr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( n + 1 ) e. RR )
266 chtcl 
 |-  ( ( n + 1 ) e. RR -> ( theta ` ( n + 1 ) ) e. RR )
267 265 266 syl 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( theta ` ( n + 1 ) ) e. RR )
268 191 198 readdcld 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) e. RR )
269 zmulcl 
 |-  ( ( 2 e. ZZ /\ ( n + 1 ) e. ZZ ) -> ( 2 x. ( n + 1 ) ) e. ZZ )
270 117 263 269 sylancr 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 2 x. ( n + 1 ) ) e. ZZ )
271 270 zred 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 2 x. ( n + 1 ) ) e. RR )
272 resubcl 
 |-  ( ( ( 2 x. ( n + 1 ) ) e. RR /\ 3 e. RR ) -> ( ( 2 x. ( n + 1 ) ) - 3 ) e. RR )
273 271 29 272 sylancl 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( 2 x. ( n + 1 ) ) - 3 ) e. RR )
274 273 adantr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( n + 1 ) ) - 3 ) e. RR )
275 remulcl 
 |-  ( ( ( log ` 2 ) e. RR /\ ( ( 2 x. ( n + 1 ) ) - 3 ) e. RR ) -> ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) e. RR )
276 100 274 275 sylancr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) e. RR )
277 lelttr 
 |-  ( ( ( theta ` ( n + 1 ) ) e. RR /\ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) e. RR /\ ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) e. RR ) -> ( ( ( theta ` ( n + 1 ) ) <_ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) /\ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
278 267 268 276 277 syl3anc 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( ( theta ` ( n + 1 ) ) <_ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) /\ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
279 260 278 mpand 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
280 227 279 sylbid 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
281 161 280 syld 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
282 eluzfz2 
 |-  ( n e. ( ZZ>= ` 3 ) -> n e. ( 3 ... n ) )
283 fveq2 
 |-  ( k = n -> ( theta ` k ) = ( theta ` n ) )
284 oveq2 
 |-  ( k = n -> ( 2 x. k ) = ( 2 x. n ) )
285 284 oveq1d 
 |-  ( k = n -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. n ) - 3 ) )
286 285 oveq2d 
 |-  ( k = n -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) )
287 283 286 breq12d 
 |-  ( k = n -> ( ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) ) )
288 287 rspcv 
 |-  ( n e. ( 3 ... n ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) ) )
289 282 288 syl 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) ) )
290 289 adantr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( ( n + 1 ) / 2 ) e. ZZ ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) ) )
291 210 zred 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 2 x. n ) e. RR )
292 29 a1i 
 |-  ( n e. ( ZZ>= ` 3 ) -> 3 e. RR )
293 122 ltp1d 
 |-  ( n e. ( ZZ>= ` 3 ) -> n < ( n + 1 ) )
294 23 a1i 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 2 e. RR /\ 0 < 2 ) )
295 ltmul2 
 |-  ( ( n e. RR /\ ( n + 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( n < ( n + 1 ) <-> ( 2 x. n ) < ( 2 x. ( n + 1 ) ) ) )
296 122 264 294 295 syl3anc 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( n < ( n + 1 ) <-> ( 2 x. n ) < ( 2 x. ( n + 1 ) ) ) )
297 293 296 mpbid 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 2 x. n ) < ( 2 x. ( n + 1 ) ) )
298 291 271 292 297 ltsub1dd 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( 2 x. n ) - 3 ) < ( ( 2 x. ( n + 1 ) ) - 3 ) )
299 resubcl 
 |-  ( ( ( 2 x. n ) e. RR /\ 3 e. RR ) -> ( ( 2 x. n ) - 3 ) e. RR )
300 291 29 299 sylancl 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( 2 x. n ) - 3 ) e. RR )
301 6 a1i 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) )
302 ltmul2 
 |-  ( ( ( ( 2 x. n ) - 3 ) e. RR /\ ( ( 2 x. ( n + 1 ) ) - 3 ) e. RR /\ ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) ) -> ( ( ( 2 x. n ) - 3 ) < ( ( 2 x. ( n + 1 ) ) - 3 ) <-> ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
303 300 273 301 302 syl3anc 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( ( 2 x. n ) - 3 ) < ( ( 2 x. ( n + 1 ) ) - 3 ) <-> ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
304 298 303 mpbid 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) )
305 chtcl 
 |-  ( n e. RR -> ( theta ` n ) e. RR )
306 122 305 syl 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( theta ` n ) e. RR )
307 remulcl 
 |-  ( ( ( log ` 2 ) e. RR /\ ( ( 2 x. n ) - 3 ) e. RR ) -> ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) e. RR )
308 100 300 307 sylancr 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) e. RR )
309 100 273 275 sylancr 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) e. RR )
310 lttr 
 |-  ( ( ( theta ` n ) e. RR /\ ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) e. RR /\ ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) e. RR ) -> ( ( ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) /\ ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) -> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
311 306 308 309 310 syl3anc 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) /\ ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) -> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
312 304 311 mpan2d 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) -> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
313 312 adantr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( ( n + 1 ) / 2 ) e. ZZ ) -> ( ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) -> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
314 evend2 
 |-  ( ( n + 1 ) e. ZZ -> ( 2 || ( n + 1 ) <-> ( ( n + 1 ) / 2 ) e. ZZ ) )
315 263 314 syl 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 2 || ( n + 1 ) <-> ( ( n + 1 ) / 2 ) e. ZZ ) )
316 2lt3 
 |-  2 < 3
317 1 29 ltnlei 
 |-  ( 2 < 3 <-> -. 3 <_ 2 )
318 316 317 mpbi 
 |-  -. 3 <_ 2
319 breq2 
 |-  ( 2 = ( n + 1 ) -> ( 3 <_ 2 <-> 3 <_ ( n + 1 ) ) )
320 318 319 mtbii 
 |-  ( 2 = ( n + 1 ) -> -. 3 <_ ( n + 1 ) )
321 eluzle 
 |-  ( ( n + 1 ) e. ( ZZ>= ` 3 ) -> 3 <_ ( n + 1 ) )
322 261 321 syl 
 |-  ( n e. ( ZZ>= ` 3 ) -> 3 <_ ( n + 1 ) )
323 320 322 nsyl3 
 |-  ( n e. ( ZZ>= ` 3 ) -> -. 2 = ( n + 1 ) )
324 323 adantr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n + 1 ) e. Prime ) -> -. 2 = ( n + 1 ) )
325 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
326 117 325 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
327 simpr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n + 1 ) e. Prime ) -> ( n + 1 ) e. Prime )
328 dvdsprm 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ ( n + 1 ) e. Prime ) -> ( 2 || ( n + 1 ) <-> 2 = ( n + 1 ) ) )
329 326 327 328 sylancr 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n + 1 ) e. Prime ) -> ( 2 || ( n + 1 ) <-> 2 = ( n + 1 ) ) )
330 324 329 mtbird 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( n + 1 ) e. Prime ) -> -. 2 || ( n + 1 ) )
331 330 ex 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( n + 1 ) e. Prime -> -. 2 || ( n + 1 ) ) )
332 331 con2d 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 2 || ( n + 1 ) -> -. ( n + 1 ) e. Prime ) )
333 315 332 sylbird 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( ( n + 1 ) / 2 ) e. ZZ -> -. ( n + 1 ) e. Prime ) )
334 333 imp 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( ( n + 1 ) / 2 ) e. ZZ ) -> -. ( n + 1 ) e. Prime )
335 chtnprm 
 |-  ( ( n e. ZZ /\ -. ( n + 1 ) e. Prime ) -> ( theta ` ( n + 1 ) ) = ( theta ` n ) )
336 118 334 335 syl2an2r 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( ( n + 1 ) / 2 ) e. ZZ ) -> ( theta ` ( n + 1 ) ) = ( theta ` n ) )
337 336 breq1d 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( ( n + 1 ) / 2 ) e. ZZ ) -> ( ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) <-> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
338 313 337 sylibrd 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( ( n + 1 ) / 2 ) e. ZZ ) -> ( ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
339 290 338 syld 
 |-  ( ( n e. ( ZZ>= ` 3 ) /\ ( ( n + 1 ) / 2 ) e. ZZ ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
340 zeo 
 |-  ( n e. ZZ -> ( ( n / 2 ) e. ZZ \/ ( ( n + 1 ) / 2 ) e. ZZ ) )
341 118 340 syl 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( n / 2 ) e. ZZ \/ ( ( n + 1 ) / 2 ) e. ZZ ) )
342 281 339 341 mpjaodan 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
343 ovex 
 |-  ( n + 1 ) e. _V
344 fveq2 
 |-  ( k = ( n + 1 ) -> ( theta ` k ) = ( theta ` ( n + 1 ) ) )
345 oveq2 
 |-  ( k = ( n + 1 ) -> ( 2 x. k ) = ( 2 x. ( n + 1 ) ) )
346 345 oveq1d 
 |-  ( k = ( n + 1 ) -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. ( n + 1 ) ) - 3 ) )
347 346 oveq2d 
 |-  ( k = ( n + 1 ) -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) )
348 344 347 breq12d 
 |-  ( k = ( n + 1 ) -> ( ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
349 343 348 ralsn 
 |-  ( A. k e. { ( n + 1 ) } ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) )
350 342 349 imbitrrdi 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> A. k e. { ( n + 1 ) } ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
351 350 ancld 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) /\ A. k e. { ( n + 1 ) } ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) ) )
352 ralun 
 |-  ( ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) /\ A. k e. { ( n + 1 ) } ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) -> A. k e. ( ( 3 ... n ) u. { ( n + 1 ) } ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) )
353 fzsuc 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( 3 ... ( n + 1 ) ) = ( ( 3 ... n ) u. { ( n + 1 ) } ) )
354 353 raleqdv 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( A. k e. ( 3 ... ( n + 1 ) ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> A. k e. ( ( 3 ... n ) u. { ( n + 1 ) } ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
355 352 354 imbitrrid 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) /\ A. k e. { ( n + 1 ) } ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) -> A. k e. ( 3 ... ( n + 1 ) ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
356 351 355 syld 
 |-  ( n e. ( ZZ>= ` 3 ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> A. k e. ( 3 ... ( n + 1 ) ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
357 69 71 73 75 112 356 uzind4i 
 |-  ( ( |_ ` N ) e. ( ZZ>= ` 3 ) -> A. k e. ( 3 ... ( |_ ` N ) ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) )
358 eluzfz2 
 |-  ( ( |_ ` N ) e. ( ZZ>= ` 3 ) -> ( |_ ` N ) e. ( 3 ... ( |_ ` N ) ) )
359 67 357 358 rspcdva 
 |-  ( ( |_ ` N ) e. ( ZZ>= ` 3 ) -> ( theta ` ( |_ ` N ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) )
360 62 359 syl 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( theta ` ( |_ ` N ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) )
361 58 360 eqbrtrrd 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( theta ` N ) < ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) )
362 33 adantr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( 2 x. N ) e. RR )
363 29 a1i 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> 3 e. RR )
364 flle 
 |-  ( N e. RR -> ( |_ ` N ) <_ N )
365 364 ad2antrr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( |_ ` N ) <_ N )
366 21 adantr 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> N e. RR )
367 23 a1i 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( 2 e. RR /\ 0 < 2 ) )
368 lemul2 
 |-  ( ( ( |_ ` N ) e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( |_ ` N ) <_ N <-> ( 2 x. ( |_ ` N ) ) <_ ( 2 x. N ) ) )
369 48 366 367 368 syl3anc 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( |_ ` N ) <_ N <-> ( 2 x. ( |_ ` N ) ) <_ ( 2 x. N ) ) )
370 365 369 mpbid 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( 2 x. ( |_ ` N ) ) <_ ( 2 x. N ) )
371 50 362 363 370 lesub1dd 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( 2 x. ( |_ ` N ) ) - 3 ) <_ ( ( 2 x. N ) - 3 ) )
372 6 a1i 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) )
373 lemul2 
 |-  ( ( ( ( 2 x. ( |_ ` N ) ) - 3 ) e. RR /\ ( ( 2 x. N ) - 3 ) e. RR /\ ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) ) -> ( ( ( 2 x. ( |_ ` N ) ) - 3 ) <_ ( ( 2 x. N ) - 3 ) <-> ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) <_ ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) ) )
374 52 55 372 373 syl3anc 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( ( 2 x. ( |_ ` N ) ) - 3 ) <_ ( ( 2 x. N ) - 3 ) <-> ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) <_ ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) ) )
375 371 374 mpbid 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) <_ ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )
376 46 54 57 361 375 ltletrd 
 |-  ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( theta ` N ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )
377 117 a1i 
 |-  ( ( N e. RR /\ 2 < N ) -> 2 e. ZZ )
378 flcl 
 |-  ( N e. RR -> ( |_ ` N ) e. ZZ )
379 378 adantr 
 |-  ( ( N e. RR /\ 2 < N ) -> ( |_ ` N ) e. ZZ )
380 ltle 
 |-  ( ( 2 e. RR /\ N e. RR ) -> ( 2 < N -> 2 <_ N ) )
381 1 380 mpan 
 |-  ( N e. RR -> ( 2 < N -> 2 <_ N ) )
382 flge 
 |-  ( ( N e. RR /\ 2 e. ZZ ) -> ( 2 <_ N <-> 2 <_ ( |_ ` N ) ) )
383 117 382 mpan2 
 |-  ( N e. RR -> ( 2 <_ N <-> 2 <_ ( |_ ` N ) ) )
384 381 383 sylibd 
 |-  ( N e. RR -> ( 2 < N -> 2 <_ ( |_ ` N ) ) )
385 384 imp 
 |-  ( ( N e. RR /\ 2 < N ) -> 2 <_ ( |_ ` N ) )
386 eluz2 
 |-  ( ( |_ ` N ) e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ( |_ ` N ) e. ZZ /\ 2 <_ ( |_ ` N ) ) )
387 377 379 385 386 syl3anbrc 
 |-  ( ( N e. RR /\ 2 < N ) -> ( |_ ` N ) e. ( ZZ>= ` 2 ) )
388 uzp1 
 |-  ( ( |_ ` N ) e. ( ZZ>= ` 2 ) -> ( ( |_ ` N ) = 2 \/ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) )
389 387 388 syl 
 |-  ( ( N e. RR /\ 2 < N ) -> ( ( |_ ` N ) = 2 \/ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) )
390 44 376 389 mpjaodan 
 |-  ( ( N e. RR /\ 2 < N ) -> ( theta ` N ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )