MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bposlem9 Structured version   Visualization version   GIF version

Theorem bposlem9 24951
Description: Lemma for bpos 24952. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.)
Hypotheses
Ref Expression
bposlem7.1 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))
bposlem7.2 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))
bposlem9.3 (𝜑𝑁 ∈ ℕ)
bposlem9.4 (𝜑64 < 𝑁)
bposlem9.5 (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
Assertion
Ref Expression
bposlem9 (𝜑𝜓)
Distinct variable groups:   𝑛,𝑁   𝑛,𝐺   𝜑,𝑛   𝑁,𝑝   𝑥,𝑁
Allowed substitution hints:   𝜑(𝑥,𝑝)   𝜓(𝑥,𝑛,𝑝)   𝐹(𝑥,𝑛,𝑝)   𝐺(𝑥,𝑝)

Proof of Theorem bposlem9
Dummy variable 𝑞 is distinct from all other variables.
StepHypRef Expression
1 bposlem9.4 . . 3 (𝜑64 < 𝑁)
2 bposlem7.1 . . . 4 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))
3 bposlem7.2 . . . 4 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))
4 6nn0 11273 . . . . . 6 6 ∈ ℕ0
5 4nn 11147 . . . . . 6 4 ∈ ℕ
64, 5decnncl 11478 . . . . 5 64 ∈ ℕ
76a1i 11 . . . 4 (𝜑64 ∈ ℕ)
8 bposlem9.3 . . . 4 (𝜑𝑁 ∈ ℕ)
9 ere 14763 . . . . . . . 8 e ∈ ℝ
10 8re 11065 . . . . . . . 8 8 ∈ ℝ
11 egt2lt3 14878 . . . . . . . . . 10 (2 < e ∧ e < 3)
1211simpri 478 . . . . . . . . 9 e < 3
13 3lt8 11179 . . . . . . . . 9 3 < 8
14 3re 11054 . . . . . . . . . 10 3 ∈ ℝ
159, 14, 10lttri 10123 . . . . . . . . 9 ((e < 3 ∧ 3 < 8) → e < 8)
1612, 13, 15mp2an 707 . . . . . . . 8 e < 8
179, 10, 16ltleii 10120 . . . . . . 7 e ≤ 8
18 0re 10000 . . . . . . . . 9 0 ∈ ℝ
19 epos 14879 . . . . . . . . 9 0 < e
2018, 9, 19ltleii 10120 . . . . . . . 8 0 ≤ e
21 8pos 11081 . . . . . . . . 9 0 < 8
2218, 10, 21ltleii 10120 . . . . . . . 8 0 ≤ 8
23 le2sq 12894 . . . . . . . 8 (((e ∈ ℝ ∧ 0 ≤ e) ∧ (8 ∈ ℝ ∧ 0 ≤ 8)) → (e ≤ 8 ↔ (e↑2) ≤ (8↑2)))
249, 20, 10, 22, 23mp4an 708 . . . . . . 7 (e ≤ 8 ↔ (e↑2) ≤ (8↑2))
2517, 24mpbi 220 . . . . . 6 (e↑2) ≤ (8↑2)
2610recni 10012 . . . . . . . 8 8 ∈ ℂ
2726sqvali 12899 . . . . . . 7 (8↑2) = (8 · 8)
28 8t8e64 11622 . . . . . . 7 (8 · 8) = 64
2927, 28eqtri 2643 . . . . . 6 (8↑2) = 64
3025, 29breqtri 4648 . . . . 5 (e↑2) ≤ 64
3130a1i 11 . . . 4 (𝜑 → (e↑2) ≤ 64)
329resqcli 12905 . . . . . 6 (e↑2) ∈ ℝ
3332a1i 11 . . . . 5 (𝜑 → (e↑2) ∈ ℝ)
346nnrei 10989 . . . . . 6 64 ∈ ℝ
3534a1i 11 . . . . 5 (𝜑64 ∈ ℝ)
368nnred 10995 . . . . 5 (𝜑𝑁 ∈ ℝ)
37 ltle 10086 . . . . . . 7 ((64 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (64 < 𝑁64 ≤ 𝑁))
3834, 36, 37sylancr 694 . . . . . 6 (𝜑 → (64 < 𝑁64 ≤ 𝑁))
391, 38mpd 15 . . . . 5 (𝜑64 ≤ 𝑁)
4033, 35, 36, 31, 39letrd 10154 . . . 4 (𝜑 → (e↑2) ≤ 𝑁)
412, 3, 7, 8, 31, 40bposlem7 24949 . . 3 (𝜑 → (64 < 𝑁 → (𝐹𝑁) < (𝐹64)))
421, 41mpd 15 . 2 (𝜑 → (𝐹𝑁) < (𝐹64))
432, 3bposlem8 24950 . . . . 5 ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2))
4443a1i 11 . . . 4 (𝜑 → ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2)))
4544simpld 475 . . 3 (𝜑 → (𝐹64) ∈ ℝ)
46 fveq2 6158 . . . . . . . . . 10 (𝑛 = 𝑁 → (√‘𝑛) = (√‘𝑁))
4746fveq2d 6162 . . . . . . . . 9 (𝑛 = 𝑁 → (𝐺‘(√‘𝑛)) = (𝐺‘(√‘𝑁)))
4847oveq2d 6631 . . . . . . . 8 (𝑛 = 𝑁 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · (𝐺‘(√‘𝑁))))
49 oveq1 6622 . . . . . . . . . 10 (𝑛 = 𝑁 → (𝑛 / 2) = (𝑁 / 2))
5049fveq2d 6162 . . . . . . . . 9 (𝑛 = 𝑁 → (𝐺‘(𝑛 / 2)) = (𝐺‘(𝑁 / 2)))
5150oveq2d 6631 . . . . . . . 8 (𝑛 = 𝑁 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · (𝐺‘(𝑁 / 2))))
5248, 51oveq12d 6633 . . . . . . 7 (𝑛 = 𝑁 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))))
53 oveq2 6623 . . . . . . . . 9 (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
5453fveq2d 6162 . . . . . . . 8 (𝑛 = 𝑁 → (√‘(2 · 𝑛)) = (√‘(2 · 𝑁)))
5554oveq2d 6631 . . . . . . 7 (𝑛 = 𝑁 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / (√‘(2 · 𝑁))))
5652, 55oveq12d 6633 . . . . . 6 (𝑛 = 𝑁 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
57 ovex 6643 . . . . . 6 ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ V
5856, 2, 57fvmpt 6249 . . . . 5 (𝑁 ∈ ℕ → (𝐹𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
598, 58syl 17 . . . 4 (𝜑 → (𝐹𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
60 sqrt2re 14923 . . . . . . 7 (√‘2) ∈ ℝ
618nnrpd 11830 . . . . . . . . . 10 (𝜑𝑁 ∈ ℝ+)
6261rpsqrtcld 14100 . . . . . . . . 9 (𝜑 → (√‘𝑁) ∈ ℝ+)
63 fveq2 6158 . . . . . . . . . . 11 (𝑥 = (√‘𝑁) → (log‘𝑥) = (log‘(√‘𝑁)))
64 id 22 . . . . . . . . . . 11 (𝑥 = (√‘𝑁) → 𝑥 = (√‘𝑁))
6563, 64oveq12d 6633 . . . . . . . . . 10 (𝑥 = (√‘𝑁) → ((log‘𝑥) / 𝑥) = ((log‘(√‘𝑁)) / (√‘𝑁)))
66 ovex 6643 . . . . . . . . . 10 ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ V
6765, 3, 66fvmpt 6249 . . . . . . . . 9 ((√‘𝑁) ∈ ℝ+ → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
6862, 67syl 17 . . . . . . . 8 (𝜑 → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
6962relogcld 24307 . . . . . . . . 9 (𝜑 → (log‘(√‘𝑁)) ∈ ℝ)
7069, 62rerpdivcld 11863 . . . . . . . 8 (𝜑 → ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ ℝ)
7168, 70eqeltrd 2698 . . . . . . 7 (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℝ)
72 remulcl 9981 . . . . . . 7 (((√‘2) ∈ ℝ ∧ (𝐺‘(√‘𝑁)) ∈ ℝ) → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
7360, 71, 72sylancr 694 . . . . . 6 (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
74 9re 11067 . . . . . . . 8 9 ∈ ℝ
75 4re 11057 . . . . . . . 8 4 ∈ ℝ
76 4ne0 11077 . . . . . . . 8 4 ≠ 0
7774, 75, 76redivcli 10752 . . . . . . 7 (9 / 4) ∈ ℝ
7861rphalfcld 11844 . . . . . . . . 9 (𝜑 → (𝑁 / 2) ∈ ℝ+)
79 fveq2 6158 . . . . . . . . . . 11 (𝑥 = (𝑁 / 2) → (log‘𝑥) = (log‘(𝑁 / 2)))
80 id 22 . . . . . . . . . . 11 (𝑥 = (𝑁 / 2) → 𝑥 = (𝑁 / 2))
8179, 80oveq12d 6633 . . . . . . . . . 10 (𝑥 = (𝑁 / 2) → ((log‘𝑥) / 𝑥) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
82 ovex 6643 . . . . . . . . . 10 ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ V
8381, 3, 82fvmpt 6249 . . . . . . . . 9 ((𝑁 / 2) ∈ ℝ+ → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
8478, 83syl 17 . . . . . . . 8 (𝜑 → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
8578relogcld 24307 . . . . . . . . 9 (𝜑 → (log‘(𝑁 / 2)) ∈ ℝ)
8685, 78rerpdivcld 11863 . . . . . . . 8 (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℝ)
8784, 86eqeltrd 2698 . . . . . . 7 (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℝ)
88 remulcl 9981 . . . . . . 7 (((9 / 4) ∈ ℝ ∧ (𝐺‘(𝑁 / 2)) ∈ ℝ) → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
8977, 87, 88sylancr 694 . . . . . 6 (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
9073, 89readdcld 10029 . . . . 5 (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℝ)
91 2rp 11797 . . . . . . 7 2 ∈ ℝ+
92 relogcl 24260 . . . . . . 7 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
9391, 92ax-mp 5 . . . . . 6 (log‘2) ∈ ℝ
94 rpmulcl 11815 . . . . . . . 8 ((2 ∈ ℝ+𝑁 ∈ ℝ+) → (2 · 𝑁) ∈ ℝ+)
9591, 61, 94sylancr 694 . . . . . . 7 (𝜑 → (2 · 𝑁) ∈ ℝ+)
9695rpsqrtcld 14100 . . . . . 6 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ+)
97 rerpdivcl 11821 . . . . . 6 (((log‘2) ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ+) → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
9893, 96, 97sylancr 694 . . . . 5 (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
9990, 98readdcld 10029 . . . 4 (𝜑 → ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ ℝ)
10059, 99eqeltrd 2698 . . 3 (𝜑 → (𝐹𝑁) ∈ ℝ)
10193a1i 11 . . . 4 (𝜑 → (log‘2) ∈ ℝ)
10244simprd 479 . . . 4 (𝜑 → (𝐹64) < (log‘2))
103 nnrp 11802 . . . . . . . . . . 11 (4 ∈ ℕ → 4 ∈ ℝ+)
1045, 103ax-mp 5 . . . . . . . . . 10 4 ∈ ℝ+
105 relogcl 24260 . . . . . . . . . 10 (4 ∈ ℝ+ → (log‘4) ∈ ℝ)
106104, 105ax-mp 5 . . . . . . . . 9 (log‘4) ∈ ℝ
107 remulcl 9981 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ (log‘4) ∈ ℝ) → (𝑁 · (log‘4)) ∈ ℝ)
10836, 106, 107sylancl 693 . . . . . . . 8 (𝜑 → (𝑁 · (log‘4)) ∈ ℝ)
10961relogcld 24307 . . . . . . . 8 (𝜑 → (log‘𝑁) ∈ ℝ)
110108, 109resubcld 10418 . . . . . . 7 (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) ∈ ℝ)
111 rpre 11799 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℝ+ → (2 · 𝑁) ∈ ℝ)
112 rpge0 11805 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℝ+ → 0 ≤ (2 · 𝑁))
113111, 112resqrtcld 14106 . . . . . . . . . . . 12 ((2 · 𝑁) ∈ ℝ+ → (√‘(2 · 𝑁)) ∈ ℝ)
11495, 113syl 17 . . . . . . . . . . 11 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
115 3nn 11146 . . . . . . . . . . 11 3 ∈ ℕ
116 nndivre 11016 . . . . . . . . . . 11 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
117114, 115, 116sylancl 693 . . . . . . . . . 10 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
118 2re 11050 . . . . . . . . . 10 2 ∈ ℝ
119 readdcl 9979 . . . . . . . . . 10 ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
120117, 118, 119sylancl 693 . . . . . . . . 9 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
12195relogcld 24307 . . . . . . . . 9 (𝜑 → (log‘(2 · 𝑁)) ∈ ℝ)
122120, 121remulcld 10030 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℝ)
123 remulcl 9981 . . . . . . . . . . . 12 ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (4 · 𝑁) ∈ ℝ)
12475, 36, 123sylancr 694 . . . . . . . . . . 11 (𝜑 → (4 · 𝑁) ∈ ℝ)
125 nndivre 11016 . . . . . . . . . . 11 (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
126124, 115, 125sylancl 693 . . . . . . . . . 10 (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
127 5re 11059 . . . . . . . . . 10 5 ∈ ℝ
128 resubcl 10305 . . . . . . . . . 10 ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
129126, 127, 128sylancl 693 . . . . . . . . 9 (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
130 remulcl 9981 . . . . . . . . 9 (((((4 · 𝑁) / 3) − 5) ∈ ℝ ∧ (log‘2) ∈ ℝ) → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
131129, 93, 130sylancl 693 . . . . . . . 8 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
132122, 131readdcld 10029 . . . . . . 7 (𝜑 → (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ∈ ℝ)
133 remulcl 9981 . . . . . . . . 9 ((((4 · 𝑁) / 3) ∈ ℝ ∧ (log‘2) ∈ ℝ) → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
134126, 93, 133sylancl 693 . . . . . . . 8 (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
135134, 109resubcld 10418 . . . . . . 7 (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℝ)
1368nnzd 11441 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
137 df-5 11042 . . . . . . . . . . . 12 5 = (4 + 1)
13875a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 4 ∈ ℝ)
139 6nn 11149 . . . . . . . . . . . . . . . 16 6 ∈ ℕ
140 4nn0 11271 . . . . . . . . . . . . . . . 16 4 ∈ ℕ0
141 4lt10 11638 . . . . . . . . . . . . . . . 16 4 < 10
142139, 140, 140, 141declti 11506 . . . . . . . . . . . . . . 15 4 < 64
143142a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 4 < 64)
144138, 35, 36, 143, 1lttrd 10158 . . . . . . . . . . . . 13 (𝜑 → 4 < 𝑁)
145 4z 11371 . . . . . . . . . . . . . 14 4 ∈ ℤ
146 zltp1le 11387 . . . . . . . . . . . . . 14 ((4 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
147145, 136, 146sylancr 694 . . . . . . . . . . . . 13 (𝜑 → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
148144, 147mpbid 222 . . . . . . . . . . . 12 (𝜑 → (4 + 1) ≤ 𝑁)
149137, 148syl5eqbr 4658 . . . . . . . . . . 11 (𝜑 → 5 ≤ 𝑁)
150 5nn 11148 . . . . . . . . . . . . 13 5 ∈ ℕ
151150nnzi 11361 . . . . . . . . . . . 12 5 ∈ ℤ
152151eluz1i 11655 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘5) ↔ (𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
153136, 149, 152sylanbrc 697 . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ‘5))
154 bposlem9.5 . . . . . . . . . . 11 (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
155 breq2 4627 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → (𝑁 < 𝑝𝑁 < 𝑞))
156 breq1 4626 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → (𝑝 ≤ (2 · 𝑁) ↔ 𝑞 ≤ (2 · 𝑁)))
157155, 156anbi12d 746 . . . . . . . . . . . 12 (𝑝 = 𝑞 → ((𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)) ↔ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁))))
158157cbvrexv 3164 . . . . . . . . . . 11 (∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)) ↔ ∃𝑞 ∈ ℙ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁)))
159154, 158sylnib 318 . . . . . . . . . 10 (𝜑 → ¬ ∃𝑞 ∈ ℙ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁)))
160 eqid 2621 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
161 eqid 2621 . . . . . . . . . 10 (⌊‘((2 · 𝑁) / 3)) = (⌊‘((2 · 𝑁) / 3))
162 eqid 2621 . . . . . . . . . 10 (⌊‘(√‘(2 · 𝑁))) = (⌊‘(√‘(2 · 𝑁)))
163153, 159, 160, 161, 162bposlem6 24948 . . . . . . . . 9 (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
164 reexplog 24279 . . . . . . . . . . . 12 ((4 ∈ ℝ+𝑁 ∈ ℤ) → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
165104, 136, 164sylancr 694 . . . . . . . . . . 11 (𝜑 → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
16661reeflogd 24308 . . . . . . . . . . . 12 (𝜑 → (exp‘(log‘𝑁)) = 𝑁)
167166eqcomd 2627 . . . . . . . . . . 11 (𝜑𝑁 = (exp‘(log‘𝑁)))
168165, 167oveq12d 6633 . . . . . . . . . 10 (𝜑 → ((4↑𝑁) / 𝑁) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
169108recnd 10028 . . . . . . . . . . 11 (𝜑 → (𝑁 · (log‘4)) ∈ ℂ)
170109recnd 10028 . . . . . . . . . . 11 (𝜑 → (log‘𝑁) ∈ ℂ)
171 efsub 14774 . . . . . . . . . . 11 (((𝑁 · (log‘4)) ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
172169, 170, 171syl2anc 692 . . . . . . . . . 10 (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
173168, 172eqtr4d 2658 . . . . . . . . 9 (𝜑 → ((4↑𝑁) / 𝑁) = (exp‘((𝑁 · (log‘4)) − (log‘𝑁))))
17495rpcnd 11834 . . . . . . . . . . . 12 (𝜑 → (2 · 𝑁) ∈ ℂ)
17595rpne0d 11837 . . . . . . . . . . . 12 (𝜑 → (2 · 𝑁) ≠ 0)
176120recnd 10028 . . . . . . . . . . . 12 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℂ)
177174, 175, 176cxpefd 24392 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) = (exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))))
178 2cn 11051 . . . . . . . . . . . 12 2 ∈ ℂ
179 2ne0 11073 . . . . . . . . . . . 12 2 ≠ 0
180129recnd 10028 . . . . . . . . . . . 12 (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℂ)
181 cxpef 24345 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ (((4 · 𝑁) / 3) − 5) ∈ ℂ) → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
182178, 179, 180, 181mp3an12i 1425 . . . . . . . . . . 11 (𝜑 → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
183177, 182oveq12d 6633 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
184122recnd 10028 . . . . . . . . . . 11 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℂ)
185131recnd 10028 . . . . . . . . . . 11 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℂ)
186 efadd 14768 . . . . . . . . . . 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)))))
187184, 185, 186syl2anc 692 . . . . . . . . . 10 (𝜑 → (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
188183, 187eqtr4d 2658 . . . . . . . . 9 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
189163, 173, 1883brtr3d 4654 . . . . . . . 8 (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
190 eflt 14791 . . . . . . . . 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))))))
191110, 132, 190syl2anc 692 . . . . . . . 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))))))
192189, 191mpbird 247 . . . . . . 7 (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))
193110, 132, 135, 192ltsub1dd 10599 . . . . . 6 (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) < ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
19436recnd 10028 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
195 mulcom 9982 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) = (𝑁 · 2))
196178, 194, 195sylancr 694 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) = (𝑁 · 2))
197196oveq1d 6630 . . . . . . . . 9 (𝜑 → ((2 · 𝑁) · (log‘2)) = ((𝑁 · 2) · (log‘2)))
19893recni 10012 . . . . . . . . . . . 12 (log‘2) ∈ ℂ
199 mulass 9984 . . . . . . . . . . . 12 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ (log‘2) ∈ ℂ) → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
200178, 198, 199mp3an23 1413 . . . . . . . . . . 11 (𝑁 ∈ ℂ → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
201194, 200syl 17 . . . . . . . . . 10 (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
2021982timesi 11107 . . . . . . . . . . . 12 (2 · (log‘2)) = ((log‘2) + (log‘2))
203 relogmul 24276 . . . . . . . . . . . . 13 ((2 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(2 · 2)) = ((log‘2) + (log‘2)))
20491, 91, 203mp2an 707 . . . . . . . . . . . 12 (log‘(2 · 2)) = ((log‘2) + (log‘2))
205 2t2e4 11137 . . . . . . . . . . . . 13 (2 · 2) = 4
206205fveq2i 6161 . . . . . . . . . . . 12 (log‘(2 · 2)) = (log‘4)
207202, 204, 2063eqtr2i 2649 . . . . . . . . . . 11 (2 · (log‘2)) = (log‘4)
208207oveq2i 6626 . . . . . . . . . 10 (𝑁 · (2 · (log‘2))) = (𝑁 · (log‘4))
209201, 208syl6eq 2671 . . . . . . . . 9 (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (log‘4)))
210197, 209eqtrd 2655 . . . . . . . 8 (𝜑 → ((2 · 𝑁) · (log‘2)) = (𝑁 · (log‘4)))
211210oveq1d 6630 . . . . . . 7 (𝜑 → (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
212 4p2e6 11122 . . . . . . . . . . . . . . 15 (4 + 2) = 6
213212oveq1i 6625 . . . . . . . . . . . . . 14 ((4 + 2) · 𝑁) = (6 · 𝑁)
214 4cn 11058 . . . . . . . . . . . . . . 15 4 ∈ ℂ
215 adddir 9991 . . . . . . . . . . . . . . 15 ((4 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
216214, 178, 194, 215mp3an12i 1425 . . . . . . . . . . . . . 14 (𝜑 → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
217213, 216syl5eqr 2669 . . . . . . . . . . . . 13 (𝜑 → (6 · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
218217oveq1d 6630 . . . . . . . . . . . 12 (𝜑 → ((6 · 𝑁) / 3) = (((4 · 𝑁) + (2 · 𝑁)) / 3))
219 6cn 11062 . . . . . . . . . . . . . . 15 6 ∈ ℂ
220 3cn 11055 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
221 3ne0 11075 . . . . . . . . . . . . . . . 16 3 ≠ 0
222220, 221pm3.2i 471 . . . . . . . . . . . . . . 15 (3 ∈ ℂ ∧ 3 ≠ 0)
223 div23 10664 . . . . . . . . . . . . . . 15 ((6 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
224219, 222, 223mp3an13 1412 . . . . . . . . . . . . . 14 (𝑁 ∈ ℂ → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
225194, 224syl 17 . . . . . . . . . . . . 13 (𝜑 → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
226 3t2e6 11139 . . . . . . . . . . . . . . . 16 (3 · 2) = 6
227226oveq1i 6625 . . . . . . . . . . . . . . 15 ((3 · 2) / 3) = (6 / 3)
228178, 220, 221divcan3i 10731 . . . . . . . . . . . . . . 15 ((3 · 2) / 3) = 2
229227, 228eqtr3i 2645 . . . . . . . . . . . . . 14 (6 / 3) = 2
230229oveq1i 6625 . . . . . . . . . . . . 13 ((6 / 3) · 𝑁) = (2 · 𝑁)
231225, 230syl6eq 2671 . . . . . . . . . . . 12 (𝜑 → ((6 · 𝑁) / 3) = (2 · 𝑁))
232124recnd 10028 . . . . . . . . . . . . 13 (𝜑 → (4 · 𝑁) ∈ ℂ)
233 remulcl 9981 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
234118, 36, 233sylancr 694 . . . . . . . . . . . . . 14 (𝜑 → (2 · 𝑁) ∈ ℝ)
235234recnd 10028 . . . . . . . . . . . . 13 (𝜑 → (2 · 𝑁) ∈ ℂ)
236 divdir 10670 . . . . . . . . . . . . . 14 (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
237222, 236mp3an3 1410 . . . . . . . . . . . . 13 (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
238232, 235, 237syl2anc 692 . . . . . . . . . . . 12 (𝜑 → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
239218, 231, 2383eqtr3d 2663 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
240239oveq1d 6630 . . . . . . . . . 10 (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)) − ((4 · 𝑁) / 3)))
241126recnd 10028 . . . . . . . . . . 11 (𝜑 → ((4 · 𝑁) / 3) ∈ ℂ)
242 3rp 11798 . . . . . . . . . . . . 13 3 ∈ ℝ+
243 rpdivcl 11816 . . . . . . . . . . . . 13 (((2 · 𝑁) ∈ ℝ+ ∧ 3 ∈ ℝ+) → ((2 · 𝑁) / 3) ∈ ℝ+)
24495, 242, 243sylancl 693 . . . . . . . . . . . 12 (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ+)
245244rpcnd 11834 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) / 3) ∈ ℂ)
246241, 245pncan2d 10354 . . . . . . . . . 10 (𝜑 → ((((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
247240, 246eqtrd 2655 . . . . . . . . 9 (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
248247oveq1d 6630 . . . . . . . 8 (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) / 3) · (log‘2)))
249101recnd 10028 . . . . . . . . 9 (𝜑 → (log‘2) ∈ ℂ)
250235, 241, 249subdird 10447 . . . . . . . 8 (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
251248, 250eqtr3d 2657 . . . . . . 7 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
252134recnd 10028 . . . . . . . 8 (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℂ)
253169, 252, 170nnncan2d 10387 . . . . . . 7 (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
254211, 251, 2533eqtr4d 2665 . . . . . 6 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
255117recnd 10028 . . . . . . . . . 10 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℂ)
256178a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℂ)
257121recnd 10028 . . . . . . . . . 10 (𝜑 → (log‘(2 · 𝑁)) ∈ ℂ)
258255, 256, 257adddird 10025 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))))
259 relogmul 24276 . . . . . . . . . . . . 13 ((2 ∈ ℝ+𝑁 ∈ ℝ+) → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
26091, 61, 259sylancr 694 . . . . . . . . . . . 12 (𝜑 → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
261260oveq2d 6631 . . . . . . . . . . 11 (𝜑 → (2 · (log‘(2 · 𝑁))) = (2 · ((log‘2) + (log‘𝑁))))
262256, 249, 170adddid 10024 . . . . . . . . . . 11 (𝜑 → (2 · ((log‘2) + (log‘𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
263261, 262eqtrd 2655 . . . . . . . . . 10 (𝜑 → (2 · (log‘(2 · 𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
264263oveq2d 6631 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
265258, 264eqtrd 2655 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
266 5cn 11060 . . . . . . . . . . . 12 5 ∈ ℂ
267266a1i 11 . . . . . . . . . . 11 (𝜑 → 5 ∈ ℂ)
268241, 267, 249subdird 10447 . . . . . . . . . 10 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) = ((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))))
269268oveq1d 6630 . . . . . . . . 9 (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
270266, 198mulcli 10005 . . . . . . . . . . 11 (5 · (log‘2)) ∈ ℂ
271270a1i 11 . . . . . . . . . 10 (𝜑 → (5 · (log‘2)) ∈ ℂ)
272252, 271, 170nnncan1d 10386 . . . . . . . . 9 (𝜑 → (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
273269, 272eqtrd 2655 . . . . . . . 8 (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
274265, 273oveq12d 6633 . . . . . . 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)))))
275135recnd 10028 . . . . . . . 8 (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℂ)
276184, 185, 275addsubassd 10372 . . . . . . 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‘𝑁)))))
277266, 220, 198subdiri 10440 . . . . . . . . . . . . 13 ((5 − 3) · (log‘2)) = ((5 · (log‘2)) − (3 · (log‘2)))
278 3p2e5 11120 . . . . . . . . . . . . . . . 16 (3 + 2) = 5
279278oveq1i 6625 . . . . . . . . . . . . . . 15 ((3 + 2) − 3) = (5 − 3)
280 pncan2 10248 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
281220, 178, 280mp2an 707 . . . . . . . . . . . . . . 15 ((3 + 2) − 3) = 2
282279, 281eqtr3i 2645 . . . . . . . . . . . . . 14 (5 − 3) = 2
283282oveq1i 6625 . . . . . . . . . . . . 13 ((5 − 3) · (log‘2)) = (2 · (log‘2))
284277, 283eqtr3i 2645 . . . . . . . . . . . 12 ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2))
285284a1i 11 . . . . . . . . . . 11 (𝜑 → ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2)))
286 df-3 11040 . . . . . . . . . . . . . . . 16 3 = (2 + 1)
287286oveq1i 6625 . . . . . . . . . . . . . . 15 (3 · (log‘𝑁)) = ((2 + 1) · (log‘𝑁))
288 1cnd 10016 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℂ)
289256, 288, 170adddird 10025 . . . . . . . . . . . . . . 15 (𝜑 → ((2 + 1) · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
290287, 289syl5eq 2667 . . . . . . . . . . . . . 14 (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
291170mulid2d 10018 . . . . . . . . . . . . . . 15 (𝜑 → (1 · (log‘𝑁)) = (log‘𝑁))
292291oveq2d 6631 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (log‘𝑁)) + (1 · (log‘𝑁))) = ((2 · (log‘𝑁)) + (log‘𝑁)))
293290, 292eqtrd 2655 . . . . . . . . . . . . 13 (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (log‘𝑁)))
294293oveq1d 6630 . . . . . . . . . . . 12 (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))))
295 mulcl 9980 . . . . . . . . . . . . . 14 ((2 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (2 · (log‘𝑁)) ∈ ℂ)
296178, 170, 295sylancr 694 . . . . . . . . . . . . 13 (𝜑 → (2 · (log‘𝑁)) ∈ ℂ)
297296, 170, 271addsubassd 10372 . . . . . . . . . . . 12 (𝜑 → (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
298294, 297eqtrd 2655 . . . . . . . . . . 11 (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
299285, 298oveq12d 6633 . . . . . . . . . 10 (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
300 relogdiv 24277 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
30161, 91, 300sylancl 693 . . . . . . . . . . . . 13 (𝜑 → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
302301oveq2d 6631 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘(𝑁 / 2))) = (3 · ((log‘𝑁) − (log‘2))))
303 subdi 10423 . . . . . . . . . . . . . 14 ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
304220, 198, 303mp3an13 1412 . . . . . . . . . . . . 13 ((log‘𝑁) ∈ ℂ → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
305170, 304syl 17 . . . . . . . . . . . 12 (𝜑 → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
306302, 305eqtrd 2655 . . . . . . . . . . 11 (𝜑 → (3 · (log‘(𝑁 / 2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
307 div23 10664 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
308178, 222, 307mp3an13 1412 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℂ → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
309194, 308syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
310220, 178, 220, 178, 179, 179divmuldivi 10745 . . . . . . . . . . . . . . . . 17 ((3 / 2) · (3 / 2)) = ((3 · 3) / (2 · 2))
311 3t3e9 11140 . . . . . . . . . . . . . . . . . 18 (3 · 3) = 9
312311, 205oveq12i 6627 . . . . . . . . . . . . . . . . 17 ((3 · 3) / (2 · 2)) = (9 / 4)
313310, 312eqtr2i 2644 . . . . . . . . . . . . . . . 16 (9 / 4) = ((3 / 2) · (3 / 2))
314313a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (9 / 4) = ((3 / 2) · (3 / 2)))
315309, 314oveq12d 6633 . . . . . . . . . . . . . 14 (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))))
316178, 220, 221divcli 10727 . . . . . . . . . . . . . . 15 (2 / 3) ∈ ℂ
317220, 178, 179divcli 10727 . . . . . . . . . . . . . . . 16 (3 / 2) ∈ ℂ
318 mul4 10165 . . . . . . . . . . . . . . . 16 ((((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ ((3 / 2) ∈ ℂ ∧ (3 / 2) ∈ ℂ)) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
319317, 317, 318mpanr12 720 . . . . . . . . . . . . . . 15 (((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
320316, 194, 319sylancr 694 . . . . . . . . . . . . . 14 (𝜑 → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
321 divcan6 10692 . . . . . . . . . . . . . . . . . 18 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 / 3) · (3 / 2)) = 1)
322178, 179, 220, 221, 321mp4an 708 . . . . . . . . . . . . . . . . 17 ((2 / 3) · (3 / 2)) = 1
323322oveq1i 6625 . . . . . . . . . . . . . . . 16 (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (1 · (𝑁 · (3 / 2)))
324 mulcl 9980 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℂ ∧ (3 / 2) ∈ ℂ) → (𝑁 · (3 / 2)) ∈ ℂ)
325194, 317, 324sylancl 693 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 · (3 / 2)) ∈ ℂ)
326325mulid2d 10018 . . . . . . . . . . . . . . . 16 (𝜑 → (1 · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
327323, 326syl5eq 2667 . . . . . . . . . . . . . . 15 (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
328 2cnne0 11202 . . . . . . . . . . . . . . . . 17 (2 ∈ ℂ ∧ 2 ≠ 0)
329 div12 10667 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℂ ∧ 3 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
330220, 328, 329mp3an23 1413 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℂ → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
331194, 330syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
332327, 331eqtrd 2655 . . . . . . . . . . . . . 14 (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (3 · (𝑁 / 2)))
333315, 320, 3323eqtrd 2659 . . . . . . . . . . . . 13 (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (3 · (𝑁 / 2)))
334333, 84oveq12d 6633 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))))
33577recni 10012 . . . . . . . . . . . . . 14 (9 / 4) ∈ ℂ
336335a1i 11 . . . . . . . . . . . . 13 (𝜑 → (9 / 4) ∈ ℂ)
33787recnd 10028 . . . . . . . . . . . . 13 (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℂ)
338245, 336, 337mulassd 10023 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))
339220a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 3 ∈ ℂ)
34078rpcnd 11834 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 / 2) ∈ ℂ)
34185recnd 10028 . . . . . . . . . . . . . . 15 (𝜑 → (log‘(𝑁 / 2)) ∈ ℂ)
34278rpne0d 11837 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 / 2) ≠ 0)
343341, 340, 342divcld 10761 . . . . . . . . . . . . . 14 (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℂ)
344339, 340, 343mulassd 10023 . . . . . . . . . . . . 13 (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))))
345341, 340, 342divcan2d 10763 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (log‘(𝑁 / 2)))
346345oveq2d 6631 . . . . . . . . . . . . 13 (𝜑 → (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
347344, 346eqtrd 2655 . . . . . . . . . . . 12 (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · (log‘(𝑁 / 2))))
348334, 338, 3473eqtr3d 2663 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
349220, 198mulcli 10005 . . . . . . . . . . . . 13 (3 · (log‘2)) ∈ ℂ
350349a1i 11 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘2)) ∈ ℂ)
351 mulcl 9980 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (3 · (log‘𝑁)) ∈ ℂ)
352220, 170, 351sylancr 694 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘𝑁)) ∈ ℂ)
353271, 350, 352npncan3d 10388 . . . . . . . . . . 11 (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
354306, 348, 3533eqtr4d 2665 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))))
355118, 93remulcli 10014 . . . . . . . . . . . . 13 (2 · (log‘2)) ∈ ℝ
356355recni 10012 . . . . . . . . . . . 12 (2 · (log‘2)) ∈ ℂ
357356a1i 11 . . . . . . . . . . 11 (𝜑 → (2 · (log‘2)) ∈ ℂ)
358 subcl 10240 . . . . . . . . . . . 12 (((log‘𝑁) ∈ ℂ ∧ (5 · (log‘2)) ∈ ℂ) → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
359170, 270, 358sylancl 693 . . . . . . . . . . 11 (𝜑 → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
360357, 296, 359addassd 10022 . . . . . . . . . 10 (𝜑 → (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
361299, 354, 3603eqtr4d 2665 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))))
362361oveq2d 6631 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2))))))
363 mulcl 9980 . . . . . . . . . . 11 ((((√‘(2 · 𝑁)) / 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
364255, 198, 363sylancl 693 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
365255, 170mulcld 10020 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) ∈ ℂ)
36689recnd 10028 . . . . . . . . . . 11 (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℂ)
367245, 366mulcld 10020 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
368364, 365, 367addassd 10022 . . . . . . . . 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)))))))
369260oveq2d 6631 . . . . . . . . . . 11 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))))
370255, 249, 170adddid 10024 . . . . . . . . . . 11 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
371369, 370eqtrd 2655 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
372371oveq1d 6630 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
37359oveq2d 6631 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))))
37490recnd 10028 . . . . . . . . . . . 12 (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
37598recnd 10028 . . . . . . . . . . . 12 (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℂ)
376245, 374, 375adddid 10024 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
377373, 376eqtrd 2655 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
37873recnd 10028 . . . . . . . . . . . . 13 (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℂ)
379245, 378, 366adddid 10024 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
38095rpge0d 11836 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 ≤ (2 · 𝑁))
381 remsqsqrt 13947 . . . . . . . . . . . . . . . . . 18 (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
382234, 380, 381syl2anc 692 . . . . . . . . . . . . . . . . 17 (𝜑 → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
383382oveq1d 6630 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = ((2 · 𝑁) / 3))
384114recnd 10028 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘(2 · 𝑁)) ∈ ℂ)
385221a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ≠ 0)
386384, 384, 339, 385div23d 10798 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
387383, 386eqtr3d 2657 . . . . . . . . . . . . . . 15 (𝜑 → ((2 · 𝑁) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
388387oveq1d 6630 . . . . . . . . . . . . . 14 (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))))
389255, 384, 378mulassd 10023 . . . . . . . . . . . . . 14 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))))
390 0le2 11071 . . . . . . . . . . . . . . . . . . 19 0 ≤ 2
391118, 390pm3.2i 471 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ ∧ 0 ≤ 2)
39261rprege0d 11839 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
393 sqrtmul 13950 . . . . . . . . . . . . . . . . . 18 (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
394391, 392, 393sylancr 694 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
395394oveq1d 6630 . . . . . . . . . . . . . . . 16 (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))))
39660recni 10012 . . . . . . . . . . . . . . . . . 18 (√‘2) ∈ ℂ
397396a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘2) ∈ ℂ)
39862rpcnd 11834 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘𝑁) ∈ ℂ)
39971recnd 10028 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℂ)
400397, 398, 397, 399mul4d 10208 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))))
401 remsqsqrt 13947 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
402118, 390, 401mp2an 707 . . . . . . . . . . . . . . . . . . 19 ((√‘2) · (√‘2)) = 2
403402a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((√‘2) · (√‘2)) = 2)
40468oveq2d 6631 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))))
40569recnd 10028 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (log‘(√‘𝑁)) ∈ ℂ)
40662rpne0d 11837 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (√‘𝑁) ≠ 0)
407405, 398, 406divcan2d 10763 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))) = (log‘(√‘𝑁)))
408404, 407eqtrd 2655 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = (log‘(√‘𝑁)))
409403, 408oveq12d 6633 . . . . . . . . . . . . . . . . 17 (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (2 · (log‘(√‘𝑁))))
4104052timesd 11235 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 · (log‘(√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
41162, 62relogmuld 24309 . . . . . . . . . . . . . . . . . 18 (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
412 remsqsqrt 13947 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
413392, 412syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
414413fveq2d 6162 . . . . . . . . . . . . . . . . . 18 (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = (log‘𝑁))
415411, 414eqtr3d 2657 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘(√‘𝑁)) + (log‘(√‘𝑁))) = (log‘𝑁))
416409, 410, 4153eqtrd 2659 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
417395, 400, 4163eqtrd 2659 . . . . . . . . . . . . . . 15 (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
418417oveq2d 6631 . . . . . . . . . . . . . 14 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
419388, 389, 4183eqtrd 2659 . . . . . . . . . . . . 13 (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
420419oveq1d 6630 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
421379, 420eqtrd 2655 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
422387oveq1d 6630 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))))
423255, 384, 375mulassd 10023 . . . . . . . . . . . 12 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))))
42496rpne0d 11837 . . . . . . . . . . . . . 14 (𝜑 → (√‘(2 · 𝑁)) ≠ 0)
425249, 384, 424divcan2d 10763 . . . . . . . . . . . . 13 (𝜑 → ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁)))) = (log‘2))
426425oveq2d 6631 . . . . . . . . . . . 12 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
427422, 423, 4263eqtrd 2659 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
428421, 427oveq12d 6633 . . . . . . . . . 10 (𝜑 → ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((√‘(2 · 𝑁)) / 3) · (log‘2))))
429365, 367addcld 10019 . . . . . . . . . . 11 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) ∈ ℂ)
430429, 364addcomd 10198 . . . . . . . . . 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)))))))
431377, 428, 4303eqtrd 2659 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
432368, 372, 4313eqtr4rd 2666 . . . . . . . 8 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
433255, 257mulcld 10020 . . . . . . . . 9 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) ∈ ℂ)
434 addcl 9978 . . . . . . . . . 10 (((2 · (log‘2)) ∈ ℂ ∧ (2 · (log‘𝑁)) ∈ ℂ) → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
435356, 296, 434sylancr 694 . . . . . . . . 9 (𝜑 → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
436433, 435, 359addassd 10022 . . . . . . . 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))))))
437362, 432, 4363eqtr4d 2665 . . . . . . 7 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))))
438274, 276, 4373eqtr4rd 2666 . . . . . 6 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
439193, 254, 4383brtr4d 4655 . . . . 5 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹𝑁)))
440101, 100, 244ltmul2d 11874 . . . . 5 (𝜑 → ((log‘2) < (𝐹𝑁) ↔ (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹𝑁))))
441439, 440mpbird 247 . . . 4 (𝜑 → (log‘2) < (𝐹𝑁))
44245, 101, 100, 102, 441lttrd 10158 . . 3 (𝜑 → (𝐹64) < (𝐹𝑁))
44345, 100, 442ltnsymd 10146 . 2 (𝜑 → ¬ (𝐹𝑁) < (𝐹64))
44442, 443pm2.21dd 186 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  wrex 2909  ifcif 4064   class class class wbr 4623  cmpt 4683  cfv 5857  (class class class)co 6615  cc 9894  cr 9895  0cc0 9896  1c1 9897   + caddc 9899   · cmul 9901   < clt 10034  cle 10035  cmin 10226   / cdiv 10644  cn 10980  2c2 11030  3c3 11031  4c4 11032  5c5 11033  6c6 11034  8c8 11036  9c9 11037  cz 11337  cdc 11453  cuz 11647  +crp 11792  cfl 12547  cexp 12816  Ccbc 13045  csqrt 13923  expce 14736  eceu 14737  cprime 15328   pCnt cpc 15484  logclog 24239  𝑐ccxp 24240
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974  ax-addf 9975  ax-mulf 9976
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-iin 4495  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-supp 7256  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-2o 7521  df-oadd 7524  df-er 7702  df-map 7819  df-pm 7820  df-ixp 7869  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-fsupp 8236  df-fi 8277  df-sup 8308  df-inf 8309  df-oi 8375  df-card 8725  df-cda 8950  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-7 11044  df-8 11045  df-9 11046  df-n0 11253  df-xnn0 11324  df-z 11338  df-dec 11454  df-uz 11648  df-q 11749  df-rp 11793  df-xneg 11906  df-xadd 11907  df-xmul 11908  df-ioo 12137  df-ioc 12138  df-ico 12139  df-icc 12140  df-fz 12285  df-fzo 12423  df-fl 12549  df-mod 12625  df-seq 12758  df-exp 12817  df-fac 13017  df-bc 13046  df-hash 13074  df-shft 13757  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-limsup 14152  df-clim 14169  df-rlim 14170  df-sum 14367  df-ef 14742  df-e 14743  df-sin 14744  df-cos 14745  df-pi 14747  df-dvds 14927  df-gcd 15160  df-prm 15329  df-pc 15485  df-struct 15802  df-ndx 15803  df-slot 15804  df-base 15805  df-sets 15806  df-ress 15807  df-plusg 15894  df-mulr 15895  df-starv 15896  df-sca 15897  df-vsca 15898  df-ip 15899  df-tset 15900  df-ple 15901  df-ds 15904  df-unif 15905  df-hom 15906  df-cco 15907  df-rest 16023  df-topn 16024  df-0g 16042  df-gsum 16043  df-topgen 16044  df-pt 16045  df-prds 16048  df-xrs 16102  df-qtop 16107  df-imas 16108  df-xps 16110  df-mre 16186  df-mrc 16187  df-acs 16189  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-submnd 17276  df-mulg 17481  df-cntz 17690  df-cmn 18135  df-psmet 19678  df-xmet 19679  df-met 19680  df-bl 19681  df-mopn 19682  df-fbas 19683  df-fg 19684  df-cnfld 19687  df-top 20639  df-topon 20656  df-topsp 20677  df-bases 20690  df-cld 20763  df-ntr 20764  df-cls 20765  df-nei 20842  df-lp 20880  df-perf 20881  df-cn 20971  df-cnp 20972  df-haus 21059  df-tx 21305  df-hmeo 21498  df-fil 21590  df-fm 21682  df-flim 21683  df-flf 21684  df-xms 22065  df-ms 22066  df-tms 22067  df-cncf 22621  df-limc 23570  df-dv 23571  df-log 24241  df-cxp 24242  df-cht 24757  df-ppi 24760
This theorem is referenced by:  bpos  24952
  Copyright terms: Public domain W3C validator