# Metamath Proof Explorer

## Theorem bposlem9

Description: Lemma for bpos . Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014) (Proof shortened by AV, 15-Sep-2021)

Ref Expression
Hypotheses bposlem7.1 ${⊢}{F}=\left({n}\in ℕ⟼\sqrt{2}{G}\left(\sqrt{{n}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{n}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{n}}}\right)\right)$
bposlem7.2 ${⊢}{G}=\left({x}\in {ℝ}^{+}⟼\frac{\mathrm{log}{x}}{{x}}\right)$
bposlem9.3 ${⊢}{\phi }\to {N}\in ℕ$
bposlem9.4 ${⊢}{\phi }\to 64<{N}$
bposlem9.5 ${⊢}{\phi }\to ¬\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\left({N}<{p}\wedge {p}\le 2\cdot {N}\right)$
Assertion bposlem9 ${⊢}{\phi }\to {\psi }$

### Proof

Step Hyp Ref Expression
1 bposlem7.1 ${⊢}{F}=\left({n}\in ℕ⟼\sqrt{2}{G}\left(\sqrt{{n}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{n}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{n}}}\right)\right)$
2 bposlem7.2 ${⊢}{G}=\left({x}\in {ℝ}^{+}⟼\frac{\mathrm{log}{x}}{{x}}\right)$
3 bposlem9.3 ${⊢}{\phi }\to {N}\in ℕ$
4 bposlem9.4 ${⊢}{\phi }\to 64<{N}$
5 bposlem9.5 ${⊢}{\phi }\to ¬\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\left({N}<{p}\wedge {p}\le 2\cdot {N}\right)$
6 6nn0 ${⊢}6\in {ℕ}_{0}$
7 4nn ${⊢}4\in ℕ$
8 6 7 decnncl ${⊢}64\in ℕ$
9 8 a1i ${⊢}{\phi }\to 64\in ℕ$
10 ere ${⊢}\mathrm{e}\in ℝ$
11 8re ${⊢}8\in ℝ$
12 egt2lt3 ${⊢}\left(2<\mathrm{e}\wedge \mathrm{e}<3\right)$
13 12 simpri ${⊢}\mathrm{e}<3$
14 3lt8 ${⊢}3<8$
15 3re ${⊢}3\in ℝ$
16 10 15 11 lttri ${⊢}\left(\mathrm{e}<3\wedge 3<8\right)\to \mathrm{e}<8$
17 13 14 16 mp2an ${⊢}\mathrm{e}<8$
18 10 11 17 ltleii ${⊢}\mathrm{e}\le 8$
19 0re ${⊢}0\in ℝ$
20 epos ${⊢}0<\mathrm{e}$
21 19 10 20 ltleii ${⊢}0\le \mathrm{e}$
22 8pos ${⊢}0<8$
23 19 11 22 ltleii ${⊢}0\le 8$
24 le2sq ${⊢}\left(\left(\mathrm{e}\in ℝ\wedge 0\le \mathrm{e}\right)\wedge \left(8\in ℝ\wedge 0\le 8\right)\right)\to \left(\mathrm{e}\le 8↔{\mathrm{e}}^{2}\le {8}^{2}\right)$
25 10 21 11 23 24 mp4an ${⊢}\mathrm{e}\le 8↔{\mathrm{e}}^{2}\le {8}^{2}$
26 18 25 mpbi ${⊢}{\mathrm{e}}^{2}\le {8}^{2}$
27 11 recni ${⊢}8\in ℂ$
28 27 sqvali ${⊢}{8}^{2}=8\cdot 8$
29 8t8e64 ${⊢}8\cdot 8=64$
30 28 29 eqtri ${⊢}{8}^{2}=64$
31 26 30 breqtri ${⊢}{\mathrm{e}}^{2}\le 64$
32 31 a1i ${⊢}{\phi }\to {\mathrm{e}}^{2}\le 64$
33 10 resqcli ${⊢}{\mathrm{e}}^{2}\in ℝ$
34 33 a1i ${⊢}{\phi }\to {\mathrm{e}}^{2}\in ℝ$
35 8 nnrei ${⊢}64\in ℝ$
36 35 a1i ${⊢}{\phi }\to 64\in ℝ$
37 3 nnred ${⊢}{\phi }\to {N}\in ℝ$
38 ltle ${⊢}\left(64\in ℝ\wedge {N}\in ℝ\right)\to \left(64<{N}\to 64\le {N}\right)$
39 35 37 38 sylancr ${⊢}{\phi }\to \left(64<{N}\to 64\le {N}\right)$
40 4 39 mpd ${⊢}{\phi }\to 64\le {N}$
41 34 36 37 32 40 letrd ${⊢}{\phi }\to {\mathrm{e}}^{2}\le {N}$
42 1 2 9 3 32 41 bposlem7 ${⊢}{\phi }\to \left(64<{N}\to {F}\left({N}\right)<{F}\left(64\right)\right)$
43 4 42 mpd ${⊢}{\phi }\to {F}\left({N}\right)<{F}\left(64\right)$
44 1 2 bposlem8 ${⊢}\left({F}\left(64\right)\in ℝ\wedge {F}\left(64\right)<\mathrm{log}2\right)$
45 44 a1i ${⊢}{\phi }\to \left({F}\left(64\right)\in ℝ\wedge {F}\left(64\right)<\mathrm{log}2\right)$
46 45 simpld ${⊢}{\phi }\to {F}\left(64\right)\in ℝ$
47 2fveq3 ${⊢}{n}={N}\to {G}\left(\sqrt{{n}}\right)={G}\left(\sqrt{{N}}\right)$
48 47 oveq2d ${⊢}{n}={N}\to \sqrt{2}{G}\left(\sqrt{{n}}\right)=\sqrt{2}{G}\left(\sqrt{{N}}\right)$
49 fvoveq1 ${⊢}{n}={N}\to {G}\left(\frac{{n}}{2}\right)={G}\left(\frac{{N}}{2}\right)$
50 49 oveq2d ${⊢}{n}={N}\to \left(\frac{9}{4}\right){G}\left(\frac{{n}}{2}\right)=\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)$
51 48 50 oveq12d ${⊢}{n}={N}\to \sqrt{2}{G}\left(\sqrt{{n}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{n}}{2}\right)=\sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)$
52 oveq2 ${⊢}{n}={N}\to 2{n}=2\cdot {N}$
53 52 fveq2d ${⊢}{n}={N}\to \sqrt{2{n}}=\sqrt{2\cdot {N}}$
54 53 oveq2d ${⊢}{n}={N}\to \frac{\mathrm{log}2}{\sqrt{2{n}}}=\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}$
55 51 54 oveq12d ${⊢}{n}={N}\to \sqrt{2}{G}\left(\sqrt{{n}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{n}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{n}}}\right)=\sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)$
56 ovex ${⊢}\sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)\in \mathrm{V}$
57 55 1 56 fvmpt ${⊢}{N}\in ℕ\to {F}\left({N}\right)=\sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)$
58 3 57 syl ${⊢}{\phi }\to {F}\left({N}\right)=\sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)$
59 sqrt2re ${⊢}\sqrt{2}\in ℝ$
60 3 nnrpd ${⊢}{\phi }\to {N}\in {ℝ}^{+}$
61 60 rpsqrtcld ${⊢}{\phi }\to \sqrt{{N}}\in {ℝ}^{+}$
62 fveq2 ${⊢}{x}=\sqrt{{N}}\to \mathrm{log}{x}=\mathrm{log}\sqrt{{N}}$
63 id ${⊢}{x}=\sqrt{{N}}\to {x}=\sqrt{{N}}$
64 62 63 oveq12d ${⊢}{x}=\sqrt{{N}}\to \frac{\mathrm{log}{x}}{{x}}=\frac{\mathrm{log}\sqrt{{N}}}{\sqrt{{N}}}$
65 ovex ${⊢}\frac{\mathrm{log}\sqrt{{N}}}{\sqrt{{N}}}\in \mathrm{V}$
66 64 2 65 fvmpt ${⊢}\sqrt{{N}}\in {ℝ}^{+}\to {G}\left(\sqrt{{N}}\right)=\frac{\mathrm{log}\sqrt{{N}}}{\sqrt{{N}}}$
67 61 66 syl ${⊢}{\phi }\to {G}\left(\sqrt{{N}}\right)=\frac{\mathrm{log}\sqrt{{N}}}{\sqrt{{N}}}$
68 61 relogcld ${⊢}{\phi }\to \mathrm{log}\sqrt{{N}}\in ℝ$
69 68 61 rerpdivcld ${⊢}{\phi }\to \frac{\mathrm{log}\sqrt{{N}}}{\sqrt{{N}}}\in ℝ$
70 67 69 eqeltrd ${⊢}{\phi }\to {G}\left(\sqrt{{N}}\right)\in ℝ$
71 remulcl ${⊢}\left(\sqrt{2}\in ℝ\wedge {G}\left(\sqrt{{N}}\right)\in ℝ\right)\to \sqrt{2}{G}\left(\sqrt{{N}}\right)\in ℝ$
72 59 70 71 sylancr ${⊢}{\phi }\to \sqrt{2}{G}\left(\sqrt{{N}}\right)\in ℝ$
73 9re ${⊢}9\in ℝ$
74 4re ${⊢}4\in ℝ$
75 4ne0 ${⊢}4\ne 0$
76 73 74 75 redivcli ${⊢}\frac{9}{4}\in ℝ$
77 60 rphalfcld ${⊢}{\phi }\to \frac{{N}}{2}\in {ℝ}^{+}$
78 fveq2 ${⊢}{x}=\frac{{N}}{2}\to \mathrm{log}{x}=\mathrm{log}\left(\frac{{N}}{2}\right)$
79 id ${⊢}{x}=\frac{{N}}{2}\to {x}=\frac{{N}}{2}$
80 78 79 oveq12d ${⊢}{x}=\frac{{N}}{2}\to \frac{\mathrm{log}{x}}{{x}}=\frac{\mathrm{log}\left(\frac{{N}}{2}\right)}{\frac{{N}}{2}}$
81 ovex ${⊢}\frac{\mathrm{log}\left(\frac{{N}}{2}\right)}{\frac{{N}}{2}}\in \mathrm{V}$
82 80 2 81 fvmpt ${⊢}\frac{{N}}{2}\in {ℝ}^{+}\to {G}\left(\frac{{N}}{2}\right)=\frac{\mathrm{log}\left(\frac{{N}}{2}\right)}{\frac{{N}}{2}}$
83 77 82 syl ${⊢}{\phi }\to {G}\left(\frac{{N}}{2}\right)=\frac{\mathrm{log}\left(\frac{{N}}{2}\right)}{\frac{{N}}{2}}$
84 77 relogcld ${⊢}{\phi }\to \mathrm{log}\left(\frac{{N}}{2}\right)\in ℝ$
85 84 77 rerpdivcld ${⊢}{\phi }\to \frac{\mathrm{log}\left(\frac{{N}}{2}\right)}{\frac{{N}}{2}}\in ℝ$
86 83 85 eqeltrd ${⊢}{\phi }\to {G}\left(\frac{{N}}{2}\right)\in ℝ$
87 remulcl ${⊢}\left(\frac{9}{4}\in ℝ\wedge {G}\left(\frac{{N}}{2}\right)\in ℝ\right)\to \left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)\in ℝ$
88 76 86 87 sylancr ${⊢}{\phi }\to \left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)\in ℝ$
89 72 88 readdcld ${⊢}{\phi }\to \sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)\in ℝ$
90 2rp ${⊢}2\in {ℝ}^{+}$
91 relogcl ${⊢}2\in {ℝ}^{+}\to \mathrm{log}2\in ℝ$
92 90 91 ax-mp ${⊢}\mathrm{log}2\in ℝ$
93 rpmulcl ${⊢}\left(2\in {ℝ}^{+}\wedge {N}\in {ℝ}^{+}\right)\to 2\cdot {N}\in {ℝ}^{+}$
94 90 60 93 sylancr ${⊢}{\phi }\to 2\cdot {N}\in {ℝ}^{+}$
95 94 rpsqrtcld ${⊢}{\phi }\to \sqrt{2\cdot {N}}\in {ℝ}^{+}$
96 rerpdivcl ${⊢}\left(\mathrm{log}2\in ℝ\wedge \sqrt{2\cdot {N}}\in {ℝ}^{+}\right)\to \frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\in ℝ$
97 92 95 96 sylancr ${⊢}{\phi }\to \frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\in ℝ$
98 89 97 readdcld ${⊢}{\phi }\to \sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)\in ℝ$
99 58 98 eqeltrd ${⊢}{\phi }\to {F}\left({N}\right)\in ℝ$
100 92 a1i ${⊢}{\phi }\to \mathrm{log}2\in ℝ$
101 45 simprd ${⊢}{\phi }\to {F}\left(64\right)<\mathrm{log}2$
102 nnrp ${⊢}4\in ℕ\to 4\in {ℝ}^{+}$
103 7 102 ax-mp ${⊢}4\in {ℝ}^{+}$
104 relogcl ${⊢}4\in {ℝ}^{+}\to \mathrm{log}4\in ℝ$
105 103 104 ax-mp ${⊢}\mathrm{log}4\in ℝ$
106 remulcl ${⊢}\left({N}\in ℝ\wedge \mathrm{log}4\in ℝ\right)\to {N}\mathrm{log}4\in ℝ$
107 37 105 106 sylancl ${⊢}{\phi }\to {N}\mathrm{log}4\in ℝ$
108 60 relogcld ${⊢}{\phi }\to \mathrm{log}{N}\in ℝ$
109 107 108 resubcld ${⊢}{\phi }\to {N}\mathrm{log}4-\mathrm{log}{N}\in ℝ$
110 rpre ${⊢}2\cdot {N}\in {ℝ}^{+}\to 2\cdot {N}\in ℝ$
111 rpge0 ${⊢}2\cdot {N}\in {ℝ}^{+}\to 0\le 2\cdot {N}$
112 110 111 resqrtcld ${⊢}2\cdot {N}\in {ℝ}^{+}\to \sqrt{2\cdot {N}}\in ℝ$
113 94 112 syl ${⊢}{\phi }\to \sqrt{2\cdot {N}}\in ℝ$
114 3nn ${⊢}3\in ℕ$
115 nndivre ${⊢}\left(\sqrt{2\cdot {N}}\in ℝ\wedge 3\in ℕ\right)\to \frac{\sqrt{2\cdot {N}}}{3}\in ℝ$
116 113 114 115 sylancl ${⊢}{\phi }\to \frac{\sqrt{2\cdot {N}}}{3}\in ℝ$
117 2re ${⊢}2\in ℝ$
118 readdcl ${⊢}\left(\frac{\sqrt{2\cdot {N}}}{3}\in ℝ\wedge 2\in ℝ\right)\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\in ℝ$
119 116 117 118 sylancl ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\in ℝ$
120 94 relogcld ${⊢}{\phi }\to \mathrm{log}2\cdot {N}\in ℝ$
121 119 120 remulcld ${⊢}{\phi }\to \left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}\in ℝ$
122 remulcl ${⊢}\left(4\in ℝ\wedge {N}\in ℝ\right)\to 4\cdot {N}\in ℝ$
123 74 37 122 sylancr ${⊢}{\phi }\to 4\cdot {N}\in ℝ$
124 nndivre ${⊢}\left(4\cdot {N}\in ℝ\wedge 3\in ℕ\right)\to \frac{4\cdot {N}}{3}\in ℝ$
125 123 114 124 sylancl ${⊢}{\phi }\to \frac{4\cdot {N}}{3}\in ℝ$
126 5re ${⊢}5\in ℝ$
127 resubcl ${⊢}\left(\frac{4\cdot {N}}{3}\in ℝ\wedge 5\in ℝ\right)\to \left(\frac{4\cdot {N}}{3}\right)-5\in ℝ$
128 125 126 127 sylancl ${⊢}{\phi }\to \left(\frac{4\cdot {N}}{3}\right)-5\in ℝ$
129 remulcl ${⊢}\left(\left(\frac{4\cdot {N}}{3}\right)-5\in ℝ\wedge \mathrm{log}2\in ℝ\right)\to \left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2\in ℝ$
130 128 92 129 sylancl ${⊢}{\phi }\to \left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2\in ℝ$
131 121 130 readdcld ${⊢}{\phi }\to \left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2\in ℝ$
132 remulcl ${⊢}\left(\frac{4\cdot {N}}{3}\in ℝ\wedge \mathrm{log}2\in ℝ\right)\to \left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2\in ℝ$
133 125 92 132 sylancl ${⊢}{\phi }\to \left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2\in ℝ$
134 133 108 resubcld ${⊢}{\phi }\to \left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-\mathrm{log}{N}\in ℝ$
135 3 nnzd ${⊢}{\phi }\to {N}\in ℤ$
136 df-5 ${⊢}5=4+1$
137 74 a1i ${⊢}{\phi }\to 4\in ℝ$
138 6nn ${⊢}6\in ℕ$
139 4nn0 ${⊢}4\in {ℕ}_{0}$
140 4lt10 ${⊢}4<10$
141 138 139 139 140 declti ${⊢}4<64$
142 141 a1i ${⊢}{\phi }\to 4<64$
143 137 36 37 142 4 lttrd ${⊢}{\phi }\to 4<{N}$
144 4z ${⊢}4\in ℤ$
145 zltp1le ${⊢}\left(4\in ℤ\wedge {N}\in ℤ\right)\to \left(4<{N}↔4+1\le {N}\right)$
146 144 135 145 sylancr ${⊢}{\phi }\to \left(4<{N}↔4+1\le {N}\right)$
147 143 146 mpbid ${⊢}{\phi }\to 4+1\le {N}$
148 136 147 eqbrtrid ${⊢}{\phi }\to 5\le {N}$
149 5nn ${⊢}5\in ℕ$
150 149 nnzi ${⊢}5\in ℤ$
151 150 eluz1i ${⊢}{N}\in {ℤ}_{\ge 5}↔\left({N}\in ℤ\wedge 5\le {N}\right)$
152 135 148 151 sylanbrc ${⊢}{\phi }\to {N}\in {ℤ}_{\ge 5}$
153 breq2 ${⊢}{p}={q}\to \left({N}<{p}↔{N}<{q}\right)$
154 breq1 ${⊢}{p}={q}\to \left({p}\le 2\cdot {N}↔{q}\le 2\cdot {N}\right)$
155 153 154 anbi12d ${⊢}{p}={q}\to \left(\left({N}<{p}\wedge {p}\le 2\cdot {N}\right)↔\left({N}<{q}\wedge {q}\le 2\cdot {N}\right)\right)$
156 155 cbvrexvw ${⊢}\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\left({N}<{p}\wedge {p}\le 2\cdot {N}\right)↔\exists {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({N}<{q}\wedge {q}\le 2\cdot {N}\right)$
157 5 156 sylnib ${⊢}{\phi }\to ¬\exists {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({N}<{q}\wedge {q}\le 2\cdot {N}\right)$
158 eqid ${⊢}\left({n}\in ℕ⟼if\left({n}\in ℙ,{{n}}^{{n}\mathrm{pCnt}\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)},1\right)\right)=\left({n}\in ℕ⟼if\left({n}\in ℙ,{{n}}^{{n}\mathrm{pCnt}\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)},1\right)\right)$
159 eqid ${⊢}⌊\frac{2\cdot {N}}{3}⌋=⌊\frac{2\cdot {N}}{3}⌋$
160 eqid ${⊢}⌊\sqrt{2\cdot {N}}⌋=⌊\sqrt{2\cdot {N}}⌋$
161 152 157 158 159 160 bposlem6 ${⊢}{\phi }\to \frac{{4}^{{N}}}{{N}}<{2\cdot {N}}^{\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2}{2}^{\left(\frac{4\cdot {N}}{3}\right)-5}$
162 reexplog ${⊢}\left(4\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to {4}^{{N}}={\mathrm{e}}^{{N}\mathrm{log}4}$
163 103 135 162 sylancr ${⊢}{\phi }\to {4}^{{N}}={\mathrm{e}}^{{N}\mathrm{log}4}$
164 60 reeflogd ${⊢}{\phi }\to {\mathrm{e}}^{\mathrm{log}{N}}={N}$
165 164 eqcomd ${⊢}{\phi }\to {N}={\mathrm{e}}^{\mathrm{log}{N}}$
166 163 165 oveq12d ${⊢}{\phi }\to \frac{{4}^{{N}}}{{N}}=\frac{{\mathrm{e}}^{{N}\mathrm{log}4}}{{\mathrm{e}}^{\mathrm{log}{N}}}$
167 107 recnd ${⊢}{\phi }\to {N}\mathrm{log}4\in ℂ$
168 108 recnd ${⊢}{\phi }\to \mathrm{log}{N}\in ℂ$
169 efsub ${⊢}\left({N}\mathrm{log}4\in ℂ\wedge \mathrm{log}{N}\in ℂ\right)\to {\mathrm{e}}^{{N}\mathrm{log}4-\mathrm{log}{N}}=\frac{{\mathrm{e}}^{{N}\mathrm{log}4}}{{\mathrm{e}}^{\mathrm{log}{N}}}$
170 167 168 169 syl2anc ${⊢}{\phi }\to {\mathrm{e}}^{{N}\mathrm{log}4-\mathrm{log}{N}}=\frac{{\mathrm{e}}^{{N}\mathrm{log}4}}{{\mathrm{e}}^{\mathrm{log}{N}}}$
171 166 170 eqtr4d ${⊢}{\phi }\to \frac{{4}^{{N}}}{{N}}={\mathrm{e}}^{{N}\mathrm{log}4-\mathrm{log}{N}}$
172 94 rpcnd ${⊢}{\phi }\to 2\cdot {N}\in ℂ$
173 94 rpne0d ${⊢}{\phi }\to 2\cdot {N}\ne 0$
174 119 recnd ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\in ℂ$
175 172 173 174 cxpefd ${⊢}{\phi }\to {2\cdot {N}}^{\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2}={\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}}$
176 2cn ${⊢}2\in ℂ$
177 2ne0 ${⊢}2\ne 0$
178 128 recnd ${⊢}{\phi }\to \left(\frac{4\cdot {N}}{3}\right)-5\in ℂ$
179 cxpef ${⊢}\left(2\in ℂ\wedge 2\ne 0\wedge \left(\frac{4\cdot {N}}{3}\right)-5\in ℂ\right)\to {2}^{\left(\frac{4\cdot {N}}{3}\right)-5}={\mathrm{e}}^{\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2}$
180 176 177 178 179 mp3an12i ${⊢}{\phi }\to {2}^{\left(\frac{4\cdot {N}}{3}\right)-5}={\mathrm{e}}^{\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2}$
181 175 180 oveq12d ${⊢}{\phi }\to {2\cdot {N}}^{\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2}{2}^{\left(\frac{4\cdot {N}}{3}\right)-5}={\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}}{\mathrm{e}}^{\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2}$
182 121 recnd ${⊢}{\phi }\to \left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}\in ℂ$
183 130 recnd ${⊢}{\phi }\to \left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2\in ℂ$
184 efadd ${⊢}\left(\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}\in ℂ\wedge \left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2\in ℂ\right)\to {\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2}={\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}}{\mathrm{e}}^{\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2}$
185 182 183 184 syl2anc ${⊢}{\phi }\to {\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2}={\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}}{\mathrm{e}}^{\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2}$
186 181 185 eqtr4d ${⊢}{\phi }\to {2\cdot {N}}^{\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2}{2}^{\left(\frac{4\cdot {N}}{3}\right)-5}={\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2}$
187 161 171 186 3brtr3d ${⊢}{\phi }\to {\mathrm{e}}^{{N}\mathrm{log}4-\mathrm{log}{N}}<{\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2}$
188 eflt ${⊢}\left({N}\mathrm{log}4-\mathrm{log}{N}\in ℝ\wedge \left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2\in ℝ\right)\to \left({N}\mathrm{log}4-\mathrm{log}{N}<\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2↔{\mathrm{e}}^{{N}\mathrm{log}4-\mathrm{log}{N}}<{\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2}\right)$
189 109 131 188 syl2anc ${⊢}{\phi }\to \left({N}\mathrm{log}4-\mathrm{log}{N}<\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2↔{\mathrm{e}}^{{N}\mathrm{log}4-\mathrm{log}{N}}<{\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2}\right)$
190 187 189 mpbird ${⊢}{\phi }\to {N}\mathrm{log}4-\mathrm{log}{N}<\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2$
191 109 131 134 190 ltsub1dd ${⊢}{\phi }\to {N}\mathrm{log}4-\mathrm{log}{N}-\left(\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-\mathrm{log}{N}\right)<\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2-\left(\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-\mathrm{log}{N}\right)$
192 37 recnd ${⊢}{\phi }\to {N}\in ℂ$
193 mulcom ${⊢}\left(2\in ℂ\wedge {N}\in ℂ\right)\to 2\cdot {N}={N}\cdot 2$
194 176 192 193 sylancr ${⊢}{\phi }\to 2\cdot {N}={N}\cdot 2$
195 194 oveq1d ${⊢}{\phi }\to 2\cdot {N}\mathrm{log}2={N}\cdot 2\mathrm{log}2$
196 92 recni ${⊢}\mathrm{log}2\in ℂ$
197 mulass ${⊢}\left({N}\in ℂ\wedge 2\in ℂ\wedge \mathrm{log}2\in ℂ\right)\to {N}\cdot 2\mathrm{log}2={N}2\mathrm{log}2$
198 176 196 197 mp3an23 ${⊢}{N}\in ℂ\to {N}\cdot 2\mathrm{log}2={N}2\mathrm{log}2$
199 192 198 syl ${⊢}{\phi }\to {N}\cdot 2\mathrm{log}2={N}2\mathrm{log}2$
200 196 2timesi ${⊢}2\mathrm{log}2=\mathrm{log}2+\mathrm{log}2$
201 relogmul ${⊢}\left(2\in {ℝ}^{+}\wedge 2\in {ℝ}^{+}\right)\to \mathrm{log}2\cdot 2=\mathrm{log}2+\mathrm{log}2$
202 90 90 201 mp2an ${⊢}\mathrm{log}2\cdot 2=\mathrm{log}2+\mathrm{log}2$
203 2t2e4 ${⊢}2\cdot 2=4$
204 203 fveq2i ${⊢}\mathrm{log}2\cdot 2=\mathrm{log}4$
205 200 202 204 3eqtr2i ${⊢}2\mathrm{log}2=\mathrm{log}4$
206 205 oveq2i ${⊢}{N}2\mathrm{log}2={N}\mathrm{log}4$
207 199 206 syl6eq ${⊢}{\phi }\to {N}\cdot 2\mathrm{log}2={N}\mathrm{log}4$
208 195 207 eqtrd ${⊢}{\phi }\to 2\cdot {N}\mathrm{log}2={N}\mathrm{log}4$
209 208 oveq1d ${⊢}{\phi }\to 2\cdot {N}\mathrm{log}2-\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2={N}\mathrm{log}4-\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2$
210 125 recnd ${⊢}{\phi }\to \frac{4\cdot {N}}{3}\in ℂ$
211 3rp ${⊢}3\in {ℝ}^{+}$
212 rpdivcl ${⊢}\left(2\cdot {N}\in {ℝ}^{+}\wedge 3\in {ℝ}^{+}\right)\to \frac{2\cdot {N}}{3}\in {ℝ}^{+}$
213 94 211 212 sylancl ${⊢}{\phi }\to \frac{2\cdot {N}}{3}\in {ℝ}^{+}$
214 213 rpcnd ${⊢}{\phi }\to \frac{2\cdot {N}}{3}\in ℂ$
215 4p2e6 ${⊢}4+2=6$
216 215 oveq1i ${⊢}\left(4+2\right)\cdot {N}=6\cdot {N}$
217 4cn ${⊢}4\in ℂ$
218 adddir ${⊢}\left(4\in ℂ\wedge 2\in ℂ\wedge {N}\in ℂ\right)\to \left(4+2\right)\cdot {N}=4\cdot {N}+2\cdot {N}$
219 217 176 192 218 mp3an12i ${⊢}{\phi }\to \left(4+2\right)\cdot {N}=4\cdot {N}+2\cdot {N}$
220 216 219 syl5eqr ${⊢}{\phi }\to 6\cdot {N}=4\cdot {N}+2\cdot {N}$
221 220 oveq1d ${⊢}{\phi }\to \frac{6\cdot {N}}{3}=\frac{4\cdot {N}+2\cdot {N}}{3}$
222 6cn ${⊢}6\in ℂ$
223 3cn ${⊢}3\in ℂ$
224 3ne0 ${⊢}3\ne 0$
225 223 224 pm3.2i ${⊢}\left(3\in ℂ\wedge 3\ne 0\right)$
226 div23 ${⊢}\left(6\in ℂ\wedge {N}\in ℂ\wedge \left(3\in ℂ\wedge 3\ne 0\right)\right)\to \frac{6\cdot {N}}{3}=\left(\frac{6}{3}\right)\cdot {N}$
227 222 225 226 mp3an13 ${⊢}{N}\in ℂ\to \frac{6\cdot {N}}{3}=\left(\frac{6}{3}\right)\cdot {N}$
228 192 227 syl ${⊢}{\phi }\to \frac{6\cdot {N}}{3}=\left(\frac{6}{3}\right)\cdot {N}$
229 3t2e6 ${⊢}3\cdot 2=6$
230 229 oveq1i ${⊢}\frac{3\cdot 2}{3}=\frac{6}{3}$
231 176 223 224 divcan3i ${⊢}\frac{3\cdot 2}{3}=2$
232 230 231 eqtr3i ${⊢}\frac{6}{3}=2$
233 232 oveq1i ${⊢}\left(\frac{6}{3}\right)\cdot {N}=2\cdot {N}$
234 228 233 syl6eq ${⊢}{\phi }\to \frac{6\cdot {N}}{3}=2\cdot {N}$
235 123 recnd ${⊢}{\phi }\to 4\cdot {N}\in ℂ$
236 remulcl ${⊢}\left(2\in ℝ\wedge {N}\in ℝ\right)\to 2\cdot {N}\in ℝ$
237 117 37 236 sylancr ${⊢}{\phi }\to 2\cdot {N}\in ℝ$
238 237 recnd ${⊢}{\phi }\to 2\cdot {N}\in ℂ$
239 divdir ${⊢}\left(4\cdot {N}\in ℂ\wedge 2\cdot {N}\in ℂ\wedge \left(3\in ℂ\wedge 3\ne 0\right)\right)\to \frac{4\cdot {N}+2\cdot {N}}{3}=\left(\frac{4\cdot {N}}{3}\right)+\left(\frac{2\cdot {N}}{3}\right)$
240 225 239 mp3an3 ${⊢}\left(4\cdot {N}\in ℂ\wedge 2\cdot {N}\in ℂ\right)\to \frac{4\cdot {N}+2\cdot {N}}{3}=\left(\frac{4\cdot {N}}{3}\right)+\left(\frac{2\cdot {N}}{3}\right)$
241 235 238 240 syl2anc ${⊢}{\phi }\to \frac{4\cdot {N}+2\cdot {N}}{3}=\left(\frac{4\cdot {N}}{3}\right)+\left(\frac{2\cdot {N}}{3}\right)$
242 221 234 241 3eqtr3d ${⊢}{\phi }\to 2\cdot {N}=\left(\frac{4\cdot {N}}{3}\right)+\left(\frac{2\cdot {N}}{3}\right)$
243 210 214 242 mvrladdd ${⊢}{\phi }\to 2\cdot {N}-\left(\frac{4\cdot {N}}{3}\right)=\frac{2\cdot {N}}{3}$
244 243 oveq1d ${⊢}{\phi }\to \left(2\cdot {N}-\left(\frac{4\cdot {N}}{3}\right)\right)\mathrm{log}2=\left(\frac{2\cdot {N}}{3}\right)\mathrm{log}2$
245 100 recnd ${⊢}{\phi }\to \mathrm{log}2\in ℂ$
246 238 210 245 subdird ${⊢}{\phi }\to \left(2\cdot {N}-\left(\frac{4\cdot {N}}{3}\right)\right)\mathrm{log}2=2\cdot {N}\mathrm{log}2-\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2$
247 244 246 eqtr3d ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\mathrm{log}2=2\cdot {N}\mathrm{log}2-\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2$
248 133 recnd ${⊢}{\phi }\to \left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2\in ℂ$
249 167 248 168 nnncan2d ${⊢}{\phi }\to {N}\mathrm{log}4-\mathrm{log}{N}-\left(\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-\mathrm{log}{N}\right)={N}\mathrm{log}4-\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2$
250 209 247 249 3eqtr4d ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\mathrm{log}2={N}\mathrm{log}4-\mathrm{log}{N}-\left(\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-\mathrm{log}{N}\right)$
251 116 recnd ${⊢}{\phi }\to \frac{\sqrt{2\cdot {N}}}{3}\in ℂ$
252 176 a1i ${⊢}{\phi }\to 2\in ℂ$
253 120 recnd ${⊢}{\phi }\to \mathrm{log}2\cdot {N}\in ℂ$
254 251 252 253 adddird ${⊢}{\phi }\to \left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}+2\mathrm{log}2\cdot {N}$
255 relogmul ${⊢}\left(2\in {ℝ}^{+}\wedge {N}\in {ℝ}^{+}\right)\to \mathrm{log}2\cdot {N}=\mathrm{log}2+\mathrm{log}{N}$
256 90 60 255 sylancr ${⊢}{\phi }\to \mathrm{log}2\cdot {N}=\mathrm{log}2+\mathrm{log}{N}$
257 256 oveq2d ${⊢}{\phi }\to 2\mathrm{log}2\cdot {N}=2\left(\mathrm{log}2+\mathrm{log}{N}\right)$
258 252 245 168 adddid ${⊢}{\phi }\to 2\left(\mathrm{log}2+\mathrm{log}{N}\right)=2\mathrm{log}2+2\mathrm{log}{N}$
259 257 258 eqtrd ${⊢}{\phi }\to 2\mathrm{log}2\cdot {N}=2\mathrm{log}2+2\mathrm{log}{N}$
260 259 oveq2d ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}+2\mathrm{log}2\cdot {N}=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}+2\mathrm{log}2+2\mathrm{log}{N}$
261 254 260 eqtrd ${⊢}{\phi }\to \left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}+2\mathrm{log}2+2\mathrm{log}{N}$
262 5cn ${⊢}5\in ℂ$
263 262 a1i ${⊢}{\phi }\to 5\in ℂ$
264 210 263 245 subdird ${⊢}{\phi }\to \left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2=\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-5\mathrm{log}2$
265 264 oveq1d ${⊢}{\phi }\to \left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2-\left(\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-\mathrm{log}{N}\right)=\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-5\mathrm{log}2-\left(\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-\mathrm{log}{N}\right)$
266 262 196 mulcli ${⊢}5\mathrm{log}2\in ℂ$
267 266 a1i ${⊢}{\phi }\to 5\mathrm{log}2\in ℂ$
268 248 267 168 nnncan1d ${⊢}{\phi }\to \left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-5\mathrm{log}2-\left(\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-\mathrm{log}{N}\right)=\mathrm{log}{N}-5\mathrm{log}2$
269 265 268 eqtrd ${⊢}{\phi }\to \left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2-\left(\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-\mathrm{log}{N}\right)=\mathrm{log}{N}-5\mathrm{log}2$
270 261 269 oveq12d ${⊢}{\phi }\to \left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2-\left(\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-\mathrm{log}{N}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}+\left(2\mathrm{log}2+2\mathrm{log}{N}\right)+\left(\mathrm{log}{N}-5\mathrm{log}2\right)$
271 134 recnd ${⊢}{\phi }\to \left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-\mathrm{log}{N}\in ℂ$
272 182 183 271 addsubassd ${⊢}{\phi }\to \left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2-\left(\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-\mathrm{log}{N}\right)=\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2-\left(\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-\mathrm{log}{N}\right)$
273 262 223 196 subdiri ${⊢}\left(5-3\right)\mathrm{log}2=5\mathrm{log}2-3\mathrm{log}2$
274 3p2e5 ${⊢}3+2=5$
275 274 oveq1i ${⊢}3+2-3=5-3$
276 pncan2 ${⊢}\left(3\in ℂ\wedge 2\in ℂ\right)\to 3+2-3=2$
277 223 176 276 mp2an ${⊢}3+2-3=2$
278 275 277 eqtr3i ${⊢}5-3=2$
279 278 oveq1i ${⊢}\left(5-3\right)\mathrm{log}2=2\mathrm{log}2$
280 273 279 eqtr3i ${⊢}5\mathrm{log}2-3\mathrm{log}2=2\mathrm{log}2$
281 280 a1i ${⊢}{\phi }\to 5\mathrm{log}2-3\mathrm{log}2=2\mathrm{log}2$
282 mulcl ${⊢}\left(2\in ℂ\wedge \mathrm{log}{N}\in ℂ\right)\to 2\mathrm{log}{N}\in ℂ$
283 176 168 282 sylancr ${⊢}{\phi }\to 2\mathrm{log}{N}\in ℂ$
284 df-3 ${⊢}3=2+1$
285 284 oveq1i ${⊢}3\mathrm{log}{N}=\left(2+1\right)\mathrm{log}{N}$
286 1cnd ${⊢}{\phi }\to 1\in ℂ$
287 252 286 168 adddird ${⊢}{\phi }\to \left(2+1\right)\mathrm{log}{N}=2\mathrm{log}{N}+1\mathrm{log}{N}$
288 285 287 syl5eq ${⊢}{\phi }\to 3\mathrm{log}{N}=2\mathrm{log}{N}+1\mathrm{log}{N}$
289 168 mulid2d ${⊢}{\phi }\to 1\mathrm{log}{N}=\mathrm{log}{N}$
290 289 oveq2d ${⊢}{\phi }\to 2\mathrm{log}{N}+1\mathrm{log}{N}=2\mathrm{log}{N}+\mathrm{log}{N}$
291 288 290 eqtrd ${⊢}{\phi }\to 3\mathrm{log}{N}=2\mathrm{log}{N}+\mathrm{log}{N}$
292 291 oveq1d ${⊢}{\phi }\to 3\mathrm{log}{N}-5\mathrm{log}2=2\mathrm{log}{N}+\mathrm{log}{N}-5\mathrm{log}2$
293 283 168 267 292 assraddsubd ${⊢}{\phi }\to 3\mathrm{log}{N}-5\mathrm{log}2=2\mathrm{log}{N}+\mathrm{log}{N}-5\mathrm{log}2$
294 281 293 oveq12d ${⊢}{\phi }\to \left(5\mathrm{log}2-3\mathrm{log}2\right)+3\mathrm{log}{N}-5\mathrm{log}2=2\mathrm{log}2+2\mathrm{log}{N}+\left(\mathrm{log}{N}-5\mathrm{log}2\right)$
295 relogdiv ${⊢}\left({N}\in {ℝ}^{+}\wedge 2\in {ℝ}^{+}\right)\to \mathrm{log}\left(\frac{{N}}{2}\right)=\mathrm{log}{N}-\mathrm{log}2$
296 60 90 295 sylancl ${⊢}{\phi }\to \mathrm{log}\left(\frac{{N}}{2}\right)=\mathrm{log}{N}-\mathrm{log}2$
297 296 oveq2d ${⊢}{\phi }\to 3\mathrm{log}\left(\frac{{N}}{2}\right)=3\left(\mathrm{log}{N}-\mathrm{log}2\right)$
298 subdi ${⊢}\left(3\in ℂ\wedge \mathrm{log}{N}\in ℂ\wedge \mathrm{log}2\in ℂ\right)\to 3\left(\mathrm{log}{N}-\mathrm{log}2\right)=3\mathrm{log}{N}-3\mathrm{log}2$
299 223 196 298 mp3an13 ${⊢}\mathrm{log}{N}\in ℂ\to 3\left(\mathrm{log}{N}-\mathrm{log}2\right)=3\mathrm{log}{N}-3\mathrm{log}2$
300 168 299 syl ${⊢}{\phi }\to 3\left(\mathrm{log}{N}-\mathrm{log}2\right)=3\mathrm{log}{N}-3\mathrm{log}2$
301 297 300 eqtrd ${⊢}{\phi }\to 3\mathrm{log}\left(\frac{{N}}{2}\right)=3\mathrm{log}{N}-3\mathrm{log}2$
302 div23 ${⊢}\left(2\in ℂ\wedge {N}\in ℂ\wedge \left(3\in ℂ\wedge 3\ne 0\right)\right)\to \frac{2\cdot {N}}{3}=\left(\frac{2}{3}\right)\cdot {N}$
303 176 225 302 mp3an13 ${⊢}{N}\in ℂ\to \frac{2\cdot {N}}{3}=\left(\frac{2}{3}\right)\cdot {N}$
304 192 303 syl ${⊢}{\phi }\to \frac{2\cdot {N}}{3}=\left(\frac{2}{3}\right)\cdot {N}$
305 223 176 223 176 177 177 divmuldivi ${⊢}\left(\frac{3}{2}\right)\left(\frac{3}{2}\right)=\frac{3\cdot 3}{2\cdot 2}$
306 3t3e9 ${⊢}3\cdot 3=9$
307 306 203 oveq12i ${⊢}\frac{3\cdot 3}{2\cdot 2}=\frac{9}{4}$
308 305 307 eqtr2i ${⊢}\frac{9}{4}=\left(\frac{3}{2}\right)\left(\frac{3}{2}\right)$
309 308 a1i ${⊢}{\phi }\to \frac{9}{4}=\left(\frac{3}{2}\right)\left(\frac{3}{2}\right)$
310 304 309 oveq12d ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right)=\left(\frac{2}{3}\right)\cdot {N}\left(\frac{3}{2}\right)\left(\frac{3}{2}\right)$
311 176 223 224 divcli ${⊢}\frac{2}{3}\in ℂ$
312 223 176 177 divcli ${⊢}\frac{3}{2}\in ℂ$
313 mul4 ${⊢}\left(\left(\frac{2}{3}\in ℂ\wedge {N}\in ℂ\right)\wedge \left(\frac{3}{2}\in ℂ\wedge \frac{3}{2}\in ℂ\right)\right)\to \left(\frac{2}{3}\right)\cdot {N}\left(\frac{3}{2}\right)\left(\frac{3}{2}\right)=\left(\frac{2}{3}\right)\left(\frac{3}{2}\right){N}\left(\frac{3}{2}\right)$
314 312 312 313 mpanr12 ${⊢}\left(\frac{2}{3}\in ℂ\wedge {N}\in ℂ\right)\to \left(\frac{2}{3}\right)\cdot {N}\left(\frac{3}{2}\right)\left(\frac{3}{2}\right)=\left(\frac{2}{3}\right)\left(\frac{3}{2}\right){N}\left(\frac{3}{2}\right)$
315 311 192 314 sylancr ${⊢}{\phi }\to \left(\frac{2}{3}\right)\cdot {N}\left(\frac{3}{2}\right)\left(\frac{3}{2}\right)=\left(\frac{2}{3}\right)\left(\frac{3}{2}\right){N}\left(\frac{3}{2}\right)$
316 divcan6 ${⊢}\left(\left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(3\in ℂ\wedge 3\ne 0\right)\right)\to \left(\frac{2}{3}\right)\left(\frac{3}{2}\right)=1$
317 176 177 223 224 316 mp4an ${⊢}\left(\frac{2}{3}\right)\left(\frac{3}{2}\right)=1$
318 317 oveq1i ${⊢}\left(\frac{2}{3}\right)\left(\frac{3}{2}\right){N}\left(\frac{3}{2}\right)=1{N}\left(\frac{3}{2}\right)$
319 mulcl ${⊢}\left({N}\in ℂ\wedge \frac{3}{2}\in ℂ\right)\to {N}\left(\frac{3}{2}\right)\in ℂ$
320 192 312 319 sylancl ${⊢}{\phi }\to {N}\left(\frac{3}{2}\right)\in ℂ$
321 320 mulid2d ${⊢}{\phi }\to 1{N}\left(\frac{3}{2}\right)={N}\left(\frac{3}{2}\right)$
322 318 321 syl5eq ${⊢}{\phi }\to \left(\frac{2}{3}\right)\left(\frac{3}{2}\right){N}\left(\frac{3}{2}\right)={N}\left(\frac{3}{2}\right)$
323 2cnne0 ${⊢}\left(2\in ℂ\wedge 2\ne 0\right)$
324 div12 ${⊢}\left({N}\in ℂ\wedge 3\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to {N}\left(\frac{3}{2}\right)=3\left(\frac{{N}}{2}\right)$
325 223 323 324 mp3an23 ${⊢}{N}\in ℂ\to {N}\left(\frac{3}{2}\right)=3\left(\frac{{N}}{2}\right)$
326 192 325 syl ${⊢}{\phi }\to {N}\left(\frac{3}{2}\right)=3\left(\frac{{N}}{2}\right)$
327 322 326 eqtrd ${⊢}{\phi }\to \left(\frac{2}{3}\right)\left(\frac{3}{2}\right){N}\left(\frac{3}{2}\right)=3\left(\frac{{N}}{2}\right)$
328 310 315 327 3eqtrd ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right)=3\left(\frac{{N}}{2}\right)$
329 328 83 oveq12d ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)=3\left(\frac{{N}}{2}\right)\left(\frac{\mathrm{log}\left(\frac{{N}}{2}\right)}{\frac{{N}}{2}}\right)$
330 76 recni ${⊢}\frac{9}{4}\in ℂ$
331 330 a1i ${⊢}{\phi }\to \frac{9}{4}\in ℂ$
332 86 recnd ${⊢}{\phi }\to {G}\left(\frac{{N}}{2}\right)\in ℂ$
333 214 331 332 mulassd ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)=\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)$
334 223 a1i ${⊢}{\phi }\to 3\in ℂ$
335 77 rpcnd ${⊢}{\phi }\to \frac{{N}}{2}\in ℂ$
336 84 recnd ${⊢}{\phi }\to \mathrm{log}\left(\frac{{N}}{2}\right)\in ℂ$
337 77 rpne0d ${⊢}{\phi }\to \frac{{N}}{2}\ne 0$
338 336 335 337 divcld ${⊢}{\phi }\to \frac{\mathrm{log}\left(\frac{{N}}{2}\right)}{\frac{{N}}{2}}\in ℂ$
339 334 335 338 mulassd ${⊢}{\phi }\to 3\left(\frac{{N}}{2}\right)\left(\frac{\mathrm{log}\left(\frac{{N}}{2}\right)}{\frac{{N}}{2}}\right)=3\left(\frac{{N}}{2}\right)\left(\frac{\mathrm{log}\left(\frac{{N}}{2}\right)}{\frac{{N}}{2}}\right)$
340 336 335 337 divcan2d ${⊢}{\phi }\to \left(\frac{{N}}{2}\right)\left(\frac{\mathrm{log}\left(\frac{{N}}{2}\right)}{\frac{{N}}{2}}\right)=\mathrm{log}\left(\frac{{N}}{2}\right)$
341 340 oveq2d ${⊢}{\phi }\to 3\left(\frac{{N}}{2}\right)\left(\frac{\mathrm{log}\left(\frac{{N}}{2}\right)}{\frac{{N}}{2}}\right)=3\mathrm{log}\left(\frac{{N}}{2}\right)$
342 339 341 eqtrd ${⊢}{\phi }\to 3\left(\frac{{N}}{2}\right)\left(\frac{\mathrm{log}\left(\frac{{N}}{2}\right)}{\frac{{N}}{2}}\right)=3\mathrm{log}\left(\frac{{N}}{2}\right)$
343 329 333 342 3eqtr3d ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)=3\mathrm{log}\left(\frac{{N}}{2}\right)$
344 223 196 mulcli ${⊢}3\mathrm{log}2\in ℂ$
345 344 a1i ${⊢}{\phi }\to 3\mathrm{log}2\in ℂ$
346 mulcl ${⊢}\left(3\in ℂ\wedge \mathrm{log}{N}\in ℂ\right)\to 3\mathrm{log}{N}\in ℂ$
347 223 168 346 sylancr ${⊢}{\phi }\to 3\mathrm{log}{N}\in ℂ$
348 267 345 347 npncan3d ${⊢}{\phi }\to \left(5\mathrm{log}2-3\mathrm{log}2\right)+3\mathrm{log}{N}-5\mathrm{log}2=3\mathrm{log}{N}-3\mathrm{log}2$
349 301 343 348 3eqtr4d ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)=\left(5\mathrm{log}2-3\mathrm{log}2\right)+3\mathrm{log}{N}-5\mathrm{log}2$
350 117 92 remulcli ${⊢}2\mathrm{log}2\in ℝ$
351 350 recni ${⊢}2\mathrm{log}2\in ℂ$
352 351 a1i ${⊢}{\phi }\to 2\mathrm{log}2\in ℂ$
353 subcl ${⊢}\left(\mathrm{log}{N}\in ℂ\wedge 5\mathrm{log}2\in ℂ\right)\to \mathrm{log}{N}-5\mathrm{log}2\in ℂ$
354 168 266 353 sylancl ${⊢}{\phi }\to \mathrm{log}{N}-5\mathrm{log}2\in ℂ$
355 352 283 354 addassd ${⊢}{\phi }\to 2\mathrm{log}2+2\mathrm{log}{N}+\left(\mathrm{log}{N}-5\mathrm{log}2\right)=2\mathrm{log}2+2\mathrm{log}{N}+\left(\mathrm{log}{N}-5\mathrm{log}2\right)$
356 294 349 355 3eqtr4d ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)=2\mathrm{log}2+2\mathrm{log}{N}+\left(\mathrm{log}{N}-5\mathrm{log}2\right)$
357 356 oveq2d ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}+\left(2\mathrm{log}2+2\mathrm{log}{N}\right)+\left(\mathrm{log}{N}-5\mathrm{log}2\right)$
358 mulcl ${⊢}\left(\frac{\sqrt{2\cdot {N}}}{3}\in ℂ\wedge \mathrm{log}2\in ℂ\right)\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\in ℂ$
359 251 196 358 sylancl ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\in ℂ$
360 251 168 mulcld ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}\in ℂ$
361 88 recnd ${⊢}{\phi }\to \left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)\in ℂ$
362 214 361 mulcld ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)\in ℂ$
363 359 360 362 addassd ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2+\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2+\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)$
364 256 oveq2d ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\left(\mathrm{log}2+\mathrm{log}{N}\right)$
365 251 245 168 adddid ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\left(\mathrm{log}2+\mathrm{log}{N}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2+\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}$
366 364 365 eqtrd ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2+\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}$
367 366 oveq1d ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2+\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)$
368 58 oveq2d ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right){F}\left({N}\right)=\left(\frac{2\cdot {N}}{3}\right)\left(\sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)\right)$
369 89 recnd ${⊢}{\phi }\to \sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)\in ℂ$
370 97 recnd ${⊢}{\phi }\to \frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\in ℂ$
371 214 369 370 adddid ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\left(\sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)\right)=\left(\frac{2\cdot {N}}{3}\right)\left(\sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)\right)+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)$
372 368 371 eqtrd ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right){F}\left({N}\right)=\left(\frac{2\cdot {N}}{3}\right)\left(\sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)\right)+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)$
373 72 recnd ${⊢}{\phi }\to \sqrt{2}{G}\left(\sqrt{{N}}\right)\in ℂ$
374 214 373 361 adddid ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\left(\sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)\right)=\left(\frac{2\cdot {N}}{3}\right)\sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)$
375 94 rpge0d ${⊢}{\phi }\to 0\le 2\cdot {N}$
376 remsqsqrt ${⊢}\left(2\cdot {N}\in ℝ\wedge 0\le 2\cdot {N}\right)\to \sqrt{2\cdot {N}}\sqrt{2\cdot {N}}=2\cdot {N}$
377 237 375 376 syl2anc ${⊢}{\phi }\to \sqrt{2\cdot {N}}\sqrt{2\cdot {N}}=2\cdot {N}$
378 377 oveq1d ${⊢}{\phi }\to \frac{\sqrt{2\cdot {N}}\sqrt{2\cdot {N}}}{3}=\frac{2\cdot {N}}{3}$
379 113 recnd ${⊢}{\phi }\to \sqrt{2\cdot {N}}\in ℂ$
380 224 a1i ${⊢}{\phi }\to 3\ne 0$
381 379 379 334 380 div23d ${⊢}{\phi }\to \frac{\sqrt{2\cdot {N}}\sqrt{2\cdot {N}}}{3}=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\sqrt{2\cdot {N}}$
382 378 381 eqtr3d ${⊢}{\phi }\to \frac{2\cdot {N}}{3}=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\sqrt{2\cdot {N}}$
383 382 oveq1d ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\sqrt{2}{G}\left(\sqrt{{N}}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\sqrt{2\cdot {N}}\sqrt{2}{G}\left(\sqrt{{N}}\right)$
384 251 379 373 mulassd ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\sqrt{2\cdot {N}}\sqrt{2}{G}\left(\sqrt{{N}}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\sqrt{2\cdot {N}}\sqrt{2}{G}\left(\sqrt{{N}}\right)$
385 0le2 ${⊢}0\le 2$
386 117 385 pm3.2i ${⊢}\left(2\in ℝ\wedge 0\le 2\right)$
387 60 rprege0d ${⊢}{\phi }\to \left({N}\in ℝ\wedge 0\le {N}\right)$
388 sqrtmul ${⊢}\left(\left(2\in ℝ\wedge 0\le 2\right)\wedge \left({N}\in ℝ\wedge 0\le {N}\right)\right)\to \sqrt{2\cdot {N}}=\sqrt{2}\sqrt{{N}}$
389 386 387 388 sylancr ${⊢}{\phi }\to \sqrt{2\cdot {N}}=\sqrt{2}\sqrt{{N}}$
390 389 oveq1d ${⊢}{\phi }\to \sqrt{2\cdot {N}}\sqrt{2}{G}\left(\sqrt{{N}}\right)=\sqrt{2}\sqrt{{N}}\sqrt{2}{G}\left(\sqrt{{N}}\right)$
391 59 recni ${⊢}\sqrt{2}\in ℂ$
392 391 a1i ${⊢}{\phi }\to \sqrt{2}\in ℂ$
393 61 rpcnd ${⊢}{\phi }\to \sqrt{{N}}\in ℂ$
394 70 recnd ${⊢}{\phi }\to {G}\left(\sqrt{{N}}\right)\in ℂ$
395 392 393 392 394 mul4d ${⊢}{\phi }\to \sqrt{2}\sqrt{{N}}\sqrt{2}{G}\left(\sqrt{{N}}\right)=\sqrt{2}\sqrt{2}\sqrt{{N}}{G}\left(\sqrt{{N}}\right)$
396 remsqsqrt ${⊢}\left(2\in ℝ\wedge 0\le 2\right)\to \sqrt{2}\sqrt{2}=2$
397 117 385 396 mp2an ${⊢}\sqrt{2}\sqrt{2}=2$
398 397 a1i ${⊢}{\phi }\to \sqrt{2}\sqrt{2}=2$
399 67 oveq2d ${⊢}{\phi }\to \sqrt{{N}}{G}\left(\sqrt{{N}}\right)=\sqrt{{N}}\left(\frac{\mathrm{log}\sqrt{{N}}}{\sqrt{{N}}}\right)$
400 68 recnd ${⊢}{\phi }\to \mathrm{log}\sqrt{{N}}\in ℂ$
401 61 rpne0d ${⊢}{\phi }\to \sqrt{{N}}\ne 0$
402 400 393 401 divcan2d ${⊢}{\phi }\to \sqrt{{N}}\left(\frac{\mathrm{log}\sqrt{{N}}}{\sqrt{{N}}}\right)=\mathrm{log}\sqrt{{N}}$
403 399 402 eqtrd ${⊢}{\phi }\to \sqrt{{N}}{G}\left(\sqrt{{N}}\right)=\mathrm{log}\sqrt{{N}}$
404 398 403 oveq12d ${⊢}{\phi }\to \sqrt{2}\sqrt{2}\sqrt{{N}}{G}\left(\sqrt{{N}}\right)=2\mathrm{log}\sqrt{{N}}$
405 400 2timesd ${⊢}{\phi }\to 2\mathrm{log}\sqrt{{N}}=\mathrm{log}\sqrt{{N}}+\mathrm{log}\sqrt{{N}}$
406 61 61 relogmuld ${⊢}{\phi }\to \mathrm{log}\sqrt{{N}}\sqrt{{N}}=\mathrm{log}\sqrt{{N}}+\mathrm{log}\sqrt{{N}}$
407 remsqsqrt ${⊢}\left({N}\in ℝ\wedge 0\le {N}\right)\to \sqrt{{N}}\sqrt{{N}}={N}$
408 387 407 syl ${⊢}{\phi }\to \sqrt{{N}}\sqrt{{N}}={N}$
409 408 fveq2d ${⊢}{\phi }\to \mathrm{log}\sqrt{{N}}\sqrt{{N}}=\mathrm{log}{N}$
410 406 409 eqtr3d ${⊢}{\phi }\to \mathrm{log}\sqrt{{N}}+\mathrm{log}\sqrt{{N}}=\mathrm{log}{N}$
411 404 405 410 3eqtrd ${⊢}{\phi }\to \sqrt{2}\sqrt{2}\sqrt{{N}}{G}\left(\sqrt{{N}}\right)=\mathrm{log}{N}$
412 390 395 411 3eqtrd ${⊢}{\phi }\to \sqrt{2\cdot {N}}\sqrt{2}{G}\left(\sqrt{{N}}\right)=\mathrm{log}{N}$
413 412 oveq2d ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\sqrt{2\cdot {N}}\sqrt{2}{G}\left(\sqrt{{N}}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}$
414 383 384 413 3eqtrd ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\sqrt{2}{G}\left(\sqrt{{N}}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}$
415 414 oveq1d ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)$
416 374 415 eqtrd ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\left(\sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)$
417 382 oveq1d ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\sqrt{2\cdot {N}}\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)$
418 251 379 370 mulassd ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\sqrt{2\cdot {N}}\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\sqrt{2\cdot {N}}\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)$
419 95 rpne0d ${⊢}{\phi }\to \sqrt{2\cdot {N}}\ne 0$
420 245 379 419 divcan2d ${⊢}{\phi }\to \sqrt{2\cdot {N}}\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)=\mathrm{log}2$
421 420 oveq2d ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\sqrt{2\cdot {N}}\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2$
422 417 418 421 3eqtrd ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2$
423 416 422 oveq12d ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\left(\sqrt{2}{G}\left(\sqrt{{N}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)\right)+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{\mathrm{log}2}{\sqrt{2\cdot {N}}}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)+\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2$
424 360 362 addcld ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)\in ℂ$
425 424 359 addcomd ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)+\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2+\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)$
426 372 423 425 3eqtrd ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right){F}\left({N}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2+\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}{N}+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)$
427 363 367 426 3eqtr4rd ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right){F}\left({N}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}+\left(\frac{2\cdot {N}}{3}\right)\left(\frac{9}{4}\right){G}\left(\frac{{N}}{2}\right)$
428 251 253 mulcld ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}\in ℂ$
429 addcl ${⊢}\left(2\mathrm{log}2\in ℂ\wedge 2\mathrm{log}{N}\in ℂ\right)\to 2\mathrm{log}2+2\mathrm{log}{N}\in ℂ$
430 351 283 429 sylancr ${⊢}{\phi }\to 2\mathrm{log}2+2\mathrm{log}{N}\in ℂ$
431 428 430 354 addassd ${⊢}{\phi }\to \left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}+\left(2\mathrm{log}2+2\mathrm{log}{N}\right)+\left(\mathrm{log}{N}-5\mathrm{log}2\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}+\left(2\mathrm{log}2+2\mathrm{log}{N}\right)+\left(\mathrm{log}{N}-5\mathrm{log}2\right)$
432 357 427 431 3eqtr4d ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right){F}\left({N}\right)=\left(\frac{\sqrt{2\cdot {N}}}{3}\right)\mathrm{log}2\cdot {N}+\left(2\mathrm{log}2+2\mathrm{log}{N}\right)+\left(\mathrm{log}{N}-5\mathrm{log}2\right)$
433 270 272 432 3eqtr4rd ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right){F}\left({N}\right)=\left(\left(\frac{\sqrt{2\cdot {N}}}{3}\right)+2\right)\mathrm{log}2\cdot {N}+\left(\left(\frac{4\cdot {N}}{3}\right)-5\right)\mathrm{log}2-\left(\left(\frac{4\cdot {N}}{3}\right)\mathrm{log}2-\mathrm{log}{N}\right)$
434 191 250 433 3brtr4d ${⊢}{\phi }\to \left(\frac{2\cdot {N}}{3}\right)\mathrm{log}2<\left(\frac{2\cdot {N}}{3}\right){F}\left({N}\right)$
435 100 99 213 ltmul2d ${⊢}{\phi }\to \left(\mathrm{log}2<{F}\left({N}\right)↔\left(\frac{2\cdot {N}}{3}\right)\mathrm{log}2<\left(\frac{2\cdot {N}}{3}\right){F}\left({N}\right)\right)$
436 434 435 mpbird ${⊢}{\phi }\to \mathrm{log}2<{F}\left({N}\right)$
437 46 100 99 101 436 lttrd ${⊢}{\phi }\to {F}\left(64\right)<{F}\left({N}\right)$
438 46 99 437 ltnsymd ${⊢}{\phi }\to ¬{F}\left({N}\right)<{F}\left(64\right)$
439 43 438 pm2.21dd ${⊢}{\phi }\to {\psi }$