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 \mathbb{N}⟼\sqrt{2}G\left(\sqrt{n}\right)+\left(\frac{9}{4}\right)G\left(\frac{n}{2}\right)+\left(\frac{\log 2}{\sqrt{2n}}\right)\right)$$
	bposlem7.2	$$⊢G=\left(x\in {ℝ}^{+}⟼\frac{\log x}{x}\right)$$
	bposlem9.3	$$⊢\phi \to N\in \mathbb{N}$$
	bposlem9.4	$$⊢\phi \to 64<N$$
	bposlem9.5	$$⊢\phi \to \neg \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
Assertion	bposlem9	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		bposlem7.1	$$⊢F=\left(n\in \mathbb{N}⟼\sqrt{2}G\left(\sqrt{n}\right)+\left(\frac{9}{4}\right)G\left(\frac{n}{2}\right)+\left(\frac{\log 2}{\sqrt{2n}}\right)\right)$$
2		bposlem7.2	$$⊢G=\left(x\in {ℝ}^{+}⟼\frac{\log x}{x}\right)$$
3		bposlem9.3	$$⊢\phi \to N\in \mathbb{N}$$
4		bposlem9.4	$$⊢\phi \to 64<N$$
5		bposlem9.5	$$⊢\phi \to \neg \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
6		6nn0	$$⊢6\in {\mathbb{N}}_0$$
7		4nn	$$⊢4\in \mathbb{N}$$
8	6 7	decnncl	$$⊢64\in \mathbb{N}$$
9	8	a1i	$$⊢\phi \to 64\in \mathbb{N}$$
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\leftrightarrow {\mathrm{e}}^2\le 8^2\right)$$
25	10 21 11 23 24	mp4an	$$⊢\mathrm{e}\le 8\leftrightarrow {\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)<\log 2\right)$$
45	44	a1i	$$⊢\phi \to \left(F\left(64\right)\in ℝ\wedge F\left(64\right)<\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 2n=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
53	52	fveq2d	$$⊢n=N\to \sqrt{2n}=\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
54	53	oveq2d	$$⊢n=N\to \frac{\log 2}{\sqrt{2n}}=\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}$$
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{\log 2}{\sqrt{2n}}\right)=\sqrt{2}G\left(\sqrt{N}\right)+\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)+\left(\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\right)$$
56		ovex	$$⊢\sqrt{2}G\left(\sqrt{N}\right)+\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)+\left(\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\right)\in \mathrm{V}$$
57	55 1 56	fvmpt	$$⊢N\in \mathbb{N}\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{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\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{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\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 \log x=\log \sqrt{N}$$
63		id	$$⊢x=\sqrt{N}\to x=\sqrt{N}$$
64	62 63	oveq12d	$$⊢x=\sqrt{N}\to \frac{\log x}{x}=\frac{\log \sqrt{N}}{\sqrt{N}}$$
65		ovex	$$⊢\frac{\log \sqrt{N}}{\sqrt{N}}\in \mathrm{V}$$
66	64 2 65	fvmpt	$$⊢\sqrt{N}\in {ℝ}^{+}\to G\left(\sqrt{N}\right)=\frac{\log \sqrt{N}}{\sqrt{N}}$$
67	61 66	syl	$$⊢\phi \to G\left(\sqrt{N}\right)=\frac{\log \sqrt{N}}{\sqrt{N}}$$
68	61	relogcld	$$⊢\phi \to \log \sqrt{N}\in ℝ$$
69	68 61	rerpdivcld	$$⊢\phi \to \frac{\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 \log x=\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{\log x}{x}=\frac{\log \left(\frac{N}{2}\right)}{\frac{N}{2}}$$
81		ovex	$$⊢\frac{\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{\log \left(\frac{N}{2}\right)}{\frac{N}{2}}$$
83	77 82	syl	$$⊢\phi \to G\left(\frac{N}{2}\right)=\frac{\log \left(\frac{N}{2}\right)}{\frac{N}{2}}$$
84	77	relogcld	$$⊢\phi \to \log \left(\frac{N}{2}\right)\in ℝ$$
85	84 77	rerpdivcld	$$⊢\phi \to \frac{\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 \log 2\in ℝ$$
92	90 91	ax-mp	$$⊢\log 2\in ℝ$$
93		rpmulcl	$$⊢\left(2\in {ℝ}^{+}\wedge N\in {ℝ}^{+}\right)\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {ℝ}^{+}$$
94	90 60 93	sylancr	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {ℝ}^{+}$$
95	94	rpsqrtcld	$$⊢\phi \to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in {ℝ}^{+}$$
96		rerpdivcl	$$⊢\left(\log 2\in ℝ\wedge \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in {ℝ}^{+}\right)\to \frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\in ℝ$$
97	92 95 96	sylancr	$$⊢\phi \to \frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\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{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\right)\in ℝ$$
99	58 98	eqeltrd	$$⊢\phi \to F\left(N\right)\in ℝ$$
100	92	a1i	$$⊢\phi \to \log 2\in ℝ$$
101	45	simprd	$$⊢\phi \to F\left(64\right)<\log 2$$
102		nnrp	$$⊢4\in \mathbb{N}\to 4\in {ℝ}^{+}$$
103	7 102	ax-mp	$$⊢4\in {ℝ}^{+}$$
104		relogcl	$$⊢4\in {ℝ}^{+}\to \log 4\in ℝ$$
105	103 104	ax-mp	$$⊢\log 4\in ℝ$$
106		remulcl	$$⊢\left(N\in ℝ\wedge \log 4\in ℝ\right)\to N\log 4\in ℝ$$
107	37 105 106	sylancl	$$⊢\phi \to N\log 4\in ℝ$$
108	60	relogcld	$$⊢\phi \to \log N\in ℝ$$
109	107 108	resubcld	$$⊢\phi \to N\log 4-\log N\in ℝ$$
110		rpre	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {ℝ}^{+}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
111		rpge0	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {ℝ}^{+}\to 0\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
112	110 111	resqrtcld	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {ℝ}^{+}\to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in ℝ$$
113	94 112	syl	$$⊢\phi \to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in ℝ$$
114		3nn	$$⊢3\in \mathbb{N}$$
115		nndivre	$$⊢\left(\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in ℝ\wedge 3\in \mathbb{N}\right)\to \frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\in ℝ$$
116	113 114 115	sylancl	$$⊢\phi \to \frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\in ℝ$$
117		2re	$$⊢2\in ℝ$$
118		readdcl	$$⊢\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\in ℝ\wedge 2\in ℝ\right)\to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\in ℝ$$
119	116 117 118	sylancl	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\in ℝ$$
120	94	relogcld	$$⊢\phi \to \log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
121	119 120	remulcld	$$⊢\phi \to \left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
122		remulcl	$$⊢\left(4\in ℝ\wedge N\in ℝ\right)\to 4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
123	74 37 122	sylancr	$$⊢\phi \to 4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
124		nndivre	$$⊢\left(4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ\wedge 3\in \mathbb{N}\right)\to \frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\in ℝ$$
125	123 114 124	sylancl	$$⊢\phi \to \frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\in ℝ$$
126		5re	$$⊢5\in ℝ$$
127		resubcl	$$⊢\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\in ℝ\wedge 5\in ℝ\right)\to \left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\in ℝ$$
128	125 126 127	sylancl	$$⊢\phi \to \left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\in ℝ$$
129		remulcl	$$⊢\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\in ℝ\wedge \log 2\in ℝ\right)\to \left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2\in ℝ$$
130	128 92 129	sylancl	$$⊢\phi \to \left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2\in ℝ$$
131	121 130	readdcld	$$⊢\phi \to \left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2\in ℝ$$
132		remulcl	$$⊢\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\in ℝ\wedge \log 2\in ℝ\right)\to \left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2\in ℝ$$
133	125 92 132	sylancl	$$⊢\phi \to \left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2\in ℝ$$
134	133 108	resubcld	$$⊢\phi \to \left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-\log N\in ℝ$$
135	3	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
136		df-5	$$⊢5=4+1$$
137	74	a1i	$$⊢\phi \to 4\in ℝ$$
138		6nn	$$⊢6\in \mathbb{N}$$
139		4nn0	$$⊢4\in {\mathbb{N}}_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 \mathbb{Z}$$
145		zltp1le	$$⊢\left(4\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(4<N\leftrightarrow 4+1\le N\right)$$
146	144 135 145	sylancr	$$⊢\phi \to \left(4<N\leftrightarrow 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 \mathbb{N}$$
150	149	nnzi	$$⊢5\in \mathbb{Z}$$
151	150	eluz1i	$$⊢N\in {\mathbb{Z}}_{\ge 5}\leftrightarrow \left(N\in \mathbb{Z}\wedge 5\le N\right)$$
152	135 148 151	sylanbrc	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 5}$$
153		breq2	$$⊢p=q\to \left(N<p\leftrightarrow N<q\right)$$
154		breq1	$$⊢p=q\to \left(p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\leftrightarrow q\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
155	153 154	anbi12d	$$⊢p=q\to \left(\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\leftrightarrow \left(N<q\wedge q\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
156	155	cbvrexvw	$$⊢\exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\leftrightarrow \exists q\in \mathbb{P}\left(N<q\wedge q\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
157	5 156	sylnib	$$⊢\phi \to \neg \exists q\in \mathbb{P}\left(N<q\wedge q\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
158		eqid	$$⊢\left(n\in \mathbb{N}⟼if\left(n\in \mathbb{P},n^{n\mathrm{pCnt}\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{N}\right)},1\right)\right)=\left(n\in \mathbb{N}⟼if\left(n\in \mathbb{P},n^{n\mathrm{pCnt}\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{N}\right)},1\right)\right)$$
159		eqid	$$⊢⌊\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}⌋=⌊\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}⌋$$
160		eqid	$$⊢⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋=⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋$$
161	152 157 158 159 160	bposlem6	$$⊢\phi \to \frac{4^N}{N}<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2}{2}^{\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5}$$
162		reexplog	$$⊢\left(4\in {ℝ}^{+}\wedge N\in \mathbb{Z}\right)\to 4^N={\mathrm{e}}^{N\log 4}$$
163	103 135 162	sylancr	$$⊢\phi \to 4^N={\mathrm{e}}^{N\log 4}$$
164	60	reeflogd	$$⊢\phi \to {\mathrm{e}}^{\log N}=N$$
165	164	eqcomd	$$⊢\phi \to N={\mathrm{e}}^{\log N}$$
166	163 165	oveq12d	$$⊢\phi \to \frac{4^N}{N}=\frac{{\mathrm{e}}^{N\log 4}}{{\mathrm{e}}^{\log N}}$$
167	107	recnd	$$⊢\phi \to N\log 4\in ℂ$$
168	108	recnd	$$⊢\phi \to \log N\in ℂ$$
169		efsub	$$⊢\left(N\log 4\in ℂ\wedge \log N\in ℂ\right)\to {\mathrm{e}}^{N\log 4-\log N}=\frac{{\mathrm{e}}^{N\log 4}}{{\mathrm{e}}^{\log N}}$$
170	167 168 169	syl2anc	$$⊢\phi \to {\mathrm{e}}^{N\log 4-\log N}=\frac{{\mathrm{e}}^{N\log 4}}{{\mathrm{e}}^{\log N}}$$
171	166 170	eqtr4d	$$⊢\phi \to \frac{4^N}{N}={\mathrm{e}}^{N\log 4-\log N}$$
172	94	rpcnd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
173	94	rpne0d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0$$
174	119	recnd	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\in ℂ$$
175	172 173 174	cxpefd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2}={\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
176		2cn	$$⊢2\in ℂ$$
177		2ne0	$$⊢2\ne 0$$
178	128	recnd	$$⊢\phi \to \left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\in ℂ$$
179		cxpef	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge \left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\in ℂ\right)\to 2^{\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5}={\mathrm{e}}^{\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2}$$
180	176 177 178 179	mp3an12i	$$⊢\phi \to 2^{\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5}={\mathrm{e}}^{\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2}$$
181	175 180	oveq12d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2}{2}^{\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5}={\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\mathrm{e}}^{\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2}$$
182	121	recnd	$$⊢\phi \to \left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
183	130	recnd	$$⊢\phi \to \left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2\in ℂ$$
184		efadd	$$⊢\left(\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge \left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2\in ℂ\right)\to {\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2}={\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\mathrm{e}}^{\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2}$$
185	182 183 184	syl2anc	$$⊢\phi \to {\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2}={\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\mathrm{e}}^{\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2}$$
186	181 185	eqtr4d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2}{2}^{\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5}={\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2}$$
187	161 171 186	3brtr3d	$$⊢\phi \to {\mathrm{e}}^{N\log 4-\log N}<{\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2}$$
188		eflt	$$⊢\left(N\log 4-\log N\in ℝ\wedge \left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2\in ℝ\right)\to \left(N\log 4-\log N<\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2\leftrightarrow {\mathrm{e}}^{N\log 4-\log N}<{\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2}\right)$$
189	109 131 188	syl2anc	$$⊢\phi \to \left(N\log 4-\log N<\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2\leftrightarrow {\mathrm{e}}^{N\log 4-\log N}<{\mathrm{e}}^{\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2}\right)$$
190	187 189	mpbird	$$⊢\phi \to N\log 4-\log N<\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2$$
191	109 131 134 190	ltsub1dd	$$⊢\phi \to N\log 4-\log N-\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-\log N\right)<\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2-\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-\log N\right)$$
192	37	recnd	$$⊢\phi \to N\in ℂ$$
193		mulcom	$$⊢\left(2\in ℂ\wedge N\in ℂ\right)\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2$$
194	176 192 193	sylancr	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2$$
195	194	oveq1d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\log 2=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\log 2$$
196	92	recni	$$⊢\log 2\in ℂ$$
197		mulass	$$⊢\left(N\in ℂ\wedge 2\in ℂ\wedge \log 2\in ℂ\right)\to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\log 2=N2\log 2$$
198	176 196 197	mp3an23	$$⊢N\in ℂ\to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\log 2=N2\log 2$$
199	192 198	syl	$$⊢\phi \to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\log 2=N2\log 2$$
200	196	2timesi	$$⊢2\log 2=\log 2+\log 2$$
201		relogmul	$$⊢\left(2\in {ℝ}^{+}\wedge 2\in {ℝ}^{+}\right)\to \log 2\cdot 2=\log 2+\log 2$$
202	90 90 201	mp2an	$$⊢\log 2\cdot 2=\log 2+\log 2$$
203		2t2e4	$$⊢2\cdot 2=4$$
204	203	fveq2i	$$⊢\log 2\cdot 2=\log 4$$
205	200 202 204	3eqtr2i	$$⊢2\log 2=\log 4$$
206	205	oveq2i	$$⊢N2\log 2=N\log 4$$
207	199 206	eqtrdi	$$⊢\phi \to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\log 2=N\log 4$$
208	195 207	eqtrd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\log 2=N\log 4$$
209	208	oveq1d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\log 2-\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2=N\log 4-\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2$$
210	125	recnd	$$⊢\phi \to \frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\in ℂ$$
211		3rp	$$⊢3\in {ℝ}^{+}$$
212		rpdivcl	$$⊢\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {ℝ}^{+}\wedge 3\in {ℝ}^{+}\right)\to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\in {ℝ}^{+}$$
213	94 211 212	sylancl	$$⊢\phi \to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\in {ℝ}^{+}$$
214	213	rpcnd	$$⊢\phi \to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\in ℂ$$
215		4p2e6	$$⊢4+2=6$$
216	215	oveq1i	$$⊢\left(4+2\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=6\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
217		4cn	$$⊢4\in ℂ$$
218		adddir	$$⊢\left(4\in ℂ\wedge 2\in ℂ\wedge N\in ℂ\right)\to \left(4+2\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
219	217 176 192 218	mp3an12i	$$⊢\phi \to \left(4+2\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
220	216 219	eqtr3id	$$⊢\phi \to 6\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
221	220	oveq1d	$$⊢\phi \to \frac{6\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}=\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}=\left(\frac{6}{3}\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
227	222 225 226	mp3an13	$$⊢N\in ℂ\to \frac{6\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}=\left(\frac{6}{3}\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
228	192 227	syl	$$⊢\phi \to \frac{6\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}=\left(\frac{6}{3}\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
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 \mathrm{<mi\; mathcolor="\#808">N</mi>}=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
234	228 233	eqtrdi	$$⊢\phi \to \frac{6\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
235	123	recnd	$$⊢\phi \to 4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
236		remulcl	$$⊢\left(2\in ℝ\wedge N\in ℝ\right)\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
237	117 37 236	sylancr	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
238	237	recnd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
239		divdir	$$⊢\left(4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge \left(3\in ℂ\wedge 3\ne 0\right)\right)\to \frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}=\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)$$
240	225 239	mp3an3	$$⊢\left(4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\right)\to \frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}=\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)$$
241	235 238 240	syl2anc	$$⊢\phi \to \frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}=\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)$$
242	221 234 241	3eqtr3d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)$$
243	210 214 242	mvrladdd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)=\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}$$
244	243	oveq1d	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\right)\log 2=\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2$$
245	100	recnd	$$⊢\phi \to \log 2\in ℂ$$
246	238 210 245	subdird	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\right)\log 2=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\log 2-\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2$$
247	244 246	eqtr3d	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\log 2-\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2$$
248	133	recnd	$$⊢\phi \to \left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2\in ℂ$$
249	167 248 168	nnncan2d	$$⊢\phi \to N\log 4-\log N-\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-\log N\right)=N\log 4-\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2$$
250	209 247 249	3eqtr4d	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2=N\log 4-\log N-\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-\log N\right)$$
251	116	recnd	$$⊢\phi \to \frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\in ℂ$$
252	176	a1i	$$⊢\phi \to 2\in ℂ$$
253	120	recnd	$$⊢\phi \to \log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
254	251 252 253	adddird	$$⊢\phi \to \left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
255		relogmul	$$⊢\left(2\in {ℝ}^{+}\wedge N\in {ℝ}^{+}\right)\to \log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\log 2+\log N$$
256	90 60 255	sylancr	$$⊢\phi \to \log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\log 2+\log N$$
257	256	oveq2d	$$⊢\phi \to 2\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=2\left(\log 2+\log N\right)$$
258	252 245 168	adddid	$$⊢\phi \to 2\left(\log 2+\log N\right)=2\log 2+2\log N$$
259	257 258	eqtrd	$$⊢\phi \to 2\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=2\log 2+2\log N$$
260	259	oveq2d	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\log 2+2\log N$$
261	254 260	eqtrd	$$⊢\phi \to \left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\log 2+2\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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2=\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-5\log 2$$
265	264	oveq1d	$$⊢\phi \to \left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2-\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-\log N\right)=\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-5\log 2-\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-\log N\right)$$
266	262 196	mulcli	$$⊢5\log 2\in ℂ$$
267	266	a1i	$$⊢\phi \to 5\log 2\in ℂ$$
268	248 267 168	nnncan1d	$$⊢\phi \to \left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-5\log 2-\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-\log N\right)=\log N-5\log 2$$
269	265 268	eqtrd	$$⊢\phi \to \left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2-\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-\log N\right)=\log N-5\log 2$$
270	261 269	oveq12d	$$⊢\phi \to \left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2-\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-\log N\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(2\log 2+2\log N\right)+\left(\log N-5\log 2\right)$$
271	134	recnd	$$⊢\phi \to \left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-\log N\in ℂ$$
272	182 183 271	addsubassd	$$⊢\phi \to \left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2-\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-\log N\right)=\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2-\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-\log N\right)$$
273	262 223 196	subdiri	$$⊢\left(5-3\right)\log 2=5\log 2-3\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)\log 2=2\log 2$$
280	273 279	eqtr3i	$$⊢5\log 2-3\log 2=2\log 2$$
281	280	a1i	$$⊢\phi \to 5\log 2-3\log 2=2\log 2$$
282		mulcl	$$⊢\left(2\in ℂ\wedge \log N\in ℂ\right)\to 2\log N\in ℂ$$
283	176 168 282	sylancr	$$⊢\phi \to 2\log N\in ℂ$$
284		df-3	$$⊢3=2+1$$
285	284	oveq1i	$$⊢3\log N=\left(2+1\right)\log N$$
286		1cnd	$$⊢\phi \to 1\in ℂ$$
287	252 286 168	adddird	$$⊢\phi \to \left(2+1\right)\log N=2\log N+1\log N$$
288	285 287	eqtrid	$$⊢\phi \to 3\log N=2\log N+1\log N$$
289	168	mullidd	$$⊢\phi \to 1\log N=\log N$$
290	289	oveq2d	$$⊢\phi \to 2\log N+1\log N=2\log N+\log N$$
291	288 290	eqtrd	$$⊢\phi \to 3\log N=2\log N+\log N$$
292	291	oveq1d	$$⊢\phi \to 3\log N-5\log 2=2\log N+\log N-5\log 2$$
293	283 168 267 292	assraddsubd	$$⊢\phi \to 3\log N-5\log 2=2\log N+\log N-5\log 2$$
294	281 293	oveq12d	$$⊢\phi \to \left(5\log 2-3\log 2\right)+3\log N-5\log 2=2\log 2+2\log N+\left(\log N-5\log 2\right)$$
295		relogdiv	$$⊢\left(N\in {ℝ}^{+}\wedge 2\in {ℝ}^{+}\right)\to \log \left(\frac{N}{2}\right)=\log N-\log 2$$
296	60 90 295	sylancl	$$⊢\phi \to \log \left(\frac{N}{2}\right)=\log N-\log 2$$
297	296	oveq2d	$$⊢\phi \to 3\log \left(\frac{N}{2}\right)=3\left(\log N-\log 2\right)$$
298		subdi	$$⊢\left(3\in ℂ\wedge \log N\in ℂ\wedge \log 2\in ℂ\right)\to 3\left(\log N-\log 2\right)=3\log N-3\log 2$$
299	223 196 298	mp3an13	$$⊢\log N\in ℂ\to 3\left(\log N-\log 2\right)=3\log N-3\log 2$$
300	168 299	syl	$$⊢\phi \to 3\left(\log N-\log 2\right)=3\log N-3\log 2$$
301	297 300	eqtrd	$$⊢\phi \to 3\log \left(\frac{N}{2}\right)=3\log N-3\log 2$$
302		div23	$$⊢\left(2\in ℂ\wedge N\in ℂ\wedge \left(3\in ℂ\wedge 3\ne 0\right)\right)\to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}=\left(\frac{2}{3}\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
303	176 225 302	mp3an13	$$⊢N\in ℂ\to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}=\left(\frac{2}{3}\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
304	192 303	syl	$$⊢\phi \to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}=\left(\frac{2}{3}\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)=\left(\frac{2}{3}\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\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 \mathrm{<mi\; mathcolor="\#808">N</mi>}\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 \mathrm{<mi\; mathcolor="\#808">N</mi>}\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 \mathrm{<mi\; mathcolor="\#808">N</mi>}\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)=1N\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	mullidd	$$⊢\phi \to 1N\left(\frac{3}{2}\right)=N\left(\frac{3}{2}\right)$$
322	318 321	eqtrid	$$⊢\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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)=3\left(\frac{N}{2}\right)$$
329	328 83	oveq12d	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)=3\left(\frac{N}{2}\right)\left(\frac{\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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)=\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{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 \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{\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{\log \left(\frac{N}{2}\right)}{\frac{N}{2}}\right)=3\left(\frac{N}{2}\right)\left(\frac{\log \left(\frac{N}{2}\right)}{\frac{N}{2}}\right)$$
340	336 335 337	divcan2d	$$⊢\phi \to \left(\frac{N}{2}\right)\left(\frac{\log \left(\frac{N}{2}\right)}{\frac{N}{2}}\right)=\log \left(\frac{N}{2}\right)$$
341	340	oveq2d	$$⊢\phi \to 3\left(\frac{N}{2}\right)\left(\frac{\log \left(\frac{N}{2}\right)}{\frac{N}{2}}\right)=3\log \left(\frac{N}{2}\right)$$
342	339 341	eqtrd	$$⊢\phi \to 3\left(\frac{N}{2}\right)\left(\frac{\log \left(\frac{N}{2}\right)}{\frac{N}{2}}\right)=3\log \left(\frac{N}{2}\right)$$
343	329 333 342	3eqtr3d	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)=3\log \left(\frac{N}{2}\right)$$
344	223 196	mulcli	$$⊢3\log 2\in ℂ$$
345	344	a1i	$$⊢\phi \to 3\log 2\in ℂ$$
346		mulcl	$$⊢\left(3\in ℂ\wedge \log N\in ℂ\right)\to 3\log N\in ℂ$$
347	223 168 346	sylancr	$$⊢\phi \to 3\log N\in ℂ$$
348	267 345 347	npncan3d	$$⊢\phi \to \left(5\log 2-3\log 2\right)+3\log N-5\log 2=3\log N-3\log 2$$
349	301 343 348	3eqtr4d	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)=\left(5\log 2-3\log 2\right)+3\log N-5\log 2$$
350	117 92	remulcli	$$⊢2\log 2\in ℝ$$
351	350	recni	$$⊢2\log 2\in ℂ$$
352	351	a1i	$$⊢\phi \to 2\log 2\in ℂ$$
353		subcl	$$⊢\left(\log N\in ℂ\wedge 5\log 2\in ℂ\right)\to \log N-5\log 2\in ℂ$$
354	168 266 353	sylancl	$$⊢\phi \to \log N-5\log 2\in ℂ$$
355	352 283 354	addassd	$$⊢\phi \to 2\log 2+2\log N+\left(\log N-5\log 2\right)=2\log 2+2\log N+\left(\log N-5\log 2\right)$$
356	294 349 355	3eqtr4d	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)=2\log 2+2\log N+\left(\log N-5\log 2\right)$$
357	356	oveq2d	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(2\log 2+2\log N\right)+\left(\log N-5\log 2\right)$$
358		mulcl	$$⊢\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\in ℂ\wedge \log 2\in ℂ\right)\to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\in ℂ$$
359	251 196 358	sylancl	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\in ℂ$$
360	251 168	mulcld	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}{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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2+\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log N+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2+\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log N+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)$$
364	256	oveq2d	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\left(\log 2+\log N\right)$$
365	251 245 168	adddid	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\left(\log 2+\log N\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2+\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log N$$
366	364 365	eqtrd	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2+\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log N$$
367	366	oveq1d	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2+\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log N+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)$$
368	58	oveq2d	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)F\left(N\right)=\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\sqrt{2}G\left(\sqrt{N}\right)+\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)+\left(\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\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{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\in ℂ$$
371	214 369 370	adddid	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\sqrt{2}G\left(\sqrt{N}\right)+\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)+\left(\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\right)\right)=\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\right)$$
372	368 371	eqtrd	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)F\left(N\right)=\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}{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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\sqrt{2}G\left(\sqrt{N}\right)+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)$$
375	94	rpge0d	$$⊢\phi \to 0\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
376		remsqsqrt	$$⊢\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ\wedge 0\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
377	237 375 376	syl2anc	$$⊢\phi \to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
378	377	oveq1d	$$⊢\phi \to \frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}=\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}$$
379	113	recnd	$$⊢\phi \to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in ℂ$$
380	224	a1i	$$⊢\phi \to 3\ne 0$$
381	379 379 334 380	div23d	$$⊢\phi \to \frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
382	378 381	eqtr3d	$$⊢\phi \to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
383	382	oveq1d	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\sqrt{2}G\left(\sqrt{N}\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\sqrt{2}G\left(\sqrt{N}\right)$$
384	251 379 373	mulassd	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\sqrt{2}G\left(\sqrt{N}\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}=\sqrt{2}\sqrt{N}$$
389	386 387 388	sylancr	$$⊢\phi \to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}=\sqrt{2}\sqrt{N}$$
390	389	oveq1d	$$⊢\phi \to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\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{\log \sqrt{N}}{\sqrt{N}}\right)$$
400	68	recnd	$$⊢\phi \to \log \sqrt{N}\in ℂ$$
401	61	rpne0d	$$⊢\phi \to \sqrt{N}\ne 0$$
402	400 393 401	divcan2d	$$⊢\phi \to \sqrt{N}\left(\frac{\log \sqrt{N}}{\sqrt{N}}\right)=\log \sqrt{N}$$
403	399 402	eqtrd	$$⊢\phi \to \sqrt{N}G\left(\sqrt{N}\right)=\log \sqrt{N}$$
404	398 403	oveq12d	$$⊢\phi \to \sqrt{2}\sqrt{2}\sqrt{N}G\left(\sqrt{N}\right)=2\log \sqrt{N}$$
405	400	2timesd	$$⊢\phi \to 2\log \sqrt{N}=\log \sqrt{N}+\log \sqrt{N}$$
406	61 61	relogmuld	$$⊢\phi \to \log \sqrt{N}\sqrt{N}=\log \sqrt{N}+\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 \log \sqrt{N}\sqrt{N}=\log N$$
410	406 409	eqtr3d	$$⊢\phi \to \log \sqrt{N}+\log \sqrt{N}=\log N$$
411	404 405 410	3eqtrd	$$⊢\phi \to \sqrt{2}\sqrt{2}\sqrt{N}G\left(\sqrt{N}\right)=\log N$$
412	390 395 411	3eqtrd	$$⊢\phi \to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\sqrt{2}G\left(\sqrt{N}\right)=\log N$$
413	412	oveq2d	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\sqrt{2}G\left(\sqrt{N}\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log N$$
414	383 384 413	3eqtrd	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\sqrt{2}G\left(\sqrt{N}\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log N$$
415	414	oveq1d	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\sqrt{2}G\left(\sqrt{N}\right)+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log N+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)$$
416	374 415	eqtrd	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log N+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)$$
417	382	oveq1d	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\left(\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\right)$$
418	251 379 370	mulassd	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\left(\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\left(\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\right)$$
419	95	rpne0d	$$⊢\phi \to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\ne 0$$
420	245 379 419	divcan2d	$$⊢\phi \to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\left(\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\right)=\log 2$$
421	420	oveq2d	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\left(\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2$$
422	417 418 421	3eqtrd	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2$$
423	416 422	oveq12d	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{\log 2}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log N+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)+\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2$$
424	360 362	addcld	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log N+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{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 \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log N+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)+\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2+\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log N+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)$$
426	372 423 425	3eqtrd	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)F\left(N\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2+\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log N+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)$$
427	363 367 426	3eqtr4rd	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)F\left(N\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\left(\frac{9}{4}\right)G\left(\frac{N}{2}\right)$$
428	251 253	mulcld	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
429		addcl	$$⊢\left(2\log 2\in ℂ\wedge 2\log N\in ℂ\right)\to 2\log 2+2\log N\in ℂ$$
430	351 283 429	sylancr	$$⊢\phi \to 2\log 2+2\log N\in ℂ$$
431	428 430 354	addassd	$$⊢\phi \to \left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(2\log 2+2\log N\right)+\left(\log N-5\log 2\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(2\log 2+2\log N\right)+\left(\log N-5\log 2\right)$$
432	357 427 431	3eqtr4d	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)F\left(N\right)=\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(2\log 2+2\log N\right)+\left(\log N-5\log 2\right)$$
433	270 272 432	3eqtr4rd	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)F\left(N\right)=\left(\left(\frac{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}}{3}\right)+2\right)\log 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)-5\right)\log 2-\left(\left(\frac{4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2-\log N\right)$$
434	191 250 433	3brtr4d	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2<\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)F\left(N\right)$$
435	100 99 213	ltmul2d	$$⊢\phi \to \left(\log 2<F\left(N\right)\leftrightarrow \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\log 2<\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)F\left(N\right)\right)$$
436	434 435	mpbird	$$⊢\phi \to \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 \neg F\left(N\right)<F\left(64\right)$$
439	43 438	pm2.21dd	$$⊢\phi \to \psi$$