Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . 5
⊢
((⌊‘𝑁) =
2 → (θ‘(⌊‘𝑁)) = (θ‘2)) |
2 | | 2re 10967 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
3 | | 1lt2 11071 |
. . . . . . . . . . 11
⊢ 1 <
2 |
4 | | rplogcl 24154 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ 1 < 2) → (log‘2) ∈
ℝ+) |
5 | 2, 3, 4 | mp2an 704 |
. . . . . . . . . 10
⊢
(log‘2) ∈ ℝ+ |
6 | | elrp 11710 |
. . . . . . . . . 10
⊢
((log‘2) ∈ ℝ+ ↔ ((log‘2) ∈
ℝ ∧ 0 < (log‘2))) |
7 | 5, 6 | mpbi 219 |
. . . . . . . . 9
⊢
((log‘2) ∈ ℝ ∧ 0 <
(log‘2)) |
8 | 7 | simpli 473 |
. . . . . . . 8
⊢
(log‘2) ∈ ℝ |
9 | 8 | recni 9931 |
. . . . . . 7
⊢
(log‘2) ∈ ℂ |
10 | 9 | mulid1i 9921 |
. . . . . 6
⊢
((log‘2) · 1) = (log‘2) |
11 | | cht2 24698 |
. . . . . 6
⊢
(θ‘2) = (log‘2) |
12 | 10, 11 | eqtr4i 2635 |
. . . . 5
⊢
((log‘2) · 1) = (θ‘2) |
13 | 1, 12 | syl6reqr 2663 |
. . . 4
⊢
((⌊‘𝑁) =
2 → ((log‘2) · 1) = (θ‘(⌊‘𝑁))) |
14 | | chtfl 24675 |
. . . . 5
⊢ (𝑁 ∈ ℝ →
(θ‘(⌊‘𝑁)) = (θ‘𝑁)) |
15 | 14 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) →
(θ‘(⌊‘𝑁)) = (θ‘𝑁)) |
16 | 13, 15 | sylan9eqr 2666 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ ((log‘2) · 1) = (θ‘𝑁)) |
17 | | 2t2e4 11054 |
. . . . . . 7
⊢ (2
· 2) = 4 |
18 | | df-4 10958 |
. . . . . . 7
⊢ 4 = (3 +
1) |
19 | 17, 18 | eqtri 2632 |
. . . . . 6
⊢ (2
· 2) = (3 + 1) |
20 | | simplr 788 |
. . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ 2 < 𝑁) |
21 | 2 | a1i 11 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ 2 ∈ ℝ) |
22 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) → 𝑁 ∈ ℝ) |
23 | 22 | adantr 480 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ 𝑁 ∈
ℝ) |
24 | | 2pos 10989 |
. . . . . . . . . 10
⊢ 0 <
2 |
25 | 2, 24 | pm3.2i 470 |
. . . . . . . . 9
⊢ (2 ∈
ℝ ∧ 0 < 2) |
26 | 25 | a1i 11 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ (2 ∈ ℝ ∧ 0 < 2)) |
27 | | ltmul2 10753 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (2 < 𝑁 ↔ (2 · 2) < (2
· 𝑁))) |
28 | 21, 23, 26, 27 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ (2 < 𝑁 ↔ (2
· 2) < (2 · 𝑁))) |
29 | 20, 28 | mpbid 221 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ (2 · 2) < (2 · 𝑁)) |
30 | 19, 29 | syl5eqbrr 4619 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ (3 + 1) < (2 · 𝑁)) |
31 | | 3re 10971 |
. . . . . . 7
⊢ 3 ∈
ℝ |
32 | 31 | a1i 11 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ 3 ∈ ℝ) |
33 | | 1red 9934 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ 1 ∈ ℝ) |
34 | | remulcl 9900 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ) → (2 · 𝑁) ∈ ℝ) |
35 | 2, 22, 34 | sylancr 694 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) → (2 · 𝑁) ∈
ℝ) |
36 | 35 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ (2 · 𝑁)
∈ ℝ) |
37 | 32, 33, 36 | ltaddsub2d 10507 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ ((3 + 1) < (2 · 𝑁) ↔ 1 < ((2 · 𝑁) − 3))) |
38 | 30, 37 | mpbid 221 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ 1 < ((2 · 𝑁) − 3)) |
39 | | resubcl 10224 |
. . . . . . 7
⊢ (((2
· 𝑁) ∈ ℝ
∧ 3 ∈ ℝ) → ((2 · 𝑁) − 3) ∈
ℝ) |
40 | 35, 31, 39 | sylancl 693 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) → ((2 ·
𝑁) − 3) ∈
ℝ) |
41 | 40 | adantr 480 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ ((2 · 𝑁)
− 3) ∈ ℝ) |
42 | 7 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ ((log‘2) ∈ ℝ ∧ 0 <
(log‘2))) |
43 | | ltmul2 10753 |
. . . . 5
⊢ ((1
∈ ℝ ∧ ((2 · 𝑁) − 3) ∈ ℝ ∧
((log‘2) ∈ ℝ ∧ 0 < (log‘2))) → (1 < ((2
· 𝑁) − 3)
↔ ((log‘2) · 1) < ((log‘2) · ((2 ·
𝑁) −
3)))) |
44 | 33, 41, 42, 43 | syl3anc 1318 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ (1 < ((2 · 𝑁) − 3) ↔ ((log‘2) ·
1) < ((log‘2) · ((2 · 𝑁) − 3)))) |
45 | 38, 44 | mpbid 221 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ ((log‘2) · 1) < ((log‘2) · ((2 ·
𝑁) −
3))) |
46 | 16, 45 | eqbrtrrd 4607 |
. 2
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) = 2)
→ (θ‘𝑁)
< ((log‘2) · ((2 · 𝑁) − 3))) |
47 | | chtcl 24635 |
. . . 4
⊢ (𝑁 ∈ ℝ →
(θ‘𝑁) ∈
ℝ) |
48 | 47 | ad2antrr 758 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (θ‘𝑁) ∈ ℝ) |
49 | | reflcl 12459 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ →
(⌊‘𝑁) ∈
ℝ) |
50 | 49 | ad2antrr 758 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (⌊‘𝑁) ∈ ℝ) |
51 | | remulcl 9900 |
. . . . . 6
⊢ ((2
∈ ℝ ∧ (⌊‘𝑁) ∈ ℝ) → (2 ·
(⌊‘𝑁)) ∈
ℝ) |
52 | 2, 50, 51 | sylancr 694 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (2 · (⌊‘𝑁)) ∈
ℝ) |
53 | | resubcl 10224 |
. . . . 5
⊢ (((2
· (⌊‘𝑁))
∈ ℝ ∧ 3 ∈ ℝ) → ((2 · (⌊‘𝑁)) − 3) ∈
ℝ) |
54 | 52, 31, 53 | sylancl 693 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((2 ·
(⌊‘𝑁)) −
3) ∈ ℝ) |
55 | | remulcl 9900 |
. . . 4
⊢
(((log‘2) ∈ ℝ ∧ ((2 · (⌊‘𝑁)) − 3) ∈ ℝ)
→ ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ∈
ℝ) |
56 | 8, 54, 55 | sylancr 694 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((log‘2) · ((2
· (⌊‘𝑁))
− 3)) ∈ ℝ) |
57 | 40 | adantr 480 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((2 · 𝑁) − 3) ∈
ℝ) |
58 | | remulcl 9900 |
. . . 4
⊢
(((log‘2) ∈ ℝ ∧ ((2 · 𝑁) − 3) ∈ ℝ) →
((log‘2) · ((2 · 𝑁) − 3)) ∈
ℝ) |
59 | 8, 57, 58 | sylancr 694 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((log‘2) · ((2
· 𝑁) − 3))
∈ ℝ) |
60 | 15 | adantr 480 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) →
(θ‘(⌊‘𝑁)) = (θ‘𝑁)) |
61 | | simpr 476 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (⌊‘𝑁) ∈ (ℤ≥‘(2 +
1))) |
62 | | df-3 10957 |
. . . . . . 7
⊢ 3 = (2 +
1) |
63 | 62 | fveq2i 6106 |
. . . . . 6
⊢
(ℤ≥‘3) = (ℤ≥‘(2 +
1)) |
64 | 61, 63 | syl6eleqr 2699 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (⌊‘𝑁) ∈
(ℤ≥‘3)) |
65 | | eluzfz2 12220 |
. . . . . 6
⊢
((⌊‘𝑁)
∈ (ℤ≥‘3) → (⌊‘𝑁) ∈ (3...(⌊‘𝑁))) |
66 | | 3z 11287 |
. . . . . . 7
⊢ 3 ∈
ℤ |
67 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 3 → (3...𝑥) = (3...3)) |
68 | 67 | raleqdv 3121 |
. . . . . . 7
⊢ (𝑥 = 3 → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) ↔
∀𝑘 ∈
(3...3)(θ‘𝑘)
< ((log‘2) · ((2 · 𝑘) − 3)))) |
69 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (3...𝑥) = (3...𝑛)) |
70 | 69 | raleqdv 3121 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) ↔
∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) −
3)))) |
71 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → (3...𝑥) = (3...(𝑛 + 1))) |
72 | 71 | raleqdv 3121 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) ↔
∀𝑘 ∈
(3...(𝑛 +
1))(θ‘𝑘) <
((log‘2) · ((2 · 𝑘) − 3)))) |
73 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = (⌊‘𝑁) → (3...𝑥) = (3...(⌊‘𝑁))) |
74 | 73 | raleqdv 3121 |
. . . . . . 7
⊢ (𝑥 = (⌊‘𝑁) → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) ↔
∀𝑘 ∈
(3...(⌊‘𝑁))(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) −
3)))) |
75 | | 6lt8 11093 |
. . . . . . . . . . 11
⊢ 6 <
8 |
76 | | 6re 10978 |
. . . . . . . . . . . . 13
⊢ 6 ∈
ℝ |
77 | | 6pos 10996 |
. . . . . . . . . . . . 13
⊢ 0 <
6 |
78 | 76, 77 | elrpii 11711 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℝ+ |
79 | | 8re 10982 |
. . . . . . . . . . . . 13
⊢ 8 ∈
ℝ |
80 | | 8pos 10998 |
. . . . . . . . . . . . 13
⊢ 0 <
8 |
81 | 79, 80 | elrpii 11711 |
. . . . . . . . . . . 12
⊢ 8 ∈
ℝ+ |
82 | | logltb 24150 |
. . . . . . . . . . . 12
⊢ ((6
∈ ℝ+ ∧ 8 ∈ ℝ+) → (6 < 8
↔ (log‘6) < (log‘8))) |
83 | 78, 81, 82 | mp2an 704 |
. . . . . . . . . . 11
⊢ (6 < 8
↔ (log‘6) < (log‘8)) |
84 | 75, 83 | mpbi 219 |
. . . . . . . . . 10
⊢
(log‘6) < (log‘8) |
85 | 84 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 ∈ (3...3) →
(log‘6) < (log‘8)) |
86 | | elfz1eq 12223 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (3...3) → 𝑘 = 3) |
87 | 86 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (3...3) →
(θ‘𝑘) =
(θ‘3)) |
88 | | cht3 24699 |
. . . . . . . . . 10
⊢
(θ‘3) = (log‘6) |
89 | 87, 88 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑘 ∈ (3...3) →
(θ‘𝑘) =
(log‘6)) |
90 | 86 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (3...3) → (2
· 𝑘) = (2 ·
3)) |
91 | 90 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (3...3) → ((2
· 𝑘) − 3) =
((2 · 3) − 3)) |
92 | | 3cn 10972 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℂ |
93 | 92 | 2timesi 11024 |
. . . . . . . . . . . . . 14
⊢ (2
· 3) = (3 + 3) |
94 | 93 | oveq1i 6559 |
. . . . . . . . . . . . 13
⊢ ((2
· 3) − 3) = ((3 + 3) − 3) |
95 | 92, 92 | pncan3oi 10176 |
. . . . . . . . . . . . 13
⊢ ((3 + 3)
− 3) = 3 |
96 | 94, 95 | eqtri 2632 |
. . . . . . . . . . . 12
⊢ ((2
· 3) − 3) = 3 |
97 | 91, 96 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (3...3) → ((2
· 𝑘) − 3) =
3) |
98 | 97 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (3...3) →
((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) ·
3)) |
99 | | 2rp 11713 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ+ |
100 | | relogcl 24126 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℝ+ → (log‘2) ∈ ℝ) |
101 | 99, 100 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(log‘2) ∈ ℝ |
102 | 101 | recni 9931 |
. . . . . . . . . . . . 13
⊢
(log‘2) ∈ ℂ |
103 | 102, 92 | mulcomi 9925 |
. . . . . . . . . . . 12
⊢
((log‘2) · 3) = (3 · (log‘2)) |
104 | | relogexp 24146 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ+ ∧ 3 ∈ ℤ) →
(log‘(2↑3)) = (3 · (log‘2))) |
105 | 99, 66, 104 | mp2an 704 |
. . . . . . . . . . . 12
⊢
(log‘(2↑3)) = (3 · (log‘2)) |
106 | 103, 105 | eqtr4i 2635 |
. . . . . . . . . . 11
⊢
((log‘2) · 3) = (log‘(2↑3)) |
107 | | cu2 12825 |
. . . . . . . . . . . 12
⊢
(2↑3) = 8 |
108 | 107 | fveq2i 6106 |
. . . . . . . . . . 11
⊢
(log‘(2↑3)) = (log‘8) |
109 | 106, 108 | eqtri 2632 |
. . . . . . . . . 10
⊢
((log‘2) · 3) = (log‘8) |
110 | 98, 109 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑘 ∈ (3...3) →
((log‘2) · ((2 · 𝑘) − 3)) =
(log‘8)) |
111 | 85, 89, 110 | 3brtr4d 4615 |
. . . . . . . 8
⊢ (𝑘 ∈ (3...3) →
(θ‘𝑘) <
((log‘2) · ((2 · 𝑘) − 3))) |
112 | 111 | rgen 2906 |
. . . . . . 7
⊢
∀𝑘 ∈
(3...3)(θ‘𝑘)
< ((log‘2) · ((2 · 𝑘) − 3)) |
113 | | df-2 10956 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 = (1 +
1) |
114 | | 2div2e1 11027 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2 / 2) =
1 |
115 | | eluzle 11576 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈
(ℤ≥‘3) → 3 ≤ 𝑛) |
116 | 62, 115 | syl5eqbrr 4619 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 + 1) ≤ 𝑛) |
117 | | 2z 11286 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℤ |
118 | | eluzelz 11573 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈
(ℤ≥‘3) → 𝑛 ∈ ℤ) |
119 | | zltp1le 11304 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℤ) → (2 < 𝑛 ↔ (2 + 1) ≤ 𝑛)) |
120 | 117, 118,
119 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 < 𝑛 ↔ (2 + 1) ≤ 𝑛)) |
121 | 116, 120 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈
(ℤ≥‘3) → 2 < 𝑛) |
122 | | eluzelre 11574 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈
(ℤ≥‘3) → 𝑛 ∈ ℝ) |
123 | | ltdiv1 10766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
∈ ℝ ∧ 𝑛
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (2 < 𝑛 ↔ (2 / 2) < (𝑛 / 2))) |
124 | 2, 25, 123 | mp3an13 1407 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ℝ → (2 <
𝑛 ↔ (2 / 2) <
(𝑛 / 2))) |
125 | 122, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 < 𝑛 ↔ (2 / 2) < (𝑛 / 2))) |
126 | 121, 125 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 / 2) < (𝑛 / 2)) |
127 | 114, 126 | syl5eqbrr 4619 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈
(ℤ≥‘3) → 1 < (𝑛 / 2)) |
128 | 122 | rehalfcld 11156 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈
(ℤ≥‘3) → (𝑛 / 2) ∈ ℝ) |
129 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℝ |
130 | | ltadd1 10374 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℝ ∧ (𝑛 /
2) ∈ ℝ ∧ 1 ∈ ℝ) → (1 < (𝑛 / 2) ↔ (1 + 1) < ((𝑛 / 2) + 1))) |
131 | 129, 129,
130 | mp3an13 1407 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 / 2) ∈ ℝ → (1
< (𝑛 / 2) ↔ (1 + 1)
< ((𝑛 / 2) +
1))) |
132 | 128, 131 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈
(ℤ≥‘3) → (1 < (𝑛 / 2) ↔ (1 + 1) < ((𝑛 / 2) + 1))) |
133 | 127, 132 | mpbid 221 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘3) → (1 + 1) < ((𝑛 / 2) + 1)) |
134 | 113, 133 | syl5eqbr 4618 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → 2 < ((𝑛 / 2) + 1)) |
135 | 134 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 2 < ((𝑛 / 2) + 1)) |
136 | | peano2z 11295 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 / 2) ∈ ℤ →
((𝑛 / 2) + 1) ∈
ℤ) |
137 | 136 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈
ℤ) |
138 | | zltp1le 11304 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℤ ∧ ((𝑛 /
2) + 1) ∈ ℤ) → (2 < ((𝑛 / 2) + 1) ↔ (2 + 1) ≤ ((𝑛 / 2) + 1))) |
139 | 117, 137,
138 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 < ((𝑛 / 2) + 1) ↔ (2 + 1) ≤
((𝑛 / 2) +
1))) |
140 | 135, 139 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 + 1) ≤
((𝑛 / 2) +
1)) |
141 | 62, 140 | syl5eqbr 4618 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 3 ≤ ((𝑛 / 2) + 1)) |
142 | | 1red 9934 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → 1 ∈ ℝ) |
143 | | ltle 10005 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℝ ∧ (𝑛 /
2) ∈ ℝ) → (1 < (𝑛 / 2) → 1 ≤ (𝑛 / 2))) |
144 | 129, 128,
143 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘3) → (1 < (𝑛 / 2) → 1 ≤ (𝑛 / 2))) |
145 | 127, 144 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → 1 ≤ (𝑛 / 2)) |
146 | 142, 128,
128, 145 | leadd2dd 10521 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → ((𝑛 / 2) + 1) ≤ ((𝑛 / 2) + (𝑛 / 2))) |
147 | 122 | recnd 9947 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → 𝑛 ∈ ℂ) |
148 | 147 | 2halvesd 11155 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → ((𝑛 / 2) + (𝑛 / 2)) = 𝑛) |
149 | 146, 148 | breqtrd 4609 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘3) → ((𝑛 / 2) + 1) ≤ 𝑛) |
150 | 149 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ≤ 𝑛) |
151 | | elfz 12203 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑛 / 2) + 1) ∈ ℤ ∧
3 ∈ ℤ ∧ 𝑛
∈ ℤ) → (((𝑛
/ 2) + 1) ∈ (3...𝑛)
↔ (3 ≤ ((𝑛 / 2) +
1) ∧ ((𝑛 / 2) + 1) ≤
𝑛))) |
152 | 66, 151 | mp3an2 1404 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑛 / 2) + 1) ∈ ℤ ∧
𝑛 ∈ ℤ) →
(((𝑛 / 2) + 1) ∈
(3...𝑛) ↔ (3 ≤
((𝑛 / 2) + 1) ∧ ((𝑛 / 2) + 1) ≤ 𝑛))) |
153 | 136, 118,
152 | syl2anr 494 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((𝑛 / 2) + 1) ∈ (3...𝑛) ↔ (3 ≤ ((𝑛 / 2) + 1) ∧ ((𝑛 / 2) + 1) ≤ 𝑛))) |
154 | 141, 150,
153 | mpbir2and 959 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ (3...𝑛)) |
155 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = ((𝑛 / 2) + 1) → (θ‘𝑘) = (θ‘((𝑛 / 2) + 1))) |
156 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = ((𝑛 / 2) + 1) → (2 · 𝑘) = (2 · ((𝑛 / 2) + 1))) |
157 | 156 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = ((𝑛 / 2) + 1) → ((2 · 𝑘) − 3) = ((2 ·
((𝑛 / 2) + 1)) −
3)) |
158 | 157 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = ((𝑛 / 2) + 1) → ((log‘2) · ((2
· 𝑘) − 3)) =
((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3))) |
159 | 155, 158 | breq12d 4596 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = ((𝑛 / 2) + 1) → ((θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) − 3))
↔ (θ‘((𝑛 /
2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)))) |
160 | 159 | rspcv 3278 |
. . . . . . . . . . . . 13
⊢ (((𝑛 / 2) + 1) ∈ (3...𝑛) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(θ‘((𝑛 / 2) +
1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)))) |
161 | 154, 160 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(θ‘((𝑛 / 2) +
1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)))) |
162 | 128 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈
(ℤ≥‘3) → (𝑛 / 2) ∈ ℂ) |
163 | 162 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 / 2) ∈
ℂ) |
164 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℂ |
165 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℂ |
166 | | adddi 9904 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ ℂ ∧ (𝑛 /
2) ∈ ℂ ∧ 1 ∈ ℂ) → (2 · ((𝑛 / 2) + 1)) = ((2 ·
(𝑛 / 2)) + (2 ·
1))) |
167 | 164, 165,
166 | mp3an13 1407 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 / 2) ∈ ℂ → (2
· ((𝑛 / 2) + 1)) =
((2 · (𝑛 / 2)) + (2
· 1))) |
168 | 163, 167 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 ·
((𝑛 / 2) + 1)) = ((2
· (𝑛 / 2)) + (2
· 1))) |
169 | 147 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 𝑛 ∈
ℂ) |
170 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ≠
0 |
171 | | divcan2 10572 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (2 · (𝑛 / 2)) = 𝑛) |
172 | 164, 170,
171 | mp3an23 1408 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℂ → (2
· (𝑛 / 2)) = 𝑛) |
173 | 169, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 ·
(𝑛 / 2)) = 𝑛) |
174 | 164 | mulid1i 9921 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 1) = 2 |
175 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · 1) =
2) |
176 | 173, 175 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
(𝑛 / 2)) + (2 · 1))
= (𝑛 + 2)) |
177 | 168, 176 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 ·
((𝑛 / 2) + 1)) = (𝑛 + 2)) |
178 | 177 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
((𝑛 / 2) + 1)) − 3) =
((𝑛 + 2) −
3)) |
179 | | 2p1e3 11028 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2 + 1) =
3 |
180 | 92, 164, 165, 179 | subaddrii 10249 |
. . . . . . . . . . . . . . . . . . 19
⊢ (3
− 2) = 1 |
181 | 180 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 − (3 − 2)) = (𝑛 − 1) |
182 | | subsub3 10192 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℂ ∧ 3 ∈
ℂ ∧ 2 ∈ ℂ) → (𝑛 − (3 − 2)) = ((𝑛 + 2) −
3)) |
183 | 92, 164, 182 | mp3an23 1408 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℂ → (𝑛 − (3 − 2)) =
((𝑛 + 2) −
3)) |
184 | 169, 183 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − (3 − 2)) =
((𝑛 + 2) −
3)) |
185 | 181, 184 | syl5reqr 2659 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 3) = (𝑛 − 1)) |
186 | 178, 185 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
((𝑛 / 2) + 1)) − 3) =
(𝑛 −
1)) |
187 | 186 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2)
· ((2 · ((𝑛 /
2) + 1)) − 3)) = ((log‘2) · (𝑛 − 1))) |
188 | 187 | breq2d 4595 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
((θ‘((𝑛 / 2) +
1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) ↔
(θ‘((𝑛 / 2) +
1)) < ((log‘2) · (𝑛 − 1)))) |
189 | 137 | zred 11358 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈
ℝ) |
190 | | chtcl 24635 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 / 2) + 1) ∈ ℝ →
(θ‘((𝑛 / 2) +
1)) ∈ ℝ) |
191 | 189, 190 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
(θ‘((𝑛 / 2) +
1)) ∈ ℝ) |
192 | 122 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 𝑛 ∈
ℝ) |
193 | | peano2rem 10227 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈
ℝ) |
194 | 192, 193 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − 1) ∈
ℝ) |
195 | | remulcl 9900 |
. . . . . . . . . . . . . . . 16
⊢
(((log‘2) ∈ ℝ ∧ (𝑛 − 1) ∈ ℝ) →
((log‘2) · (𝑛
− 1)) ∈ ℝ) |
196 | 101, 194,
195 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2)
· (𝑛 − 1))
∈ ℝ) |
197 | | remulcl 9900 |
. . . . . . . . . . . . . . . 16
⊢
(((log‘2) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((log‘2)
· 𝑛) ∈
ℝ) |
198 | 101, 192,
197 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2)
· 𝑛) ∈
ℝ) |
199 | 191, 196,
198 | ltadd1d 10499 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
((θ‘((𝑛 / 2) +
1)) < ((log‘2) · (𝑛 − 1)) ↔ ((θ‘((𝑛 / 2) + 1)) + ((log‘2)
· 𝑛)) <
(((log‘2) · (𝑛
− 1)) + ((log‘2) · 𝑛)))) |
200 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (log‘2)
∈ ℂ) |
201 | 194 | recnd 9947 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − 1) ∈
ℂ) |
202 | 200, 201,
169 | adddid 9943 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2)
· ((𝑛 − 1) +
𝑛)) = (((log‘2)
· (𝑛 − 1)) +
((log‘2) · 𝑛))) |
203 | | adddi 9904 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2
∈ ℂ ∧ 𝑛
∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1))) |
204 | 164, 165,
203 | mp3an13 1407 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℂ → (2
· (𝑛 + 1)) = ((2
· 𝑛) + (2 ·
1))) |
205 | 169, 204 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 ·
(𝑛 + 1)) = ((2 ·
𝑛) + (2 ·
1))) |
206 | 174 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
· 𝑛) + (2 ·
1)) = ((2 · 𝑛) +
2) |
207 | 205, 206 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 ·
(𝑛 + 1)) = ((2 ·
𝑛) + 2)) |
208 | 207 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
(𝑛 + 1)) − 3) = (((2
· 𝑛) + 2) −
3)) |
209 | | zmulcl 11303 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℤ) → (2 · 𝑛) ∈ ℤ) |
210 | 117, 118,
209 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 · 𝑛) ∈ ℤ) |
211 | 210 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 · 𝑛) ∈ ℂ) |
212 | 211 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 ·
𝑛) ∈
ℂ) |
213 | | subsub3 10192 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((2
· 𝑛) ∈ ℂ
∧ 3 ∈ ℂ ∧ 2 ∈ ℂ) → ((2 · 𝑛) − (3 − 2)) = (((2
· 𝑛) + 2) −
3)) |
214 | 92, 164, 213 | mp3an23 1408 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
· 𝑛) ∈ ℂ
→ ((2 · 𝑛)
− (3 − 2)) = (((2 · 𝑛) + 2) − 3)) |
215 | 212, 214 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
𝑛) − (3 − 2)) =
(((2 · 𝑛) + 2)
− 3)) |
216 | 180 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
· 𝑛) − (3
− 2)) = ((2 · 𝑛) − 1) |
217 | 169 | 2timesd 11152 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 ·
𝑛) = (𝑛 + 𝑛)) |
218 | 217 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
𝑛) − 1) = ((𝑛 + 𝑛) − 1)) |
219 | 165 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 1 ∈
ℂ) |
220 | 169, 169,
219 | addsubd 10292 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 𝑛) − 1) = ((𝑛 − 1) + 𝑛)) |
221 | 218, 220 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
𝑛) − 1) = ((𝑛 − 1) + 𝑛)) |
222 | 216, 221 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
𝑛) − (3 − 2)) =
((𝑛 − 1) + 𝑛)) |
223 | 208, 215,
222 | 3eqtr2rd 2651 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 − 1) + 𝑛) = ((2 · (𝑛 + 1)) − 3)) |
224 | 223 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2)
· ((𝑛 − 1) +
𝑛)) = ((log‘2)
· ((2 · (𝑛 +
1)) − 3))) |
225 | 202, 224 | eqtr3d 2646 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((log‘2)
· (𝑛 − 1)) +
((log‘2) · 𝑛))
= ((log‘2) · ((2 · (𝑛 + 1)) − 3))) |
226 | 225 | breq2d 4595 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘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 293 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
((θ‘((𝑛 / 2) +
1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) ↔
((θ‘((𝑛 / 2) +
1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 ·
(𝑛 + 1)) −
3)))) |
228 | | 3nn 11063 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℕ |
229 | | elfzuz 12209 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 / 2) + 1) ∈ (3...𝑛) → ((𝑛 / 2) + 1) ∈
(ℤ≥‘3)) |
230 | 154, 229 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈
(ℤ≥‘3)) |
231 | | eluznn 11634 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
∈ ℕ ∧ ((𝑛 /
2) + 1) ∈ (ℤ≥‘3)) → ((𝑛 / 2) + 1) ∈ ℕ) |
232 | 228, 230,
231 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈
ℕ) |
233 | | chtublem 24736 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 / 2) + 1) ∈ ℕ →
(θ‘((2 · ((𝑛 / 2) + 1)) − 1)) ≤
((θ‘((𝑛 / 2) +
1)) + ((log‘4) · (((𝑛 / 2) + 1) − 1)))) |
234 | 232, 233 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
(θ‘((2 · ((𝑛 / 2) + 1)) − 1)) ≤
((θ‘((𝑛 / 2) +
1)) + ((log‘4) · (((𝑛 / 2) + 1) − 1)))) |
235 | 177 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
((𝑛 / 2) + 1)) − 1) =
((𝑛 + 2) −
1)) |
236 | | addsubass 10170 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℂ ∧ 2 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 2) − 1) = (𝑛 + (2 − 1))) |
237 | 164, 165,
236 | mp3an23 1408 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℂ → ((𝑛 + 2) − 1) = (𝑛 + (2 −
1))) |
238 | 169, 237 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 1) = (𝑛 + (2 −
1))) |
239 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
− 1) = 1 |
240 | 239 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 + (2 − 1)) = (𝑛 + 1) |
241 | 238, 240 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 1) = (𝑛 + 1)) |
242 | 235, 241 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
((𝑛 / 2) + 1)) − 1) =
(𝑛 + 1)) |
243 | 242 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
(θ‘((2 · ((𝑛 / 2) + 1)) − 1)) =
(θ‘(𝑛 +
1))) |
244 | | pncan 10166 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 / 2) ∈ ℂ ∧ 1
∈ ℂ) → (((𝑛
/ 2) + 1) − 1) = (𝑛 /
2)) |
245 | 163, 165,
244 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((𝑛 / 2) + 1) − 1) = (𝑛 / 2)) |
246 | 245 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4)
· (((𝑛 / 2) + 1)
− 1)) = ((log‘4) · (𝑛 / 2))) |
247 | | relogexp 24146 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ ℝ+ ∧ 2 ∈ ℤ) →
(log‘(2↑2)) = (2 · (log‘2))) |
248 | 99, 117, 247 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(log‘(2↑2)) = (2 · (log‘2)) |
249 | | sq2 12822 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(2↑2) = 4 |
250 | 249 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(log‘(2↑2)) = (log‘4) |
251 | 164, 102 | mulcomi 9925 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2
· (log‘2)) = ((log‘2) · 2) |
252 | 248, 250,
251 | 3eqtr3i 2640 |
. . . . . . . . . . . . . . . . . . 19
⊢
(log‘4) = ((log‘2) · 2) |
253 | 252 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . 18
⊢
((log‘4) · (𝑛 / 2)) = (((log‘2) · 2) ·
(𝑛 / 2)) |
254 | 164 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 2 ∈
ℂ) |
255 | 200, 254,
163 | mulassd 9942 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((log‘2)
· 2) · (𝑛 /
2)) = ((log‘2) · (2 · (𝑛 / 2)))) |
256 | 253, 255 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4)
· (𝑛 / 2)) =
((log‘2) · (2 · (𝑛 / 2)))) |
257 | 173 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2)
· (2 · (𝑛 /
2))) = ((log‘2) · 𝑛)) |
258 | 246, 256,
257 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4)
· (((𝑛 / 2) + 1)
− 1)) = ((log‘2) · 𝑛)) |
259 | 258 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
((θ‘((𝑛 / 2) +
1)) + ((log‘4) · (((𝑛 / 2) + 1) − 1))) =
((θ‘((𝑛 / 2) +
1)) + ((log‘2) · 𝑛))) |
260 | 234, 243,
259 | 3brtr3d 4614 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
(θ‘(𝑛 + 1))
≤ ((θ‘((𝑛 /
2) + 1)) + ((log‘2) · 𝑛))) |
261 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈
(ℤ≥‘3) → (𝑛 + 1) ∈
(ℤ≥‘3)) |
262 | | eluzelz 11573 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 + 1) ∈
(ℤ≥‘3) → (𝑛 + 1) ∈ ℤ) |
263 | 261, 262 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘3) → (𝑛 + 1) ∈ ℤ) |
264 | 263 | zred 11358 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → (𝑛 + 1) ∈ ℝ) |
265 | 264 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 + 1) ∈
ℝ) |
266 | | chtcl 24635 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 + 1) ∈ ℝ →
(θ‘(𝑛 + 1))
∈ ℝ) |
267 | 265, 266 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
(θ‘(𝑛 + 1))
∈ ℝ) |
268 | 191, 198 | readdcld 9948 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
((θ‘((𝑛 / 2) +
1)) + ((log‘2) · 𝑛)) ∈ ℝ) |
269 | | zmulcl 11303 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ ℤ ∧ (𝑛 +
1) ∈ ℤ) → (2 · (𝑛 + 1)) ∈ ℤ) |
270 | 117, 263,
269 | sylancr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 · (𝑛 + 1)) ∈ ℤ) |
271 | 270 | zred 11358 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 · (𝑛 + 1)) ∈ ℝ) |
272 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· (𝑛 + 1)) ∈
ℝ ∧ 3 ∈ ℝ) → ((2 · (𝑛 + 1)) − 3) ∈
ℝ) |
273 | 271, 31, 272 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → ((2 · (𝑛 + 1)) − 3) ∈
ℝ) |
274 | 273 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 ·
(𝑛 + 1)) − 3) ∈
ℝ) |
275 | | remulcl 9900 |
. . . . . . . . . . . . . . . 16
⊢
(((log‘2) ∈ ℝ ∧ ((2 · (𝑛 + 1)) − 3) ∈ ℝ) →
((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈
ℝ) |
276 | 101, 274,
275 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2)
· ((2 · (𝑛 +
1)) − 3)) ∈ ℝ) |
277 | | lelttr 10007 |
. . . . . . . . . . . . . . 15
⊢
(((θ‘(𝑛
+ 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 1318 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘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 707 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
(((θ‘((𝑛 / 2) +
1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 ·
(𝑛 + 1)) − 3)) →
(θ‘(𝑛 + 1))
< ((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
280 | 227, 279 | sylbid 229 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) →
((θ‘((𝑛 / 2) +
1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) →
(θ‘(𝑛 + 1))
< ((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
281 | 161, 280 | syld 46 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(θ‘(𝑛 + 1))
< ((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
282 | | eluzfz2 12220 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘3) → 𝑛 ∈ (3...𝑛)) |
283 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (θ‘𝑘) = (θ‘𝑛)) |
284 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛)) |
285 | 284 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → ((2 · 𝑘) − 3) = ((2 · 𝑛) − 3)) |
286 | 285 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → ((log‘2) · ((2 ·
𝑘) − 3)) =
((log‘2) · ((2 · 𝑛) − 3))) |
287 | 283, 286 | breq12d 4596 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → ((θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) ↔
(θ‘𝑛) <
((log‘2) · ((2 · 𝑛) − 3)))) |
288 | 287 | rspcv 3278 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (3...𝑛) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(θ‘𝑛) <
((log‘2) · ((2 · 𝑛) − 3)))) |
289 | 282, 288 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(θ‘𝑛) <
((log‘2) · ((2 · 𝑛) − 3)))) |
290 | 289 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) →
(∀𝑘 ∈
(3...𝑛)(θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) − 3))
→ (θ‘𝑛)
< ((log‘2) · ((2 · 𝑛) − 3)))) |
291 | 210 | zred 11358 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 · 𝑛) ∈ ℝ) |
292 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → 3 ∈ ℝ) |
293 | 122 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘3) → 𝑛 < (𝑛 + 1)) |
294 | 25 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 ∈ ℝ ∧ 0 <
2)) |
295 | | ltmul2 10753 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → (𝑛 < (𝑛 + 1) ↔ (2 · 𝑛) < (2 · (𝑛 + 1)))) |
296 | 122, 264,
294, 295 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘3) → (𝑛 < (𝑛 + 1) ↔ (2 · 𝑛) < (2 · (𝑛 + 1)))) |
297 | 293, 296 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 · 𝑛) < (2 · (𝑛 + 1))) |
298 | 291, 271,
292, 297 | ltsub1dd 10518 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → ((2 · 𝑛) − 3) < ((2 · (𝑛 + 1)) −
3)) |
299 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· 𝑛) ∈ ℝ
∧ 3 ∈ ℝ) → ((2 · 𝑛) − 3) ∈ ℝ) |
300 | 291, 31, 299 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → ((2 · 𝑛) − 3) ∈ ℝ) |
301 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → ((log‘2) ∈ ℝ ∧ 0
< (log‘2))) |
302 | | ltmul2 10753 |
. . . . . . . . . . . . . . . . 17
⊢ ((((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 1318 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → (((2 · 𝑛) − 3) < ((2 · (𝑛 + 1)) − 3) ↔
((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) ·
((2 · (𝑛 + 1))
− 3)))) |
304 | 298, 303 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘3) → ((log‘2) · ((2 ·
𝑛) − 3)) <
((log‘2) · ((2 · (𝑛 + 1)) − 3))) |
305 | | chtcl 24635 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ →
(θ‘𝑛) ∈
ℝ) |
306 | 122, 305 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → (θ‘𝑛) ∈ ℝ) |
307 | | remulcl 9900 |
. . . . . . . . . . . . . . . . 17
⊢
(((log‘2) ∈ ℝ ∧ ((2 · 𝑛) − 3) ∈ ℝ) →
((log‘2) · ((2 · 𝑛) − 3)) ∈
ℝ) |
308 | 101, 300,
307 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → ((log‘2) · ((2 ·
𝑛) − 3)) ∈
ℝ) |
309 | 101, 273,
275 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → ((log‘2) · ((2 ·
(𝑛 + 1)) − 3)) ∈
ℝ) |
310 | | lttr 9993 |
. . . . . . . . . . . . . . . 16
⊢
(((θ‘𝑛)
∈ ℝ ∧ ((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 1318 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘3) → (((θ‘𝑛) < ((log‘2) · ((2 ·
𝑛) − 3)) ∧
((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) ·
((2 · (𝑛 + 1))
− 3))) → (θ‘𝑛) < ((log‘2) · ((2 ·
(𝑛 + 1)) −
3)))) |
312 | 304, 311 | mpan2d 706 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘3) → ((θ‘𝑛) < ((log‘2) · ((2 ·
𝑛) − 3)) →
(θ‘𝑛) <
((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
313 | 312 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) →
((θ‘𝑛) <
((log‘2) · ((2 · 𝑛) − 3)) → (θ‘𝑛) < ((log‘2) ·
((2 · (𝑛 + 1))
− 3)))) |
314 | 118 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → 𝑛 ∈
ℤ) |
315 | | dvdsval2 14824 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℤ ∧ 2 ≠ 0 ∧ (𝑛 + 1) ∈ ℤ) → (2 ∥
(𝑛 + 1) ↔ ((𝑛 + 1) / 2) ∈
ℤ)) |
316 | 117, 170,
315 | mp3an12 1406 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 + 1) ∈ ℤ → (2
∥ (𝑛 + 1) ↔
((𝑛 + 1) / 2) ∈
ℤ)) |
317 | 263, 316 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 ∥ (𝑛 + 1) ↔ ((𝑛 + 1) / 2) ∈ ℤ)) |
318 | | 2lt3 11072 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 <
3 |
319 | 2, 31 | ltnlei 10037 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 < 3
↔ ¬ 3 ≤ 2) |
320 | 318, 319 | mpbi 219 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ¬ 3
≤ 2 |
321 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2 =
(𝑛 + 1) → (3 ≤ 2
↔ 3 ≤ (𝑛 +
1))) |
322 | 320, 321 | mtbii 315 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 =
(𝑛 + 1) → ¬ 3 ≤
(𝑛 + 1)) |
323 | | eluzle 11576 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 + 1) ∈
(ℤ≥‘3) → 3 ≤ (𝑛 + 1)) |
324 | 261, 323 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈
(ℤ≥‘3) → 3 ≤ (𝑛 + 1)) |
325 | 322, 324 | nsyl3 132 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈
(ℤ≥‘3) → ¬ 2 = (𝑛 + 1)) |
326 | 325 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 + 1) ∈ ℙ) → ¬ 2 = (𝑛 + 1)) |
327 | | uzid 11578 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
328 | 117, 327 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
(ℤ≥‘2) |
329 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 + 1) ∈ ℙ) → (𝑛 + 1) ∈
ℙ) |
330 | | dvdsprm 15253 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ (ℤ≥‘2) ∧ (𝑛 + 1) ∈ ℙ) → (2 ∥
(𝑛 + 1) ↔ 2 = (𝑛 + 1))) |
331 | 328, 329,
330 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 + 1) ∈ ℙ) → (2 ∥
(𝑛 + 1) ↔ 2 = (𝑛 + 1))) |
332 | 326, 331 | mtbird 314 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ (𝑛 + 1) ∈ ℙ) → ¬ 2 ∥
(𝑛 + 1)) |
333 | 332 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘3) → ((𝑛 + 1) ∈ ℙ → ¬ 2 ∥
(𝑛 + 1))) |
334 | 333 | con2d 128 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘3) → (2 ∥ (𝑛 + 1) → ¬ (𝑛 + 1) ∈ ℙ)) |
335 | 317, 334 | sylbird 249 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘3) → (((𝑛 + 1) / 2) ∈ ℤ → ¬ (𝑛 + 1) ∈
ℙ)) |
336 | 335 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → ¬
(𝑛 + 1) ∈
ℙ) |
337 | | chtnprm 24680 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℤ ∧ ¬
(𝑛 + 1) ∈ ℙ)
→ (θ‘(𝑛 +
1)) = (θ‘𝑛)) |
338 | 314, 336,
337 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) →
(θ‘(𝑛 + 1)) =
(θ‘𝑛)) |
339 | 338 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) →
((θ‘(𝑛 + 1))
< ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ↔
(θ‘𝑛) <
((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
340 | 313, 339 | sylibrd 248 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) →
((θ‘𝑛) <
((log‘2) · ((2 · 𝑛) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2)
· ((2 · (𝑛 +
1)) − 3)))) |
341 | 290, 340 | syld 46 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) →
(∀𝑘 ∈
(3...𝑛)(θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) − 3))
→ (θ‘(𝑛 +
1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
342 | | zeo 11339 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → ((𝑛 / 2) ∈ ℤ ∨
((𝑛 + 1) / 2) ∈
ℤ)) |
343 | 118, 342 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘3) → ((𝑛 / 2) ∈ ℤ ∨ ((𝑛 + 1) / 2) ∈
ℤ)) |
344 | 281, 341,
343 | mpjaodan 823 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(θ‘(𝑛 + 1))
< ((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
345 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑛 + 1) ∈ V |
346 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑛 + 1) → (θ‘𝑘) = (θ‘(𝑛 + 1))) |
347 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑛 + 1) → (2 · 𝑘) = (2 · (𝑛 + 1))) |
348 | 347 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 + 1) → ((2 · 𝑘) − 3) = ((2 · (𝑛 + 1)) −
3)) |
349 | 348 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑛 + 1) → ((log‘2) · ((2
· 𝑘) − 3)) =
((log‘2) · ((2 · (𝑛 + 1)) − 3))) |
350 | 346, 349 | breq12d 4596 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑛 + 1) → ((θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) − 3))
↔ (θ‘(𝑛 +
1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)))) |
351 | 345, 350 | ralsn 4169 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
{(𝑛 + 1)}
(θ‘𝑘) <
((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘(𝑛 + 1)) < ((log‘2)
· ((2 · (𝑛 +
1)) − 3))) |
352 | 344, 351 | syl6ibr 241 |
. . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) −
3)))) |
353 | 352 | ancld 574 |
. . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(∀𝑘 ∈
(3...𝑛)(θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) − 3))
∧ ∀𝑘 ∈
{(𝑛 + 1)}
(θ‘𝑘) <
((log‘2) · ((2 · 𝑘) − 3))))) |
354 | | ralun 3757 |
. . . . . . . . 9
⊢
((∀𝑘 ∈
(3...𝑛)(θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) − 3))
∧ ∀𝑘 ∈
{(𝑛 + 1)}
(θ‘𝑘) <
((log‘2) · ((2 · 𝑘) − 3))) → ∀𝑘 ∈ ((3...𝑛) ∪ {(𝑛 + 1)})(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) −
3))) |
355 | | fzsuc 12258 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘3) → (3...(𝑛 + 1)) = ((3...𝑛) ∪ {(𝑛 + 1)})) |
356 | 355 | raleqdv 3121 |
. . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘3) → (∀𝑘 ∈ (3...(𝑛 + 1))(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) ↔
∀𝑘 ∈
((3...𝑛) ∪ {(𝑛 + 1)})(θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) −
3)))) |
357 | 354, 356 | syl5ibr 235 |
. . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘3) → ((∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) ∧
∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) −
3))) → ∀𝑘
∈ (3...(𝑛 +
1))(θ‘𝑘) <
((log‘2) · ((2 · 𝑘) − 3)))) |
358 | 353, 357 | syld 46 |
. . . . . . 7
⊢ (𝑛 ∈
(ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
∀𝑘 ∈
(3...(𝑛 +
1))(θ‘𝑘) <
((log‘2) · ((2 · 𝑘) − 3)))) |
359 | 66, 68, 70, 72, 74, 112, 358 | uzind4i 11626 |
. . . . . 6
⊢
((⌊‘𝑁)
∈ (ℤ≥‘3) → ∀𝑘 ∈ (3...(⌊‘𝑁))(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) −
3))) |
360 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = (⌊‘𝑁) → (θ‘𝑘) =
(θ‘(⌊‘𝑁))) |
361 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑘 = (⌊‘𝑁) → (2 · 𝑘) = (2 ·
(⌊‘𝑁))) |
362 | 361 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑘 = (⌊‘𝑁) → ((2 · 𝑘) − 3) = ((2 ·
(⌊‘𝑁)) −
3)) |
363 | 362 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑘 = (⌊‘𝑁) → ((log‘2) ·
((2 · 𝑘) − 3))
= ((log‘2) · ((2 · (⌊‘𝑁)) − 3))) |
364 | 360, 363 | breq12d 4596 |
. . . . . . 7
⊢ (𝑘 = (⌊‘𝑁) → ((θ‘𝑘) < ((log‘2) ·
((2 · 𝑘) − 3))
↔ (θ‘(⌊‘𝑁)) < ((log‘2) · ((2 ·
(⌊‘𝑁)) −
3)))) |
365 | 364 | rspcv 3278 |
. . . . . 6
⊢
((⌊‘𝑁)
∈ (3...(⌊‘𝑁)) → (∀𝑘 ∈ (3...(⌊‘𝑁))(θ‘𝑘) < ((log‘2) · ((2 ·
𝑘) − 3)) →
(θ‘(⌊‘𝑁)) < ((log‘2) · ((2 ·
(⌊‘𝑁)) −
3)))) |
366 | 65, 359, 365 | sylc 63 |
. . . . 5
⊢
((⌊‘𝑁)
∈ (ℤ≥‘3) →
(θ‘(⌊‘𝑁)) < ((log‘2) · ((2 ·
(⌊‘𝑁)) −
3))) |
367 | 64, 366 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) →
(θ‘(⌊‘𝑁)) < ((log‘2) · ((2 ·
(⌊‘𝑁)) −
3))) |
368 | 60, 367 | eqbrtrrd 4607 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (θ‘𝑁) < ((log‘2) · ((2 ·
(⌊‘𝑁)) −
3))) |
369 | 35 | adantr 480 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (2 · 𝑁) ∈ ℝ) |
370 | 31 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → 3 ∈
ℝ) |
371 | | flle 12462 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ →
(⌊‘𝑁) ≤
𝑁) |
372 | 371 | ad2antrr 758 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (⌊‘𝑁) ≤ 𝑁) |
373 | 22 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → 𝑁 ∈ ℝ) |
374 | 25 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (2 ∈ ℝ ∧ 0 <
2)) |
375 | | lemul2 10755 |
. . . . . . 7
⊢
(((⌊‘𝑁)
∈ ℝ ∧ 𝑁
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) →
((⌊‘𝑁) ≤
𝑁 ↔ (2 ·
(⌊‘𝑁)) ≤ (2
· 𝑁))) |
376 | 50, 373, 374, 375 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((⌊‘𝑁) ≤ 𝑁 ↔ (2 · (⌊‘𝑁)) ≤ (2 · 𝑁))) |
377 | 372, 376 | mpbid 221 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (2 · (⌊‘𝑁)) ≤ (2 · 𝑁)) |
378 | 52, 369, 370, 377 | lesub1dd 10522 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((2 ·
(⌊‘𝑁)) −
3) ≤ ((2 · 𝑁)
− 3)) |
379 | 7 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((log‘2) ∈ ℝ
∧ 0 < (log‘2))) |
380 | | lemul2 10755 |
. . . . 5
⊢ ((((2
· (⌊‘𝑁))
− 3) ∈ ℝ ∧ ((2 · 𝑁) − 3) ∈ ℝ ∧
((log‘2) ∈ ℝ ∧ 0 < (log‘2))) → (((2 ·
(⌊‘𝑁)) −
3) ≤ ((2 · 𝑁)
− 3) ↔ ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ≤
((log‘2) · ((2 · 𝑁) − 3)))) |
381 | 54, 57, 379, 380 | syl3anc 1318 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (((2 ·
(⌊‘𝑁)) −
3) ≤ ((2 · 𝑁)
− 3) ↔ ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ≤
((log‘2) · ((2 · 𝑁) − 3)))) |
382 | 378, 381 | mpbid 221 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → ((log‘2) · ((2
· (⌊‘𝑁))
− 3)) ≤ ((log‘2) · ((2 · 𝑁) − 3))) |
383 | 48, 56, 59, 368, 382 | ltletrd 10076 |
. 2
⊢ (((𝑁 ∈ ℝ ∧ 2 <
𝑁) ∧
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1))) → (θ‘𝑁) < ((log‘2) · ((2 ·
𝑁) −
3))) |
384 | 117 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) → 2 ∈
ℤ) |
385 | | flcl 12458 |
. . . . 5
⊢ (𝑁 ∈ ℝ →
(⌊‘𝑁) ∈
ℤ) |
386 | 385 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) →
(⌊‘𝑁) ∈
ℤ) |
387 | | ltle 10005 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ) → (2 < 𝑁 → 2 ≤ 𝑁)) |
388 | 2, 387 | mpan 702 |
. . . . . 6
⊢ (𝑁 ∈ ℝ → (2 <
𝑁 → 2 ≤ 𝑁)) |
389 | | flge 12468 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 2 ∈
ℤ) → (2 ≤ 𝑁
↔ 2 ≤ (⌊‘𝑁))) |
390 | 117, 389 | mpan2 703 |
. . . . . 6
⊢ (𝑁 ∈ ℝ → (2 ≤
𝑁 ↔ 2 ≤
(⌊‘𝑁))) |
391 | 388, 390 | sylibd 228 |
. . . . 5
⊢ (𝑁 ∈ ℝ → (2 <
𝑁 → 2 ≤
(⌊‘𝑁))) |
392 | 391 | imp 444 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) → 2 ≤
(⌊‘𝑁)) |
393 | | eluz2 11569 |
. . . 4
⊢
((⌊‘𝑁)
∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧
(⌊‘𝑁) ∈
ℤ ∧ 2 ≤ (⌊‘𝑁))) |
394 | 384, 386,
392, 393 | syl3anbrc 1239 |
. . 3
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) →
(⌊‘𝑁) ∈
(ℤ≥‘2)) |
395 | | uzp1 11597 |
. . 3
⊢
((⌊‘𝑁)
∈ (ℤ≥‘2) → ((⌊‘𝑁) = 2 ∨ (⌊‘𝑁) ∈
(ℤ≥‘(2 + 1)))) |
396 | 394, 395 | syl 17 |
. 2
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) →
((⌊‘𝑁) = 2 ∨
(⌊‘𝑁) ∈
(ℤ≥‘(2 + 1)))) |
397 | 46, 383, 396 | mpjaodan 823 |
1
⊢ ((𝑁 ∈ ℝ ∧ 2 <
𝑁) →
(θ‘𝑁) <
((log‘2) · ((2 · 𝑁) − 3))) |