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 ( ( 𝑁 ∈ ℝ ∧ 2 < 𝑁 ) → ( θ ‘ 𝑁 ) < ( ( log ‘ 2 ) · ( ( 2 · 𝑁 ) − 3 ) ) )

Proof

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