| Step | Hyp | Ref
| Expression |
| 1 | | bposlem9.4 |
. . 3
⊢ (𝜑 → ;64 < 𝑁) |
| 2 | | bposlem7.1 |
. . . 4
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2)
· (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2
· 𝑛))))) |
| 3 | | bposlem7.2 |
. . . 4
⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦
((log‘𝑥) / 𝑥)) |
| 4 | | 6nn0 12547 |
. . . . . 6
⊢ 6 ∈
ℕ0 |
| 5 | | 4nn 12349 |
. . . . . 6
⊢ 4 ∈
ℕ |
| 6 | 4, 5 | decnncl 12753 |
. . . . 5
⊢ ;64 ∈ ℕ |
| 7 | 6 | a1i 11 |
. . . 4
⊢ (𝜑 → ;64 ∈ ℕ) |
| 8 | | bposlem9.3 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 9 | | ere 16125 |
. . . . . . . 8
⊢ e ∈
ℝ |
| 10 | | 8re 12362 |
. . . . . . . 8
⊢ 8 ∈
ℝ |
| 11 | | egt2lt3 16242 |
. . . . . . . . . 10
⊢ (2 < e
∧ e < 3) |
| 12 | 11 | simpri 485 |
. . . . . . . . 9
⊢ e <
3 |
| 13 | | 3lt8 12462 |
. . . . . . . . 9
⊢ 3 <
8 |
| 14 | | 3re 12346 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
| 15 | 9, 14, 10 | lttri 11387 |
. . . . . . . . 9
⊢ ((e <
3 ∧ 3 < 8) → e < 8) |
| 16 | 12, 13, 15 | mp2an 692 |
. . . . . . . 8
⊢ e <
8 |
| 17 | 9, 10, 16 | ltleii 11384 |
. . . . . . 7
⊢ e ≤
8 |
| 18 | | 0re 11263 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
| 19 | | epos 16243 |
. . . . . . . . 9
⊢ 0 <
e |
| 20 | 18, 9, 19 | ltleii 11384 |
. . . . . . . 8
⊢ 0 ≤
e |
| 21 | | 8pos 12378 |
. . . . . . . . 9
⊢ 0 <
8 |
| 22 | 18, 10, 21 | ltleii 11384 |
. . . . . . . 8
⊢ 0 ≤
8 |
| 23 | | le2sq 14174 |
. . . . . . . 8
⊢ (((e
∈ ℝ ∧ 0 ≤ e) ∧ (8 ∈ ℝ ∧ 0 ≤ 8)) →
(e ≤ 8 ↔ (e↑2) ≤ (8↑2))) |
| 24 | 9, 20, 10, 22, 23 | mp4an 693 |
. . . . . . 7
⊢ (e ≤ 8
↔ (e↑2) ≤ (8↑2)) |
| 25 | 17, 24 | mpbi 230 |
. . . . . 6
⊢
(e↑2) ≤ (8↑2) |
| 26 | 10 | recni 11275 |
. . . . . . . 8
⊢ 8 ∈
ℂ |
| 27 | 26 | sqvali 14219 |
. . . . . . 7
⊢
(8↑2) = (8 · 8) |
| 28 | | 8t8e64 12854 |
. . . . . . 7
⊢ (8
· 8) = ;64 |
| 29 | 27, 28 | eqtri 2765 |
. . . . . 6
⊢
(8↑2) = ;64 |
| 30 | 25, 29 | breqtri 5168 |
. . . . 5
⊢
(e↑2) ≤ ;64 |
| 31 | 30 | a1i 11 |
. . . 4
⊢ (𝜑 → (e↑2) ≤ ;64) |
| 32 | 9 | resqcli 14225 |
. . . . . 6
⊢
(e↑2) ∈ ℝ |
| 33 | 32 | a1i 11 |
. . . . 5
⊢ (𝜑 → (e↑2) ∈
ℝ) |
| 34 | 6 | nnrei 12275 |
. . . . . 6
⊢ ;64 ∈ ℝ |
| 35 | 34 | a1i 11 |
. . . . 5
⊢ (𝜑 → ;64 ∈ ℝ) |
| 36 | 8 | nnred 12281 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 37 | | ltle 11349 |
. . . . . . 7
⊢ ((;64 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (;64 < 𝑁 → ;64 ≤ 𝑁)) |
| 38 | 34, 36, 37 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → (;64 < 𝑁 → ;64 ≤ 𝑁)) |
| 39 | 1, 38 | mpd 15 |
. . . . 5
⊢ (𝜑 → ;64 ≤ 𝑁) |
| 40 | 33, 35, 36, 31, 39 | letrd 11418 |
. . . 4
⊢ (𝜑 → (e↑2) ≤ 𝑁) |
| 41 | 2, 3, 7, 8, 31, 40 | bposlem7 27334 |
. . 3
⊢ (𝜑 → (;64 < 𝑁 → (𝐹‘𝑁) < (𝐹‘;64))) |
| 42 | 1, 41 | mpd 15 |
. 2
⊢ (𝜑 → (𝐹‘𝑁) < (𝐹‘;64)) |
| 43 | 2, 3 | bposlem8 27335 |
. . . . 5
⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2)) |
| 44 | 43 | a1i 11 |
. . . 4
⊢ (𝜑 → ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2))) |
| 45 | 44 | simpld 494 |
. . 3
⊢ (𝜑 → (𝐹‘;64) ∈ ℝ) |
| 46 | | 2fveq3 6911 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → (𝐺‘(√‘𝑛)) = (𝐺‘(√‘𝑁))) |
| 47 | 46 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2)
· (𝐺‘(√‘𝑁)))) |
| 48 | | fvoveq1 7454 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → (𝐺‘(𝑛 / 2)) = (𝐺‘(𝑁 / 2))) |
| 49 | 48 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · (𝐺‘(𝑁 / 2)))) |
| 50 | 47, 49 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = (((√‘2) ·
(𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) |
| 51 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁)) |
| 52 | 51 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (√‘(2 · 𝑛)) = (√‘(2 ·
𝑁))) |
| 53 | 52 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ((log‘2) / (√‘(2
· 𝑛))) =
((log‘2) / (√‘(2 · 𝑁)))) |
| 54 | 50, 53 | oveq12d 7449 |
. . . . . 6
⊢ (𝑛 = 𝑁 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2
· 𝑛)))) =
((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) /
(√‘(2 · 𝑁))))) |
| 55 | | ovex 7464 |
. . . . . 6
⊢
((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) /
(√‘(2 · 𝑁)))) ∈ V |
| 56 | 54, 2, 55 | fvmpt 7016 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝐹‘𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) /
(√‘(2 · 𝑁))))) |
| 57 | 8, 56 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹‘𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) /
(√‘(2 · 𝑁))))) |
| 58 | | sqrt2re 16286 |
. . . . . . 7
⊢
(√‘2) ∈ ℝ |
| 59 | 8 | nnrpd 13075 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
| 60 | 59 | rpsqrtcld 15450 |
. . . . . . . . 9
⊢ (𝜑 → (√‘𝑁) ∈
ℝ+) |
| 61 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑥 = (√‘𝑁) → (log‘𝑥) =
(log‘(√‘𝑁))) |
| 62 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 = (√‘𝑁) → 𝑥 = (√‘𝑁)) |
| 63 | 61, 62 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑥 = (√‘𝑁) → ((log‘𝑥) / 𝑥) = ((log‘(√‘𝑁)) / (√‘𝑁))) |
| 64 | | ovex 7464 |
. . . . . . . . . 10
⊢
((log‘(√‘𝑁)) / (√‘𝑁)) ∈ V |
| 65 | 63, 3, 64 | fvmpt 7016 |
. . . . . . . . 9
⊢
((√‘𝑁)
∈ ℝ+ → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁))) |
| 66 | 60, 65 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁))) |
| 67 | 60 | relogcld 26665 |
. . . . . . . . 9
⊢ (𝜑 →
(log‘(√‘𝑁)) ∈ ℝ) |
| 68 | 67, 60 | rerpdivcld 13108 |
. . . . . . . 8
⊢ (𝜑 →
((log‘(√‘𝑁)) / (√‘𝑁)) ∈ ℝ) |
| 69 | 66, 68 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℝ) |
| 70 | | remulcl 11240 |
. . . . . . 7
⊢
(((√‘2) ∈ ℝ ∧ (𝐺‘(√‘𝑁)) ∈ ℝ) → ((√‘2)
· (𝐺‘(√‘𝑁))) ∈ ℝ) |
| 71 | 58, 69, 70 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → ((√‘2)
· (𝐺‘(√‘𝑁))) ∈ ℝ) |
| 72 | | 9re 12365 |
. . . . . . . 8
⊢ 9 ∈
ℝ |
| 73 | | 4re 12350 |
. . . . . . . 8
⊢ 4 ∈
ℝ |
| 74 | | 4ne0 12374 |
. . . . . . . 8
⊢ 4 ≠
0 |
| 75 | 72, 73, 74 | redivcli 12034 |
. . . . . . 7
⊢ (9 / 4)
∈ ℝ |
| 76 | 59 | rphalfcld 13089 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 / 2) ∈
ℝ+) |
| 77 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑁 / 2) → (log‘𝑥) = (log‘(𝑁 / 2))) |
| 78 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑁 / 2) → 𝑥 = (𝑁 / 2)) |
| 79 | 77, 78 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑁 / 2) → ((log‘𝑥) / 𝑥) = ((log‘(𝑁 / 2)) / (𝑁 / 2))) |
| 80 | | ovex 7464 |
. . . . . . . . . 10
⊢
((log‘(𝑁 / 2))
/ (𝑁 / 2)) ∈
V |
| 81 | 79, 3, 80 | fvmpt 7016 |
. . . . . . . . 9
⊢ ((𝑁 / 2) ∈ ℝ+
→ (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2))) |
| 82 | 76, 81 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2))) |
| 83 | 76 | relogcld 26665 |
. . . . . . . . 9
⊢ (𝜑 → (log‘(𝑁 / 2)) ∈
ℝ) |
| 84 | 83, 76 | rerpdivcld 13108 |
. . . . . . . 8
⊢ (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℝ) |
| 85 | 82, 84 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℝ) |
| 86 | | remulcl 11240 |
. . . . . . 7
⊢ (((9 / 4)
∈ ℝ ∧ (𝐺‘(𝑁 / 2)) ∈ ℝ) → ((9 / 4)
· (𝐺‘(𝑁 / 2))) ∈
ℝ) |
| 87 | 75, 85, 86 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ) |
| 88 | 71, 87 | readdcld 11290 |
. . . . 5
⊢ (𝜑 → (((√‘2)
· (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℝ) |
| 89 | | 2rp 13039 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
| 90 | | relogcl 26617 |
. . . . . . 7
⊢ (2 ∈
ℝ+ → (log‘2) ∈ ℝ) |
| 91 | 89, 90 | ax-mp 5 |
. . . . . 6
⊢
(log‘2) ∈ ℝ |
| 92 | | rpmulcl 13058 |
. . . . . . . 8
⊢ ((2
∈ ℝ+ ∧ 𝑁 ∈ ℝ+) → (2
· 𝑁) ∈
ℝ+) |
| 93 | 89, 59, 92 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ+) |
| 94 | 93 | rpsqrtcld 15450 |
. . . . . 6
⊢ (𝜑 → (√‘(2 ·
𝑁)) ∈
ℝ+) |
| 95 | | rerpdivcl 13065 |
. . . . . 6
⊢
(((log‘2) ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ+)
→ ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ) |
| 96 | 91, 94, 95 | sylancr 587 |
. . . . 5
⊢ (𝜑 → ((log‘2) /
(√‘(2 · 𝑁))) ∈ ℝ) |
| 97 | 88, 96 | readdcld 11290 |
. . . 4
⊢ (𝜑 → ((((√‘2)
· (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) /
(√‘(2 · 𝑁)))) ∈ ℝ) |
| 98 | 57, 97 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ) |
| 99 | 91 | a1i 11 |
. . . 4
⊢ (𝜑 → (log‘2) ∈
ℝ) |
| 100 | 44 | simprd 495 |
. . . 4
⊢ (𝜑 → (𝐹‘;64) < (log‘2)) |
| 101 | | nnrp 13046 |
. . . . . . . . . . 11
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
| 102 | 5, 101 | ax-mp 5 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ+ |
| 103 | | relogcl 26617 |
. . . . . . . . . 10
⊢ (4 ∈
ℝ+ → (log‘4) ∈ ℝ) |
| 104 | 102, 103 | ax-mp 5 |
. . . . . . . . 9
⊢
(log‘4) ∈ ℝ |
| 105 | | remulcl 11240 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧
(log‘4) ∈ ℝ) → (𝑁 · (log‘4)) ∈
ℝ) |
| 106 | 36, 104, 105 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 · (log‘4)) ∈
ℝ) |
| 107 | 59 | relogcld 26665 |
. . . . . . . 8
⊢ (𝜑 → (log‘𝑁) ∈
ℝ) |
| 108 | 106, 107 | resubcld 11691 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 · (log‘4)) −
(log‘𝑁)) ∈
ℝ) |
| 109 | | rpre 13043 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑁) ∈
ℝ+ → (2 · 𝑁) ∈ ℝ) |
| 110 | | rpge0 13048 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑁) ∈
ℝ+ → 0 ≤ (2 · 𝑁)) |
| 111 | 109, 110 | resqrtcld 15456 |
. . . . . . . . . . . 12
⊢ ((2
· 𝑁) ∈
ℝ+ → (√‘(2 · 𝑁)) ∈ ℝ) |
| 112 | 93, 111 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (√‘(2 ·
𝑁)) ∈
ℝ) |
| 113 | | 3nn 12345 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ |
| 114 | | nndivre 12307 |
. . . . . . . . . . 11
⊢
(((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ)
→ ((√‘(2 · 𝑁)) / 3) ∈ ℝ) |
| 115 | 112, 113,
114 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝜑 → ((√‘(2
· 𝑁)) / 3) ∈
ℝ) |
| 116 | | 2re 12340 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
| 117 | | readdcl 11238 |
. . . . . . . . . 10
⊢
((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈
ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈
ℝ) |
| 118 | 115, 116,
117 | sylancl 586 |
. . . . . . . . 9
⊢ (𝜑 → (((√‘(2
· 𝑁)) / 3) + 2)
∈ ℝ) |
| 119 | 93 | relogcld 26665 |
. . . . . . . . 9
⊢ (𝜑 → (log‘(2 ·
𝑁)) ∈
ℝ) |
| 120 | 118, 119 | remulcld 11291 |
. . . . . . . 8
⊢ (𝜑 → ((((√‘(2
· 𝑁)) / 3) + 2)
· (log‘(2 · 𝑁))) ∈ ℝ) |
| 121 | | remulcl 11240 |
. . . . . . . . . . . 12
⊢ ((4
∈ ℝ ∧ 𝑁
∈ ℝ) → (4 · 𝑁) ∈ ℝ) |
| 122 | 73, 36, 121 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (4 · 𝑁) ∈
ℝ) |
| 123 | | nndivre 12307 |
. . . . . . . . . . 11
⊢ (((4
· 𝑁) ∈ ℝ
∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ) |
| 124 | 122, 113,
123 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝜑 → ((4 · 𝑁) / 3) ∈
ℝ) |
| 125 | | 5re 12353 |
. . . . . . . . . 10
⊢ 5 ∈
ℝ |
| 126 | | resubcl 11573 |
. . . . . . . . . 10
⊢ ((((4
· 𝑁) / 3) ∈
ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈
ℝ) |
| 127 | 124, 125,
126 | sylancl 586 |
. . . . . . . . 9
⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈
ℝ) |
| 128 | | remulcl 11240 |
. . . . . . . . 9
⊢ (((((4
· 𝑁) / 3) − 5)
∈ ℝ ∧ (log‘2) ∈ ℝ) → ((((4 · 𝑁) / 3) − 5) ·
(log‘2)) ∈ ℝ) |
| 129 | 127, 91, 128 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) ·
(log‘2)) ∈ ℝ) |
| 130 | 120, 129 | readdcld 11290 |
. . . . . . 7
⊢ (𝜑 → (((((√‘(2
· 𝑁)) / 3) + 2)
· (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))
∈ ℝ) |
| 131 | | remulcl 11240 |
. . . . . . . . 9
⊢ ((((4
· 𝑁) / 3) ∈
ℝ ∧ (log‘2) ∈ ℝ) → (((4 · 𝑁) / 3) · (log‘2))
∈ ℝ) |
| 132 | 124, 91, 131 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → (((4 · 𝑁) / 3) · (log‘2))
∈ ℝ) |
| 133 | 132, 107 | resubcld 11691 |
. . . . . . 7
⊢ (𝜑 → ((((4 · 𝑁) / 3) · (log‘2))
− (log‘𝑁))
∈ ℝ) |
| 134 | 8 | nnzd 12640 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 135 | | df-5 12332 |
. . . . . . . . . . . 12
⊢ 5 = (4 +
1) |
| 136 | 73 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 4 ∈
ℝ) |
| 137 | | 6nn 12355 |
. . . . . . . . . . . . . . . 16
⊢ 6 ∈
ℕ |
| 138 | | 4nn0 12545 |
. . . . . . . . . . . . . . . 16
⊢ 4 ∈
ℕ0 |
| 139 | | 4lt10 12869 |
. . . . . . . . . . . . . . . 16
⊢ 4 <
;10 |
| 140 | 137, 138,
138, 139 | declti 12771 |
. . . . . . . . . . . . . . 15
⊢ 4 <
;64 |
| 141 | 140 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 4 < ;64) |
| 142 | 136, 35, 36, 141, 1 | lttrd 11422 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 4 < 𝑁) |
| 143 | | 4z 12651 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℤ |
| 144 | | zltp1le 12667 |
. . . . . . . . . . . . . 14
⊢ ((4
∈ ℤ ∧ 𝑁
∈ ℤ) → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁)) |
| 145 | 143, 134,
144 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁)) |
| 146 | 142, 145 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → (4 + 1) ≤ 𝑁) |
| 147 | 135, 146 | eqbrtrid 5178 |
. . . . . . . . . . 11
⊢ (𝜑 → 5 ≤ 𝑁) |
| 148 | | 5nn 12352 |
. . . . . . . . . . . . 13
⊢ 5 ∈
ℕ |
| 149 | 148 | nnzi 12641 |
. . . . . . . . . . . 12
⊢ 5 ∈
ℤ |
| 150 | 149 | eluz1i 12886 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘5) ↔ (𝑁 ∈ ℤ ∧ 5 ≤ 𝑁)) |
| 151 | 134, 147,
150 | sylanbrc 583 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘5)) |
| 152 | | bposlem9.5 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) |
| 153 | | breq2 5147 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑞 → (𝑁 < 𝑝 ↔ 𝑁 < 𝑞)) |
| 154 | | breq1 5146 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑞 → (𝑝 ≤ (2 · 𝑁) ↔ 𝑞 ≤ (2 · 𝑁))) |
| 155 | 153, 154 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑞 → ((𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁)))) |
| 156 | 155 | cbvrexvw 3238 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈
ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ ∃𝑞 ∈ ℙ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁))) |
| 157 | 152, 156 | sylnib 328 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ ∃𝑞 ∈ ℙ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁))) |
| 158 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) |
| 159 | | eqid 2737 |
. . . . . . . . . 10
⊢
(⌊‘((2 · 𝑁) / 3)) = (⌊‘((2 · 𝑁) / 3)) |
| 160 | | eqid 2737 |
. . . . . . . . . 10
⊢
(⌊‘(√‘(2 · 𝑁))) = (⌊‘(√‘(2
· 𝑁))) |
| 161 | 151, 157,
158, 159, 160 | bposlem6 27333 |
. . . . . . . . 9
⊢ (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5)))) |
| 162 | | reexplog 26637 |
. . . . . . . . . . . 12
⊢ ((4
∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (4↑𝑁) = (exp‘(𝑁 ·
(log‘4)))) |
| 163 | 102, 134,
162 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (4↑𝑁) = (exp‘(𝑁 · (log‘4)))) |
| 164 | 59 | reeflogd 26666 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(exp‘(log‘𝑁)) =
𝑁) |
| 165 | 164 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 = (exp‘(log‘𝑁))) |
| 166 | 163, 165 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝜑 → ((4↑𝑁) / 𝑁) = ((exp‘(𝑁 · (log‘4))) /
(exp‘(log‘𝑁)))) |
| 167 | 106 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 · (log‘4)) ∈
ℂ) |
| 168 | 107 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘𝑁) ∈
ℂ) |
| 169 | | efsub 16136 |
. . . . . . . . . . 11
⊢ (((𝑁 · (log‘4)) ∈
ℂ ∧ (log‘𝑁)
∈ ℂ) → (exp‘((𝑁 · (log‘4)) −
(log‘𝑁))) =
((exp‘(𝑁 ·
(log‘4))) / (exp‘(log‘𝑁)))) |
| 170 | 167, 168,
169 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (exp‘((𝑁 · (log‘4)) −
(log‘𝑁))) =
((exp‘(𝑁 ·
(log‘4))) / (exp‘(log‘𝑁)))) |
| 171 | 166, 170 | eqtr4d 2780 |
. . . . . . . . 9
⊢ (𝜑 → ((4↑𝑁) / 𝑁) = (exp‘((𝑁 · (log‘4)) −
(log‘𝑁)))) |
| 172 | 93 | rpcnd 13079 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) |
| 173 | 93 | rpne0d 13082 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 · 𝑁) ≠ 0) |
| 174 | 118 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((√‘(2
· 𝑁)) / 3) + 2)
∈ ℂ) |
| 175 | 172, 173,
174 | cxpefd 26754 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2)) =
(exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁))))) |
| 176 | | 2cn 12341 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
| 177 | | 2ne0 12370 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
| 178 | 127 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈
ℂ) |
| 179 | | cxpef 26707 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ (((4 · 𝑁) / 3) − 5) ∈ ℂ) →
(2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4
· 𝑁) / 3) − 5)
· (log‘2)))) |
| 180 | 176, 177,
178, 179 | mp3an12i 1467 |
. . . . . . . . . . 11
⊢ (𝜑 →
(2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4
· 𝑁) / 3) − 5)
· (log‘2)))) |
| 181 | 175, 180 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5))) =
((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁)))) ·
(exp‘((((4 · 𝑁)
/ 3) − 5) · (log‘2))))) |
| 182 | 120 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((√‘(2
· 𝑁)) / 3) + 2)
· (log‘(2 · 𝑁))) ∈ ℂ) |
| 183 | 129 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) ·
(log‘2)) ∈ ℂ) |
| 184 | | efadd 16130 |
. . . . . . . . . . 11
⊢
((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁))) ∈ ℂ ∧
((((4 · 𝑁) / 3)
− 5) · (log‘2)) ∈ ℂ) →
(exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁))) + ((((4 · 𝑁) / 3) − 5) ·
(log‘2)))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁)))) ·
(exp‘((((4 · 𝑁) / 3) − 5) ·
(log‘2))))) |
| 185 | 182, 183,
184 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 →
(exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁))) + ((((4 · 𝑁) / 3) − 5) ·
(log‘2)))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁)))) ·
(exp‘((((4 · 𝑁) / 3) − 5) ·
(log‘2))))) |
| 186 | 181, 185 | eqtr4d 2780 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5))) =
(exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁))) + ((((4 · 𝑁) / 3) − 5) ·
(log‘2))))) |
| 187 | 161, 171,
186 | 3brtr3d 5174 |
. . . . . . . 8
⊢ (𝜑 → (exp‘((𝑁 · (log‘4)) −
(log‘𝑁))) <
(exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁))) + ((((4 · 𝑁) / 3) − 5) ·
(log‘2))))) |
| 188 | | eflt 16153 |
. . . . . . . . 9
⊢ ((((𝑁 · (log‘4)) −
(log‘𝑁)) ∈
ℝ ∧ (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁))) + ((((4 · 𝑁) / 3) − 5) ·
(log‘2))) ∈ ℝ) → (((𝑁 · (log‘4)) −
(log‘𝑁)) <
(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁))) + ((((4 · 𝑁) / 3) − 5) ·
(log‘2))) ↔ (exp‘((𝑁 · (log‘4)) −
(log‘𝑁))) <
(exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁))) + ((((4 · 𝑁) / 3) − 5) ·
(log‘2)))))) |
| 189 | 108, 130,
188 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (((𝑁 · (log‘4)) −
(log‘𝑁)) <
(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁))) + ((((4 · 𝑁) / 3) − 5) ·
(log‘2))) ↔ (exp‘((𝑁 · (log‘4)) −
(log‘𝑁))) <
(exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁))) + ((((4 · 𝑁) / 3) − 5) ·
(log‘2)))))) |
| 190 | 187, 189 | mpbird 257 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 · (log‘4)) −
(log‘𝑁)) <
(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 ·
𝑁))) + ((((4 · 𝑁) / 3) − 5) ·
(log‘2)))) |
| 191 | 108, 130,
133, 190 | ltsub1dd 11875 |
. . . . . 6
⊢ (𝜑 → (((𝑁 · (log‘4)) −
(log‘𝑁)) −
((((4 · 𝑁) / 3)
· (log‘2)) − (log‘𝑁))) < ((((((√‘(2 ·
𝑁)) / 3) + 2) ·
(log‘(2 · 𝑁)))
+ ((((4 · 𝑁) / 3)
− 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) −
(log‘𝑁)))) |
| 192 | 36 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 193 | | mulcom 11241 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑁
∈ ℂ) → (2 · 𝑁) = (𝑁 · 2)) |
| 194 | 176, 192,
193 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) = (𝑁 · 2)) |
| 195 | 194 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · 𝑁) · (log‘2)) =
((𝑁 · 2) ·
(log‘2))) |
| 196 | 91 | recni 11275 |
. . . . . . . . . . . 12
⊢
(log‘2) ∈ ℂ |
| 197 | | mulass 11243 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ ∧ (log‘2) ∈ ℂ) → ((𝑁 · 2) · (log‘2)) =
(𝑁 · (2 ·
(log‘2)))) |
| 198 | 176, 196,
197 | mp3an23 1455 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℂ → ((𝑁 · 2) ·
(log‘2)) = (𝑁
· (2 · (log‘2)))) |
| 199 | 192, 198 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 · 2) · (log‘2)) =
(𝑁 · (2 ·
(log‘2)))) |
| 200 | 196 | 2timesi 12404 |
. . . . . . . . . . . 12
⊢ (2
· (log‘2)) = ((log‘2) + (log‘2)) |
| 201 | | relogmul 26634 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ+ ∧ 2 ∈ ℝ+) →
(log‘(2 · 2)) = ((log‘2) + (log‘2))) |
| 202 | 89, 89, 201 | mp2an 692 |
. . . . . . . . . . . 12
⊢
(log‘(2 · 2)) = ((log‘2) +
(log‘2)) |
| 203 | | 2t2e4 12430 |
. . . . . . . . . . . . 13
⊢ (2
· 2) = 4 |
| 204 | 203 | fveq2i 6909 |
. . . . . . . . . . . 12
⊢
(log‘(2 · 2)) = (log‘4) |
| 205 | 200, 202,
204 | 3eqtr2i 2771 |
. . . . . . . . . . 11
⊢ (2
· (log‘2)) = (log‘4) |
| 206 | 205 | oveq2i 7442 |
. . . . . . . . . 10
⊢ (𝑁 · (2 ·
(log‘2))) = (𝑁
· (log‘4)) |
| 207 | 199, 206 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 · 2) · (log‘2)) =
(𝑁 ·
(log‘4))) |
| 208 | 195, 207 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → ((2 · 𝑁) · (log‘2)) =
(𝑁 ·
(log‘4))) |
| 209 | 208 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → (((2 · 𝑁) · (log‘2))
− (((4 · 𝑁) /
3) · (log‘2))) = ((𝑁 · (log‘4)) − (((4
· 𝑁) / 3) ·
(log‘2)))) |
| 210 | 124 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → ((4 · 𝑁) / 3) ∈
ℂ) |
| 211 | | 3rp 13040 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℝ+ |
| 212 | | rpdivcl 13060 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑁) ∈
ℝ+ ∧ 3 ∈ ℝ+) → ((2 ·
𝑁) / 3) ∈
ℝ+) |
| 213 | 93, 211, 212 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝑁) / 3) ∈
ℝ+) |
| 214 | 213 | rpcnd 13079 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 · 𝑁) / 3) ∈
ℂ) |
| 215 | | 4p2e6 12419 |
. . . . . . . . . . . . . 14
⊢ (4 + 2) =
6 |
| 216 | 215 | oveq1i 7441 |
. . . . . . . . . . . . 13
⊢ ((4 + 2)
· 𝑁) = (6 ·
𝑁) |
| 217 | | 4cn 12351 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℂ |
| 218 | | adddir 11252 |
. . . . . . . . . . . . . 14
⊢ ((4
∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((4 + 2) ·
𝑁) = ((4 · 𝑁) + (2 · 𝑁))) |
| 219 | 217, 176,
192, 218 | mp3an12i 1467 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁))) |
| 220 | 216, 219 | eqtr3id 2791 |
. . . . . . . . . . . 12
⊢ (𝜑 → (6 · 𝑁) = ((4 · 𝑁) + (2 · 𝑁))) |
| 221 | 220 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝜑 → ((6 · 𝑁) / 3) = (((4 · 𝑁) + (2 · 𝑁)) / 3)) |
| 222 | | 6cn 12357 |
. . . . . . . . . . . . . 14
⊢ 6 ∈
ℂ |
| 223 | | 3cn 12347 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℂ |
| 224 | | 3ne0 12372 |
. . . . . . . . . . . . . . 15
⊢ 3 ≠
0 |
| 225 | 223, 224 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
| 226 | | div23 11941 |
. . . . . . . . . . . . . 14
⊢ ((6
∈ ℂ ∧ 𝑁
∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((6 ·
𝑁) / 3) = ((6 / 3) ·
𝑁)) |
| 227 | 222, 225,
226 | mp3an13 1454 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℂ → ((6
· 𝑁) / 3) = ((6 / 3)
· 𝑁)) |
| 228 | 192, 227 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁)) |
| 229 | | 3t2e6 12432 |
. . . . . . . . . . . . . . 15
⊢ (3
· 2) = 6 |
| 230 | 229 | oveq1i 7441 |
. . . . . . . . . . . . . 14
⊢ ((3
· 2) / 3) = (6 / 3) |
| 231 | 176, 223,
224 | divcan3i 12013 |
. . . . . . . . . . . . . 14
⊢ ((3
· 2) / 3) = 2 |
| 232 | 230, 231 | eqtr3i 2767 |
. . . . . . . . . . . . 13
⊢ (6 / 3) =
2 |
| 233 | 232 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ ((6 / 3)
· 𝑁) = (2 ·
𝑁) |
| 234 | 228, 233 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝜑 → ((6 · 𝑁) / 3) = (2 · 𝑁)) |
| 235 | 122 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → (4 · 𝑁) ∈
ℂ) |
| 236 | | remulcl 11240 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ) → (2 · 𝑁) ∈ ℝ) |
| 237 | 116, 36, 236 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) |
| 238 | 237 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) |
| 239 | | divdir 11947 |
. . . . . . . . . . . . 13
⊢ (((4
· 𝑁) ∈ ℂ
∧ (2 · 𝑁) ∈
ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3))) |
| 240 | 225, 239 | mp3an3 1452 |
. . . . . . . . . . . 12
⊢ (((4
· 𝑁) ∈ ℂ
∧ (2 · 𝑁) ∈
ℂ) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3))) |
| 241 | 235, 238,
240 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3))) |
| 242 | 221, 234,
241 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3))) |
| 243 | 210, 214,
242 | mvrladdd 11676 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3)) |
| 244 | 243 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2))
= (((2 · 𝑁) / 3)
· (log‘2))) |
| 245 | 99 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → (log‘2) ∈
ℂ) |
| 246 | 238, 210,
245 | subdird 11720 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2))
= (((2 · 𝑁) ·
(log‘2)) − (((4 · 𝑁) / 3) ·
(log‘2)))) |
| 247 | 244, 246 | eqtr3d 2779 |
. . . . . . 7
⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) =
(((2 · 𝑁) ·
(log‘2)) − (((4 · 𝑁) / 3) ·
(log‘2)))) |
| 248 | 132 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → (((4 · 𝑁) / 3) · (log‘2))
∈ ℂ) |
| 249 | 167, 248,
168 | nnncan2d 11655 |
. . . . . . 7
⊢ (𝜑 → (((𝑁 · (log‘4)) −
(log‘𝑁)) −
((((4 · 𝑁) / 3)
· (log‘2)) − (log‘𝑁))) = ((𝑁 · (log‘4)) − (((4
· 𝑁) / 3) ·
(log‘2)))) |
| 250 | 209, 247,
249 | 3eqtr4d 2787 |
. . . . . 6
⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) =
(((𝑁 ·
(log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) −
(log‘𝑁)))) |
| 251 | 115 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → ((√‘(2
· 𝑁)) / 3) ∈
ℂ) |
| 252 | 176 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℂ) |
| 253 | 119 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → (log‘(2 ·
𝑁)) ∈
ℂ) |
| 254 | 251, 252,
253 | adddird 11286 |
. . . . . . . . 9
⊢ (𝜑 → ((((√‘(2
· 𝑁)) / 3) + 2)
· (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2
· 𝑁))) + (2 ·
(log‘(2 · 𝑁))))) |
| 255 | | relogmul 26634 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ+ ∧ 𝑁 ∈ ℝ+) →
(log‘(2 · 𝑁))
= ((log‘2) + (log‘𝑁))) |
| 256 | 89, 59, 255 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log‘(2 ·
𝑁)) = ((log‘2) +
(log‘𝑁))) |
| 257 | 256 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · (log‘(2
· 𝑁))) = (2 ·
((log‘2) + (log‘𝑁)))) |
| 258 | 252, 245,
168 | adddid 11285 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · ((log‘2)
+ (log‘𝑁))) = ((2
· (log‘2)) + (2 · (log‘𝑁)))) |
| 259 | 257, 258 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · (log‘(2
· 𝑁))) = ((2
· (log‘2)) + (2 · (log‘𝑁)))) |
| 260 | 259 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → ((((√‘(2
· 𝑁)) / 3) ·
(log‘(2 · 𝑁)))
+ (2 · (log‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2
· 𝑁))) + ((2
· (log‘2)) + (2 · (log‘𝑁))))) |
| 261 | 254, 260 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → ((((√‘(2
· 𝑁)) / 3) + 2)
· (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2
· 𝑁))) + ((2
· (log‘2)) + (2 · (log‘𝑁))))) |
| 262 | | 5cn 12354 |
. . . . . . . . . . . 12
⊢ 5 ∈
ℂ |
| 263 | 262 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 5 ∈
ℂ) |
| 264 | 210, 263,
245 | subdird 11720 |
. . . . . . . . . 10
⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) ·
(log‘2)) = ((((4 · 𝑁) / 3) · (log‘2)) − (5
· (log‘2)))) |
| 265 | 264 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → (((((4 · 𝑁) / 3) − 5) ·
(log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) −
(log‘𝑁))) = (((((4
· 𝑁) / 3) ·
(log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2))
− (log‘𝑁)))) |
| 266 | 262, 196 | mulcli 11268 |
. . . . . . . . . . 11
⊢ (5
· (log‘2)) ∈ ℂ |
| 267 | 266 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (5 · (log‘2))
∈ ℂ) |
| 268 | 248, 267,
168 | nnncan1d 11654 |
. . . . . . . . 9
⊢ (𝜑 → (((((4 · 𝑁) / 3) · (log‘2))
− (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) −
(log‘𝑁))) =
((log‘𝑁) − (5
· (log‘2)))) |
| 269 | 265, 268 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → (((((4 · 𝑁) / 3) − 5) ·
(log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) −
(log‘𝑁))) =
((log‘𝑁) − (5
· (log‘2)))) |
| 270 | 261, 269 | oveq12d 7449 |
. . . . . . 7
⊢ (𝜑 → (((((√‘(2
· 𝑁)) / 3) + 2)
· (log‘(2 · 𝑁))) + (((((4 · 𝑁) / 3) − 5) · (log‘2))
− ((((4 · 𝑁) /
3) · (log‘2)) − (log‘𝑁)))) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2
· 𝑁))) + ((2
· (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 ·
(log‘2))))) |
| 271 | 133 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → ((((4 · 𝑁) / 3) · (log‘2))
− (log‘𝑁))
∈ ℂ) |
| 272 | 182, 183,
271 | addsubassd 11640 |
. . . . . . 7
⊢ (𝜑 → ((((((√‘(2
· 𝑁)) / 3) + 2)
· (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))
− ((((4 · 𝑁) /
3) · (log‘2)) − (log‘𝑁))) = (((((√‘(2 · 𝑁)) / 3) + 2) ·
(log‘(2 · 𝑁)))
+ (((((4 · 𝑁) / 3)
− 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) −
(log‘𝑁))))) |
| 273 | 262, 223,
196 | subdiri 11713 |
. . . . . . . . . . . . 13
⊢ ((5
− 3) · (log‘2)) = ((5 · (log‘2)) − (3
· (log‘2))) |
| 274 | | 3p2e5 12417 |
. . . . . . . . . . . . . . . 16
⊢ (3 + 2) =
5 |
| 275 | 274 | oveq1i 7441 |
. . . . . . . . . . . . . . 15
⊢ ((3 + 2)
− 3) = (5 − 3) |
| 276 | | pncan2 11515 |
. . . . . . . . . . . . . . . 16
⊢ ((3
∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) =
2) |
| 277 | 223, 176,
276 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ ((3 + 2)
− 3) = 2 |
| 278 | 275, 277 | eqtr3i 2767 |
. . . . . . . . . . . . . 14
⊢ (5
− 3) = 2 |
| 279 | 278 | oveq1i 7441 |
. . . . . . . . . . . . 13
⊢ ((5
− 3) · (log‘2)) = (2 ·
(log‘2)) |
| 280 | 273, 279 | eqtr3i 2767 |
. . . . . . . . . . . 12
⊢ ((5
· (log‘2)) − (3 · (log‘2))) = (2 ·
(log‘2)) |
| 281 | 280 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ((5 ·
(log‘2)) − (3 · (log‘2))) = (2 ·
(log‘2))) |
| 282 | | mulcl 11239 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (2 ·
(log‘𝑁)) ∈
ℂ) |
| 283 | 176, 168,
282 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 ·
(log‘𝑁)) ∈
ℂ) |
| 284 | | df-3 12330 |
. . . . . . . . . . . . . . . 16
⊢ 3 = (2 +
1) |
| 285 | 284 | oveq1i 7441 |
. . . . . . . . . . . . . . 15
⊢ (3
· (log‘𝑁)) =
((2 + 1) · (log‘𝑁)) |
| 286 | | 1cnd 11256 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℂ) |
| 287 | 252, 286,
168 | adddird 11286 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2 + 1) ·
(log‘𝑁)) = ((2
· (log‘𝑁)) +
(1 · (log‘𝑁)))) |
| 288 | 285, 287 | eqtrid 2789 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (3 ·
(log‘𝑁)) = ((2
· (log‘𝑁)) +
(1 · (log‘𝑁)))) |
| 289 | 168 | mullidd 11279 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 ·
(log‘𝑁)) =
(log‘𝑁)) |
| 290 | 289 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 ·
(log‘𝑁)) + (1
· (log‘𝑁))) =
((2 · (log‘𝑁))
+ (log‘𝑁))) |
| 291 | 288, 290 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (3 ·
(log‘𝑁)) = ((2
· (log‘𝑁)) +
(log‘𝑁))) |
| 292 | 291 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((3 ·
(log‘𝑁)) − (5
· (log‘2))) = (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 ·
(log‘2)))) |
| 293 | 283, 168,
267, 292 | assraddsubd 11677 |
. . . . . . . . . . 11
⊢ (𝜑 → ((3 ·
(log‘𝑁)) − (5
· (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 ·
(log‘2))))) |
| 294 | 281, 293 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝜑 → (((5 ·
(log‘2)) − (3 · (log‘2))) + ((3 ·
(log‘𝑁)) − (5
· (log‘2)))) = ((2 · (log‘2)) + ((2 ·
(log‘𝑁)) +
((log‘𝑁) − (5
· (log‘2)))))) |
| 295 | | relogdiv 26635 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ+
∧ 2 ∈ ℝ+) → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2))) |
| 296 | 59, 89, 295 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (log‘(𝑁 / 2)) = ((log‘𝑁) −
(log‘2))) |
| 297 | 296 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝜑 → (3 ·
(log‘(𝑁 / 2))) = (3
· ((log‘𝑁)
− (log‘2)))) |
| 298 | | subdi 11696 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℂ ∧ (log‘𝑁) ∈ ℂ ∧ (log‘2) ∈
ℂ) → (3 · ((log‘𝑁) − (log‘2))) = ((3 ·
(log‘𝑁)) − (3
· (log‘2)))) |
| 299 | 223, 196,
298 | mp3an13 1454 |
. . . . . . . . . . . . 13
⊢
((log‘𝑁)
∈ ℂ → (3 · ((log‘𝑁) − (log‘2))) = ((3 ·
(log‘𝑁)) − (3
· (log‘2)))) |
| 300 | 168, 299 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (3 ·
((log‘𝑁) −
(log‘2))) = ((3 · (log‘𝑁)) − (3 ·
(log‘2)))) |
| 301 | 297, 300 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → (3 ·
(log‘(𝑁 / 2))) = ((3
· (log‘𝑁))
− (3 · (log‘2)))) |
| 302 | | div23 11941 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℂ ∧ 𝑁
∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 ·
𝑁) / 3) = ((2 / 3) ·
𝑁)) |
| 303 | 176, 225,
302 | mp3an13 1454 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℂ → ((2
· 𝑁) / 3) = ((2 / 3)
· 𝑁)) |
| 304 | 192, 303 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁)) |
| 305 | 223, 176,
223, 176, 177, 177 | divmuldivi 12027 |
. . . . . . . . . . . . . . . . 17
⊢ ((3 / 2)
· (3 / 2)) = ((3 · 3) / (2 · 2)) |
| 306 | | 3t3e9 12433 |
. . . . . . . . . . . . . . . . . 18
⊢ (3
· 3) = 9 |
| 307 | 306, 203 | oveq12i 7443 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
· 3) / (2 · 2)) = (9 / 4) |
| 308 | 305, 307 | eqtr2i 2766 |
. . . . . . . . . . . . . . . 16
⊢ (9 / 4) =
((3 / 2) · (3 / 2)) |
| 309 | 308 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (9 / 4) = ((3 / 2)
· (3 / 2))) |
| 310 | 304, 309 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (((2
/ 3) · 𝑁) ·
((3 / 2) · (3 / 2)))) |
| 311 | 176, 223,
224 | divcli 12009 |
. . . . . . . . . . . . . . 15
⊢ (2 / 3)
∈ ℂ |
| 312 | 223, 176,
177 | divcli 12009 |
. . . . . . . . . . . . . . . 16
⊢ (3 / 2)
∈ ℂ |
| 313 | | mul4 11429 |
. . . . . . . . . . . . . . . 16
⊢ ((((2 /
3) ∈ ℂ ∧ 𝑁
∈ ℂ) ∧ ((3 / 2) ∈ ℂ ∧ (3 / 2) ∈ ℂ))
→ (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) =
(((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2)))) |
| 314 | 312, 312,
313 | mpanr12 705 |
. . . . . . . . . . . . . . 15
⊢ (((2 / 3)
∈ ℂ ∧ 𝑁
∈ ℂ) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) =
(((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2)))) |
| 315 | 311, 192,
314 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 / 3) · 𝑁) · ((3 / 2) · (3
/ 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2)))) |
| 316 | | divcan6 11974 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) →
((2 / 3) · (3 / 2)) = 1) |
| 317 | 176, 177,
223, 224, 316 | mp4an 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((2 / 3)
· (3 / 2)) = 1 |
| 318 | 317 | oveq1i 7441 |
. . . . . . . . . . . . . . . 16
⊢ (((2 / 3)
· (3 / 2)) · (𝑁 · (3 / 2))) = (1 · (𝑁 · (3 /
2))) |
| 319 | | mulcl 11239 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℂ ∧ (3 / 2)
∈ ℂ) → (𝑁
· (3 / 2)) ∈ ℂ) |
| 320 | 192, 312,
319 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 · (3 / 2)) ∈
ℂ) |
| 321 | 320 | mullidd 11279 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 · (𝑁 · (3 / 2))) = (𝑁 · (3 /
2))) |
| 322 | 318, 321 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2 / 3) · (3 /
2)) · (𝑁 · (3
/ 2))) = (𝑁 · (3 /
2))) |
| 323 | | 2cnne0 12476 |
. . . . . . . . . . . . . . . . 17
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
| 324 | | div12 11944 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℂ ∧ 3 ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2))) |
| 325 | 223, 323,
324 | mp3an23 1455 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℂ → (𝑁 · (3 / 2)) = (3 ·
(𝑁 / 2))) |
| 326 | 192, 325 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2))) |
| 327 | 322, 326 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 / 3) · (3 /
2)) · (𝑁 · (3
/ 2))) = (3 · (𝑁 /
2))) |
| 328 | 310, 315,
327 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (3
· (𝑁 /
2))) |
| 329 | 328, 82 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4))
· (𝐺‘(𝑁 / 2))) = ((3 · (𝑁 / 2)) ·
((log‘(𝑁 / 2)) /
(𝑁 / 2)))) |
| 330 | 75 | recni 11275 |
. . . . . . . . . . . . . 14
⊢ (9 / 4)
∈ ℂ |
| 331 | 330 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (9 / 4) ∈
ℂ) |
| 332 | 85 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℂ) |
| 333 | 214, 331,
332 | mulassd 11284 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4))
· (𝐺‘(𝑁 / 2))) = (((2 · 𝑁) / 3) · ((9 / 4)
· (𝐺‘(𝑁 / 2))))) |
| 334 | 223 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 3 ∈
ℂ) |
| 335 | 76 | rpcnd 13079 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 / 2) ∈ ℂ) |
| 336 | 83 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (log‘(𝑁 / 2)) ∈
ℂ) |
| 337 | 76 | rpne0d 13082 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 / 2) ≠ 0) |
| 338 | 336, 335,
337 | divcld 12043 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℂ) |
| 339 | 334, 335,
338 | mulassd 11284 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((3 · (𝑁 / 2)) ·
((log‘(𝑁 / 2)) /
(𝑁 / 2))) = (3 ·
((𝑁 / 2) ·
((log‘(𝑁 / 2)) /
(𝑁 /
2))))) |
| 340 | 336, 335,
337 | divcan2d 12045 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (log‘(𝑁 / 2))) |
| 341 | 340 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (3 · ((𝑁 / 2) ·
((log‘(𝑁 / 2)) /
(𝑁 / 2)))) = (3 ·
(log‘(𝑁 /
2)))) |
| 342 | 339, 341 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((3 · (𝑁 / 2)) ·
((log‘(𝑁 / 2)) /
(𝑁 / 2))) = (3 ·
(log‘(𝑁 /
2)))) |
| 343 | 329, 333,
342 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4)
· (𝐺‘(𝑁 / 2)))) = (3 ·
(log‘(𝑁 /
2)))) |
| 344 | 223, 196 | mulcli 11268 |
. . . . . . . . . . . . 13
⊢ (3
· (log‘2)) ∈ ℂ |
| 345 | 344 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (3 · (log‘2))
∈ ℂ) |
| 346 | | mulcl 11239 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (3 ·
(log‘𝑁)) ∈
ℂ) |
| 347 | 223, 168,
346 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (3 ·
(log‘𝑁)) ∈
ℂ) |
| 348 | 267, 345,
347 | npncan3d 11656 |
. . . . . . . . . . 11
⊢ (𝜑 → (((5 ·
(log‘2)) − (3 · (log‘2))) + ((3 ·
(log‘𝑁)) − (5
· (log‘2)))) = ((3 · (log‘𝑁)) − (3 ·
(log‘2)))) |
| 349 | 301, 343,
348 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4)
· (𝐺‘(𝑁 / 2)))) = (((5 ·
(log‘2)) − (3 · (log‘2))) + ((3 ·
(log‘𝑁)) − (5
· (log‘2))))) |
| 350 | 116, 91 | remulcli 11277 |
. . . . . . . . . . . . 13
⊢ (2
· (log‘2)) ∈ ℝ |
| 351 | 350 | recni 11275 |
. . . . . . . . . . . 12
⊢ (2
· (log‘2)) ∈ ℂ |
| 352 | 351 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · (log‘2))
∈ ℂ) |
| 353 | | subcl 11507 |
. . . . . . . . . . . 12
⊢
(((log‘𝑁)
∈ ℂ ∧ (5 · (log‘2)) ∈ ℂ) →
((log‘𝑁) − (5
· (log‘2))) ∈ ℂ) |
| 354 | 168, 266,
353 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → ((log‘𝑁) − (5 ·
(log‘2))) ∈ ℂ) |
| 355 | 352, 283,
354 | addassd 11283 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 ·
(log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))) = ((2
· (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 ·
(log‘2)))))) |
| 356 | 294, 349,
355 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4)
· (𝐺‘(𝑁 / 2)))) = (((2 ·
(log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 ·
(log‘2))))) |
| 357 | 356 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → ((((√‘(2
· 𝑁)) / 3) ·
(log‘(2 · 𝑁)))
+ (((2 · 𝑁) / 3)
· ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 ·
𝑁)) / 3) ·
(log‘(2 · 𝑁)))
+ (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 ·
(log‘2)))))) |
| 358 | | mulcl 11239 |
. . . . . . . . . . 11
⊢
((((√‘(2 · 𝑁)) / 3) ∈ ℂ ∧ (log‘2)
∈ ℂ) → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈
ℂ) |
| 359 | 251, 196,
358 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝜑 → (((√‘(2
· 𝑁)) / 3) ·
(log‘2)) ∈ ℂ) |
| 360 | 251, 168 | mulcld 11281 |
. . . . . . . . . 10
⊢ (𝜑 → (((√‘(2
· 𝑁)) / 3) ·
(log‘𝑁)) ∈
ℂ) |
| 361 | 87 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℂ) |
| 362 | 214, 361 | mulcld 11281 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4)
· (𝐺‘(𝑁 / 2)))) ∈
ℂ) |
| 363 | 359, 360,
362 | addassd 11283 |
. . . . . . . . 9
⊢ (𝜑 → (((((√‘(2
· 𝑁)) / 3) ·
(log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4)
· (𝐺‘(𝑁 / 2))))) = ((((√‘(2
· 𝑁)) / 3) ·
(log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4)
· (𝐺‘(𝑁 / 2))))))) |
| 364 | 256 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝜑 → (((√‘(2
· 𝑁)) / 3) ·
(log‘(2 · 𝑁)))
= (((√‘(2 · 𝑁)) / 3) · ((log‘2) +
(log‘𝑁)))) |
| 365 | 251, 245,
168 | adddid 11285 |
. . . . . . . . . . 11
⊢ (𝜑 → (((√‘(2
· 𝑁)) / 3) ·
((log‘2) + (log‘𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2))
+ (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))) |
| 366 | 364, 365 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (((√‘(2
· 𝑁)) / 3) ·
(log‘(2 · 𝑁)))
= ((((√‘(2 · 𝑁)) / 3) · (log‘2)) +
(((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))) |
| 367 | 366 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → ((((√‘(2
· 𝑁)) / 3) ·
(log‘(2 · 𝑁)))
+ (((2 · 𝑁) / 3)
· ((9 / 4) · (𝐺‘(𝑁 / 2))))) = (((((√‘(2 ·
𝑁)) / 3) ·
(log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4)
· (𝐺‘(𝑁 / 2)))))) |
| 368 | 57 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = (((2 · 𝑁) / 3) · ((((√‘2)
· (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) /
(√‘(2 · 𝑁)))))) |
| 369 | 88 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((√‘2)
· (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ) |
| 370 | 96 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((log‘2) /
(√‘(2 · 𝑁))) ∈ ℂ) |
| 371 | 214, 369,
370 | adddid 11285 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝑁) / 3) ·
((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) /
(√‘(2 · 𝑁))))) = ((((2 · 𝑁) / 3) · (((√‘2) ·
(𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) /
(√‘(2 · 𝑁)))))) |
| 372 | 368, 371 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((2 · 𝑁) / 3) · (((√‘2) ·
(𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) /
(√‘(2 · 𝑁)))))) |
| 373 | 71 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((√‘2)
· (𝐺‘(√‘𝑁))) ∈ ℂ) |
| 374 | 214, 373,
361 | adddid 11285 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2 · 𝑁) / 3) ·
(((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((2 · 𝑁) / 3) · ((√‘2) ·
(𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))) |
| 375 | 93 | rpge0d 13081 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 ≤ (2 · 𝑁)) |
| 376 | | remsqsqrt 15295 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· 𝑁) ∈ ℝ
∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁)) · (√‘(2
· 𝑁))) = (2 ·
𝑁)) |
| 377 | 237, 375,
376 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((√‘(2
· 𝑁)) ·
(√‘(2 · 𝑁))) = (2 · 𝑁)) |
| 378 | 377 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((√‘(2
· 𝑁)) ·
(√‘(2 · 𝑁))) / 3) = ((2 · 𝑁) / 3)) |
| 379 | 112 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (√‘(2 ·
𝑁)) ∈
ℂ) |
| 380 | 224 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 3 ≠ 0) |
| 381 | 379, 379,
334, 380 | div23d 12080 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((√‘(2
· 𝑁)) ·
(√‘(2 · 𝑁))) / 3) = (((√‘(2 ·
𝑁)) / 3) ·
(√‘(2 · 𝑁)))) |
| 382 | 378, 381 | eqtr3d 2779 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2 · 𝑁) / 3) = (((√‘(2
· 𝑁)) / 3) ·
(√‘(2 · 𝑁)))) |
| 383 | 382 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 · 𝑁) / 3) ·
((√‘2) · (𝐺‘(√‘𝑁)))) = ((((√‘(2 · 𝑁)) / 3) ·
(√‘(2 · 𝑁))) · ((√‘2) ·
(𝐺‘(√‘𝑁))))) |
| 384 | 251, 379,
373 | mulassd 11284 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((√‘(2
· 𝑁)) / 3) ·
(√‘(2 · 𝑁))) · ((√‘2) ·
(𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) ·
((√‘(2 · 𝑁)) · ((√‘2) ·
(𝐺‘(√‘𝑁)))))) |
| 385 | | 0le2 12368 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ≤
2 |
| 386 | 116, 385 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 ∈
ℝ ∧ 0 ≤ 2) |
| 387 | 59 | rprege0d 13084 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) |
| 388 | | sqrtmul 15298 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
∈ ℝ ∧ 0 ≤ 2) ∧ (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) → (√‘(2
· 𝑁)) =
((√‘2) · (√‘𝑁))) |
| 389 | 386, 387,
388 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (√‘(2 ·
𝑁)) = ((√‘2)
· (√‘𝑁))) |
| 390 | 389 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((√‘(2
· 𝑁)) ·
((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) ·
(√‘𝑁)) ·
((√‘2) · (𝐺‘(√‘𝑁))))) |
| 391 | 58 | recni 11275 |
. . . . . . . . . . . . . . . . . 18
⊢
(√‘2) ∈ ℂ |
| 392 | 391 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (√‘2) ∈
ℂ) |
| 393 | 60 | rpcnd 13079 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (√‘𝑁) ∈
ℂ) |
| 394 | 69 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℂ) |
| 395 | 392, 393,
392, 394 | mul4d 11473 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((√‘2)
· (√‘𝑁))
· ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) ·
(√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁))))) |
| 396 | | remsqsqrt 15295 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ ℝ ∧ 0 ≤ 2) → ((√‘2) ·
(√‘2)) = 2) |
| 397 | 116, 385,
396 | mp2an 692 |
. . . . . . . . . . . . . . . . . . 19
⊢
((√‘2) · (√‘2)) = 2 |
| 398 | 397 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((√‘2)
· (√‘2)) = 2) |
| 399 | 66 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁)))) |
| 400 | 67 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 →
(log‘(√‘𝑁)) ∈ ℂ) |
| 401 | 60 | rpne0d 13082 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (√‘𝑁) ≠ 0) |
| 402 | 400, 393,
401 | divcan2d 12045 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((√‘𝑁) ·
((log‘(√‘𝑁)) / (√‘𝑁))) = (log‘(√‘𝑁))) |
| 403 | 399, 402 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = (log‘(√‘𝑁))) |
| 404 | 398, 403 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((√‘2)
· (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (2 ·
(log‘(√‘𝑁)))) |
| 405 | 400 | 2timesd 12509 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 ·
(log‘(√‘𝑁))) = ((log‘(√‘𝑁)) +
(log‘(√‘𝑁)))) |
| 406 | 60, 60 | relogmuld 26667 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(log‘((√‘𝑁) · (√‘𝑁))) = ((log‘(√‘𝑁)) +
(log‘(√‘𝑁)))) |
| 407 | | remsqsqrt 15295 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) →
((√‘𝑁) ·
(√‘𝑁)) = 𝑁) |
| 408 | 387, 407 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((√‘𝑁) · (√‘𝑁)) = 𝑁) |
| 409 | 408 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(log‘((√‘𝑁) · (√‘𝑁))) = (log‘𝑁)) |
| 410 | 406, 409 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((log‘(√‘𝑁)) + (log‘(√‘𝑁))) = (log‘𝑁)) |
| 411 | 404, 405,
410 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((√‘2)
· (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (log‘𝑁)) |
| 412 | 390, 395,
411 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((√‘(2
· 𝑁)) ·
((√‘2) · (𝐺‘(√‘𝑁)))) = (log‘𝑁)) |
| 413 | 412 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((√‘(2
· 𝑁)) / 3) ·
((√‘(2 · 𝑁)) · ((√‘2) ·
(𝐺‘(√‘𝑁))))) = (((√‘(2 · 𝑁)) / 3) ·
(log‘𝑁))) |
| 414 | 383, 384,
413 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2 · 𝑁) / 3) ·
((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) ·
(log‘𝑁))) |
| 415 | 414 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((2 · 𝑁) / 3) ·
((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 ·
𝑁)) / 3) ·
(log‘𝑁)) + (((2
· 𝑁) / 3) ·
((9 / 4) · (𝐺‘(𝑁 / 2)))))) |
| 416 | 374, 415 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝑁) / 3) ·
(((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 ·
𝑁)) / 3) ·
(log‘𝑁)) + (((2
· 𝑁) / 3) ·
((9 / 4) · (𝐺‘(𝑁 / 2)))))) |
| 417 | 382 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) /
(√‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) ·
(√‘(2 · 𝑁))) · ((log‘2) /
(√‘(2 · 𝑁))))) |
| 418 | 251, 379,
370 | mulassd 11284 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((√‘(2
· 𝑁)) / 3) ·
(√‘(2 · 𝑁))) · ((log‘2) /
(√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) ·
((√‘(2 · 𝑁)) · ((log‘2) /
(√‘(2 · 𝑁)))))) |
| 419 | 94 | rpne0d 13082 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (√‘(2 ·
𝑁)) ≠
0) |
| 420 | 245, 379,
419 | divcan2d 12045 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((√‘(2
· 𝑁)) ·
((log‘2) / (√‘(2 · 𝑁)))) = (log‘2)) |
| 421 | 420 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((√‘(2
· 𝑁)) / 3) ·
((√‘(2 · 𝑁)) · ((log‘2) /
(√‘(2 · 𝑁))))) = (((√‘(2 · 𝑁)) / 3) ·
(log‘2))) |
| 422 | 417, 418,
421 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) /
(√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) ·
(log‘2))) |
| 423 | 416, 422 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝜑 → ((((2 · 𝑁) / 3) ·
(((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) /
(√‘(2 · 𝑁))))) = (((((√‘(2 · 𝑁)) / 3) ·
(log‘𝑁)) + (((2
· 𝑁) / 3) ·
((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((√‘(2 ·
𝑁)) / 3) ·
(log‘2)))) |
| 424 | 360, 362 | addcld 11280 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((√‘(2
· 𝑁)) / 3) ·
(log‘𝑁)) + (((2
· 𝑁) / 3) ·
((9 / 4) · (𝐺‘(𝑁 / 2))))) ∈ ℂ) |
| 425 | 424, 359 | addcomd 11463 |
. . . . . . . . . 10
⊢ (𝜑 → (((((√‘(2
· 𝑁)) / 3) ·
(log‘𝑁)) + (((2
· 𝑁) / 3) ·
((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((√‘(2 ·
𝑁)) / 3) ·
(log‘2))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) +
((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4)
· (𝐺‘(𝑁 / 2))))))) |
| 426 | 372, 423,
425 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘2))
+ ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4)
· (𝐺‘(𝑁 / 2))))))) |
| 427 | 363, 367,
426 | 3eqtr4rd 2788 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2
· 𝑁))) + (((2
· 𝑁) / 3) ·
((9 / 4) · (𝐺‘(𝑁 / 2)))))) |
| 428 | 251, 253 | mulcld 11281 |
. . . . . . . . 9
⊢ (𝜑 → (((√‘(2
· 𝑁)) / 3) ·
(log‘(2 · 𝑁)))
∈ ℂ) |
| 429 | | addcl 11237 |
. . . . . . . . . 10
⊢ (((2
· (log‘2)) ∈ ℂ ∧ (2 · (log‘𝑁)) ∈ ℂ) → ((2
· (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ) |
| 430 | 351, 283,
429 | sylancr 587 |
. . . . . . . . 9
⊢ (𝜑 → ((2 ·
(log‘2)) + (2 · (log‘𝑁))) ∈ ℂ) |
| 431 | 428, 430,
354 | addassd 11283 |
. . . . . . . 8
⊢ (𝜑 → (((((√‘(2
· 𝑁)) / 3) ·
(log‘(2 · 𝑁)))
+ ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))) =
((((√‘(2 · 𝑁)) / 3) · (log‘(2 ·
𝑁))) + (((2 ·
(log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 ·
(log‘2)))))) |
| 432 | 357, 427,
431 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2
· 𝑁))) + ((2
· (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 ·
(log‘2))))) |
| 433 | 270, 272,
432 | 3eqtr4rd 2788 |
. . . . . 6
⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((((√‘(2 · 𝑁)) / 3) + 2) ·
(log‘(2 · 𝑁)))
+ ((((4 · 𝑁) / 3)
− 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) −
(log‘𝑁)))) |
| 434 | 191, 250,
433 | 3brtr4d 5175 |
. . . . 5
⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2))
< (((2 · 𝑁) / 3)
· (𝐹‘𝑁))) |
| 435 | 99, 98, 213 | ltmul2d 13119 |
. . . . 5
⊢ (𝜑 → ((log‘2) < (𝐹‘𝑁) ↔ (((2 · 𝑁) / 3) · (log‘2)) < (((2
· 𝑁) / 3) ·
(𝐹‘𝑁)))) |
| 436 | 434, 435 | mpbird 257 |
. . . 4
⊢ (𝜑 → (log‘2) < (𝐹‘𝑁)) |
| 437 | 45, 99, 98, 100, 436 | lttrd 11422 |
. . 3
⊢ (𝜑 → (𝐹‘;64) < (𝐹‘𝑁)) |
| 438 | 45, 98, 437 | ltnsymd 11410 |
. 2
⊢ (𝜑 → ¬ (𝐹‘𝑁) < (𝐹‘;64)) |
| 439 | 42, 438 | pm2.21dd 195 |
1
⊢ (𝜑 → 𝜓) |