Theorem bposlem9 25017

Description: Lemma for bpos 25018. 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 11313	. . . . . 6 ⊢ 6 ∈ ℕ0
5		4nn 11187	. . . . . 6 ⊢ 4 ∈ ℕ
6	4, 5	decnncl 11518	. . . . 5 ⊢ ;64 ∈ ℕ
7	6	a1i 11	. . . 4 ⊢ (𝜑 → ;64 ∈ ℕ)
8		bposlem9.3	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
9		ere 14819	. . . . . . . 8 ⊢ e ∈ ℝ
10		8re 11105	. . . . . . . 8 ⊢ 8 ∈ ℝ
11		egt2lt3 14934	. . . . . . . . . 10 ⊢ (2 < e ∧ e < 3)
12	11	simpri 478	. . . . . . . . 9 ⊢ e < 3
13		3lt8 11219	. . . . . . . . 9 ⊢ 3 < 8
14		3re 11094	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
15	9, 14, 10	lttri 10163	. . . . . . . . 9 ⊢ ((e < 3 ∧ 3 < 8) → e < 8)
16	12, 13, 15	mp2an 708	. . . . . . . 8 ⊢ e < 8
17	9, 10, 16	ltleii 10160	. . . . . . 7 ⊢ e ≤ 8
18		0re 10040	. . . . . . . . 9 ⊢ 0 ∈ ℝ
19		epos 14935	. . . . . . . . 9 ⊢ 0 < e
20	18, 9, 19	ltleii 10160	. . . . . . . 8 ⊢ 0 ≤ e
21		8pos 11121	. . . . . . . . 9 ⊢ 0 < 8
22	18, 10, 21	ltleii 10160	. . . . . . . 8 ⊢ 0 ≤ 8
23		le2sq 12938	. . . . . . . 8 ⊢ (((e ∈ ℝ ∧ 0 ≤ e) ∧ (8 ∈ ℝ ∧ 0 ≤ 8)) → (e ≤ 8 ↔ (e↑2) ≤ (8↑2)))
24	9, 20, 10, 22, 23	mp4an 709	. . . . . . 7 ⊢ (e ≤ 8 ↔ (e↑2) ≤ (8↑2))
25	17, 24	mpbi 220	. . . . . 6 ⊢ (e↑2) ≤ (8↑2)
26	10	recni 10052	. . . . . . . 8 ⊢ 8 ∈ ℂ
27	26	sqvali 12943	. . . . . . 7 ⊢ (8↑2) = (8 · 8)
28		8t8e64 11662	. . . . . . 7 ⊢ (8 · 8) = ;64
29	27, 28	eqtri 2644	. . . . . 6 ⊢ (8↑2) = ;64
30	25, 29	breqtri 4678	. . . . 5 ⊢ (e↑2) ≤ ;64
31	30	a1i 11	. . . 4 ⊢ (𝜑 → (e↑2) ≤ ;64)
32	9	resqcli 12949	. . . . . 6 ⊢ (e↑2) ∈ ℝ
33	32	a1i 11	. . . . 5 ⊢ (𝜑 → (e↑2) ∈ ℝ)
34	6	nnrei 11029	. . . . . 6 ⊢ ;64 ∈ ℝ
35	34	a1i 11	. . . . 5 ⊢ (𝜑 → ;64 ∈ ℝ)
36	8	nnred 11035	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℝ)
37		ltle 10126	. . . . . . 7 ⊢ ((;64 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (;64 < 𝑁 → ;64 ≤ 𝑁))
38	34, 36, 37	sylancr 695	. . . . . 6 ⊢ (𝜑 → (;64 < 𝑁 → ;64 ≤ 𝑁))
39	1, 38	mpd 15	. . . . 5 ⊢ (𝜑 → ;64 ≤ 𝑁)
40	33, 35, 36, 31, 39	letrd 10194	. . . 4 ⊢ (𝜑 → (e↑2) ≤ 𝑁)
41	2, 3, 7, 8, 31, 40	bposlem7 25015	. . 3 ⊢ (𝜑 → (;64 < 𝑁 → (𝐹‘𝑁) < (𝐹‘;64)))
42	1, 41	mpd 15	. 2 ⊢ (𝜑 → (𝐹‘𝑁) < (𝐹‘;64))
43	2, 3	bposlem8 25016	. . . . 5 ⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2))
44	43	a1i 11	. . . 4 ⊢ (𝜑 → ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2)))
45	44	simpld 475	. . 3 ⊢ (𝜑 → (𝐹‘;64) ∈ ℝ)
46		fveq2 6191	. . . . . . . . . 10 ⊢ (𝑛 = 𝑁 → (√‘𝑛) = (√‘𝑁))
47	46	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (𝐺‘(√‘𝑛)) = (𝐺‘(√‘𝑁)))
48	47	oveq2d 6666	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · (𝐺‘(√‘𝑁))))
49		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑛 = 𝑁 → (𝑛 / 2) = (𝑁 / 2))
50	49	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (𝐺‘(𝑛 / 2)) = (𝐺‘(𝑁 / 2)))
51	50	oveq2d 6666	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · (𝐺‘(𝑁 / 2))))
52	48, 51	oveq12d 6668	. . . . . . 7 ⊢ (𝑛 = 𝑁 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))))
53		oveq2 6658	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
54	53	fveq2d 6195	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → (√‘(2 · 𝑛)) = (√‘(2 · 𝑁)))
55	54	oveq2d 6666	. . . . . . 7 ⊢ (𝑛 = 𝑁 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / (√‘(2 · 𝑁))))
56	52, 55	oveq12d 6668	. . . . . 6 ⊢ (𝑛 = 𝑁 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
57		ovex 6678	. . . . . 6 ⊢ ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ V
58	56, 2, 57	fvmpt 6282	. . . . 5 ⊢ (𝑁 ∈ ℕ → (𝐹‘𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
59	8, 58	syl 17	. . . 4 ⊢ (𝜑 → (𝐹‘𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
60		sqrt2re 14980	. . . . . . 7 ⊢ (√‘2) ∈ ℝ
61	8	nnrpd 11870	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ+)
62	61	rpsqrtcld 14150	. . . . . . . . 9 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ+)
63		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝑥 = (√‘𝑁) → (log‘𝑥) = (log‘(√‘𝑁)))
64		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = (√‘𝑁) → 𝑥 = (√‘𝑁))
65	63, 64	oveq12d 6668	. . . . . . . . . 10 ⊢ (𝑥 = (√‘𝑁) → ((log‘𝑥) / 𝑥) = ((log‘(√‘𝑁)) / (√‘𝑁)))
66		ovex 6678	. . . . . . . . . 10 ⊢ ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ V
67	65, 3, 66	fvmpt 6282	. . . . . . . . 9 ⊢ ((√‘𝑁) ∈ ℝ+ → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
68	62, 67	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
69	62	relogcld 24369	. . . . . . . . 9 ⊢ (𝜑 → (log‘(√‘𝑁)) ∈ ℝ)
70	69, 62	rerpdivcld 11903	. . . . . . . 8 ⊢ (𝜑 → ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ ℝ)
71	68, 70	eqeltrd 2701	. . . . . . 7 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℝ)
72		remulcl 10021	. . . . . . 7 ⊢ (((√‘2) ∈ ℝ ∧ (𝐺‘(√‘𝑁)) ∈ ℝ) → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
73	60, 71, 72	sylancr 695	. . . . . 6 ⊢ (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
74		9re 11107	. . . . . . . 8 ⊢ 9 ∈ ℝ
75		4re 11097	. . . . . . . 8 ⊢ 4 ∈ ℝ
76		4ne0 11117	. . . . . . . 8 ⊢ 4 ≠ 0
77	74, 75, 76	redivcli 10792	. . . . . . 7 ⊢ (9 / 4) ∈ ℝ
78	61	rphalfcld 11884	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 / 2) ∈ ℝ+)
79		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑁 / 2) → (log‘𝑥) = (log‘(𝑁 / 2)))
80		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑁 / 2) → 𝑥 = (𝑁 / 2))
81	79, 80	oveq12d 6668	. . . . . . . . . 10 ⊢ (𝑥 = (𝑁 / 2) → ((log‘𝑥) / 𝑥) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
82		ovex 6678	. . . . . . . . . 10 ⊢ ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ V
83	81, 3, 82	fvmpt 6282	. . . . . . . . 9 ⊢ ((𝑁 / 2) ∈ ℝ+ → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
84	78, 83	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
85	78	relogcld 24369	. . . . . . . . 9 ⊢ (𝜑 → (log‘(𝑁 / 2)) ∈ ℝ)
86	85, 78	rerpdivcld 11903	. . . . . . . 8 ⊢ (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℝ)
87	84, 86	eqeltrd 2701	. . . . . . 7 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℝ)
88		remulcl 10021	. . . . . . 7 ⊢ (((9 / 4) ∈ ℝ ∧ (𝐺‘(𝑁 / 2)) ∈ ℝ) → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
89	77, 87, 88	sylancr 695	. . . . . 6 ⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
90	73, 89	readdcld 10069	. . . . 5 ⊢ (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℝ)
91		2rp 11837	. . . . . . 7 ⊢ 2 ∈ ℝ+
92		relogcl 24322	. . . . . . 7 ⊢ (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
93	91, 92	ax-mp 5	. . . . . 6 ⊢ (log‘2) ∈ ℝ
94		rpmulcl 11855	. . . . . . . 8 ⊢ ((2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+) → (2 · 𝑁) ∈ ℝ+)
95	91, 61, 94	sylancr 695	. . . . . . 7 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ+)
96	95	rpsqrtcld 14150	. . . . . 6 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ+)
97		rerpdivcl 11861	. . . . . 6 ⊢ (((log‘2) ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ+) → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
98	93, 96, 97	sylancr 695	. . . . 5 ⊢ (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
99	90, 98	readdcld 10069	. . . 4 ⊢ (𝜑 → ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ ℝ)
100	59, 99	eqeltrd 2701	. . 3 ⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ)
101	93	a1i 11	. . . 4 ⊢ (𝜑 → (log‘2) ∈ ℝ)
102	44	simprd 479	. . . 4 ⊢ (𝜑 → (𝐹‘;64) < (log‘2))
103		nnrp 11842	. . . . . . . . . . 11 ⊢ (4 ∈ ℕ → 4 ∈ ℝ+)
104	5, 103	ax-mp 5	. . . . . . . . . 10 ⊢ 4 ∈ ℝ+
105		relogcl 24322	. . . . . . . . . 10 ⊢ (4 ∈ ℝ+ → (log‘4) ∈ ℝ)
106	104, 105	ax-mp 5	. . . . . . . . 9 ⊢ (log‘4) ∈ ℝ
107		remulcl 10021	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ (log‘4) ∈ ℝ) → (𝑁 · (log‘4)) ∈ ℝ)
108	36, 106, 107	sylancl 694	. . . . . . . 8 ⊢ (𝜑 → (𝑁 · (log‘4)) ∈ ℝ)
109	61	relogcld 24369	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
110	108, 109	resubcld 10458	. . . . . . 7 ⊢ (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) ∈ ℝ)
111		rpre 11839	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ ℝ+ → (2 · 𝑁) ∈ ℝ)
112		rpge0 11845	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ ℝ+ → 0 ≤ (2 · 𝑁))
113	111, 112	resqrtcld 14156	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) ∈ ℝ+ → (√‘(2 · 𝑁)) ∈ ℝ)
114	95, 113	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
115		3nn 11186	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ
116		nndivre 11056	. . . . . . . . . . 11 ⊢ (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
117	114, 115, 116	sylancl 694	. . . . . . . . . 10 ⊢ (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
118		2re 11090	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
119		readdcl 10019	. . . . . . . . . 10 ⊢ ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
120	117, 118, 119	sylancl 694	. . . . . . . . 9 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
121	95	relogcld 24369	. . . . . . . . 9 ⊢ (𝜑 → (log‘(2 · 𝑁)) ∈ ℝ)
122	120, 121	remulcld 10070	. . . . . . . 8 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℝ)
123		remulcl 10021	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (4 · 𝑁) ∈ ℝ)
124	75, 36, 123	sylancr 695	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · 𝑁) ∈ ℝ)
125		nndivre 11056	. . . . . . . . . . 11 ⊢ (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
126	124, 115, 125	sylancl 694	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
127		5re 11099	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
128		resubcl 10345	. . . . . . . . . 10 ⊢ ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
129	126, 127, 128	sylancl 694	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
130		remulcl 10021	. . . . . . . . 9 ⊢ (((((4 · 𝑁) / 3) − 5) ∈ ℝ ∧ (log‘2) ∈ ℝ) → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
131	129, 93, 130	sylancl 694	. . . . . . . 8 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
132	122, 131	readdcld 10069	. . . . . . 7 ⊢ (𝜑 → (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ∈ ℝ)
133		remulcl 10021	. . . . . . . . 9 ⊢ ((((4 · 𝑁) / 3) ∈ ℝ ∧ (log‘2) ∈ ℝ) → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
134	126, 93, 133	sylancl 694	. . . . . . . 8 ⊢ (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
135	134, 109	resubcld 10458	. . . . . . 7 ⊢ (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℝ)
136	8	nnzd 11481	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℤ)
137		df-5 11082	. . . . . . . . . . . 12 ⊢ 5 = (4 + 1)
138	75	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 ∈ ℝ)
139		6nn 11189	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℕ
140		4nn0 11311	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ0
141		4lt10 11678	. . . . . . . . . . . . . . . 16 ⊢ 4 < ;10
142	139, 140, 140, 141	declti 11546	. . . . . . . . . . . . . . 15 ⊢ 4 < ;64
143	142	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 < ;64)
144	138, 35, 36, 143, 1	lttrd 10198	. . . . . . . . . . . . 13 ⊢ (𝜑 → 4 < 𝑁)
145		4z 11411	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℤ
146		zltp1le 11427	. . . . . . . . . . . . . 14 ⊢ ((4 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
147	145, 136, 146	sylancr 695	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
148	144, 147	mpbid 222	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 + 1) ≤ 𝑁)
149	137, 148	syl5eqbr 4688	. . . . . . . . . . 11 ⊢ (𝜑 → 5 ≤ 𝑁)
150		5nn 11188	. . . . . . . . . . . . 13 ⊢ 5 ∈ ℕ
151	150	nnzi 11401	. . . . . . . . . . . 12 ⊢ 5 ∈ ℤ
152	151	eluz1i 11695	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ≥‘5) ↔ (𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
153	136, 149, 152	sylanbrc 698	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5))
154		bposlem9.5	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
155		breq2 4657	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑁 < 𝑝 ↔ 𝑁 < 𝑞))
156		breq1 4656	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑝 ≤ (2 · 𝑁) ↔ 𝑞 ≤ (2 · 𝑁)))
157	155, 156	anbi12d 747	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑞 → ((𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁))))
158	157	cbvrexv 3172	. . . . . . . . . . 11 ⊢ (∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ ∃𝑞 ∈ ℙ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁)))
159	154, 158	sylnib 318	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ∃𝑞 ∈ ℙ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁)))
160		eqid 2622	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
161		eqid 2622	. . . . . . . . . 10 ⊢ (⌊‘((2 · 𝑁) / 3)) = (⌊‘((2 · 𝑁) / 3))
162		eqid 2622	. . . . . . . . . 10 ⊢ (⌊‘(√‘(2 · 𝑁))) = (⌊‘(√‘(2 · 𝑁)))
163	153, 159, 160, 161, 162	bposlem6 25014	. . . . . . . . 9 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
164		reexplog 24341	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
165	104, 136, 164	sylancr 695	. . . . . . . . . . 11 ⊢ (𝜑 → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
166	61	reeflogd 24370	. . . . . . . . . . . 12 ⊢ (𝜑 → (exp‘(log‘𝑁)) = 𝑁)
167	166	eqcomd 2628	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 = (exp‘(log‘𝑁)))
168	165, 167	oveq12d 6668	. . . . . . . . . 10 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
169	108	recnd 10068	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · (log‘4)) ∈ ℂ)
170	109	recnd 10068	. . . . . . . . . . 11 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
171		efsub 14830	. . . . . . . . . . 11 ⊢ (((𝑁 · (log‘4)) ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
172	169, 170, 171	syl2anc 693	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
173	168, 172	eqtr4d 2659	. . . . . . . . 9 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) = (exp‘((𝑁 · (log‘4)) − (log‘𝑁))))
174	95	rpcnd 11874	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
175	95	rpne0d 11877	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ≠ 0)
176	120	recnd 10068	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℂ)
177	174, 175, 176	cxpefd 24458	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) = (exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))))
178		2cn 11091	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
179		2ne0 11113	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
180	129	recnd 10068	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℂ)
181		cxpef 24411	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ (((4 · 𝑁) / 3) − 5) ∈ ℂ) → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
182	178, 179, 180, 181	mp3an12i 1428	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
183	177, 182	oveq12d 6668	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
184	122	recnd 10068	. . . . . . . . . . 11 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℂ)
185	131	recnd 10068	. . . . . . . . . . 11 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℂ)
186		efadd 14824	. . . . . . . . . . 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)))))
187	184, 185, 186	syl2anc 693	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
188	183, 187	eqtr4d 2659	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
189	163, 173, 188	3brtr3d 4684	. . . . . . . 8 ⊢ (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
190		eflt 14847	. . . . . . . . 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))))))
191	110, 132, 190	syl2anc 693	. . . . . . . 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))))))
192	189, 191	mpbird 247	. . . . . . 7 ⊢ (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))
193	110, 132, 135, 192	ltsub1dd 10639	. . . . . 6 ⊢ (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) < ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
194	36	recnd 10068	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
195		mulcom 10022	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) = (𝑁 · 2))
196	178, 194, 195	sylancr 695	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑁) = (𝑁 · 2))
197	196	oveq1d 6665	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝑁) · (log‘2)) = ((𝑁 · 2) · (log‘2)))
198	93	recni 10052	. . . . . . . . . . . 12 ⊢ (log‘2) ∈ ℂ
199		mulass 10024	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ (log‘2) ∈ ℂ) → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
200	178, 198, 199	mp3an23 1416	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℂ → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
201	194, 200	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
202	198	2timesi 11147	. . . . . . . . . . . 12 ⊢ (2 · (log‘2)) = ((log‘2) + (log‘2))
203		relogmul 24338	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(2 · 2)) = ((log‘2) + (log‘2)))
204	91, 91, 203	mp2an 708	. . . . . . . . . . . 12 ⊢ (log‘(2 · 2)) = ((log‘2) + (log‘2))
205		2t2e4 11177	. . . . . . . . . . . . 13 ⊢ (2 · 2) = 4
206	205	fveq2i 6194	. . . . . . . . . . . 12 ⊢ (log‘(2 · 2)) = (log‘4)
207	202, 204, 206	3eqtr2i 2650	. . . . . . . . . . 11 ⊢ (2 · (log‘2)) = (log‘4)
208	207	oveq2i 6661	. . . . . . . . . 10 ⊢ (𝑁 · (2 · (log‘2))) = (𝑁 · (log‘4))
209	201, 208	syl6eq 2672	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (log‘4)))
210	197, 209	eqtrd 2656	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝑁) · (log‘2)) = (𝑁 · (log‘4)))
211	210	oveq1d 6665	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
212		4p2e6 11162	. . . . . . . . . . . . . . 15 ⊢ (4 + 2) = 6
213	212	oveq1i 6660	. . . . . . . . . . . . . 14 ⊢ ((4 + 2) · 𝑁) = (6 · 𝑁)
214		4cn 11098	. . . . . . . . . . . . . . 15 ⊢ 4 ∈ ℂ
215		adddir 10031	. . . . . . . . . . . . . . 15 ⊢ ((4 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
216	214, 178, 194, 215	mp3an12i 1428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
217	213, 216	syl5eqr 2670	. . . . . . . . . . . . 13 ⊢ (𝜑 → (6 · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
218	217	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (𝜑 → ((6 · 𝑁) / 3) = (((4 · 𝑁) + (2 · 𝑁)) / 3))
219		6cn 11102	. . . . . . . . . . . . . . 15 ⊢ 6 ∈ ℂ
220		3cn 11095	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℂ
221		3ne0 11115	. . . . . . . . . . . . . . . 16 ⊢ 3 ≠ 0
222	220, 221	pm3.2i 471	. . . . . . . . . . . . . . 15 ⊢ (3 ∈ ℂ ∧ 3 ≠ 0)
223		div23 10704	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
224	219, 222, 223	mp3an13 1415	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℂ → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
225	194, 224	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
226		3t2e6 11179	. . . . . . . . . . . . . . . 16 ⊢ (3 · 2) = 6
227	226	oveq1i 6660	. . . . . . . . . . . . . . 15 ⊢ ((3 · 2) / 3) = (6 / 3)
228	178, 220, 221	divcan3i 10771	. . . . . . . . . . . . . . 15 ⊢ ((3 · 2) / 3) = 2
229	227, 228	eqtr3i 2646	. . . . . . . . . . . . . 14 ⊢ (6 / 3) = 2
230	229	oveq1i 6660	. . . . . . . . . . . . 13 ⊢ ((6 / 3) · 𝑁) = (2 · 𝑁)
231	225, 230	syl6eq 2672	. . . . . . . . . . . 12 ⊢ (𝜑 → ((6 · 𝑁) / 3) = (2 · 𝑁))
232	124	recnd 10068	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 · 𝑁) ∈ ℂ)
233		remulcl 10021	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
234	118, 36, 233	sylancr 695	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ)
235	234	recnd 10068	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
236		divdir 10710	. . . . . . . . . . . . . 14 ⊢ (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
237	222, 236	mp3an3 1413	. . . . . . . . . . . . 13 ⊢ (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
238	232, 235, 237	syl2anc 693	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
239	218, 231, 238	3eqtr3d 2664	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · 𝑁) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
240	239	oveq1d 6665	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)) − ((4 · 𝑁) / 3)))
241	126	recnd 10068	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝑁) / 3) ∈ ℂ)
242		3rp 11838	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℝ+
243		rpdivcl 11856	. . . . . . . . . . . . 13 ⊢ (((2 · 𝑁) ∈ ℝ+ ∧ 3 ∈ ℝ+) → ((2 · 𝑁) / 3) ∈ ℝ+)
244	95, 242, 243	sylancl 694	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ+)
245	244	rpcnd 11874	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℂ)
246	241, 245	pncan2d 10394	. . . . . . . . . 10 ⊢ (𝜑 → ((((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
247	240, 246	eqtrd 2656	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
248	247	oveq1d 6665	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) / 3) · (log‘2)))
249	101	recnd 10068	. . . . . . . . 9 ⊢ (𝜑 → (log‘2) ∈ ℂ)
250	235, 241, 249	subdird 10487	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
251	248, 250	eqtr3d 2658	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
252	134	recnd 10068	. . . . . . . 8 ⊢ (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℂ)
253	169, 252, 170	nnncan2d 10427	. . . . . . 7 ⊢ (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
254	211, 251, 253	3eqtr4d 2666	. . . . . 6 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
255	117	recnd 10068	. . . . . . . . . 10 ⊢ (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℂ)
256	178	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℂ)
257	121	recnd 10068	. . . . . . . . . 10 ⊢ (𝜑 → (log‘(2 · 𝑁)) ∈ ℂ)
258	255, 256, 257	adddird 10065	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))))
259		relogmul 24338	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+) → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
260	91, 61, 259	sylancr 695	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
261	260	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (log‘(2 · 𝑁))) = (2 · ((log‘2) + (log‘𝑁))))
262	256, 249, 170	adddid 10064	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((log‘2) + (log‘𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
263	261, 262	eqtrd 2656	. . . . . . . . . 10 ⊢ (𝜑 → (2 · (log‘(2 · 𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
264	263	oveq2d 6666	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
265	258, 264	eqtrd 2656	. . . . . . . 8 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
266		5cn 11100	. . . . . . . . . . . 12 ⊢ 5 ∈ ℂ
267	266	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 5 ∈ ℂ)
268	241, 267, 249	subdird 10487	. . . . . . . . . 10 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) = ((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))))
269	268	oveq1d 6665	. . . . . . . . 9 ⊢ (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
270	266, 198	mulcli 10045	. . . . . . . . . . 11 ⊢ (5 · (log‘2)) ∈ ℂ
271	270	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (5 · (log‘2)) ∈ ℂ)
272	252, 271, 170	nnncan1d 10426	. . . . . . . . 9 ⊢ (𝜑 → (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
273	269, 272	eqtrd 2656	. . . . . . . 8 ⊢ (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
274	265, 273	oveq12d 6668	. . . . . . 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)))))
275	135	recnd 10068	. . . . . . . 8 ⊢ (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℂ)
276	184, 185, 275	addsubassd 10412	. . . . . . 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‘𝑁)))))
277	266, 220, 198	subdiri 10480	. . . . . . . . . . . . 13 ⊢ ((5 − 3) · (log‘2)) = ((5 · (log‘2)) − (3 · (log‘2)))
278		3p2e5 11160	. . . . . . . . . . . . . . . 16 ⊢ (3 + 2) = 5
279	278	oveq1i 6660	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 3) = (5 − 3)
280		pncan2 10288	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
281	220, 178, 280	mp2an 708	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 3) = 2
282	279, 281	eqtr3i 2646	. . . . . . . . . . . . . 14 ⊢ (5 − 3) = 2
283	282	oveq1i 6660	. . . . . . . . . . . . 13 ⊢ ((5 − 3) · (log‘2)) = (2 · (log‘2))
284	277, 283	eqtr3i 2646	. . . . . . . . . . . 12 ⊢ ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2))
285	284	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2)))
286		df-3 11080	. . . . . . . . . . . . . . . 16 ⊢ 3 = (2 + 1)
287	286	oveq1i 6660	. . . . . . . . . . . . . . 15 ⊢ (3 · (log‘𝑁)) = ((2 + 1) · (log‘𝑁))
288		1cnd 10056	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℂ)
289	256, 288, 170	adddird 10065	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 + 1) · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
290	287, 289	syl5eq 2668	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
291	170	mulid2d 10058	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · (log‘𝑁)) = (log‘𝑁))
292	291	oveq2d 6666	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (log‘𝑁)) + (1 · (log‘𝑁))) = ((2 · (log‘𝑁)) + (log‘𝑁)))
293	290, 292	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (log‘𝑁)))
294	293	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))))
295		mulcl 10020	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (2 · (log‘𝑁)) ∈ ℂ)
296	178, 170, 295	sylancr 695	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (log‘𝑁)) ∈ ℂ)
297	296, 170, 271	addsubassd 10412	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
298	294, 297	eqtrd 2656	. . . . . . . . . . 11 ⊢ (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
299	285, 298	oveq12d 6668	. . . . . . . . . 10 ⊢ (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
300		relogdiv 24339	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
301	61, 91, 300	sylancl 694	. . . . . . . . . . . . 13 ⊢ (𝜑 → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
302	301	oveq2d 6666	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘(𝑁 / 2))) = (3 · ((log‘𝑁) − (log‘2))))
303		subdi 10463	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
304	220, 198, 303	mp3an13 1415	. . . . . . . . . . . . 13 ⊢ ((log‘𝑁) ∈ ℂ → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
305	170, 304	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
306	302, 305	eqtrd 2656	. . . . . . . . . . 11 ⊢ (𝜑 → (3 · (log‘(𝑁 / 2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
307		div23 10704	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
308	178, 222, 307	mp3an13 1415	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℂ → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
309	194, 308	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
310	220, 178, 220, 178, 179, 179	divmuldivi 10785	. . . . . . . . . . . . . . . . 17 ⊢ ((3 / 2) · (3 / 2)) = ((3 · 3) / (2 · 2))
311		3t3e9 11180	. . . . . . . . . . . . . . . . . 18 ⊢ (3 · 3) = 9
312	311, 205	oveq12i 6662	. . . . . . . . . . . . . . . . 17 ⊢ ((3 · 3) / (2 · 2)) = (9 / 4)
313	310, 312	eqtr2i 2645	. . . . . . . . . . . . . . . 16 ⊢ (9 / 4) = ((3 / 2) · (3 / 2))
314	313	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (9 / 4) = ((3 / 2) · (3 / 2)))
315	309, 314	oveq12d 6668	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))))
316	178, 220, 221	divcli 10767	. . . . . . . . . . . . . . 15 ⊢ (2 / 3) ∈ ℂ
317	220, 178, 179	divcli 10767	. . . . . . . . . . . . . . . 16 ⊢ (3 / 2) ∈ ℂ
318		mul4 10205	. . . . . . . . . . . . . . . 16 ⊢ ((((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ ((3 / 2) ∈ ℂ ∧ (3 / 2) ∈ ℂ)) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
319	317, 317, 318	mpanr12 721	. . . . . . . . . . . . . . 15 ⊢ (((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
320	316, 194, 319	sylancr 695	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
321		divcan6 10732	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 / 3) · (3 / 2)) = 1)
322	178, 179, 220, 221, 321	mp4an 709	. . . . . . . . . . . . . . . . 17 ⊢ ((2 / 3) · (3 / 2)) = 1
323	322	oveq1i 6660	. . . . . . . . . . . . . . . 16 ⊢ (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (1 · (𝑁 · (3 / 2)))
324		mulcl 10020	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℂ ∧ (3 / 2) ∈ ℂ) → (𝑁 · (3 / 2)) ∈ ℂ)
325	194, 317, 324	sylancl 694	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 · (3 / 2)) ∈ ℂ)
326	325	mulid2d 10058	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
327	323, 326	syl5eq 2668	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
328		2cnne0 11242	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
329		div12 10707	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℂ ∧ 3 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
330	220, 328, 329	mp3an23 1416	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℂ → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
331	194, 330	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
332	327, 331	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (3 · (𝑁 / 2)))
333	315, 320, 332	3eqtrd 2660	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (3 · (𝑁 / 2)))
334	333, 84	oveq12d 6668	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))))
335	77	recni 10052	. . . . . . . . . . . . . 14 ⊢ (9 / 4) ∈ ℂ
336	335	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (9 / 4) ∈ ℂ)
337	87	recnd 10068	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℂ)
338	245, 336, 337	mulassd 10063	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))
339	220	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 3 ∈ ℂ)
340	78	rpcnd 11874	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 2) ∈ ℂ)
341	85	recnd 10068	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (log‘(𝑁 / 2)) ∈ ℂ)
342	78	rpne0d 11877	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 / 2) ≠ 0)
343	341, 340, 342	divcld 10801	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℂ)
344	339, 340, 343	mulassd 10063	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))))
345	341, 340, 342	divcan2d 10803	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (log‘(𝑁 / 2)))
346	345	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ (𝜑 → (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
347	344, 346	eqtrd 2656	. . . . . . . . . . . 12 ⊢ (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · (log‘(𝑁 / 2))))
348	334, 338, 347	3eqtr3d 2664	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
349	220, 198	mulcli 10045	. . . . . . . . . . . . 13 ⊢ (3 · (log‘2)) ∈ ℂ
350	349	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘2)) ∈ ℂ)
351		mulcl 10020	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (3 · (log‘𝑁)) ∈ ℂ)
352	220, 170, 351	sylancr 695	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘𝑁)) ∈ ℂ)
353	271, 350, 352	npncan3d 10428	. . . . . . . . . . 11 ⊢ (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
354	306, 348, 353	3eqtr4d 2666	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))))
355	118, 93	remulcli 10054	. . . . . . . . . . . . 13 ⊢ (2 · (log‘2)) ∈ ℝ
356	355	recni 10052	. . . . . . . . . . . 12 ⊢ (2 · (log‘2)) ∈ ℂ
357	356	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (log‘2)) ∈ ℂ)
358		subcl 10280	. . . . . . . . . . . 12 ⊢ (((log‘𝑁) ∈ ℂ ∧ (5 · (log‘2)) ∈ ℂ) → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
359	170, 270, 358	sylancl 694	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
360	357, 296, 359	addassd 10062	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
361	299, 354, 360	3eqtr4d 2666	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))))
362	361	oveq2d 6666	. . . . . . . 8 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2))))))
363		mulcl 10020	. . . . . . . . . . 11 ⊢ ((((√‘(2 · 𝑁)) / 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
364	255, 198, 363	sylancl 694	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
365	255, 170	mulcld 10060	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) ∈ ℂ)
366	89	recnd 10068	. . . . . . . . . . 11 ⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℂ)
367	245, 366	mulcld 10060	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
368	364, 365, 367	addassd 10062	. . . . . . . . 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)))))))
369	260	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))))
370	255, 249, 170	adddid 10064	. . . . . . . . . . 11 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
371	369, 370	eqtrd 2656	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
372	371	oveq1d 6665	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
373	59	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))))
374	90	recnd 10068	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
375	98	recnd 10068	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℂ)
376	245, 374, 375	adddid 10064	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
377	373, 376	eqtrd 2656	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
378	73	recnd 10068	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℂ)
379	245, 378, 366	adddid 10064	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
380	95	rpge0d 11876	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ≤ (2 · 𝑁))
381		remsqsqrt 13997	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
382	234, 380, 381	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
383	382	oveq1d 6665	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = ((2 · 𝑁) / 3))
384	114	recnd 10068	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℂ)
385	221	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ≠ 0)
386	384, 384, 339, 385	div23d 10838	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
387	383, 386	eqtr3d 2658	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · 𝑁) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
388	387	oveq1d 6665	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))))
389	255, 384, 378	mulassd 10063	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))))
390		0le2 11111	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ≤ 2
391	118, 390	pm3.2i 471	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℝ ∧ 0 ≤ 2)
392	61	rprege0d 11879	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
393		sqrtmul 14000	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
394	391, 392, 393	sylancr 695	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
395	394	oveq1d 6665	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))))
396	60	recni 10052	. . . . . . . . . . . . . . . . . 18 ⊢ (√‘2) ∈ ℂ
397	396	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘2) ∈ ℂ)
398	62	rpcnd 11874	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘𝑁) ∈ ℂ)
399	71	recnd 10068	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℂ)
400	397, 398, 397, 399	mul4d 10248	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))))
401		remsqsqrt 13997	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
402	118, 390, 401	mp2an 708	. . . . . . . . . . . . . . . . . . 19 ⊢ ((√‘2) · (√‘2)) = 2
403	402	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((√‘2) · (√‘2)) = 2)
404	68	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))))
405	69	recnd 10068	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (log‘(√‘𝑁)) ∈ ℂ)
406	62	rpne0d 11877	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑁) ≠ 0)
407	405, 398, 406	divcan2d 10803	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))) = (log‘(√‘𝑁)))
408	404, 407	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = (log‘(√‘𝑁)))
409	403, 408	oveq12d 6668	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (2 · (log‘(√‘𝑁))))
410	405	2timesd 11275	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (log‘(√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
411	62, 62	relogmuld 24371	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
412		remsqsqrt 13997	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
413	392, 412	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
414	413	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = (log‘𝑁))
415	411, 414	eqtr3d 2658	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘(√‘𝑁)) + (log‘(√‘𝑁))) = (log‘𝑁))
416	409, 410, 415	3eqtrd 2660	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
417	395, 400, 416	3eqtrd 2660	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
418	417	oveq2d 6666	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
419	388, 389, 418	3eqtrd 2660	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
420	419	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
421	379, 420	eqtrd 2656	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
422	387	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))))
423	255, 384, 375	mulassd 10063	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))))
424	96	rpne0d 11877	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (√‘(2 · 𝑁)) ≠ 0)
425	249, 384, 424	divcan2d 10803	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁)))) = (log‘2))
426	425	oveq2d 6666	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
427	422, 423, 426	3eqtrd 2660	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
428	421, 427	oveq12d 6668	. . . . . . . . . 10 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((√‘(2 · 𝑁)) / 3) · (log‘2))))
429	365, 367	addcld 10059	. . . . . . . . . . 11 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) ∈ ℂ)
430	429, 364	addcomd 10238	. . . . . . . . . 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)))))))
431	377, 428, 430	3eqtrd 2660	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
432	368, 372, 431	3eqtr4rd 2667	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
433	255, 257	mulcld 10060	. . . . . . . . 9 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) ∈ ℂ)
434		addcl 10018	. . . . . . . . . 10 ⊢ (((2 · (log‘2)) ∈ ℂ ∧ (2 · (log‘𝑁)) ∈ ℂ) → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
435	356, 296, 434	sylancr 695	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
436	433, 435, 359	addassd 10062	. . . . . . . 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))))))
437	362, 432, 436	3eqtr4d 2666	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))))
438	274, 276, 437	3eqtr4rd 2667	. . . . . 6 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
439	193, 254, 438	3brtr4d 4685	. . . . 5 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹‘𝑁)))
440	101, 100, 244	ltmul2d 11914	. . . . 5 ⊢ (𝜑 → ((log‘2) < (𝐹‘𝑁) ↔ (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹‘𝑁))))
441	439, 440	mpbird 247	. . . 4 ⊢ (𝜑 → (log‘2) < (𝐹‘𝑁))
442	45, 101, 100, 102, 441	lttrd 10198	. . 3 ⊢ (𝜑 → (𝐹‘;64) < (𝐹‘𝑁))
443	45, 100, 442	ltnsymd 10186	. 2 ⊢ (𝜑 → ¬ (𝐹‘𝑁) < (𝐹‘;64))
444	42, 443	pm2.21dd 186	1 ⊢ (𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∃wrex 2913  ifcif 4086   class class class wbr 4653   ↦ cmpt 4729  ‘cfv 5888  (class class class)co 6650  ℂcc 9934  ℝcr 9935  0cc0 9936  1c1 9937   + caddc 9939   · cmul 9941   < clt 10074   ≤ cle 10075   − cmin 10266   / cdiv 10684  ℕcn 11020  2c2 11070  3c3 11071  4c4 11072  5c5 11073  6c6 11074  8c8 11076  9c9 11077  ℤcz 11377  ;cdc 11493  ℤ_≥cuz 11687  ℝ⁺crp 11832  ⌊cfl 12591  ↑cexp 12860  Ccbc 13089  √csqrt 13973  expce 14792  eceu 14793  ℙcprime 15385   pCnt cpc 15541  logclog 24301  ↑_𝑐ccxp 24302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-xnn0 11364  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ioc 12180  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-fac 13061  df-bc 13090  df-hash 13118  df-shft 13807  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-limsup 14202  df-clim 14219  df-rlim 14220  df-sum 14417  df-ef 14798  df-e 14799  df-sin 14800  df-cos 14801  df-pi 14803  df-dvds 14984  df-gcd 15217  df-prm 15386  df-pc 15542  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-xrs 16162  df-qtop 16167  df-imas 16168  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-submnd 17336  df-mulg 17541  df-cntz 17750  df-cmn 18195  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-lp 20940  df-perf 20941  df-cn 21031  df-cnp 21032  df-haus 21119  df-tx 21365  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-xms 22125  df-ms 22126  df-tms 22127  df-cncf 22681  df-limc 23630  df-dv 23631  df-log 24303  df-cxp 24304  df-cht 24823  df-ppi 24826

This theorem is referenced by:  bpos  25018