# 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 ${⊢}\left({N}\in ℝ\wedge 2<{N}\right)\to \theta \left({N}\right)<\mathrm{log}2\left(2\cdot {N}-3\right)$

### Proof

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