Theorem bposlem9 24817

Description: Lemma for bpos 24818. 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 11190	. . . . . 6 ⊢ 6 ∈ ℕ0
5		4nn 11064	. . . . . 6 ⊢ 4 ∈ ℕ
6	4, 5	decnncl 11394	. . . . 5 ⊢ ;64 ∈ ℕ
7	6	a1i 11	. . . 4 ⊢ (𝜑 → ;64 ∈ ℕ)
8		bposlem9.3	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
9		ere 14658	. . . . . . . 8 ⊢ e ∈ ℝ
10		8re 10982	. . . . . . . 8 ⊢ 8 ∈ ℝ
11		egt2lt3 14773	. . . . . . . . . 10 ⊢ (2 < e ∧ e < 3)
12	11	simpri 477	. . . . . . . . 9 ⊢ e < 3
13		3lt8 11096	. . . . . . . . 9 ⊢ 3 < 8
14		3re 10971	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
15	9, 14, 10	lttri 10042	. . . . . . . . 9 ⊢ ((e < 3 ∧ 3 < 8) → e < 8)
16	12, 13, 15	mp2an 704	. . . . . . . 8 ⊢ e < 8
17	9, 10, 16	ltleii 10039	. . . . . . 7 ⊢ e ≤ 8
18		0re 9919	. . . . . . . . 9 ⊢ 0 ∈ ℝ
19		epos 14774	. . . . . . . . 9 ⊢ 0 < e
20	18, 9, 19	ltleii 10039	. . . . . . . 8 ⊢ 0 ≤ e
21		8pos 10998	. . . . . . . . 9 ⊢ 0 < 8
22	18, 10, 21	ltleii 10039	. . . . . . . 8 ⊢ 0 ≤ 8
23		le2sq 12800	. . . . . . . 8 ⊢ (((e ∈ ℝ ∧ 0 ≤ e) ∧ (8 ∈ ℝ ∧ 0 ≤ 8)) → (e ≤ 8 ↔ (e↑2) ≤ (8↑2)))
24	9, 20, 10, 22, 23	mp4an 705	. . . . . . 7 ⊢ (e ≤ 8 ↔ (e↑2) ≤ (8↑2))
25	17, 24	mpbi 219	. . . . . 6 ⊢ (e↑2) ≤ (8↑2)
26	10	recni 9931	. . . . . . . 8 ⊢ 8 ∈ ℂ
27	26	sqvali 12805	. . . . . . 7 ⊢ (8↑2) = (8 · 8)
28		8t8e64 11538	. . . . . . 7 ⊢ (8 · 8) = ;64
29	27, 28	eqtri 2632	. . . . . 6 ⊢ (8↑2) = ;64
30	25, 29	breqtri 4608	. . . . 5 ⊢ (e↑2) ≤ ;64
31	30	a1i 11	. . . 4 ⊢ (𝜑 → (e↑2) ≤ ;64)
32	9	resqcli 12811	. . . . . 6 ⊢ (e↑2) ∈ ℝ
33	32	a1i 11	. . . . 5 ⊢ (𝜑 → (e↑2) ∈ ℝ)
34	6	nnrei 10906	. . . . . 6 ⊢ ;64 ∈ ℝ
35	34	a1i 11	. . . . 5 ⊢ (𝜑 → ;64 ∈ ℝ)
36	8	nnred 10912	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℝ)
37		ltle 10005	. . . . . . 7 ⊢ ((;64 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (;64 < 𝑁 → ;64 ≤ 𝑁))
38	34, 36, 37	sylancr 694	. . . . . 6 ⊢ (𝜑 → (;64 < 𝑁 → ;64 ≤ 𝑁))
39	1, 38	mpd 15	. . . . 5 ⊢ (𝜑 → ;64 ≤ 𝑁)
40	33, 35, 36, 31, 39	letrd 10073	. . . 4 ⊢ (𝜑 → (e↑2) ≤ 𝑁)
41	2, 3, 7, 8, 31, 40	bposlem7 24815	. . 3 ⊢ (𝜑 → (;64 < 𝑁 → (𝐹‘𝑁) < (𝐹‘;64)))
42	1, 41	mpd 15	. 2 ⊢ (𝜑 → (𝐹‘𝑁) < (𝐹‘;64))
43	2, 3	bposlem8 24816	. . . . 5 ⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2))
44	43	a1i 11	. . . 4 ⊢ (𝜑 → ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2)))
45	44	simpld 474	. . 3 ⊢ (𝜑 → (𝐹‘;64) ∈ ℝ)
46		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑛 = 𝑁 → (√‘𝑛) = (√‘𝑁))
47	46	fveq2d 6107	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (𝐺‘(√‘𝑛)) = (𝐺‘(√‘𝑁)))
48	47	oveq2d 6565	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · (𝐺‘(√‘𝑁))))
49		oveq1 6556	. . . . . . . . . 10 ⊢ (𝑛 = 𝑁 → (𝑛 / 2) = (𝑁 / 2))
50	49	fveq2d 6107	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (𝐺‘(𝑛 / 2)) = (𝐺‘(𝑁 / 2)))
51	50	oveq2d 6565	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · (𝐺‘(𝑁 / 2))))
52	48, 51	oveq12d 6567	. . . . . . 7 ⊢ (𝑛 = 𝑁 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))))
53		oveq2 6557	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
54	53	fveq2d 6107	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → (√‘(2 · 𝑛)) = (√‘(2 · 𝑁)))
55	54	oveq2d 6565	. . . . . . 7 ⊢ (𝑛 = 𝑁 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / (√‘(2 · 𝑁))))
56	52, 55	oveq12d 6567	. . . . . 6 ⊢ (𝑛 = 𝑁 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
57		ovex 6577	. . . . . 6 ⊢ ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ V
58	56, 2, 57	fvmpt 6191	. . . . 5 ⊢ (𝑁 ∈ ℕ → (𝐹‘𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
59	8, 58	syl 17	. . . 4 ⊢ (𝜑 → (𝐹‘𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
60		sqrt2re 14818	. . . . . . 7 ⊢ (√‘2) ∈ ℝ
61	8	nnrpd 11746	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ+)
62	61	rpsqrtcld 13998	. . . . . . . . 9 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ+)
63		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑥 = (√‘𝑁) → (log‘𝑥) = (log‘(√‘𝑁)))
64		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = (√‘𝑁) → 𝑥 = (√‘𝑁))
65	63, 64	oveq12d 6567	. . . . . . . . . 10 ⊢ (𝑥 = (√‘𝑁) → ((log‘𝑥) / 𝑥) = ((log‘(√‘𝑁)) / (√‘𝑁)))
66		ovex 6577	. . . . . . . . . 10 ⊢ ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ V
67	65, 3, 66	fvmpt 6191	. . . . . . . . 9 ⊢ ((√‘𝑁) ∈ ℝ+ → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
68	62, 67	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
69	62	relogcld 24173	. . . . . . . . 9 ⊢ (𝜑 → (log‘(√‘𝑁)) ∈ ℝ)
70	69, 62	rerpdivcld 11779	. . . . . . . 8 ⊢ (𝜑 → ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ ℝ)
71	68, 70	eqeltrd 2688	. . . . . . 7 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℝ)
72		remulcl 9900	. . . . . . 7 ⊢ (((√‘2) ∈ ℝ ∧ (𝐺‘(√‘𝑁)) ∈ ℝ) → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
73	60, 71, 72	sylancr 694	. . . . . 6 ⊢ (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
74		9re 10984	. . . . . . . 8 ⊢ 9 ∈ ℝ
75		4re 10974	. . . . . . . 8 ⊢ 4 ∈ ℝ
76		4ne0 10994	. . . . . . . 8 ⊢ 4 ≠ 0
77	74, 75, 76	redivcli 10671	. . . . . . 7 ⊢ (9 / 4) ∈ ℝ
78	61	rphalfcld 11760	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 / 2) ∈ ℝ+)
79		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑁 / 2) → (log‘𝑥) = (log‘(𝑁 / 2)))
80		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑁 / 2) → 𝑥 = (𝑁 / 2))
81	79, 80	oveq12d 6567	. . . . . . . . . 10 ⊢ (𝑥 = (𝑁 / 2) → ((log‘𝑥) / 𝑥) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
82		ovex 6577	. . . . . . . . . 10 ⊢ ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ V
83	81, 3, 82	fvmpt 6191	. . . . . . . . 9 ⊢ ((𝑁 / 2) ∈ ℝ+ → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
84	78, 83	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
85	78	relogcld 24173	. . . . . . . . 9 ⊢ (𝜑 → (log‘(𝑁 / 2)) ∈ ℝ)
86	85, 78	rerpdivcld 11779	. . . . . . . 8 ⊢ (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℝ)
87	84, 86	eqeltrd 2688	. . . . . . 7 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℝ)
88		remulcl 9900	. . . . . . 7 ⊢ (((9 / 4) ∈ ℝ ∧ (𝐺‘(𝑁 / 2)) ∈ ℝ) → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
89	77, 87, 88	sylancr 694	. . . . . 6 ⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
90	73, 89	readdcld 9948	. . . . 5 ⊢ (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℝ)
91		2rp 11713	. . . . . . 7 ⊢ 2 ∈ ℝ+
92		relogcl 24126	. . . . . . 7 ⊢ (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
93	91, 92	ax-mp 5	. . . . . 6 ⊢ (log‘2) ∈ ℝ
94		rpmulcl 11731	. . . . . . . 8 ⊢ ((2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+) → (2 · 𝑁) ∈ ℝ+)
95	91, 61, 94	sylancr 694	. . . . . . 7 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ+)
96	95	rpsqrtcld 13998	. . . . . 6 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ+)
97		rerpdivcl 11737	. . . . . 6 ⊢ (((log‘2) ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ+) → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
98	93, 96, 97	sylancr 694	. . . . 5 ⊢ (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
99	90, 98	readdcld 9948	. . . 4 ⊢ (𝜑 → ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ ℝ)
100	59, 99	eqeltrd 2688	. . 3 ⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ)
101	93	a1i 11	. . . 4 ⊢ (𝜑 → (log‘2) ∈ ℝ)
102	44	simprd 478	. . . 4 ⊢ (𝜑 → (𝐹‘;64) < (log‘2))
103		nnrp 11718	. . . . . . . . . . 11 ⊢ (4 ∈ ℕ → 4 ∈ ℝ+)
104	5, 103	ax-mp 5	. . . . . . . . . 10 ⊢ 4 ∈ ℝ+
105		relogcl 24126	. . . . . . . . . 10 ⊢ (4 ∈ ℝ+ → (log‘4) ∈ ℝ)
106	104, 105	ax-mp 5	. . . . . . . . 9 ⊢ (log‘4) ∈ ℝ
107		remulcl 9900	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ (log‘4) ∈ ℝ) → (𝑁 · (log‘4)) ∈ ℝ)
108	36, 106, 107	sylancl 693	. . . . . . . 8 ⊢ (𝜑 → (𝑁 · (log‘4)) ∈ ℝ)
109	61	relogcld 24173	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
110	108, 109	resubcld 10337	. . . . . . 7 ⊢ (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) ∈ ℝ)
111		rpre 11715	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ ℝ+ → (2 · 𝑁) ∈ ℝ)
112		rpge0 11721	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ ℝ+ → 0 ≤ (2 · 𝑁))
113	111, 112	resqrtcld 14004	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) ∈ ℝ+ → (√‘(2 · 𝑁)) ∈ ℝ)
114	95, 113	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
115		3nn 11063	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ
116		nndivre 10933	. . . . . . . . . . 11 ⊢ (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
117	114, 115, 116	sylancl 693	. . . . . . . . . 10 ⊢ (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
118		2re 10967	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
119		readdcl 9898	. . . . . . . . . 10 ⊢ ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
120	117, 118, 119	sylancl 693	. . . . . . . . 9 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
121	95	relogcld 24173	. . . . . . . . 9 ⊢ (𝜑 → (log‘(2 · 𝑁)) ∈ ℝ)
122	120, 121	remulcld 9949	. . . . . . . 8 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℝ)
123		remulcl 9900	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (4 · 𝑁) ∈ ℝ)
124	75, 36, 123	sylancr 694	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · 𝑁) ∈ ℝ)
125		nndivre 10933	. . . . . . . . . . 11 ⊢ (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
126	124, 115, 125	sylancl 693	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
127		5re 10976	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
128		resubcl 10224	. . . . . . . . . 10 ⊢ ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
129	126, 127, 128	sylancl 693	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
130		remulcl 9900	. . . . . . . . 9 ⊢ (((((4 · 𝑁) / 3) − 5) ∈ ℝ ∧ (log‘2) ∈ ℝ) → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
131	129, 93, 130	sylancl 693	. . . . . . . 8 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
132	122, 131	readdcld 9948	. . . . . . 7 ⊢ (𝜑 → (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ∈ ℝ)
133		remulcl 9900	. . . . . . . . 9 ⊢ ((((4 · 𝑁) / 3) ∈ ℝ ∧ (log‘2) ∈ ℝ) → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
134	126, 93, 133	sylancl 693	. . . . . . . 8 ⊢ (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
135	134, 109	resubcld 10337	. . . . . . 7 ⊢ (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℝ)
136	8	nnzd 11357	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℤ)
137		df-5 10959	. . . . . . . . . . . 12 ⊢ 5 = (4 + 1)
138	75	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 ∈ ℝ)
139		6nn 11066	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℕ
140		4nn0 11188	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ0
141		4lt10 11554	. . . . . . . . . . . . . . . 16 ⊢ 4 < ;10
142	139, 140, 140, 141	declti 11422	. . . . . . . . . . . . . . 15 ⊢ 4 < ;64
143	142	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 < ;64)
144	138, 35, 36, 143, 1	lttrd 10077	. . . . . . . . . . . . 13 ⊢ (𝜑 → 4 < 𝑁)
145		4z 11288	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℤ
146		zltp1le 11304	. . . . . . . . . . . . . 14 ⊢ ((4 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
147	145, 136, 146	sylancr 694	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
148	144, 147	mpbid 221	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 + 1) ≤ 𝑁)
149	137, 148	syl5eqbr 4618	. . . . . . . . . . 11 ⊢ (𝜑 → 5 ≤ 𝑁)
150		5nn 11065	. . . . . . . . . . . . 13 ⊢ 5 ∈ ℕ
151	150	nnzi 11278	. . . . . . . . . . . 12 ⊢ 5 ∈ ℤ
152	151	eluz1i 11571	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ≥‘5) ↔ (𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
153	136, 149, 152	sylanbrc 695	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5))
154		bposlem9.5	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
155		breq2 4587	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑁 < 𝑝 ↔ 𝑁 < 𝑞))
156		breq1 4586	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑝 ≤ (2 · 𝑁) ↔ 𝑞 ≤ (2 · 𝑁)))
157	155, 156	anbi12d 743	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑞 → ((𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁))))
158	157	cbvrexv 3148	. . . . . . . . . . 11 ⊢ (∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ ∃𝑞 ∈ ℙ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁)))
159	154, 158	sylnib 317	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ∃𝑞 ∈ ℙ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁)))
160		eqid 2610	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
161		eqid 2610	. . . . . . . . . 10 ⊢ (⌊‘((2 · 𝑁) / 3)) = (⌊‘((2 · 𝑁) / 3))
162		eqid 2610	. . . . . . . . . 10 ⊢ (⌊‘(√‘(2 · 𝑁))) = (⌊‘(√‘(2 · 𝑁)))
163	153, 159, 160, 161, 162	bposlem6 24814	. . . . . . . . 9 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
164		reexplog 24145	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
165	104, 136, 164	sylancr 694	. . . . . . . . . . 11 ⊢ (𝜑 → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
166	61	reeflogd 24174	. . . . . . . . . . . 12 ⊢ (𝜑 → (exp‘(log‘𝑁)) = 𝑁)
167	166	eqcomd 2616	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 = (exp‘(log‘𝑁)))
168	165, 167	oveq12d 6567	. . . . . . . . . 10 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
169	108	recnd 9947	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · (log‘4)) ∈ ℂ)
170	109	recnd 9947	. . . . . . . . . . 11 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
171		efsub 14669	. . . . . . . . . . 11 ⊢ (((𝑁 · (log‘4)) ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
172	169, 170, 171	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
173	168, 172	eqtr4d 2647	. . . . . . . . 9 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) = (exp‘((𝑁 · (log‘4)) − (log‘𝑁))))
174	95	rpcnd 11750	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
175	95	rpne0d 11753	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ≠ 0)
176	120	recnd 9947	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℂ)
177	174, 175, 176	cxpefd 24258	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) = (exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))))
178		2cn 10968	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
179		2ne0 10990	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
180	129	recnd 9947	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℂ)
181		cxpef 24211	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ (((4 · 𝑁) / 3) − 5) ∈ ℂ) → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
182	178, 179, 180, 181	mp3an12i 1420	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
183	177, 182	oveq12d 6567	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
184	122	recnd 9947	. . . . . . . . . . 11 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℂ)
185	131	recnd 9947	. . . . . . . . . . 11 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℂ)
186		efadd 14663	. . . . . . . . . . 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 691	. . . . . . . . . 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 2647	. . . . . . . . 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 4614	. . . . . . . 8 ⊢ (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
190		eflt 14686	. . . . . . . . 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 691	. . . . . . . 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 246	. . . . . . 7 ⊢ (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))
193	110, 132, 135, 192	ltsub1dd 10518	. . . . . 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 9947	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
195		mulcom 9901	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) = (𝑁 · 2))
196	178, 194, 195	sylancr 694	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑁) = (𝑁 · 2))
197	196	oveq1d 6564	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝑁) · (log‘2)) = ((𝑁 · 2) · (log‘2)))
198	93	recni 9931	. . . . . . . . . . . 12 ⊢ (log‘2) ∈ ℂ
199		mulass 9903	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ (log‘2) ∈ ℂ) → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
200	178, 198, 199	mp3an23 1408	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℂ → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
201	194, 200	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
202	198	2timesi 11024	. . . . . . . . . . . 12 ⊢ (2 · (log‘2)) = ((log‘2) + (log‘2))
203		relogmul 24142	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(2 · 2)) = ((log‘2) + (log‘2)))
204	91, 91, 203	mp2an 704	. . . . . . . . . . . 12 ⊢ (log‘(2 · 2)) = ((log‘2) + (log‘2))
205		2t2e4 11054	. . . . . . . . . . . . 13 ⊢ (2 · 2) = 4
206	205	fveq2i 6106	. . . . . . . . . . . 12 ⊢ (log‘(2 · 2)) = (log‘4)
207	202, 204, 206	3eqtr2i 2638	. . . . . . . . . . 11 ⊢ (2 · (log‘2)) = (log‘4)
208	207	oveq2i 6560	. . . . . . . . . 10 ⊢ (𝑁 · (2 · (log‘2))) = (𝑁 · (log‘4))
209	201, 208	syl6eq 2660	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (log‘4)))
210	197, 209	eqtrd 2644	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝑁) · (log‘2)) = (𝑁 · (log‘4)))
211	210	oveq1d 6564	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
212		4p2e6 11039	. . . . . . . . . . . . . . 15 ⊢ (4 + 2) = 6
213	212	oveq1i 6559	. . . . . . . . . . . . . 14 ⊢ ((4 + 2) · 𝑁) = (6 · 𝑁)
214		4cn 10975	. . . . . . . . . . . . . . 15 ⊢ 4 ∈ ℂ
215		adddir 9910	. . . . . . . . . . . . . . 15 ⊢ ((4 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
216	214, 178, 194, 215	mp3an12i 1420	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
217	213, 216	syl5eqr 2658	. . . . . . . . . . . . 13 ⊢ (𝜑 → (6 · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
218	217	oveq1d 6564	. . . . . . . . . . . 12 ⊢ (𝜑 → ((6 · 𝑁) / 3) = (((4 · 𝑁) + (2 · 𝑁)) / 3))
219		6cn 10979	. . . . . . . . . . . . . . 15 ⊢ 6 ∈ ℂ
220		3cn 10972	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℂ
221		3ne0 10992	. . . . . . . . . . . . . . . 16 ⊢ 3 ≠ 0
222	220, 221	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (3 ∈ ℂ ∧ 3 ≠ 0)
223		div23 10583	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
224	219, 222, 223	mp3an13 1407	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℂ → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
225	194, 224	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
226		3t2e6 11056	. . . . . . . . . . . . . . . 16 ⊢ (3 · 2) = 6
227	226	oveq1i 6559	. . . . . . . . . . . . . . 15 ⊢ ((3 · 2) / 3) = (6 / 3)
228	178, 220, 221	divcan3i 10650	. . . . . . . . . . . . . . 15 ⊢ ((3 · 2) / 3) = 2
229	227, 228	eqtr3i 2634	. . . . . . . . . . . . . 14 ⊢ (6 / 3) = 2
230	229	oveq1i 6559	. . . . . . . . . . . . 13 ⊢ ((6 / 3) · 𝑁) = (2 · 𝑁)
231	225, 230	syl6eq 2660	. . . . . . . . . . . 12 ⊢ (𝜑 → ((6 · 𝑁) / 3) = (2 · 𝑁))
232	124	recnd 9947	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 · 𝑁) ∈ ℂ)
233		remulcl 9900	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
234	118, 36, 233	sylancr 694	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ)
235	234	recnd 9947	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
236		divdir 10589	. . . . . . . . . . . . . 14 ⊢ (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
237	222, 236	mp3an3 1405	. . . . . . . . . . . . 13 ⊢ (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
238	232, 235, 237	syl2anc 691	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
239	218, 231, 238	3eqtr3d 2652	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · 𝑁) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
240	239	oveq1d 6564	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)) − ((4 · 𝑁) / 3)))
241	126	recnd 9947	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝑁) / 3) ∈ ℂ)
242		3rp 11714	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℝ+
243		rpdivcl 11732	. . . . . . . . . . . . 13 ⊢ (((2 · 𝑁) ∈ ℝ+ ∧ 3 ∈ ℝ+) → ((2 · 𝑁) / 3) ∈ ℝ+)
244	95, 242, 243	sylancl 693	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ+)
245	244	rpcnd 11750	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℂ)
246	241, 245	pncan2d 10273	. . . . . . . . . 10 ⊢ (𝜑 → ((((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
247	240, 246	eqtrd 2644	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
248	247	oveq1d 6564	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) / 3) · (log‘2)))
249	101	recnd 9947	. . . . . . . . 9 ⊢ (𝜑 → (log‘2) ∈ ℂ)
250	235, 241, 249	subdird 10366	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
251	248, 250	eqtr3d 2646	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
252	134	recnd 9947	. . . . . . . 8 ⊢ (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℂ)
253	169, 252, 170	nnncan2d 10306	. . . . . . 7 ⊢ (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
254	211, 251, 253	3eqtr4d 2654	. . . . . 6 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
255	117	recnd 9947	. . . . . . . . . 10 ⊢ (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℂ)
256	178	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℂ)
257	121	recnd 9947	. . . . . . . . . 10 ⊢ (𝜑 → (log‘(2 · 𝑁)) ∈ ℂ)
258	255, 256, 257	adddird 9944	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))))
259		relogmul 24142	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+) → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
260	91, 61, 259	sylancr 694	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
261	260	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (log‘(2 · 𝑁))) = (2 · ((log‘2) + (log‘𝑁))))
262	256, 249, 170	adddid 9943	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((log‘2) + (log‘𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
263	261, 262	eqtrd 2644	. . . . . . . . . 10 ⊢ (𝜑 → (2 · (log‘(2 · 𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
264	263	oveq2d 6565	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
265	258, 264	eqtrd 2644	. . . . . . . 8 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
266		5cn 10977	. . . . . . . . . . . 12 ⊢ 5 ∈ ℂ
267	266	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 5 ∈ ℂ)
268	241, 267, 249	subdird 10366	. . . . . . . . . 10 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) = ((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))))
269	268	oveq1d 6564	. . . . . . . . 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 9924	. . . . . . . . . . 11 ⊢ (5 · (log‘2)) ∈ ℂ
271	270	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (5 · (log‘2)) ∈ ℂ)
272	252, 271, 170	nnncan1d 10305	. . . . . . . . 9 ⊢ (𝜑 → (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
273	269, 272	eqtrd 2644	. . . . . . . 8 ⊢ (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
274	265, 273	oveq12d 6567	. . . . . . 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 9947	. . . . . . . 8 ⊢ (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℂ)
276	184, 185, 275	addsubassd 10291	. . . . . . 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 10359	. . . . . . . . . . . . 13 ⊢ ((5 − 3) · (log‘2)) = ((5 · (log‘2)) − (3 · (log‘2)))
278		3p2e5 11037	. . . . . . . . . . . . . . . 16 ⊢ (3 + 2) = 5
279	278	oveq1i 6559	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 3) = (5 − 3)
280		pncan2 10167	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
281	220, 178, 280	mp2an 704	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 3) = 2
282	279, 281	eqtr3i 2634	. . . . . . . . . . . . . 14 ⊢ (5 − 3) = 2
283	282	oveq1i 6559	. . . . . . . . . . . . 13 ⊢ ((5 − 3) · (log‘2)) = (2 · (log‘2))
284	277, 283	eqtr3i 2634	. . . . . . . . . . . 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 10957	. . . . . . . . . . . . . . . 16 ⊢ 3 = (2 + 1)
287	286	oveq1i 6559	. . . . . . . . . . . . . . 15 ⊢ (3 · (log‘𝑁)) = ((2 + 1) · (log‘𝑁))
288		1cnd 9935	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℂ)
289	256, 288, 170	adddird 9944	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 + 1) · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
290	287, 289	syl5eq 2656	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
291	170	mulid2d 9937	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · (log‘𝑁)) = (log‘𝑁))
292	291	oveq2d 6565	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (log‘𝑁)) + (1 · (log‘𝑁))) = ((2 · (log‘𝑁)) + (log‘𝑁)))
293	290, 292	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (log‘𝑁)))
294	293	oveq1d 6564	. . . . . . . . . . . 12 ⊢ (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))))
295		mulcl 9899	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (2 · (log‘𝑁)) ∈ ℂ)
296	178, 170, 295	sylancr 694	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (log‘𝑁)) ∈ ℂ)
297	296, 170, 271	addsubassd 10291	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
298	294, 297	eqtrd 2644	. . . . . . . . . . 11 ⊢ (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
299	285, 298	oveq12d 6567	. . . . . . . . . 10 ⊢ (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
300		relogdiv 24143	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
301	61, 91, 300	sylancl 693	. . . . . . . . . . . . 13 ⊢ (𝜑 → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
302	301	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘(𝑁 / 2))) = (3 · ((log‘𝑁) − (log‘2))))
303		subdi 10342	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
304	220, 198, 303	mp3an13 1407	. . . . . . . . . . . . 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 2644	. . . . . . . . . . 11 ⊢ (𝜑 → (3 · (log‘(𝑁 / 2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
307		div23 10583	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
308	178, 222, 307	mp3an13 1407	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℂ → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
309	194, 308	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
310	220, 178, 220, 178, 179, 179	divmuldivi 10664	. . . . . . . . . . . . . . . . 17 ⊢ ((3 / 2) · (3 / 2)) = ((3 · 3) / (2 · 2))
311		3t3e9 11057	. . . . . . . . . . . . . . . . . 18 ⊢ (3 · 3) = 9
312	311, 205	oveq12i 6561	. . . . . . . . . . . . . . . . 17 ⊢ ((3 · 3) / (2 · 2)) = (9 / 4)
313	310, 312	eqtr2i 2633	. . . . . . . . . . . . . . . 16 ⊢ (9 / 4) = ((3 / 2) · (3 / 2))
314	313	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (9 / 4) = ((3 / 2) · (3 / 2)))
315	309, 314	oveq12d 6567	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))))
316	178, 220, 221	divcli 10646	. . . . . . . . . . . . . . 15 ⊢ (2 / 3) ∈ ℂ
317	220, 178, 179	divcli 10646	. . . . . . . . . . . . . . . 16 ⊢ (3 / 2) ∈ ℂ
318		mul4 10084	. . . . . . . . . . . . . . . 16 ⊢ ((((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ ((3 / 2) ∈ ℂ ∧ (3 / 2) ∈ ℂ)) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
319	317, 317, 318	mpanr12 717	. . . . . . . . . . . . . . 15 ⊢ (((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
320	316, 194, 319	sylancr 694	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
321		divcan6 10611	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 / 3) · (3 / 2)) = 1)
322	178, 179, 220, 221, 321	mp4an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((2 / 3) · (3 / 2)) = 1
323	322	oveq1i 6559	. . . . . . . . . . . . . . . 16 ⊢ (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (1 · (𝑁 · (3 / 2)))
324		mulcl 9899	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℂ ∧ (3 / 2) ∈ ℂ) → (𝑁 · (3 / 2)) ∈ ℂ)
325	194, 317, 324	sylancl 693	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 · (3 / 2)) ∈ ℂ)
326	325	mulid2d 9937	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
327	323, 326	syl5eq 2656	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
328		2cnne0 11119	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
329		div12 10586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℂ ∧ 3 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
330	220, 328, 329	mp3an23 1408	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℂ → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
331	194, 330	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
332	327, 331	eqtrd 2644	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (3 · (𝑁 / 2)))
333	315, 320, 332	3eqtrd 2648	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (3 · (𝑁 / 2)))
334	333, 84	oveq12d 6567	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))))
335	77	recni 9931	. . . . . . . . . . . . . 14 ⊢ (9 / 4) ∈ ℂ
336	335	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (9 / 4) ∈ ℂ)
337	87	recnd 9947	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℂ)
338	245, 336, 337	mulassd 9942	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))
339	220	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 3 ∈ ℂ)
340	78	rpcnd 11750	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 2) ∈ ℂ)
341	85	recnd 9947	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (log‘(𝑁 / 2)) ∈ ℂ)
342	78	rpne0d 11753	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 / 2) ≠ 0)
343	341, 340, 342	divcld 10680	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℂ)
344	339, 340, 343	mulassd 9942	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))))
345	341, 340, 342	divcan2d 10682	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (log‘(𝑁 / 2)))
346	345	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ (𝜑 → (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
347	344, 346	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · (log‘(𝑁 / 2))))
348	334, 338, 347	3eqtr3d 2652	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
349	220, 198	mulcli 9924	. . . . . . . . . . . . 13 ⊢ (3 · (log‘2)) ∈ ℂ
350	349	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘2)) ∈ ℂ)
351		mulcl 9899	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (3 · (log‘𝑁)) ∈ ℂ)
352	220, 170, 351	sylancr 694	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘𝑁)) ∈ ℂ)
353	271, 350, 352	npncan3d 10307	. . . . . . . . . . 11 ⊢ (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
354	306, 348, 353	3eqtr4d 2654	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))))
355	118, 93	remulcli 9933	. . . . . . . . . . . . 13 ⊢ (2 · (log‘2)) ∈ ℝ
356	355	recni 9931	. . . . . . . . . . . 12 ⊢ (2 · (log‘2)) ∈ ℂ
357	356	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (log‘2)) ∈ ℂ)
358		subcl 10159	. . . . . . . . . . . 12 ⊢ (((log‘𝑁) ∈ ℂ ∧ (5 · (log‘2)) ∈ ℂ) → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
359	170, 270, 358	sylancl 693	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
360	357, 296, 359	addassd 9941	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
361	299, 354, 360	3eqtr4d 2654	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))))
362	361	oveq2d 6565	. . . . . . . 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 9899	. . . . . . . . . . 11 ⊢ ((((√‘(2 · 𝑁)) / 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
364	255, 198, 363	sylancl 693	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
365	255, 170	mulcld 9939	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) ∈ ℂ)
366	89	recnd 9947	. . . . . . . . . . 11 ⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℂ)
367	245, 366	mulcld 9939	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
368	364, 365, 367	addassd 9941	. . . . . . . . 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 6565	. . . . . . . . . . 11 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))))
370	255, 249, 170	adddid 9943	. . . . . . . . . . 11 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
371	369, 370	eqtrd 2644	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
372	371	oveq1d 6564	. . . . . . . . 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 6565	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))))
374	90	recnd 9947	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
375	98	recnd 9947	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℂ)
376	245, 374, 375	adddid 9943	. . . . . . . . . . 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 2644	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
378	73	recnd 9947	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℂ)
379	245, 378, 366	adddid 9943	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
380	95	rpge0d 11752	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ≤ (2 · 𝑁))
381		remsqsqrt 13845	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
382	234, 380, 381	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
383	382	oveq1d 6564	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = ((2 · 𝑁) / 3))
384	114	recnd 9947	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℂ)
385	221	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ≠ 0)
386	384, 384, 339, 385	div23d 10717	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
387	383, 386	eqtr3d 2646	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · 𝑁) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
388	387	oveq1d 6564	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))))
389	255, 384, 378	mulassd 9942	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))))
390		0le2 10988	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ≤ 2
391	118, 390	pm3.2i 470	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℝ ∧ 0 ≤ 2)
392	61	rprege0d 11755	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
393		sqrtmul 13848	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
394	391, 392, 393	sylancr 694	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
395	394	oveq1d 6564	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))))
396	60	recni 9931	. . . . . . . . . . . . . . . . . 18 ⊢ (√‘2) ∈ ℂ
397	396	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘2) ∈ ℂ)
398	62	rpcnd 11750	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘𝑁) ∈ ℂ)
399	71	recnd 9947	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℂ)
400	397, 398, 397, 399	mul4d 10127	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))))
401		remsqsqrt 13845	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
402	118, 390, 401	mp2an 704	. . . . . . . . . . . . . . . . . . 19 ⊢ ((√‘2) · (√‘2)) = 2
403	402	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((√‘2) · (√‘2)) = 2)
404	68	oveq2d 6565	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))))
405	69	recnd 9947	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (log‘(√‘𝑁)) ∈ ℂ)
406	62	rpne0d 11753	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑁) ≠ 0)
407	405, 398, 406	divcan2d 10682	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))) = (log‘(√‘𝑁)))
408	404, 407	eqtrd 2644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = (log‘(√‘𝑁)))
409	403, 408	oveq12d 6567	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (2 · (log‘(√‘𝑁))))
410	405	2timesd 11152	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (log‘(√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
411	62, 62	relogmuld 24175	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
412		remsqsqrt 13845	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
413	392, 412	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
414	413	fveq2d 6107	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = (log‘𝑁))
415	411, 414	eqtr3d 2646	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘(√‘𝑁)) + (log‘(√‘𝑁))) = (log‘𝑁))
416	409, 410, 415	3eqtrd 2648	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
417	395, 400, 416	3eqtrd 2648	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
418	417	oveq2d 6565	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
419	388, 389, 418	3eqtrd 2648	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
420	419	oveq1d 6564	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
421	379, 420	eqtrd 2644	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
422	387	oveq1d 6564	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))))
423	255, 384, 375	mulassd 9942	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))))
424	96	rpne0d 11753	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (√‘(2 · 𝑁)) ≠ 0)
425	249, 384, 424	divcan2d 10682	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁)))) = (log‘2))
426	425	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
427	422, 423, 426	3eqtrd 2648	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
428	421, 427	oveq12d 6567	. . . . . . . . . 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 9938	. . . . . . . . . . 11 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) ∈ ℂ)
430	429, 364	addcomd 10117	. . . . . . . . . 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 2648	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
432	368, 372, 431	3eqtr4rd 2655	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
433	255, 257	mulcld 9939	. . . . . . . . 9 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) ∈ ℂ)
434		addcl 9897	. . . . . . . . . 10 ⊢ (((2 · (log‘2)) ∈ ℂ ∧ (2 · (log‘𝑁)) ∈ ℂ) → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
435	356, 296, 434	sylancr 694	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
436	433, 435, 359	addassd 9941	. . . . . . . 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 2654	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))))
438	274, 276, 437	3eqtr4rd 2655	. . . . . 6 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
439	193, 254, 438	3brtr4d 4615	. . . . 5 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹‘𝑁)))
440	101, 100, 244	ltmul2d 11790	. . . . 5 ⊢ (𝜑 → ((log‘2) < (𝐹‘𝑁) ↔ (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹‘𝑁))))
441	439, 440	mpbird 246	. . . 4 ⊢ (𝜑 → (log‘2) < (𝐹‘𝑁))
442	45, 101, 100, 102, 441	lttrd 10077	. . 3 ⊢ (𝜑 → (𝐹‘;64) < (𝐹‘𝑁))
443	45, 100, 442	ltnsymd 10065	. 2 ⊢ (𝜑 → ¬ (𝐹‘𝑁) < (𝐹‘;64))
444	42, 443	pm2.21dd 185	1 ⊢ (𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953   ≤ cle 9954   − cmin 10145   / cdiv 10563  ℕcn 10897  2c2 10947  3c3 10948  4c4 10949  5c5 10950  6c6 10951  8c8 10953  9c9 10954  ℤcz 11254  ;cdc 11369  ℤ_≥cuz 11563  ℝ⁺crp 11708  ⌊cfl 12453  ↑cexp 12722  Ccbc 12951  √csqrt 13821  expce 14631  eceu 14632  ℙcprime 15223   pCnt cpc 15379  logclog 24105  ↑_𝑐ccxp 24106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-xnn0 11241  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ioc 12051  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-ef 14637  df-e 14638  df-sin 14639  df-cos 14640  df-pi 14642  df-dvds 14822  df-gcd 15055  df-prm 15224  df-pc 15380  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lp 20750  df-perf 20751  df-cn 20841  df-cnp 20842  df-haus 20929  df-tx 21175  df-hmeo 21368  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-xms 21935  df-ms 21936  df-tms 21937  df-cncf 22489  df-limc 23436  df-dv 23437  df-log 24107  df-cxp 24108  df-cht 24623  df-ppi 24626

This theorem is referenced by:  bpos  24818