hgt750leme - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hgt750leme		Structured version Visualization version GIF version

Theorem hgt750leme 35354

Description: An upper bound on the contribution of the non-prime terms in the Statement 7.50 of [Helfgott] p. 69. (Contributed by Thierry Arnoux, 29-Dec-2021.)

**Hypotheses**
Ref	Expression
hgt750leme.o	⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
hgt750leme.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
hgt750leme.0	⊢ (𝜑 → (;10↑;27) ≤ 𝑁)
hgt750leme.h	⊢ (𝜑 → 𝐻:ℕ⟶(0[,)+∞))
hgt750leme.k	⊢ (𝜑 → 𝐾:ℕ⟶(0[,)+∞))
hgt750leme.1	⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐾‘𝑚) ≤ (1._0_7_9_9_55))
hgt750leme.2	⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘𝑚) ≤ (1._4_14))

**Assertion**
Ref	Expression
hgt750leme	⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))

Distinct variable groups: 𝑧,𝑂 𝑚,𝐻 𝑚,𝐾 𝑚,𝑁,𝑛 𝑚,𝑂,𝑛,𝑧 𝜑,𝑚,𝑛 Allowed substitution hints: 𝜑(𝑧) 𝐻(𝑧, 𝑛) 𝐾(𝑧, 𝑛) 𝑁(𝑧)

Proof of Theorem hgt750leme Dummy variables 𝑎 𝑐 𝑑 𝑒 𝑖 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hgt750leme.n	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
2	1	nnnn0d 12691	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
3		3nn0 12648	. . . . . 6 ⊢ 3 ∈ ℕ₀
4	3	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ₀)
5		ssidd 3936	. . . . 5 ⊢ (𝜑 → ℕ ⊆ ℕ)
6	2, 4, 5	reprfi2 35319	. . . 4 ⊢ (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
7		diffi 9215	. . . 4 ⊢ ((ℕ(repr‘3)𝑁) ∈ Fin → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
8	6, 7	syl 18	. . 3 ⊢ (𝜑 → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
9		vmaf 27473	. . . . . . 7 ⊢ Λ:ℕ⟶ℝ
10	9	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → Λ:ℕ⟶ℝ)
11		ssidd 3936	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ℕ ⊆ ℕ)
12	1	nnzd 12743	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℤ)
13	12	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑁 ∈ ℤ)
14	3	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 3 ∈ ℕ₀)
15		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)))
16	15	eldifad 4054	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
17	11, 13, 14, 16	reprf 35308	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛:(0..^3)⟶ℕ)
18		c0ex 11324	. . . . . . . . . 10 ⊢ 0 ∈ V
19	18	tpid1 4729	. . . . . . . . 9 ⊢ 0 ∈ {0, 1, 2}
20		fzo0to3tp 13911	. . . . . . . . 9 ⊢ (0..^3) = {0, 1, 2}
21	19, 20	eleqtrri 2863	. . . . . . . 8 ⊢ 0 ∈ (0..^3)
22	21	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 0 ∈ (0..^3))
23	17, 22	ffvelcdmd 7106	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘0) ∈ ℕ)
24	10, 23	ffvelcdmd 7106	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘0)) ∈ ℝ)
25		rge0ssre 13611	. . . . . 6 ⊢ (0[,)+∞) ⊆ ℝ
26		hgt750leme.h	. . . . . . . 8 ⊢ (𝜑 → 𝐻:ℕ⟶(0[,)+∞))
27	26	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐻:ℕ⟶(0[,)+∞))
28	27, 23	ffvelcdmd 7106	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ (0[,)+∞))
29	25, 28	sselid 3911	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ ℝ)
30	24, 29	remulcld 11363	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) ∈ ℝ)
31		1eltp012 12437	. . . . . . . . . 10 ⊢ 1 ∈ {0, 1, 2}
32	31, 20	eleqtrri 2863	. . . . . . . . 9 ⊢ 1 ∈ (0..^3)
33	32	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 1 ∈ (0..^3))
34	17, 33	ffvelcdmd 7106	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘1) ∈ ℕ)
35	10, 34	ffvelcdmd 7106	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘1)) ∈ ℝ)
36		hgt750leme.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾:ℕ⟶(0[,)+∞))
37	36	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐾:ℕ⟶(0[,)+∞))
38	37, 34	ffvelcdmd 7106	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ (0[,)+∞))
39	25, 38	sselid 3911	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ ℝ)
40	35, 39	remulcld 11363	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) ∈ ℝ)
41		2ex 12444	. . . . . . . . . . 11 ⊢ 2 ∈ V
42	41	tpid3 4734	. . . . . . . . . 10 ⊢ 2 ∈ {0, 1, 2}
43	42, 20	eleqtrri 2863	. . . . . . . . 9 ⊢ 2 ∈ (0..^3)
44	43	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 2 ∈ (0..^3))
45	17, 44	ffvelcdmd 7106	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘2) ∈ ℕ)
46	10, 45	ffvelcdmd 7106	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘2)) ∈ ℝ)
47	37, 45	ffvelcdmd 7106	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ (0[,)+∞))
48	25, 47	sselid 3911	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ ℝ)
49	46, 48	remulcld 11363	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))) ∈ ℝ)
50	40, 49	remulcld 11363	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))) ∈ ℝ)
51	30, 50	remulcld 11363	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
52	8, 51	fsumrecl 15926	. 2 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
53		3re 12447	. . . 4 ⊢ 3 ∈ ℝ
54	53	a1i 11	. . 3 ⊢ (𝜑 → 3 ∈ ℝ)
55		1nn0 12646	. . . . . . . . 9 ⊢ 1 ∈ ℕ₀
56		0nn0 12645	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
57		7nn0 12652	. . . . . . . . . . 11 ⊢ 7 ∈ ℕ₀
58		9nn0 12654	. . . . . . . . . . . 12 ⊢ 9 ∈ ℕ₀
59		5nn0 12650	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℕ₀
60		5nn 12453	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℕ
61		nnrp 13156	. . . . . . . . . . . . . . 15 ⊢ (5 ∈ ℕ → 5 ∈ ℝ⁺)
62	60, 61	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℝ⁺
63	59, 62	rpdp2cl 33515	. . . . . . . . . . . . 13 ⊢ _55 ∈ ℝ⁺
64	58, 63	rpdp2cl 33515	. . . . . . . . . . . 12 ⊢ _9_55 ∈ ℝ⁺
65	58, 64	rpdp2cl 33515	. . . . . . . . . . 11 ⊢ _9_9_55 ∈ ℝ⁺
66	57, 65	rpdp2cl 33515	. . . . . . . . . 10 ⊢ _7_9_9_55 ∈ ℝ⁺
67	56, 66	rpdp2cl 33515	. . . . . . . . 9 ⊢ _0_7_9_9_55 ∈ ℝ⁺
68	55, 67	rpdpcl 33536	. . . . . . . 8 ⊢ (1._0_7_9_9_55) ∈ ℝ⁺
69	68	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℝ⁺)
70	69	rpred 13188	. . . . . 6 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℝ)
71	70	resqcld 14292	. . . . 5 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ)
72		4nn0 12649	. . . . . . . . 9 ⊢ 4 ∈ ℕ₀
73		4nn 12450	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ
74		nnrp 13156	. . . . . . . . . . 11 ⊢ (4 ∈ ℕ → 4 ∈ ℝ⁺)
75	73, 74	ax-mp 5	. . . . . . . . . 10 ⊢ 4 ∈ ℝ⁺
76	55, 75	rpdp2cl 33515	. . . . . . . . 9 ⊢ _14 ∈ ℝ⁺
77	72, 76	rpdp2cl 33515	. . . . . . . 8 ⊢ _4_14 ∈ ℝ⁺
78	55, 77	rpdpcl 33536	. . . . . . 7 ⊢ (1._4_14) ∈ ℝ⁺
79	78	a1i 11	. . . . . 6 ⊢ (𝜑 → (1._4_14) ∈ ℝ⁺)
80	79	rpred 13188	. . . . 5 ⊢ (𝜑 → (1._4_14) ∈ ℝ)
81	71, 80	remulcld 11363	. . . 4 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ)
82		fveq1 6904	. . . . . . . . . 10 ⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
83	82	eleq1d 2849	. . . . . . . . 9 ⊢ (𝑑 = 𝑐 → ((𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
84	83	notbid 321	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
85	84	cbvrabv 3426	. . . . . . 7 ⊢ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
86	85	ssrab3 4010	. . . . . 6 ⊢ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁)
87		ssfi 9213	. . . . . 6 ⊢ (((ℕ(repr‘3)𝑁) ∈ Fin ∧ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁)) → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ∈ Fin)
88	6, 86, 87	sylancl 598	. . . . 5 ⊢ (𝜑 → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ∈ Fin)
89	9	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → Λ:ℕ⟶ℝ)
90		ssidd 3936	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ℕ ⊆ ℕ)
91	12	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑁 ∈ ℤ)
92	3	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 3 ∈ ℕ₀)
93	86	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁))
94	93	sselda 3913	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
95	90, 91, 92, 94	reprf 35308	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛:(0..^3)⟶ℕ)
96	21	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 0 ∈ (0..^3))
97	95, 96	ffvelcdmd 7106	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘0) ∈ ℕ)
98	89, 97	ffvelcdmd 7106	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘0)) ∈ ℝ)
99	32	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 1 ∈ (0..^3))
100	95, 99	ffvelcdmd 7106	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘1) ∈ ℕ)
101	89, 100	ffvelcdmd 7106	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘1)) ∈ ℝ)
102	43	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 2 ∈ (0..^3))
103	95, 102	ffvelcdmd 7106	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘2) ∈ ℕ)
104	89, 103	ffvelcdmd 7106	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘2)) ∈ ℝ)
105	101, 104	remulcld 11363	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
106	98, 105	remulcld 11363	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
107	88, 106	fsumrecl 15926	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
108	81, 107	remulcld 11363	. . 3 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
109	54, 108	remulcld 11363	. 2 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ∈ ℝ)
110		4re 12451	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
111		8re 12463	. . . . . . . . . 10 ⊢ 8 ∈ ℝ
112	110, 111	pm3.2i 476	. . . . . . . . 9 ⊢ (4 ∈ ℝ ∧ 8 ∈ ℝ)
113		dp2cl 33513	. . . . . . . . 9 ⊢ ((4 ∈ ℝ ∧ 8 ∈ ℝ) → _48 ∈ ℝ)
114	112, 113	ax-mp 5	. . . . . . . 8 ⊢ _48 ∈ ℝ
115	53, 114	pm3.2i 476	. . . . . . 7 ⊢ (3 ∈ ℝ ∧ _48 ∈ ℝ)
116		dp2cl 33513	. . . . . . 7 ⊢ ((3 ∈ ℝ ∧ _48 ∈ ℝ) → _3_48 ∈ ℝ)
117	115, 116	ax-mp 5	. . . . . 6 ⊢ _3_48 ∈ ℝ
118		dpcl 33524	. . . . . 6 ⊢ ((7 ∈ ℕ₀ ∧ _3_48 ∈ ℝ) → (7._3_48) ∈ ℝ)
119	57, 117, 118	mp2an 705	. . . . 5 ⊢ (7._3_48) ∈ ℝ
120	119	a1i 11	. . . 4 ⊢ (𝜑 → (7._3_48) ∈ ℝ)
121	1	nnrpd 13186	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
122	121	relogcld 26978	. . . . 5 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
123	1	nnred 12374	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ)
124	121	rpge0d 13192	. . . . . 6 ⊢ (𝜑 → 0 ≤ 𝑁)
125	123, 124	resqrtcld 15611	. . . . 5 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ)
126	121	rpsqrtcld 15605	. . . . . 6 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
127	126	rpne0d 13193	. . . . 5 ⊢ (𝜑 → (√‘𝑁) ≠ 0)
128	122, 125, 127	redivcld 12169	. . . 4 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ)
129	120, 128	remulcld 11363	. . 3 ⊢ (𝜑 → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ∈ ℝ)
130	123	resqcld 14292	. . 3 ⊢ (𝜑 → (𝑁↑2) ∈ ℝ)
131	129, 130	remulcld 11363	. 2 ⊢ (𝜑 → (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) ∈ ℝ)
132		0re 11334	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
133		7re 12460	. . . . . . . . . . . . 13 ⊢ 7 ∈ ℝ
134		9re 12466	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℝ
135		5re 12454	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 ∈ ℝ
136	135, 135	pm3.2i 476	. . . . . . . . . . . . . . . . . 18 ⊢ (5 ∈ ℝ ∧ 5 ∈ ℝ)
137		dp2cl 33513	. . . . . . . . . . . . . . . . . 18 ⊢ ((5 ∈ ℝ ∧ 5 ∈ ℝ) → _55 ∈ ℝ)
138	136, 137	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ _55 ∈ ℝ
139	134, 138	pm3.2i 476	. . . . . . . . . . . . . . . 16 ⊢ (9 ∈ ℝ ∧ _55 ∈ ℝ)
140		dp2cl 33513	. . . . . . . . . . . . . . . 16 ⊢ ((9 ∈ ℝ ∧ _55 ∈ ℝ) → _9_55 ∈ ℝ)
141	139, 140	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _9_55 ∈ ℝ
142	134, 141	pm3.2i 476	. . . . . . . . . . . . . 14 ⊢ (9 ∈ ℝ ∧ _9_55 ∈ ℝ)
143		dp2cl 33513	. . . . . . . . . . . . . 14 ⊢ ((9 ∈ ℝ ∧ _9_55 ∈ ℝ) → _9_9_55 ∈ ℝ)
144	142, 143	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _9_9_55 ∈ ℝ
145	133, 144	pm3.2i 476	. . . . . . . . . . . 12 ⊢ (7 ∈ ℝ ∧ _9_9_55 ∈ ℝ)
146		dp2cl 33513	. . . . . . . . . . . 12 ⊢ ((7 ∈ ℝ ∧ _9_9_55 ∈ ℝ) → _7_9_9_55 ∈ ℝ)
147	145, 146	ax-mp 5	. . . . . . . . . . 11 ⊢ _7_9_9_55 ∈ ℝ
148	132, 147	pm3.2i 476	. . . . . . . . . 10 ⊢ (0 ∈ ℝ ∧ _7_9_9_55 ∈ ℝ)
149		dp2cl 33513	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ _7_9_9_55 ∈ ℝ) → _0_7_9_9_55 ∈ ℝ)
150	148, 149	ax-mp 5	. . . . . . . . 9 ⊢ _0_7_9_9_55 ∈ ℝ
151		dpcl 33524	. . . . . . . . 9 ⊢ ((1 ∈ ℕ₀ ∧ _0_7_9_9_55 ∈ ℝ) → (1._0_7_9_9_55) ∈ ℝ)
152	55, 150, 151	mp2an 705	. . . . . . . 8 ⊢ (1._0_7_9_9_55) ∈ ℝ
153	152	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℝ)
154	153	resqcld 14292	. . . . . 6 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ)
155		1re 11332	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
156	155, 110	pm3.2i 476	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ ∧ 4 ∈ ℝ)
157		dp2cl 33513	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 4 ∈ ℝ) → _14 ∈ ℝ)
158	156, 157	ax-mp 5	. . . . . . . . . 10 ⊢ _14 ∈ ℝ
159	110, 158	pm3.2i 476	. . . . . . . . 9 ⊢ (4 ∈ ℝ ∧ _14 ∈ ℝ)
160		dp2cl 33513	. . . . . . . . 9 ⊢ ((4 ∈ ℝ ∧ _14 ∈ ℝ) → _4_14 ∈ ℝ)
161	159, 160	ax-mp 5	. . . . . . . 8 ⊢ _4_14 ∈ ℝ
162		dpcl 33524	. . . . . . . 8 ⊢ ((1 ∈ ℕ₀ ∧ _4_14 ∈ ℝ) → (1._4_14) ∈ ℝ)
163	55, 161, 162	mp2an 705	. . . . . . 7 ⊢ (1._4_14) ∈ ℝ
164	163	a1i 11	. . . . . 6 ⊢ (𝜑 → (1._4_14) ∈ ℝ)
165	154, 164	remulcld 11363	. . . . 5 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ)
166	35, 46	remulcld 11363	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
167	24, 166	remulcld 11363	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
168	8, 167	fsumrecl 15926	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
169	165, 168	remulcld 11363	. . . 4 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
170	54, 107	remulcld 11363	. . . . 5 ⊢ (𝜑 → (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
171	165, 170	remulcld 11363	. . . 4 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ∈ ℝ)
172		hgt750leme.1	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐾‘𝑚) ≤ (1._0_7_9_9_55))
173		hgt750leme.2	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘𝑚) ≤ (1._4_14))
174	8, 153, 164, 26, 36, 23, 34, 45, 172, 173	hgt750lemf 35349	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
175		hgt750leme.o	. . . . . 6 ⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
176		2re 12441	. . . . . . . 8 ⊢ 2 ∈ ℝ
177	176	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ∈ ℝ)
178		10nn0 12860	. . . . . . . . . 10 ⊢ ;10 ∈ ℕ₀
179		2nn0 12647	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
180	179, 57	deccl 12853	. . . . . . . . . 10 ⊢ ;27 ∈ ℕ₀
181	178, 180	nn0expcli 14255	. . . . . . . . 9 ⊢ (;10↑;27) ∈ ℕ₀
182	181	nn0rei 12641	. . . . . . . 8 ⊢ (;10↑;27) ∈ ℝ
183	182	a1i 11	. . . . . . 7 ⊢ (𝜑 → (;10↑;27) ∈ ℝ)
184	178	numexp1 17280	. . . . . . . . . 10 ⊢ (;10↑1) = ;10
185	178	nn0rei 12641	. . . . . . . . . 10 ⊢ ;10 ∈ ℝ
186	184, 185	eqeltri 2860	. . . . . . . . 9 ⊢ (;10↑1) ∈ ℝ
187	186	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (;10↑1) ∈ ℝ)
188		1nn 12370	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
189		2lt9 12574	. . . . . . . . . . . 12 ⊢ 2 < 9
190	176, 134, 189	ltleii 11457	. . . . . . . . . . 11 ⊢ 2 ≤ 9
191	188, 56, 179, 190	declei 12879	. . . . . . . . . 10 ⊢ 2 ≤ ;10
192	191, 184	breqtrri 5135	. . . . . . . . 9 ⊢ 2 ≤ (;10↑1)
193	192	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≤ (;10↑1))
194		1z 12750	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
195	180	nn0zi 12745	. . . . . . . . . . . 12 ⊢ ;27 ∈ ℤ
196	185, 194, 195	3pm3.2i 1358	. . . . . . . . . . 11 ⊢ (;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ)
197		1lt10 12983	. . . . . . . . . . 11 ⊢ 1 < ;10
198	196, 197	pm3.2i 476	. . . . . . . . . 10 ⊢ ((;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ 1 < ;10)
199		2nn 12440	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
200		1lt9 12575	. . . . . . . . . . . 12 ⊢ 1 < 9
201	155, 134, 200	ltleii 11457	. . . . . . . . . . 11 ⊢ 1 ≤ 9
202	199, 57, 55, 201	declei 12879	. . . . . . . . . 10 ⊢ 1 ≤ ;27
203		leexp2 14338	. . . . . . . . . . 11 ⊢ (((;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ 1 < ;10) → (1 ≤ ;27 ↔ (;10↑1) ≤ (;10↑;27)))
204	203	biimpa 482	. . . . . . . . . 10 ⊢ ((((;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ 1 < ;10) ∧ 1 ≤ ;27) → (;10↑1) ≤ (;10↑;27))
205	198, 202, 204	mp2an 705	. . . . . . . . 9 ⊢ (;10↑1) ≤ (;10↑;27)
206	205	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (;10↑1) ≤ (;10↑;27))
207	177, 187, 183, 193, 206	letrd 11491	. . . . . . 7 ⊢ (𝜑 → 2 ≤ (;10↑;27))
208		hgt750leme.0	. . . . . . 7 ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)
209	177, 183, 123, 207, 208	letrd 11491	. . . . . 6 ⊢ (𝜑 → 2 ≤ 𝑁)
210		eqid 2763	. . . . . 6 ⊢ (𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ↦ (𝑒 ∘ if(𝑎 = 0, ( I ↾ (0..^3)), ((pmTrsp‘(0..^3))‘{𝑎, 0})))) = (𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ↦ (𝑒 ∘ if(𝑎 = 0, ( I ↾ (0..^3)), ((pmTrsp‘(0..^3))‘{𝑎, 0}))))
211	175, 1, 209, 85, 210	hgt750lema 35353	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
212		2z 12752	. . . . . . . . 9 ⊢ 2 ∈ ℤ
213	212	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℤ)
214	69, 213	rpexpcld 14415	. . . . . . 7 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ⁺)
215	214, 79	rpmulcld 13204	. . . . . 6 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ⁺)
216	168, 170, 215	lemul2d 13232	. . . . 5 ⊢ (𝜑 → (Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ↔ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))))
217	211, 216	mpbid 235	. . . 4 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))))
218	52, 169, 171, 174, 217	letrd 11491	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))))
219	153	recnd 11361	. . . . . 6 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℂ)
220	219	sqcld 14311	. . . . 5 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℂ)
221	164	recnd 11361	. . . . 5 ⊢ (𝜑 → (1._4_14) ∈ ℂ)
222	220, 221	mulcld 11353	. . . 4 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℂ)
223		3cn 12448	. . . . 5 ⊢ 3 ∈ ℂ
224	223	a1i 11	. . . 4 ⊢ (𝜑 → 3 ∈ ℂ)
225	107	recnd 11361	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℂ)
226	222, 224, 225	mul12d 11543	. . 3 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) = (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))))
227	218, 226	breqtrd 5134	. 2 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))))
228		fzfi 14139	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ Fin
229		diffi 9215	. . . . . . . . . . 11 ⊢ ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
230	228, 229	ax-mp 5	. . . . . . . . . 10 ⊢ ((1...𝑁) ∖ ℙ) ∈ Fin
231		snfi 9096	. . . . . . . . . 10 ⊢ {2} ∈ Fin
232		unfi 9211	. . . . . . . . . 10 ⊢ ((((1...𝑁) ∖ ℙ) ∈ Fin ∧ {2} ∈ Fin) → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
233	230, 231, 232	mp2an 705	. . . . . . . . 9 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin
234	233	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
235	9	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → Λ:ℕ⟶ℝ)
236		fz1ssnn 13713	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ ℕ
237	236	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
238	237	ssdifssd 4086	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ ℕ)
239	199	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℕ)
240	239	snssd 4747	. . . . . . . . . . 11 ⊢ (𝜑 → {2} ⊆ ℕ)
241	238, 240	unssd 4193	. . . . . . . . . 10 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
242	241	sselda 3913	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 𝑖 ∈ ℕ)
243	235, 242	ffvelcdmd 7106	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℝ)
244	234, 243	fsumrecl 15926	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) ∈ ℝ)
245		chpvalz 35324	. . . . . . . . 9 ⊢ (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
246	12, 245	syl 18	. . . . . . . 8 ⊢ (𝜑 → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
247		chpf 27477	. . . . . . . . . 10 ⊢ ψ:ℝ⟶ℝ
248	247	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ψ:ℝ⟶ℝ)
249	248, 123	ffvelcdmd 7106	. . . . . . . 8 ⊢ (𝜑 → (ψ‘𝑁) ∈ ℝ)
250	246, 249	eqeltrrd 2865	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℝ)
251	244, 250	remulcld 11363	. . . . . 6 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ∈ ℝ)
252	122, 251	remulcld 11363	. . . . 5 ⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ∈ ℝ)
253	81, 252	remulcld 11363	. . . 4 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ∈ ℝ)
254	54, 253	remulcld 11363	. . 3 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ∈ ℝ)
255	175, 1, 209, 85	hgt750lemb 35352	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
256	107, 252, 215	lemul2d 13232	. . . . 5 ⊢ (𝜑 → (Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ↔ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))))
257	255, 256	mpbid 235	. . . 4 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))))
258		3rp 13150	. . . . . 6 ⊢ 3 ∈ ℝ⁺
259	258	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℝ⁺)
260	108, 253, 259	lemul2d 13232	. . . 4 ⊢ (𝜑 → (((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ↔ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ≤ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))))))
261	257, 260	mpbid 235	. . 3 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ≤ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))))
262		6re 12457	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℝ
263	262, 53	pm3.2i 476	. . . . . . . . . . . . . . . 16 ⊢ (6 ∈ ℝ ∧ 3 ∈ ℝ)
264		dp2cl 33513	. . . . . . . . . . . . . . . 16 ⊢ ((6 ∈ ℝ ∧ 3 ∈ ℝ) → _63 ∈ ℝ)
265	263, 264	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _63 ∈ ℝ
266	176, 265	pm3.2i 476	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℝ ∧ _63 ∈ ℝ)
267		dp2cl 33513	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ _63 ∈ ℝ) → _2_63 ∈ ℝ)
268	266, 267	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _2_63 ∈ ℝ
269	110, 268	pm3.2i 476	. . . . . . . . . . . 12 ⊢ (4 ∈ ℝ ∧ _2_63 ∈ ℝ)
270		dp2cl 33513	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ ∧ _2_63 ∈ ℝ) → _4_2_63 ∈ ℝ)
271	269, 270	ax-mp 5	. . . . . . . . . . 11 ⊢ _4_2_63 ∈ ℝ
272		dpcl 33524	. . . . . . . . . . 11 ⊢ ((1 ∈ ℕ₀ ∧ _4_2_63 ∈ ℝ) → (1._4_2_63) ∈ ℝ)
273	55, 271, 272	mp2an 705	. . . . . . . . . 10 ⊢ (1._4_2_63) ∈ ℝ
274	273	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1._4_2_63) ∈ ℝ)
275	274, 125	remulcld 11363	. . . . . . . 8 ⊢ (𝜑 → ((1._4_2_63) · (√‘𝑁)) ∈ ℝ)
276	111, 53	pm3.2i 476	. . . . . . . . . . . . . . . . . 18 ⊢ (8 ∈ ℝ ∧ 3 ∈ ℝ)
277		dp2cl 33513	. . . . . . . . . . . . . . . . . 18 ⊢ ((8 ∈ ℝ ∧ 3 ∈ ℝ) → _83 ∈ ℝ)
278	276, 277	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ _83 ∈ ℝ
279	111, 278	pm3.2i 476	. . . . . . . . . . . . . . . 16 ⊢ (8 ∈ ℝ ∧ _83 ∈ ℝ)
280		dp2cl 33513	. . . . . . . . . . . . . . . 16 ⊢ ((8 ∈ ℝ ∧ _83 ∈ ℝ) → _8_83 ∈ ℝ)
281	279, 280	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _8_83 ∈ ℝ
282	53, 281	pm3.2i 476	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℝ ∧ _8_83 ∈ ℝ)
283		dp2cl 33513	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℝ ∧ _8_83 ∈ ℝ) → _3_8_83 ∈ ℝ)
284	282, 283	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _3_8_83 ∈ ℝ
285	132, 284	pm3.2i 476	. . . . . . . . . . . 12 ⊢ (0 ∈ ℝ ∧ _3_8_83 ∈ ℝ)
286		dp2cl 33513	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ _3_8_83 ∈ ℝ) → _0_3_8_83 ∈ ℝ)
287	285, 286	ax-mp 5	. . . . . . . . . . 11 ⊢ _0_3_8_83 ∈ ℝ
288		dpcl 33524	. . . . . . . . . . 11 ⊢ ((1 ∈ ℕ₀ ∧ _0_3_8_83 ∈ ℝ) → (1._0_3_8_83) ∈ ℝ)
289	55, 287, 288	mp2an 705	. . . . . . . . . 10 ⊢ (1._0_3_8_83) ∈ ℝ
290	289	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1._0_3_8_83) ∈ ℝ)
291	290, 123	remulcld 11363	. . . . . . . 8 ⊢ (𝜑 → ((1._0_3_8_83) · 𝑁) ∈ ℝ)
292	275, 291	remulcld 11363	. . . . . . 7 ⊢ (𝜑 → (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)) ∈ ℝ)
293	122, 292	remulcld 11363	. . . . . 6 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) ∈ ℝ)
294	81, 293	remulcld 11363	. . . . 5 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))) ∈ ℝ)
295	54, 294	remulcld 11363	. . . 4 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))))) ∈ ℝ)
296		vmage0 27475	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℕ → 0 ≤ (Λ‘𝑖))
297	242, 296	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 0 ≤ (Λ‘𝑖))
298	234, 243, 297	fsumge0 15988	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖))
299	1, 208	hgt750lemd 35344	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) < ((1._4_2_63) · (√‘𝑁)))
300		fzfid 14140	. . . . . . . . . 10 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
301	9	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
302	237	sselda 3913	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
303	301, 302	ffvelcdmd 7106	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
304		vmage0 27475	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → 0 ≤ (Λ‘𝑗))
305	302, 304	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 0 ≤ (Λ‘𝑗))
306	300, 303, 305	fsumge0 15988	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
307	1	hgt750lemc 35343	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) < ((1._0_3_8_83) · 𝑁))
308	244, 275, 250, 291, 298, 299, 306, 307	ltmul12ad 12282	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) < (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))
309	251, 292, 308	ltled 11482	. . . . . . 7 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ≤ (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))
310	155	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℝ)
311		1lt2 12539	. . . . . . . . . . 11 ⊢ 1 < 2
312	311	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 < 2)
313	310, 177, 123, 312, 209	ltletrd 11494	. . . . . . . . 9 ⊢ (𝜑 → 1 < 𝑁)
314	123, 313	rplogcld 26984	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ⁺)
315	251, 292, 314	lemul2d 13232	. . . . . . 7 ⊢ (𝜑 → ((Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ≤ (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)) ↔ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ≤ ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))))
316	309, 315	mpbid 235	. . . . . 6 ⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ≤ ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))))
317	252, 293, 215	lemul2d 13232	. . . . . 6 ⊢ (𝜑 → (((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ≤ ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) ↔ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))))))
318	316, 317	mpbid 235	. . . . 5 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))))
319	253, 294, 259	lemul2d 13232	. . . . 5 ⊢ (𝜑 → (((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))) ↔ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ≤ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))))))
320	318, 319	mpbid 235	. . . 4 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ≤ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))))))
321	152	resqcli 14353	. . . . . . . . . 10 ⊢ ((1._0_7_9_9_55)↑2) ∈ ℝ
322	321, 163	remulcli 11349	. . . . . . . . 9 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ
323	273, 289	remulcli 11349	. . . . . . . . 9 ⊢ ((1._4_2_63) · (1._0_3_8_83)) ∈ ℝ
324	322, 323	remulcli 11349	. . . . . . . 8 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) ∈ ℝ
325	53, 324	remulcli 11349	. . . . . . 7 ⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) ∈ ℝ
326		hgt750lem2 35348	. . . . . . 7 ⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) < (7._3_48)
327	325, 119, 326	ltleii 11457	. . . . . 6 ⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) ≤ (7._3_48)
328	325	a1i 11	. . . . . . 7 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) ∈ ℝ)
329	314, 126	rpdivcld 13205	. . . . . . . 8 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ⁺)
330	121, 213	rpexpcld 14415	. . . . . . . 8 ⊢ (𝜑 → (𝑁↑2) ∈ ℝ⁺)
331	329, 330	rpmulcld 13204	. . . . . . 7 ⊢ (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) ∈ ℝ⁺)
332	328, 120, 331	lemul1d 13231	. . . . . 6 ⊢ (𝜑 → ((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) ≤ (7._3_48) ↔ ((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))) ≤ ((7._3_48) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)))))
333	327, 332	mpbii 236	. . . . 5 ⊢ (𝜑 → ((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))) ≤ ((7._3_48) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
334	274	recnd 11361	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1._4_2_63) ∈ ℂ)
335	125	recnd 11361	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (√‘𝑁) ∈ ℂ)
336	290	recnd 11361	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1._0_3_8_83) ∈ ℂ)
337	123	recnd 11361	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℂ)
338	334, 335, 336, 337	mul4d 11546	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)) = (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)))
339	338	oveq2d 7456	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) = ((log‘𝑁) · (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁))))
340	122	recnd 11361	. . . . . . . . . . . . 13 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
341	334, 336	mulcld 11353	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1._4_2_63) · (1._0_3_8_83)) ∈ ℂ)
342	335, 337	mulcld 11353	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((√‘𝑁) · 𝑁) ∈ ℂ)
343	341, 342	mulcld 11353	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)) ∈ ℂ)
344	340, 343	mulcomd 11354	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁))) = ((((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)) · (log‘𝑁)))
345	339, 344	eqtrd 2798	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) = ((((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)) · (log‘𝑁)))
346	341, 342, 340	mulassd 11356	. . . . . . . . . . 11 ⊢ (𝜑 → ((((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)) · (log‘𝑁)) = (((1._4_2_63) · (1._0_3_8_83)) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
347	345, 346	eqtrd 2798	. . . . . . . . . 10 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) = (((1._4_2_63) · (1._0_3_8_83)) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
348	347	oveq2d 7456	. . . . . . . . 9 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))) = ((((1._0_7_9_9_55)↑2) · (1._4_14)) · (((1._4_2_63) · (1._0_3_8_83)) · (((√‘𝑁) · 𝑁) · (log‘𝑁)))))
349	81	recnd 11361	. . . . . . . . . 10 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℂ)
350	342, 340	mulcld 11353	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) ∈ ℂ)
351	349, 341, 350	mulassd 11356	. . . . . . . . 9 ⊢ (𝜑 → (((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))) = ((((1._0_7_9_9_55)↑2) · (1._4_14)) · (((1._4_2_63) · (1._0_3_8_83)) · (((√‘𝑁) · 𝑁) · (log‘𝑁)))))
352	348, 351	eqtr4d 2801	. . . . . . . 8 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))) = (((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
353	352	oveq2d 7456	. . . . . . 7 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))))) = (3 · (((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) · (((√‘𝑁) · 𝑁) · (log‘𝑁)))))
354	54	recnd 11361	. . . . . . . 8 ⊢ (𝜑 → 3 ∈ ℂ)
355	349, 341	mulcld 11353	. . . . . . . 8 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) ∈ ℂ)
356	354, 355, 350	mulassd 11356	. . . . . . 7 ⊢ (𝜑 → ((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))) = (3 · (((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) · (((√‘𝑁) · 𝑁) · (log‘𝑁)))))
357	353, 356	eqtr4d 2801	. . . . . 6 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))))) = ((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
358	130	recnd 11361	. . . . . . . . 9 ⊢ (𝜑 → (𝑁↑2) ∈ ℂ)
359	340, 335, 358, 127	div32d 12140	. . . . . . . 8 ⊢ (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) = ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))))
360	358, 335, 127	divcld 12117	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) ∈ ℂ)
361	340, 360	mulcomd 11354	. . . . . . . 8 ⊢ (𝜑 → ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))) = (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)))
362	337	sqvald 14310	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁↑2) = (𝑁 · 𝑁))
363	362	oveq1d 7455	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((𝑁 · 𝑁) / (√‘𝑁)))
364	337, 337, 335, 127	divassd 12152	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 · 𝑁) / (√‘𝑁)) = (𝑁 · (𝑁 / (√‘𝑁))))
365		divsqrtid 35290	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℝ⁺ → (𝑁 / (√‘𝑁)) = (√‘𝑁))
366	121, 365	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 / (√‘𝑁)) = (√‘𝑁))
367	366	oveq2d 7456	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · (𝑁 / (√‘𝑁))) = (𝑁 · (√‘𝑁)))
368	363, 364, 367	3eqtrd 2802	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = (𝑁 · (√‘𝑁)))
369	337, 335	mulcomd 11354	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 · (√‘𝑁)) = ((√‘𝑁) · 𝑁))
370	368, 369	eqtrd 2798	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((√‘𝑁) · 𝑁))
371	370	oveq1d 7455	. . . . . . . 8 ⊢ (𝜑 → (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)) = (((√‘𝑁) · 𝑁) · (log‘𝑁)))
372	359, 361, 371	3eqtrrd 2803	. . . . . . 7 ⊢ (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) = (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)))
373	372	oveq2d 7456	. . . . . 6 ⊢ (𝜑 → ((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))) = ((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
374	357, 373	eqtrd 2798	. . . . 5 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))))) = ((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
375	120	recnd 11361	. . . . . 6 ⊢ (𝜑 → (7._3_48) ∈ ℂ)
376	128	recnd 11361	. . . . . 6 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℂ)
377	375, 376, 358	mulassd 11356	. . . . 5 ⊢ (𝜑 → (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) = ((7._3_48) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
378	333, 374, 377	3brtr4d 5140	. . . 4 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))))) ≤ (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
379	254, 295, 131, 320, 378	letrd 11491	. . 3 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ≤ (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
380	109, 254, 131, 261, 379	letrd 11491	. 2 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ≤ (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
381	52, 109, 131, 227, 380	letrd 11491	1 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 {crab 3416 ⊆ wss 3900 ∖ cdif 4048 ∩ cin 4092 ∪ cun 4152 ifcif 4485 {csn 4588 {cpr 4590 {ctp 4592 class class class wbr 5106 ↦ cmpt 5189 I cid 5549 ↾ cres 5657 ∘ ccom 5659 ⟶wf 6551 ‘cfv 6555 (class class class)co 7440 Fincfn 8998 ℂcc 11222 ℝcr 11223 0cc0 11224 1c1 11225 · cmul 11229 +∞cpnf 11364 < clt 11367 ≤ cle 11368 / cdiv 11997 ℕcn 12359 2c2 12421 3c3 12422 4c4 12423 5c5 12424 6c6 12425 7c7 12426 8c8 12427 9c9 12428 ℕ₀cn0 12630 ℤcz 12717 cdc 12838 ℝ⁺crp 13144 [,)cico 13502 ...cfz 13663 ..^cfzo 13812 ↑cexp 14228 √csqrt 15426 Σcsu 15879 ∥ cdvds 16448 ℙcprime 16872 pmTrspcpmtr 19682 logclog 26909 Λcvma 27446 ψcchp 27447 cdp2 33504 .cdp 33521 reprcrepr 35304

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-inf2 9666 ax-ac2 10565 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301 ax-pre-sup 11302 ax-addf 11303 ax-ros335 35341 ax-ros336 35342

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-isom 6564 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-of 7714 df-om 7899 df-1st 8022 df-2nd 8023 df-supp 8202 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-2o 8502 df-oadd 8505 df-er 8742 df-map 8874 df-pm 8875 df-ixp 8951 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-fsupp 9379 df-fi 9427 df-sup 9458 df-inf 9459 df-oi 9528 df-dju 10006 df-card 10044 df-ac 10219 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-div 11998 df-nn 12360 df-2 12429 df-3 12430 df-4 12431 df-5 12432 df-6 12433 df-7 12434 df-8 12435 df-9 12436 df-n0 12631 df-xnn0 12704 df-z 12718 df-dec 12839 df-uz 12990 df-q 13100 df-rp 13145 df-xneg 13265 df-xadd 13266 df-xmul 13267 df-ioo 13504 df-ioc 13505 df-ico 13506 df-icc 13507 df-fz 13664 df-fzo 13813 df-fl 13956 df-mod 14034 df-seq 14169 df-exp 14229 df-fac 14442 df-bc 14471 df-hash 14499 df-shft 15246 df-cj 15292 df-re 15293 df-im 15294 df-sqrt 15428 df-abs 15429 df-limsup 15664 df-clim 15681 df-rlim 15682 df-sum 15880 df-prod 16099 df-ef 16259 df-sin 16261 df-cos 16262 df-tan 16263 df-pi 16264 df-dvds 16449 df-gcd 16691 df-prm 16873 df-pc 17041 df-struct 17351 df-sets 17368 df-slot 17386 df-ndx 17398 df-base 17414 df-ress 17435 df-plusg 17467 df-mulr 17468 df-starv 17469 df-sca 17470 df-vsca 17471 df-ip 17472 df-tset 17473 df-ple 17474 df-ds 17476 df-unif 17477 df-hom 17478 df-cco 17479 df-rest 17619 df-topn 17620 df-0g 17638 df-gsum 17639 df-topgen 17640 df-pt 17641 df-prds 17644 df-xrs 17700 df-qtop 17705 df-imas 17706 df-xps 17708 df-mre 17782 df-mrc 17783 df-acs 17785 df-mgm 18842 df-sgrp 18934 df-mnd 18950 df-submnd 19005 df-mulg 19304 df-cntz 19558 df-pmtr 19683 df-cmn 20023 df-psmet 21697 df-xmet 21698 df-met 21699 df-bl 21700 df-mopn 21701 df-fbas 21702 df-fg 21703 df-cnfld 21706 df-top 23239 df-topon 23256 df-topsp 23278 df-bases 23291 df-cld 23364 df-ntr 23365 df-cls 23366 df-nei 23443 df-lp 23481 df-perf 23482 df-cn 23572 df-cnp 23573 df-haus 23660 df-cmp 23732 df-tx 23908 df-hmeo 24101 df-fil 24192 df-fm 24284 df-flim 24285 df-flf 24286 df-xms 24666 df-ms 24667 df-tms 24668 df-cncf 25226 df-limc 26213 df-dv 26214 df-ulm 26731 df-log 26911 df-atan 27222 df-cht 27451 df-vma 27452 df-chp 27453 df-dp2 33505 df-dp 33522 df-repr 35305

This theorem is used by: tgoldbachgtde 35356

W3C validator