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