Theorem bposlem9 16248

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

Hypotheses

Ref	Expression
bposlem7.1	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))
bposlem7.2	⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))
bposlem9.3	⊢ (𝜑 → 𝑁 ∈ ℕ)
bposlem9.4	⊢ (𝜑 → ;64 < 𝑁)
bposlem9.5	⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))

Assertion

Ref	Expression
bposlem9	⊢ (𝜑 → 𝜓)

Distinct variable groups:   𝑛,𝑁   𝑛,𝐺   𝜑,𝑛   𝜑,𝑥   𝑁,𝑝   𝑥,𝑁

Allowed substitution hints:   𝜑(𝑝)   𝜓(𝑥, 𝑛, 𝑝)   𝐹(𝑥, 𝑛, 𝑝)   𝐺(𝑥, 𝑝)

Proof of Theorem bposlem9

Dummy variable 𝑞 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bposlem9.4	. . 3 ⊢ (𝜑 → ;64 < 𝑁)
2		bposlem7.1	. . . 4 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))
3		bposlem7.2	. . . 4 ⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))
4		6nn0 9589	. . . . . 6 ⊢ 6 ∈ ℕ0
5		4nn 9473	. . . . . 6 ⊢ 4 ∈ ℕ
6	4, 5	decnncl 9805	. . . . 5 ⊢ ;64 ∈ ℕ
7	6	a1i 9	. . . 4 ⊢ (𝜑 → ;64 ∈ ℕ)
8		bposlem9.3	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
9		ere 12456	. . . . . . . 8 ⊢ e ∈ ℝ
10		8re 9392	. . . . . . . 8 ⊢ 8 ∈ ℝ
11		egt2lt3 12566	. . . . . . . . . 10 ⊢ (2 < e ∧ e < 3)
12	11	simpri 113	. . . . . . . . 9 ⊢ e < 3
13		3lt8 9504	. . . . . . . . 9 ⊢ 3 < 8
14		3re 9381	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
15	9, 14, 10	lttri 8432	. . . . . . . . 9 ⊢ ((e < 3 ∧ 3 < 8) → e < 8)
16	12, 13, 15	mp2an 430	. . . . . . . 8 ⊢ e < 8
17	9, 10, 16	ltleii 8430	. . . . . . 7 ⊢ e ≤ 8
18		0re 8327	. . . . . . . . 9 ⊢ 0 ∈ ℝ
19		epos 12567	. . . . . . . . 9 ⊢ 0 < e
20	18, 9, 19	ltleii 8430	. . . . . . . 8 ⊢ 0 ≤ e
21		8pos 9410	. . . . . . . . 9 ⊢ 0 < 8
22	18, 10, 21	ltleii 8430	. . . . . . . 8 ⊢ 0 ≤ 8
23		le2sq 11066	. . . . . . . 8 ⊢ (((e ∈ ℝ ∧ 0 ≤ e) ∧ (8 ∈ ℝ ∧ 0 ≤ 8)) → (e ≤ 8 ↔ (e↑2) ≤ (8↑2)))
24	9, 20, 10, 22, 23	mp4an 431	. . . . . . 7 ⊢ (e ≤ 8 ↔ (e↑2) ≤ (8↑2))
25	17, 24	mpbi 145	. . . . . 6 ⊢ (e↑2) ≤ (8↑2)
26	10	recni 8339	. . . . . . . 8 ⊢ 8 ∈ ℂ
27	26	sqvali 11071	. . . . . . 7 ⊢ (8↑2) = (8 · 8)
28		8t8e64 9907	. . . . . . 7 ⊢ (8 · 8) = ;64
29	27, 28	eqtri 2259	. . . . . 6 ⊢ (8↑2) = ;64
30	25, 29	breqtri 4155	. . . . 5 ⊢ (e↑2) ≤ ;64
31	30	a1i 9	. . . 4 ⊢ (𝜑 → (e↑2) ≤ ;64)
32	9	resqcli 11076	. . . . . 6 ⊢ (e↑2) ∈ ℝ
33	32	a1i 9	. . . . 5 ⊢ (𝜑 → (e↑2) ∈ ℝ)
34	6	nnrei 9316	. . . . . 6 ⊢ ;64 ∈ ℝ
35	34	a1i 9	. . . . 5 ⊢ (𝜑 → ;64 ∈ ℝ)
36	8	nnred 9320	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℝ)
37		ltle 8414	. . . . . . 7 ⊢ ((;64 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (;64 < 𝑁 → ;64 ≤ 𝑁))
38	34, 36, 37	sylancr 418	. . . . . 6 ⊢ (𝜑 → (;64 < 𝑁 → ;64 ≤ 𝑁))
39	1, 38	mpd 13	. . . . 5 ⊢ (𝜑 → ;64 ≤ 𝑁)
40	33, 35, 36, 31, 39	letrd 8452	. . . 4 ⊢ (𝜑 → (e↑2) ≤ 𝑁)
41	2, 3, 7, 8, 31, 40	bposlem7 16246	. . 3 ⊢ (𝜑 → (;64 < 𝑁 → (𝐹‘𝑁) < (𝐹‘;64)))
42	1, 41	mpd 13	. 2 ⊢ (𝜑 → (𝐹‘𝑁) < (𝐹‘;64))
43	2, 3	bposlem8 16247	. . . . 5 ⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2))
44	43	a1i 9	. . . 4 ⊢ (𝜑 → ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2)))
45	44	simpld 112	. . 3 ⊢ (𝜑 → (𝐹‘;64) ∈ ℝ)
46		2fveq3 5700	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → (𝐺‘(√‘𝑛)) = (𝐺‘(√‘𝑁)))
47	46	oveq2d 6101	. . . . . . 7 ⊢ (𝑛 = 𝑁 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · (𝐺‘(√‘𝑁))))
48		fvoveq1 6108	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → (𝐺‘(𝑛 / 2)) = (𝐺‘(𝑁 / 2)))
49	48	oveq2d 6101	. . . . . . 7 ⊢ (𝑛 = 𝑁 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · (𝐺‘(𝑁 / 2))))
50	47, 49	oveq12d 6103	. . . . . 6 ⊢ (𝑛 = 𝑁 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))))
51		oveq2 6093	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
52	51	fveq2d 5699	. . . . . . 7 ⊢ (𝑛 = 𝑁 → (√‘(2 · 𝑛)) = (√‘(2 · 𝑁)))
53	52	oveq2d 6101	. . . . . 6 ⊢ (𝑛 = 𝑁 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / (√‘(2 · 𝑁))))
54	50, 53	oveq12d 6103	. . . . 5 ⊢ (𝑛 = 𝑁 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
55		sqrt2re 12961	. . . . . . . . 9 ⊢ (√‘2) ∈ ℝ
56	55	a1i 9	. . . . . . . 8 ⊢ (𝜑 → (√‘2) ∈ ℝ)
57		relogcl 16023	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
58	57	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
59		simpr 110	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
60	58, 59	rerpdivcld 10140	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) / 𝑥) ∈ ℝ)
61	60, 3	fmptd 5862	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:ℝ+⟶ℝ)
62	8	nnrpd 10106	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ+)
63	62	rpsqrtcld 11941	. . . . . . . . 9 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ+)
64	61, 63	ffvelcdmd 5844	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℝ)
65	56, 64	remulcld 8357	. . . . . . 7 ⊢ (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
66		9nn 9478	. . . . . . . . . . . 12 ⊢ 9 ∈ ℕ
67	66	nnzi 9670	. . . . . . . . . . 11 ⊢ 9 ∈ ℤ
68		znq 10034	. . . . . . . . . . 11 ⊢ ((9 ∈ ℤ ∧ 4 ∈ ℕ) → (9 / 4) ∈ ℚ)
69	67, 5, 68	mp2an 430	. . . . . . . . . 10 ⊢ (9 / 4) ∈ ℚ
70		qre 10035	. . . . . . . . . 10 ⊢ ((9 / 4) ∈ ℚ → (9 / 4) ∈ ℝ)
71	69, 70	ax-mp 5	. . . . . . . . 9 ⊢ (9 / 4) ∈ ℝ
72	71	a1i 9	. . . . . . . 8 ⊢ (𝜑 → (9 / 4) ∈ ℝ)
73	62	rphalfcld 10121	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 / 2) ∈ ℝ+)
74	61, 73	ffvelcdmd 5844	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℝ)
75	72, 74	remulcld 8357	. . . . . . 7 ⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
76	65, 75	readdcld 8356	. . . . . 6 ⊢ (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℝ)
77		2rp 10070	. . . . . . . . 9 ⊢ 2 ∈ ℝ+
78		relogcl 16023	. . . . . . . . 9 ⊢ (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
79	77, 78	ax-mp 5	. . . . . . . 8 ⊢ (log‘2) ∈ ℝ
80	79	a1i 9	. . . . . . 7 ⊢ (𝜑 → (log‘2) ∈ ℝ)
81		rpmulcl 10090	. . . . . . . . 9 ⊢ ((2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+) → (2 · 𝑁) ∈ ℝ+)
82	77, 62, 81	sylancr 418	. . . . . . . 8 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ+)
83	82	rpsqrtcld 11941	. . . . . . 7 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ+)
84	80, 83	rerpdivcld 10140	. . . . . 6 ⊢ (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
85	76, 84	readdcld 8356	. . . . 5 ⊢ (𝜑 → ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ ℝ)
86	2, 54, 8, 85	fvmptd3 5799	. . . 4 ⊢ (𝜑 → (𝐹‘𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
87	86, 85	eqeltrd 2315	. . 3 ⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ)
88	44	simprd 114	. . . 4 ⊢ (𝜑 → (𝐹‘;64) < (log‘2))
89		nnrp 10075	. . . . . . . . . . 11 ⊢ (4 ∈ ℕ → 4 ∈ ℝ+)
90	5, 89	ax-mp 5	. . . . . . . . . 10 ⊢ 4 ∈ ℝ+
91		relogcl 16023	. . . . . . . . . 10 ⊢ (4 ∈ ℝ+ → (log‘4) ∈ ℝ)
92	90, 91	ax-mp 5	. . . . . . . . 9 ⊢ (log‘4) ∈ ℝ
93		remulcl 8308	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ (log‘4) ∈ ℝ) → (𝑁 · (log‘4)) ∈ ℝ)
94	36, 92, 93	sylancl 417	. . . . . . . 8 ⊢ (𝜑 → (𝑁 · (log‘4)) ∈ ℝ)
95	62	relogcld 16044	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
96	94, 95	resubcld 8710	. . . . . . 7 ⊢ (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) ∈ ℝ)
97		rpre 10072	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ ℝ+ → (2 · 𝑁) ∈ ℝ)
98		rpge0 10078	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ ℝ+ → 0 ≤ (2 · 𝑁))
99	97, 98	resqrtcld 11946	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) ∈ ℝ+ → (√‘(2 · 𝑁)) ∈ ℝ)
100	82, 99	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
101		3nn 9472	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ
102		nndivre 9343	. . . . . . . . . . 11 ⊢ (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
103	100, 101, 102	sylancl 417	. . . . . . . . . 10 ⊢ (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
104		2re 9377	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
105		readdcl 8306	. . . . . . . . . 10 ⊢ ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
106	103, 104, 105	sylancl 417	. . . . . . . . 9 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
107	82	relogcld 16044	. . . . . . . . 9 ⊢ (𝜑 → (log‘(2 · 𝑁)) ∈ ℝ)
108	106, 107	remulcld 8357	. . . . . . . 8 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℝ)
109		4re 9384	. . . . . . . . . . . 12 ⊢ 4 ∈ ℝ
110		remulcl 8308	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (4 · 𝑁) ∈ ℝ)
111	109, 36, 110	sylancr 418	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · 𝑁) ∈ ℝ)
112		nndivre 9343	. . . . . . . . . . 11 ⊢ (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
113	111, 101, 112	sylancl 417	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
114		5re 9386	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
115		resubcl 8592	. . . . . . . . . 10 ⊢ ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
116	113, 114, 115	sylancl 417	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
117		remulcl 8308	. . . . . . . . 9 ⊢ (((((4 · 𝑁) / 3) − 5) ∈ ℝ ∧ (log‘2) ∈ ℝ) → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
118	116, 79, 117	sylancl 417	. . . . . . . 8 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
119	108, 118	readdcld 8356	. . . . . . 7 ⊢ (𝜑 → (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ∈ ℝ)
120		remulcl 8308	. . . . . . . . 9 ⊢ ((((4 · 𝑁) / 3) ∈ ℝ ∧ (log‘2) ∈ ℝ) → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
121	113, 79, 120	sylancl 417	. . . . . . . 8 ⊢ (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
122	121, 95	resubcld 8710	. . . . . . 7 ⊢ (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℝ)
123	8	nnzd 9772	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℤ)
124		df-5 9369	. . . . . . . . . . . 12 ⊢ 5 = (4 + 1)
125	109	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 ∈ ℝ)
126		6nn 9475	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℕ
127		4nn0 9587	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ0
128		4lt10 9922	. . . . . . . . . . . . . . . 16 ⊢ 4 < ;10
129	126, 127, 127, 128	declti 9824	. . . . . . . . . . . . . . 15 ⊢ 4 < ;64
130	129	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 < ;64)
131	125, 35, 36, 130, 1	lttrd 8454	. . . . . . . . . . . . 13 ⊢ (𝜑 → 4 < 𝑁)
132		4z 9679	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℤ
133		zltp1le 9704	. . . . . . . . . . . . . 14 ⊢ ((4 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
134	132, 123, 133	sylancr 418	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
135	131, 134	mpbid 147	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 + 1) ≤ 𝑁)
136	124, 135	eqbrtrid 4165	. . . . . . . . . . 11 ⊢ (𝜑 → 5 ≤ 𝑁)
137		5nn 9474	. . . . . . . . . . . . 13 ⊢ 5 ∈ ℕ
138	137	nnzi 9670	. . . . . . . . . . . 12 ⊢ 5 ∈ ℤ
139	138	eluz1i 9939	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ≥‘5) ↔ (𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
140	123, 136, 139	sylanbrc 421	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5))
141		bposlem9.5	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
142		breq2 4134	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑁 < 𝑝 ↔ 𝑁 < 𝑞))
143		breq1 4133	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑝 ≤ (2 · 𝑁) ↔ 𝑞 ≤ (2 · 𝑁)))
144	142, 143	anbi12d 477	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑞 → ((𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁))))
145	144	cbvrexvw 2791	. . . . . . . . . . 11 ⊢ (∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ ∃𝑞 ∈ ℙ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁)))
146	141, 145	sylnib 687	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ∃𝑞 ∈ ℙ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁)))
147		eqid 2238	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
148		eqid 2238	. . . . . . . . . 10 ⊢ (⌊‘((2 · 𝑁) / 3)) = (⌊‘((2 · 𝑁) / 3))
149		eqid 2238	. . . . . . . . . 10 ⊢ (⌊‘(√‘(2 · 𝑁))) = (⌊‘(√‘(2 · 𝑁)))
150	140, 146, 147, 148, 149	bposlem6 16245	. . . . . . . . 9 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
151		reexplog 16033	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
152	90, 123, 151	sylancr 418	. . . . . . . . . . 11 ⊢ (𝜑 → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
153	62	reeflogd 16045	. . . . . . . . . . . 12 ⊢ (𝜑 → (exp‘(log‘𝑁)) = 𝑁)
154	153	eqcomd 2244	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 = (exp‘(log‘𝑁)))
155	152, 154	oveq12d 6103	. . . . . . . . . 10 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
156	94	recnd 8355	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · (log‘4)) ∈ ℂ)
157	95	recnd 8355	. . . . . . . . . . 11 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
158		efsub 12467	. . . . . . . . . . 11 ⊢ (((𝑁 · (log‘4)) ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
159	156, 157, 158	syl2anc 415	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
160	155, 159	eqtr4d 2274	. . . . . . . . 9 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) = (exp‘((𝑁 · (log‘4)) − (log‘𝑁))))
161	106	recnd 8355	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℂ)
162		rpcxpef 16059	. . . . . . . . . . . 12 ⊢ (((2 · 𝑁) ∈ ℝ+ ∧ (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℂ) → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) = (exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))))
163	82, 161, 162	syl2anc 415	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) = (exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))))
164	116	recnd 8355	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℂ)
165		rpcxpef 16059	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ+ ∧ (((4 · 𝑁) / 3) − 5) ∈ ℂ) → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
166	77, 164, 165	sylancr 418	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
167	163, 166	oveq12d 6103	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
168	108	recnd 8355	. . . . . . . . . . 11 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℂ)
169	118	recnd 8355	. . . . . . . . . . 11 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℂ)
170		efadd 12461	. . . . . . . . . . 11 ⊢ ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℂ ∧ ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℂ) → (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
171	168, 169, 170	syl2anc 415	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
172	167, 171	eqtr4d 2274	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
173	150, 160, 172	3brtr3d 4161	. . . . . . . 8 ⊢ (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
174		eflt 15935	. . . . . . . . 9 ⊢ ((((𝑁 · (log‘4)) − (log‘𝑁)) ∈ ℝ ∧ (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ∈ ℝ) → (((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ↔ (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))))
175	96, 119, 174	syl2anc 415	. . . . . . . 8 ⊢ (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ↔ (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))))
176	173, 175	mpbird 167	. . . . . . 7 ⊢ (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))
177	96, 119, 122, 176	ltsub1dd 8887	. . . . . 6 ⊢ (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) < ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
178		2cn 9378	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
179	36	recnd 8355	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
180		mulcom 8309	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) = (𝑁 · 2))
181	178, 179, 180	sylancr 418	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑁) = (𝑁 · 2))
182	181	oveq1d 6100	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝑁) · (log‘2)) = ((𝑁 · 2) · (log‘2)))
183	79	recni 8339	. . . . . . . . . . . 12 ⊢ (log‘2) ∈ ℂ
184		mulass 8311	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ (log‘2) ∈ ℂ) → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
185	178, 183, 184	mp3an23 1370	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℂ → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
186	179, 185	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
187	183	2timesi 9437	. . . . . . . . . . . 12 ⊢ (2 · (log‘2)) = ((log‘2) + (log‘2))
188		relogmul 16031	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(2 · 2)) = ((log‘2) + (log‘2)))
189	77, 77, 188	mp2an 430	. . . . . . . . . . . 12 ⊢ (log‘(2 · 2)) = ((log‘2) + (log‘2))
190		2t2e4 9462	. . . . . . . . . . . . 13 ⊢ (2 · 2) = 4
191	190	fveq2i 5698	. . . . . . . . . . . 12 ⊢ (log‘(2 · 2)) = (log‘4)
192	187, 189, 191	3eqtr2i 2265	. . . . . . . . . . 11 ⊢ (2 · (log‘2)) = (log‘4)
193	192	oveq2i 6096	. . . . . . . . . 10 ⊢ (𝑁 · (2 · (log‘2))) = (𝑁 · (log‘4))
194	186, 193	eqtrdi 2287	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (log‘4)))
195	182, 194	eqtrd 2271	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝑁) · (log‘2)) = (𝑁 · (log‘4)))
196	195	oveq1d 6100	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
197	113	recnd 8355	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝑁) / 3) ∈ ℂ)
198		3rp 10071	. . . . . . . . . . . 12 ⊢ 3 ∈ ℝ+
199		rpdivcl 10091	. . . . . . . . . . . 12 ⊢ (((2 · 𝑁) ∈ ℝ+ ∧ 3 ∈ ℝ+) → ((2 · 𝑁) / 3) ∈ ℝ+)
200	82, 198, 199	sylancl 417	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ+)
201	200	rpcnd 10110	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℂ)
202		4p2e6 9451	. . . . . . . . . . . . . 14 ⊢ (4 + 2) = 6
203	202	oveq1i 6095	. . . . . . . . . . . . 13 ⊢ ((4 + 2) · 𝑁) = (6 · 𝑁)
204		4cn 9385	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℂ
205		adddir 8318	. . . . . . . . . . . . . 14 ⊢ ((4 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
206	204, 178, 179, 205	mp3an12i 1382	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
207	203, 206	eqtr3id 2285	. . . . . . . . . . . 12 ⊢ (𝜑 → (6 · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
208	207	oveq1d 6100	. . . . . . . . . . 11 ⊢ (𝜑 → ((6 · 𝑁) / 3) = (((4 · 𝑁) + (2 · 𝑁)) / 3))
209		6cn 9389	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℂ
210		3cn 9382	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℂ
211		3ap0 9403	. . . . . . . . . . . . . . 15 ⊢ 3 # 0
212	210, 211	pm3.2i 272	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℂ ∧ 3 # 0)
213		div23ap 9024	. . . . . . . . . . . . . 14 ⊢ ((6 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 # 0)) → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
214	209, 212, 213	mp3an13 1369	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
215	179, 214	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
216		3t2e6 9464	. . . . . . . . . . . . . . 15 ⊢ (3 · 2) = 6
217	216	oveq1i 6095	. . . . . . . . . . . . . 14 ⊢ ((3 · 2) / 3) = (6 / 3)
218	178, 210, 211	divcanap3i 9091	. . . . . . . . . . . . . 14 ⊢ ((3 · 2) / 3) = 2
219	217, 218	eqtr3i 2261	. . . . . . . . . . . . 13 ⊢ (6 / 3) = 2
220	219	oveq1i 6095	. . . . . . . . . . . 12 ⊢ ((6 / 3) · 𝑁) = (2 · 𝑁)
221	215, 220	eqtrdi 2287	. . . . . . . . . . 11 ⊢ (𝜑 → ((6 · 𝑁) / 3) = (2 · 𝑁))
222	111	recnd 8355	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 · 𝑁) ∈ ℂ)
223		remulcl 8308	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
224	104, 36, 223	sylancr 418	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ)
225	224	recnd 8355	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
226		divdirap 9030	. . . . . . . . . . . . 13 ⊢ (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 # 0)) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
227	212, 226	mp3an3 1367	. . . . . . . . . . . 12 ⊢ (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
228	222, 225, 227	syl2anc 415	. . . . . . . . . . 11 ⊢ (𝜑 → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
229	208, 221, 228	3eqtr3d 2279	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑁) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
230	197, 201, 229	mvrladdd 8695	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
231	230	oveq1d 6100	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) / 3) · (log‘2)))
232	80	recnd 8355	. . . . . . . . 9 ⊢ (𝜑 → (log‘2) ∈ ℂ)
233	225, 197, 232	subdird 8744	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
234	231, 233	eqtr3d 2273	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
235	121	recnd 8355	. . . . . . . 8 ⊢ (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℂ)
236	156, 235, 157	nnncan2d 8674	. . . . . . 7 ⊢ (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
237	196, 234, 236	3eqtr4d 2281	. . . . . 6 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
238	103	recnd 8355	. . . . . . . . . 10 ⊢ (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℂ)
239	178	a1i 9	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℂ)
240	107	recnd 8355	. . . . . . . . . 10 ⊢ (𝜑 → (log‘(2 · 𝑁)) ∈ ℂ)
241	238, 239, 240	adddird 8352	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))))
242		relogmul 16031	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+) → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
243	77, 62, 242	sylancr 418	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
244	243	oveq2d 6101	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (log‘(2 · 𝑁))) = (2 · ((log‘2) + (log‘𝑁))))
245	239, 232, 157	adddid 8351	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((log‘2) + (log‘𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
246	244, 245	eqtrd 2271	. . . . . . . . . 10 ⊢ (𝜑 → (2 · (log‘(2 · 𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
247	246	oveq2d 6101	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
248	241, 247	eqtrd 2271	. . . . . . . 8 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
249		5cn 9387	. . . . . . . . . . . 12 ⊢ 5 ∈ ℂ
250	249	a1i 9	. . . . . . . . . . 11 ⊢ (𝜑 → 5 ∈ ℂ)
251	197, 250, 232	subdird 8744	. . . . . . . . . 10 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) = ((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))))
252	251	oveq1d 6100	. . . . . . . . 9 ⊢ (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
253	249, 183	mulcli 8332	. . . . . . . . . . 11 ⊢ (5 · (log‘2)) ∈ ℂ
254	253	a1i 9	. . . . . . . . . 10 ⊢ (𝜑 → (5 · (log‘2)) ∈ ℂ)
255	235, 254, 157	nnncan1d 8673	. . . . . . . . 9 ⊢ (𝜑 → (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
256	252, 255	eqtrd 2271	. . . . . . . 8 ⊢ (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
257	248, 256	oveq12d 6103	. . . . . . 7 ⊢ (𝜑 → (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)))) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))))
258	122	recnd 8355	. . . . . . . 8 ⊢ (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℂ)
259	168, 169, 258	addsubassd 8659	. . . . . . 7 ⊢ (𝜑 → ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)))))
260	249, 210, 183	subdiri 8737	. . . . . . . . . . . . 13 ⊢ ((5 − 3) · (log‘2)) = ((5 · (log‘2)) − (3 · (log‘2)))
261		3p2e5 9449	. . . . . . . . . . . . . . . 16 ⊢ (3 + 2) = 5
262	261	oveq1i 6095	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 3) = (5 − 3)
263		pncan2 8535	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
264	210, 178, 263	mp2an 430	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 3) = 2
265	262, 264	eqtr3i 2261	. . . . . . . . . . . . . 14 ⊢ (5 − 3) = 2
266	265	oveq1i 6095	. . . . . . . . . . . . 13 ⊢ ((5 − 3) · (log‘2)) = (2 · (log‘2))
267	260, 266	eqtr3i 2261	. . . . . . . . . . . 12 ⊢ ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2))
268	267	a1i 9	. . . . . . . . . . 11 ⊢ (𝜑 → ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2)))
269		mulcl 8307	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (2 · (log‘𝑁)) ∈ ℂ)
270	178, 157, 269	sylancr 418	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · (log‘𝑁)) ∈ ℂ)
271		df-3 9367	. . . . . . . . . . . . . . . 16 ⊢ 3 = (2 + 1)
272	271	oveq1i 6095	. . . . . . . . . . . . . . 15 ⊢ (3 · (log‘𝑁)) = ((2 + 1) · (log‘𝑁))
273		1cnd 8343	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℂ)
274	239, 273, 157	adddird 8352	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 + 1) · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
275	272, 274	eqtrid 2283	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
276	157	mullidd 8345	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · (log‘𝑁)) = (log‘𝑁))
277	276	oveq2d 6101	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (log‘𝑁)) + (1 · (log‘𝑁))) = ((2 · (log‘𝑁)) + (log‘𝑁)))
278	275, 277	eqtrd 2271	. . . . . . . . . . . . 13 ⊢ (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (log‘𝑁)))
279	278	oveq1d 6100	. . . . . . . . . . . 12 ⊢ (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))))
280	270, 157, 254, 279	assraddsubd 8696	. . . . . . . . . . 11 ⊢ (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
281	268, 280	oveq12d 6103	. . . . . . . . . 10 ⊢ (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
282		relogdiv 16032	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
283	62, 77, 282	sylancl 417	. . . . . . . . . . . . 13 ⊢ (𝜑 → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
284	283	oveq2d 6101	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘(𝑁 / 2))) = (3 · ((log‘𝑁) − (log‘2))))
285		subdi 8714	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
286	210, 183, 285	mp3an13 1369	. . . . . . . . . . . . 13 ⊢ ((log‘𝑁) ∈ ℂ → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
287	157, 286	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
288	284, 287	eqtrd 2271	. . . . . . . . . . 11 ⊢ (𝜑 → (3 · (log‘(𝑁 / 2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
289		div23ap 9024	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 # 0)) → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
290	178, 212, 289	mp3an13 1369	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℂ → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
291	179, 290	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
292		2ap0 9400	. . . . . . . . . . . . . . . . . 18 ⊢ 2 # 0
293	210, 178, 210, 178, 292, 292	divmuldivapi 9105	. . . . . . . . . . . . . . . . 17 ⊢ ((3 / 2) · (3 / 2)) = ((3 · 3) / (2 · 2))
294		3t3e9 9466	. . . . . . . . . . . . . . . . . 18 ⊢ (3 · 3) = 9
295	294, 190	oveq12i 6097	. . . . . . . . . . . . . . . . 17 ⊢ ((3 · 3) / (2 · 2)) = (9 / 4)
296	293, 295	eqtr2i 2260	. . . . . . . . . . . . . . . 16 ⊢ (9 / 4) = ((3 / 2) · (3 / 2))
297	296	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (9 / 4) = ((3 / 2) · (3 / 2)))
298	291, 297	oveq12d 6103	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))))
299	178, 210, 211	divclapi 9087	. . . . . . . . . . . . . . 15 ⊢ (2 / 3) ∈ ℂ
300	210, 178, 292	divclapi 9087	. . . . . . . . . . . . . . . 16 ⊢ (3 / 2) ∈ ℂ
301		mul4 8460	. . . . . . . . . . . . . . . 16 ⊢ ((((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ ((3 / 2) ∈ ℂ ∧ (3 / 2) ∈ ℂ)) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
302	300, 300, 301	mpanr12 443	. . . . . . . . . . . . . . 15 ⊢ (((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
303	299, 179, 302	sylancr 418	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
304		divcanap6 9052	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 ∈ ℂ ∧ 2 # 0) ∧ (3 ∈ ℂ ∧ 3 # 0)) → ((2 / 3) · (3 / 2)) = 1)
305	178, 292, 210, 211, 304	mp4an 431	. . . . . . . . . . . . . . . . 17 ⊢ ((2 / 3) · (3 / 2)) = 1
306	305	oveq1i 6095	. . . . . . . . . . . . . . . 16 ⊢ (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (1 · (𝑁 · (3 / 2)))
307		mulcl 8307	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℂ ∧ (3 / 2) ∈ ℂ) → (𝑁 · (3 / 2)) ∈ ℂ)
308	179, 300, 307	sylancl 417	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 · (3 / 2)) ∈ ℂ)
309	308	mullidd 8345	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
310	306, 309	eqtrid 2283	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
311	178, 292	pm3.2i 272	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ ℂ ∧ 2 # 0)
312		div12ap 9027	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℂ ∧ 3 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 # 0)) → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
313	210, 311, 312	mp3an23 1370	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℂ → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
314	179, 313	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
315	310, 314	eqtrd 2271	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (3 · (𝑁 / 2)))
316	298, 303, 315	3eqtrd 2275	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (3 · (𝑁 / 2)))
317		fveq2 5695	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑁 / 2) → (log‘𝑥) = (log‘(𝑁 / 2)))
318		id 19	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑁 / 2) → 𝑥 = (𝑁 / 2))
319	317, 318	oveq12d 6103	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑁 / 2) → ((log‘𝑥) / 𝑥) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
320	73	relogcld 16044	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (log‘(𝑁 / 2)) ∈ ℝ)
321	320, 73	rerpdivcld 10140	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℝ)
322	3, 319, 73, 321	fvmptd3 5799	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
323	316, 322	oveq12d 6103	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))))
324		9re 9394	. . . . . . . . . . . . . . . 16 ⊢ 9 ∈ ℝ
325		4ap0 9406	. . . . . . . . . . . . . . . 16 ⊢ 4 # 0
326	324, 109, 325	redivclapi 9112	. . . . . . . . . . . . . . 15 ⊢ (9 / 4) ∈ ℝ
327	326	recni 8339	. . . . . . . . . . . . . 14 ⊢ (9 / 4) ∈ ℂ
328	327	a1i 9	. . . . . . . . . . . . 13 ⊢ (𝜑 → (9 / 4) ∈ ℂ)
329	322, 321	eqeltrd 2315	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℝ)
330	329	recnd 8355	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℂ)
331	201, 328, 330	mulassd 8350	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))
332	210	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 3 ∈ ℂ)
333	73	rpcnd 10110	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 2) ∈ ℂ)
334	320	recnd 8355	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (log‘(𝑁 / 2)) ∈ ℂ)
335	73	rpap0d 10114	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 / 2) # 0)
336	334, 333, 335	divclapd 9123	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℂ)
337	332, 333, 336	mulassd 8350	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))))
338	334, 333, 335	divcanap2d 9125	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (log‘(𝑁 / 2)))
339	338	oveq2d 6101	. . . . . . . . . . . . 13 ⊢ (𝜑 → (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
340	337, 339	eqtrd 2271	. . . . . . . . . . . 12 ⊢ (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · (log‘(𝑁 / 2))))
341	323, 331, 340	3eqtr3d 2279	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
342	210, 183	mulcli 8332	. . . . . . . . . . . . 13 ⊢ (3 · (log‘2)) ∈ ℂ
343	342	a1i 9	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘2)) ∈ ℂ)
344		mulcl 8307	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (3 · (log‘𝑁)) ∈ ℂ)
345	210, 157, 344	sylancr 418	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘𝑁)) ∈ ℂ)
346	254, 343, 345	npncan3d 8675	. . . . . . . . . . 11 ⊢ (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
347	288, 341, 346	3eqtr4d 2281	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))))
348	104, 79	remulcli 8341	. . . . . . . . . . . . 13 ⊢ (2 · (log‘2)) ∈ ℝ
349	348	recni 8339	. . . . . . . . . . . 12 ⊢ (2 · (log‘2)) ∈ ℂ
350	349	a1i 9	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (log‘2)) ∈ ℂ)
351		subcl 8527	. . . . . . . . . . . 12 ⊢ (((log‘𝑁) ∈ ℂ ∧ (5 · (log‘2)) ∈ ℂ) → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
352	157, 253, 351	sylancl 417	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
353	350, 270, 352	addassd 8349	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
354	281, 347, 353	3eqtr4d 2281	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))))
355	354	oveq2d 6101	. . . . . . . 8 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2))))))
356		mulcl 8307	. . . . . . . . . . 11 ⊢ ((((√‘(2 · 𝑁)) / 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
357	238, 183, 356	sylancl 417	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
358	238, 157	mulcld 8347	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) ∈ ℂ)
359		remulcl 8308	. . . . . . . . . . . . 13 ⊢ (((9 / 4) ∈ ℝ ∧ (𝐺‘(𝑁 / 2)) ∈ ℝ) → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
360	326, 329, 359	sylancr 418	. . . . . . . . . . . 12 ⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
361	360	recnd 8355	. . . . . . . . . . 11 ⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℂ)
362	201, 361	mulcld 8347	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
363	357, 358, 362	addassd 8349	. . . . . . . . 9 ⊢ (𝜑 → (((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
364	243	oveq2d 6101	. . . . . . . . . . 11 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))))
365	238, 232, 157	adddid 8351	. . . . . . . . . . 11 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
366	364, 365	eqtrd 2271	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
367	366	oveq1d 6100	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
368	86	oveq2d 6101	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))))
369		fveq2 5695	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (√‘𝑁) → (log‘𝑥) = (log‘(√‘𝑁)))
370		id 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (√‘𝑁) → 𝑥 = (√‘𝑁))
371	369, 370	oveq12d 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (√‘𝑁) → ((log‘𝑥) / 𝑥) = ((log‘(√‘𝑁)) / (√‘𝑁)))
372	63	relogcld 16044	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘(√‘𝑁)) ∈ ℝ)
373	372, 63	rerpdivcld 10140	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ ℝ)
374	3, 371, 63, 373	fvmptd3 5799	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
375	374, 373	eqeltrd 2315	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℝ)
376		remulcl 8308	. . . . . . . . . . . . . . 15 ⊢ (((√‘2) ∈ ℝ ∧ (𝐺‘(√‘𝑁)) ∈ ℝ) → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
377	55, 375, 376	sylancr 418	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
378	377, 360	readdcld 8356	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℝ)
379	378	recnd 8355	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
380		rerpdivcl 10096	. . . . . . . . . . . . . 14 ⊢ (((log‘2) ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ+) → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
381	79, 83, 380	sylancr 418	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
382	381	recnd 8355	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℂ)
383	201, 379, 382	adddid 8351	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
384	368, 383	eqtrd 2271	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
385	377	recnd 8355	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℂ)
386	201, 385, 361	adddid 8351	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
387	82	rpge0d 10112	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ≤ (2 · 𝑁))
388		remsqsqrt 11814	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
389	224, 387, 388	syl2anc 415	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
390	389	oveq1d 6100	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = ((2 · 𝑁) / 3))
391	100	recnd 8355	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℂ)
392	211	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 # 0)
393	391, 391, 332, 392	div23apd 9161	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
394	390, 393	eqtr3d 2273	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · 𝑁) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
395	394	oveq1d 6100	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))))
396	238, 391, 385	mulassd 8350	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))))
397		0le2 9397	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ≤ 2
398	104, 397	pm3.2i 272	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℝ ∧ 0 ≤ 2)
399	62	rprege0d 10116	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
400		sqrtmul 11817	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
401	398, 399, 400	sylancr 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
402	401	oveq1d 6100	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))))
403	55	recni 8339	. . . . . . . . . . . . . . . . . 18 ⊢ (√‘2) ∈ ℂ
404	403	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘2) ∈ ℂ)
405	63	rpcnd 10110	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘𝑁) ∈ ℂ)
406	375	recnd 8355	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℂ)
407	404, 405, 404, 406	mul4d 8483	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))))
408		remsqsqrt 11814	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
409	104, 397, 408	mp2an 430	. . . . . . . . . . . . . . . . . . 19 ⊢ ((√‘2) · (√‘2)) = 2
410	409	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((√‘2) · (√‘2)) = 2)
411	374	oveq2d 6101	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))))
412	372	recnd 8355	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (log‘(√‘𝑁)) ∈ ℂ)
413	63	rpap0d 10114	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑁) # 0)
414	412, 405, 413	divcanap2d 9125	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))) = (log‘(√‘𝑁)))
415	411, 414	eqtrd 2271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = (log‘(√‘𝑁)))
416	410, 415	oveq12d 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (2 · (log‘(√‘𝑁))))
417	412	2timesd 9553	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (log‘(√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
418	63, 63	relogmuld 16046	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
419		remsqsqrt 11814	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
420	399, 419	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
421	420	fveq2d 5699	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = (log‘𝑁))
422	418, 421	eqtr3d 2273	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘(√‘𝑁)) + (log‘(√‘𝑁))) = (log‘𝑁))
423	416, 417, 422	3eqtrd 2275	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
424	402, 407, 423	3eqtrd 2275	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
425	424	oveq2d 6101	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
426	395, 396, 425	3eqtrd 2275	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
427	426	oveq1d 6100	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
428	386, 427	eqtrd 2271	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
429	394	oveq1d 6100	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))))
430	238, 391, 382	mulassd 8350	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))))
431	83	rpap0d 10114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (√‘(2 · 𝑁)) # 0)
432	232, 391, 431	divcanap2d 9125	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁)))) = (log‘2))
433	432	oveq2d 6101	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
434	429, 430, 433	3eqtrd 2275	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
435	428, 434	oveq12d 6103	. . . . . . . . . 10 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((√‘(2 · 𝑁)) / 3) · (log‘2))))
436	358, 362	addcld 8346	. . . . . . . . . . 11 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) ∈ ℂ)
437	436, 357	addcomd 8479	. . . . . . . . . 10 ⊢ (𝜑 → (((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((√‘(2 · 𝑁)) / 3) · (log‘2))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
438	384, 435, 437	3eqtrd 2275	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
439	363, 367, 438	3eqtr4rd 2282	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
440	238, 240	mulcld 8347	. . . . . . . . 9 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) ∈ ℂ)
441		addcl 8305	. . . . . . . . . 10 ⊢ (((2 · (log‘2)) ∈ ℂ ∧ (2 · (log‘𝑁)) ∈ ℂ) → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
442	349, 270, 441	sylancr 418	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
443	440, 442, 352	addassd 8349	. . . . . . . 8 ⊢ (𝜑 → (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2))))))
444	355, 439, 443	3eqtr4d 2281	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))))
445	257, 259, 444	3eqtr4rd 2282	. . . . . 6 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
446	177, 237, 445	3brtr4d 4162	. . . . 5 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹‘𝑁)))
447	80, 87, 200	ltmul2d 10151	. . . . 5 ⊢ (𝜑 → ((log‘2) < (𝐹‘𝑁) ↔ (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹‘𝑁))))
448	446, 447	mpbird 167	. . . 4 ⊢ (𝜑 → (log‘2) < (𝐹‘𝑁))
449	45, 80, 87, 88, 448	lttrd 8454	. . 3 ⊢ (𝜑 → (𝐹‘;64) < (𝐹‘𝑁))
450	45, 87, 449	ltnsymd 8448	. 2 ⊢ (𝜑 → ¬ (𝐹‘𝑁) < (𝐹‘;64))
451	42, 450	pm2.21dd 629	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ∃wrex 2529  ifcif 3638   class class class wbr 4130   ↦ cmpt 4192  ‘cfv 5377  (class class class)co 6085  ℂcc 8178  ℝcr 8179  0cc0 8180  1c1 8181   + caddc 8183   · cmul 8185   < clt 8361   ≤ cle 8362   − cmin 8499   # cap 8912   / cdiv 9005  ℕcn 9307  2c2 9358  3c3 9359  4c4 9360  5c5 9361  6c6 9362  8c8 9364  9c9 9365  ℤcz 9649  ;cdc 9782  ℤ_≥cuz 9931  ℚcq 10029  ℝ⁺crp 10065  ⌊cfl 10714  ↑cexp 10990  Ccbc 11201  √csqrt 11778  expce 12428  eceu 12429  ℙcprime 12904   pCnt cpc 13086  logclog 16017  ↑_𝑐ccxp 16018

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735  ax-cnex 8271  ax-resscn 8272  ax-1cn 8273  ax-1re 8274  ax-icn 8275  ax-addcl 8276  ax-addrcl 8277  ax-mulcl 8278  ax-mulrcl 8279  ax-addcom 8280  ax-mulcom 8281  ax-addass 8282  ax-mulass 8283  ax-distr 8284  ax-i2m1 8285  ax-0lt1 8286  ax-1rid 8287  ax-0id 8288  ax-rnegex 8289  ax-precex 8290  ax-cnre 8291  ax-pre-ltirr 8292  ax-pre-ltwlin 8293  ax-pre-lttrn 8294  ax-pre-apti 8295  ax-pre-ltadd 8296  ax-pre-mulgt0 8297  ax-pre-mulext 8298  ax-arch 8299  ax-caucvg 8300  ax-pre-suploc 8301  ax-addf 8302  ax-mulf 8303

This proof depends on definitions:  df-bi 117  df-stab 843  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-disj 4107  df-br 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-id 4438  df-po 4441  df-iso 4442  df-iord 4511  df-on 4513  df-ilim 4514  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-isom 5386  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-of 6302  df-1st 6374  df-2nd 6375  df-recs 6576  df-irdg 6641  df-frec 6662  df-1o 6687  df-2o 6688  df-oadd 6691  df-er 6807  df-map 6924  df-pm 6925  df-en 7023  df-dom 7024  df-fin 7025  df-sup 7325  df-inf 7326  df-pnf 8363  df-mnf 8364  df-xr 8365  df-ltxr 8366  df-le 8367  df-sub 8501  df-neg 8502  df-reap 8906  df-ap 8913  df-div 9006  df-inn 9308  df-2 9366  df-3 9367  df-4 9368  df-5 9369  df-6 9370  df-7 9371  df-8 9372  df-9 9373  df-n0 9569  df-xnn0 9636  df-z 9650  df-dec 9783  df-uz 9932  df-q 10030  df-rp 10066  df-xneg 10185  df-xadd 10186  df-ioo 10305  df-ico 10307  df-icc 10308  df-fz 10423  df-fzo 10561  df-fl 10716  df-mod 10775  df-seqfrec 10900  df-exp 10991  df-fac 11180  df-bc 11202  df-ihash 11231  df-shft 11596  df-cj 11623  df-re 11624  df-im 11625  df-rsqrt 11780  df-abs 11781  df-clim 12064  df-sumdc 12139  df-ef 12434  df-e 12435  df-dvds 12574  df-gcd 12750  df-prm 12905  df-numer 12982  df-denom 12983  df-pc 13087  df-rest 13647  df-topgen 13666  df-psmet 14932  df-xmet 14933  df-met 14934  df-bl 14935  df-mopn 14936  df-top 15158  df-topon 15171  df-bases 15203  df-ntr 15256  df-cn 15348  df-cnp 15349  df-tx 15413  df-cncf 15731  df-limced 15816  df-dvap 15817  df-relog 16019  df-rpcxp 16020  df-logb 16109  df-cht 16165  df-ppi 16166

This theorem is used by:  bpos  16249