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 32638

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 12293	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
3		3nn0 12251	. . . . . 6 ⊢ 3 ∈ ℕ₀
4	3	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ₀)
5		ssidd 3944	. . . . 5 ⊢ (𝜑 → ℕ ⊆ ℕ)
6	2, 4, 5	reprfi2 32603	. . . 4 ⊢ (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
7		diffi 8962	. . . 4 ⊢ ((ℕ(repr‘3)𝑁) ∈ Fin → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
8	6, 7	syl 17	. . 3 ⊢ (𝜑 → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
9		vmaf 26268	. . . . . . 7 ⊢ Λ:ℕ⟶ℝ
10	9	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → Λ:ℕ⟶ℝ)
11		ssidd 3944	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ℕ ⊆ ℕ)
12	1	nnzd 12425	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℤ)
13	12	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑁 ∈ ℤ)
14	3	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 3 ∈ ℕ₀)
15		simpr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)))
16	15	eldifad 3899	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
17	11, 13, 14, 16	reprf 32592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛:(0..^3)⟶ℕ)
18		c0ex 10969	. . . . . . . . . 10 ⊢ 0 ∈ V
19	18	tpid1 4704	. . . . . . . . 9 ⊢ 0 ∈ {0, 1, 2}
20		fzo0to3tp 13473	. . . . . . . . 9 ⊢ (0..^3) = {0, 1, 2}
21	19, 20	eleqtrri 2838	. . . . . . . 8 ⊢ 0 ∈ (0..^3)
22	21	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 0 ∈ (0..^3))
23	17, 22	ffvelrnd 6962	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘0) ∈ ℕ)
24	10, 23	ffvelrnd 6962	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘0)) ∈ ℝ)
25		rge0ssre 13188	. . . . . 6 ⊢ (0[,)+∞) ⊆ ℝ
26		hgt750leme.h	. . . . . . . 8 ⊢ (𝜑 → 𝐻:ℕ⟶(0[,)+∞))
27	26	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐻:ℕ⟶(0[,)+∞))
28	27, 23	ffvelrnd 6962	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ (0[,)+∞))
29	25, 28	sselid 3919	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ ℝ)
30	24, 29	remulcld 11005	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) ∈ ℝ)
31		1ex 10971	. . . . . . . . . . 11 ⊢ 1 ∈ V
32	31	tpid2 4706	. . . . . . . . . 10 ⊢ 1 ∈ {0, 1, 2}
33	32, 20	eleqtrri 2838	. . . . . . . . 9 ⊢ 1 ∈ (0..^3)
34	33	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 1 ∈ (0..^3))
35	17, 34	ffvelrnd 6962	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘1) ∈ ℕ)
36	10, 35	ffvelrnd 6962	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘1)) ∈ ℝ)
37		hgt750leme.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾:ℕ⟶(0[,)+∞))
38	37	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐾:ℕ⟶(0[,)+∞))
39	38, 35	ffvelrnd 6962	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ (0[,)+∞))
40	25, 39	sselid 3919	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ ℝ)
41	36, 40	remulcld 11005	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) ∈ ℝ)
42		2ex 12050	. . . . . . . . . . 11 ⊢ 2 ∈ V
43	42	tpid3 4709	. . . . . . . . . 10 ⊢ 2 ∈ {0, 1, 2}
44	43, 20	eleqtrri 2838	. . . . . . . . 9 ⊢ 2 ∈ (0..^3)
45	44	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 2 ∈ (0..^3))
46	17, 45	ffvelrnd 6962	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘2) ∈ ℕ)
47	10, 46	ffvelrnd 6962	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘2)) ∈ ℝ)
48	38, 46	ffvelrnd 6962	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ (0[,)+∞))
49	25, 48	sselid 3919	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ ℝ)
50	47, 49	remulcld 11005	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))) ∈ ℝ)
51	41, 50	remulcld 11005	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))) ∈ ℝ)
52	30, 51	remulcld 11005	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
53	8, 52	fsumrecl 15446	. 2 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
54		3re 12053	. . . 4 ⊢ 3 ∈ ℝ
55	54	a1i 11	. . 3 ⊢ (𝜑 → 3 ∈ ℝ)
56		1nn0 12249	. . . . . . . . 9 ⊢ 1 ∈ ℕ₀
57		0nn0 12248	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
58		7nn0 12255	. . . . . . . . . . 11 ⊢ 7 ∈ ℕ₀
59		9nn0 12257	. . . . . . . . . . . 12 ⊢ 9 ∈ ℕ₀
60		5nn0 12253	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℕ₀
61		5nn 12059	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℕ
62		nnrp 12741	. . . . . . . . . . . . . . 15 ⊢ (5 ∈ ℕ → 5 ∈ ℝ⁺)
63	61, 62	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℝ⁺
64	60, 63	rpdp2cl 31156	. . . . . . . . . . . . 13 ⊢ _55 ∈ ℝ⁺
65	59, 64	rpdp2cl 31156	. . . . . . . . . . . 12 ⊢ _9_55 ∈ ℝ⁺
66	59, 65	rpdp2cl 31156	. . . . . . . . . . 11 ⊢ _9_9_55 ∈ ℝ⁺
67	58, 66	rpdp2cl 31156	. . . . . . . . . 10 ⊢ _7_9_9_55 ∈ ℝ⁺
68	57, 67	rpdp2cl 31156	. . . . . . . . 9 ⊢ _0_7_9_9_55 ∈ ℝ⁺
69	56, 68	rpdpcl 31177	. . . . . . . 8 ⊢ (1._0_7_9_9_55) ∈ ℝ⁺
70	69	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℝ⁺)
71	70	rpred 12772	. . . . . 6 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℝ)
72	71	resqcld 13965	. . . . 5 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ)
73		4nn0 12252	. . . . . . . . 9 ⊢ 4 ∈ ℕ₀
74		4nn 12056	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ
75		nnrp 12741	. . . . . . . . . . 11 ⊢ (4 ∈ ℕ → 4 ∈ ℝ⁺)
76	74, 75	ax-mp 5	. . . . . . . . . 10 ⊢ 4 ∈ ℝ⁺
77	56, 76	rpdp2cl 31156	. . . . . . . . 9 ⊢ _14 ∈ ℝ⁺
78	73, 77	rpdp2cl 31156	. . . . . . . 8 ⊢ _4_14 ∈ ℝ⁺
79	56, 78	rpdpcl 31177	. . . . . . 7 ⊢ (1._4_14) ∈ ℝ⁺
80	79	a1i 11	. . . . . 6 ⊢ (𝜑 → (1._4_14) ∈ ℝ⁺)
81	80	rpred 12772	. . . . 5 ⊢ (𝜑 → (1._4_14) ∈ ℝ)
82	72, 81	remulcld 11005	. . . 4 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ)
83		fveq1 6773	. . . . . . . . . 10 ⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
84	83	eleq1d 2823	. . . . . . . . 9 ⊢ (𝑑 = 𝑐 → ((𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
85	84	notbid 318	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
86	85	cbvrabv 3426	. . . . . . 7 ⊢ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
87	86	ssrab3 4015	. . . . . 6 ⊢ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁)
88		ssfi 8956	. . . . . 6 ⊢ (((ℕ(repr‘3)𝑁) ∈ Fin ∧ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁)) → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ∈ Fin)
89	6, 87, 88	sylancl 586	. . . . 5 ⊢ (𝜑 → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ∈ Fin)
90	9	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → Λ:ℕ⟶ℝ)
91		ssidd 3944	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ℕ ⊆ ℕ)
92	12	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑁 ∈ ℤ)
93	3	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 3 ∈ ℕ₀)
94	87	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁))
95	94	sselda 3921	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
96	91, 92, 93, 95	reprf 32592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛:(0..^3)⟶ℕ)
97	21	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 0 ∈ (0..^3))
98	96, 97	ffvelrnd 6962	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘0) ∈ ℕ)
99	90, 98	ffvelrnd 6962	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘0)) ∈ ℝ)
100	33	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 1 ∈ (0..^3))
101	96, 100	ffvelrnd 6962	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘1) ∈ ℕ)
102	90, 101	ffvelrnd 6962	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘1)) ∈ ℝ)
103	44	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 2 ∈ (0..^3))
104	96, 103	ffvelrnd 6962	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘2) ∈ ℕ)
105	90, 104	ffvelrnd 6962	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘2)) ∈ ℝ)
106	102, 105	remulcld 11005	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
107	99, 106	remulcld 11005	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
108	89, 107	fsumrecl 15446	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
109	82, 108	remulcld 11005	. . 3 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
110	55, 109	remulcld 11005	. 2 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ∈ ℝ)
111		4re 12057	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
112		8re 12069	. . . . . . . . . 10 ⊢ 8 ∈ ℝ
113	111, 112	pm3.2i 471	. . . . . . . . 9 ⊢ (4 ∈ ℝ ∧ 8 ∈ ℝ)
114		dp2cl 31154	. . . . . . . . 9 ⊢ ((4 ∈ ℝ ∧ 8 ∈ ℝ) → _48 ∈ ℝ)
115	113, 114	ax-mp 5	. . . . . . . 8 ⊢ _48 ∈ ℝ
116	54, 115	pm3.2i 471	. . . . . . 7 ⊢ (3 ∈ ℝ ∧ _48 ∈ ℝ)
117		dp2cl 31154	. . . . . . 7 ⊢ ((3 ∈ ℝ ∧ _48 ∈ ℝ) → _3_48 ∈ ℝ)
118	116, 117	ax-mp 5	. . . . . 6 ⊢ _3_48 ∈ ℝ
119		dpcl 31165	. . . . . 6 ⊢ ((7 ∈ ℕ₀ ∧ _3_48 ∈ ℝ) → (7._3_48) ∈ ℝ)
120	58, 118, 119	mp2an 689	. . . . 5 ⊢ (7._3_48) ∈ ℝ
121	120	a1i 11	. . . 4 ⊢ (𝜑 → (7._3_48) ∈ ℝ)
122	1	nnrpd 12770	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
123	122	relogcld 25778	. . . . 5 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
124	1	nnred 11988	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ)
125	122	rpge0d 12776	. . . . . 6 ⊢ (𝜑 → 0 ≤ 𝑁)
126	124, 125	resqrtcld 15129	. . . . 5 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ)
127	122	rpsqrtcld 15123	. . . . . 6 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
128	127	rpne0d 12777	. . . . 5 ⊢ (𝜑 → (√‘𝑁) ≠ 0)
129	123, 126, 128	redivcld 11803	. . . 4 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ)
130	121, 129	remulcld 11005	. . 3 ⊢ (𝜑 → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ∈ ℝ)
131	124	resqcld 13965	. . 3 ⊢ (𝜑 → (𝑁↑2) ∈ ℝ)
132	130, 131	remulcld 11005	. 2 ⊢ (𝜑 → (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) ∈ ℝ)
133		0re 10977	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
134		7re 12066	. . . . . . . . . . . . 13 ⊢ 7 ∈ ℝ
135		9re 12072	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℝ
136		5re 12060	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 ∈ ℝ
137	136, 136	pm3.2i 471	. . . . . . . . . . . . . . . . . 18 ⊢ (5 ∈ ℝ ∧ 5 ∈ ℝ)
138		dp2cl 31154	. . . . . . . . . . . . . . . . . 18 ⊢ ((5 ∈ ℝ ∧ 5 ∈ ℝ) → _55 ∈ ℝ)
139	137, 138	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ _55 ∈ ℝ
140	135, 139	pm3.2i 471	. . . . . . . . . . . . . . . 16 ⊢ (9 ∈ ℝ ∧ _55 ∈ ℝ)
141		dp2cl 31154	. . . . . . . . . . . . . . . 16 ⊢ ((9 ∈ ℝ ∧ _55 ∈ ℝ) → _9_55 ∈ ℝ)
142	140, 141	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _9_55 ∈ ℝ
143	135, 142	pm3.2i 471	. . . . . . . . . . . . . 14 ⊢ (9 ∈ ℝ ∧ _9_55 ∈ ℝ)
144		dp2cl 31154	. . . . . . . . . . . . . 14 ⊢ ((9 ∈ ℝ ∧ _9_55 ∈ ℝ) → _9_9_55 ∈ ℝ)
145	143, 144	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _9_9_55 ∈ ℝ
146	134, 145	pm3.2i 471	. . . . . . . . . . . 12 ⊢ (7 ∈ ℝ ∧ _9_9_55 ∈ ℝ)
147		dp2cl 31154	. . . . . . . . . . . 12 ⊢ ((7 ∈ ℝ ∧ _9_9_55 ∈ ℝ) → _7_9_9_55 ∈ ℝ)
148	146, 147	ax-mp 5	. . . . . . . . . . 11 ⊢ _7_9_9_55 ∈ ℝ
149	133, 148	pm3.2i 471	. . . . . . . . . 10 ⊢ (0 ∈ ℝ ∧ _7_9_9_55 ∈ ℝ)
150		dp2cl 31154	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ _7_9_9_55 ∈ ℝ) → _0_7_9_9_55 ∈ ℝ)
151	149, 150	ax-mp 5	. . . . . . . . 9 ⊢ _0_7_9_9_55 ∈ ℝ
152		dpcl 31165	. . . . . . . . 9 ⊢ ((1 ∈ ℕ₀ ∧ _0_7_9_9_55 ∈ ℝ) → (1._0_7_9_9_55) ∈ ℝ)
153	56, 151, 152	mp2an 689	. . . . . . . 8 ⊢ (1._0_7_9_9_55) ∈ ℝ
154	153	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℝ)
155	154	resqcld 13965	. . . . . 6 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ)
156		1re 10975	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
157	156, 111	pm3.2i 471	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ ∧ 4 ∈ ℝ)
158		dp2cl 31154	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 4 ∈ ℝ) → _14 ∈ ℝ)
159	157, 158	ax-mp 5	. . . . . . . . . 10 ⊢ _14 ∈ ℝ
160	111, 159	pm3.2i 471	. . . . . . . . 9 ⊢ (4 ∈ ℝ ∧ _14 ∈ ℝ)
161		dp2cl 31154	. . . . . . . . 9 ⊢ ((4 ∈ ℝ ∧ _14 ∈ ℝ) → _4_14 ∈ ℝ)
162	160, 161	ax-mp 5	. . . . . . . 8 ⊢ _4_14 ∈ ℝ
163		dpcl 31165	. . . . . . . 8 ⊢ ((1 ∈ ℕ₀ ∧ _4_14 ∈ ℝ) → (1._4_14) ∈ ℝ)
164	56, 162, 163	mp2an 689	. . . . . . 7 ⊢ (1._4_14) ∈ ℝ
165	164	a1i 11	. . . . . 6 ⊢ (𝜑 → (1._4_14) ∈ ℝ)
166	155, 165	remulcld 11005	. . . . 5 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ)
167	36, 47	remulcld 11005	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
168	24, 167	remulcld 11005	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
169	8, 168	fsumrecl 15446	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
170	166, 169	remulcld 11005	. . . 4 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
171	55, 108	remulcld 11005	. . . . 5 ⊢ (𝜑 → (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
172	166, 171	remulcld 11005	. . . 4 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ∈ ℝ)
173		hgt750leme.1	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐾‘𝑚) ≤ (1._0_7_9_9_55))
174		hgt750leme.2	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘𝑚) ≤ (1._4_14))
175	8, 154, 165, 26, 37, 23, 35, 46, 173, 174	hgt750lemf 32633	. . . 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))))))
176		hgt750leme.o	. . . . . 6 ⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
177		2re 12047	. . . . . . . 8 ⊢ 2 ∈ ℝ
178	177	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ∈ ℝ)
179		10nn0 12455	. . . . . . . . . 10 ⊢ ;10 ∈ ℕ₀
180		2nn0 12250	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
181	180, 58	deccl 12452	. . . . . . . . . 10 ⊢ ;27 ∈ ℕ₀
182	179, 181	nn0expcli 13809	. . . . . . . . 9 ⊢ (;10↑;27) ∈ ℕ₀
183	182	nn0rei 12244	. . . . . . . 8 ⊢ (;10↑;27) ∈ ℝ
184	183	a1i 11	. . . . . . 7 ⊢ (𝜑 → (;10↑;27) ∈ ℝ)
185	179	numexp1 16778	. . . . . . . . . 10 ⊢ (;10↑1) = ;10
186	179	nn0rei 12244	. . . . . . . . . 10 ⊢ ;10 ∈ ℝ
187	185, 186	eqeltri 2835	. . . . . . . . 9 ⊢ (;10↑1) ∈ ℝ
188	187	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (;10↑1) ∈ ℝ)
189		1nn 11984	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
190		2lt9 12178	. . . . . . . . . . . 12 ⊢ 2 < 9
191	177, 135, 190	ltleii 11098	. . . . . . . . . . 11 ⊢ 2 ≤ 9
192	189, 57, 180, 191	declei 12473	. . . . . . . . . 10 ⊢ 2 ≤ ;10
193	192, 185	breqtrri 5101	. . . . . . . . 9 ⊢ 2 ≤ (;10↑1)
194	193	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≤ (;10↑1))
195		1z 12350	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
196	181	nn0zi 12345	. . . . . . . . . . . 12 ⊢ ;27 ∈ ℤ
197	186, 195, 196	3pm3.2i 1338	. . . . . . . . . . 11 ⊢ (;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ)
198		1lt10 12576	. . . . . . . . . . 11 ⊢ 1 < ;10
199	197, 198	pm3.2i 471	. . . . . . . . . 10 ⊢ ((;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ 1 < ;10)
200		2nn 12046	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
201		1lt9 12179	. . . . . . . . . . . 12 ⊢ 1 < 9
202	156, 135, 201	ltleii 11098	. . . . . . . . . . 11 ⊢ 1 ≤ 9
203	200, 58, 56, 202	declei 12473	. . . . . . . . . 10 ⊢ 1 ≤ ;27
204		leexp2 13889	. . . . . . . . . . 11 ⊢ (((;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ 1 < ;10) → (1 ≤ ;27 ↔ (;10↑1) ≤ (;10↑;27)))
205	204	biimpa 477	. . . . . . . . . 10 ⊢ ((((;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ 1 < ;10) ∧ 1 ≤ ;27) → (;10↑1) ≤ (;10↑;27))
206	199, 203, 205	mp2an 689	. . . . . . . . 9 ⊢ (;10↑1) ≤ (;10↑;27)
207	206	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (;10↑1) ≤ (;10↑;27))
208	178, 188, 184, 194, 207	letrd 11132	. . . . . . 7 ⊢ (𝜑 → 2 ≤ (;10↑;27))
209		hgt750leme.0	. . . . . . 7 ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)
210	178, 184, 124, 208, 209	letrd 11132	. . . . . 6 ⊢ (𝜑 → 2 ≤ 𝑁)
211		eqid 2738	. . . . . 6 ⊢ (𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ↦ (𝑒 ∘ if(𝑎 = 0, ( I ↾ (0..^3)), ((pmTrsp‘(0..^3))‘{𝑎, 0})))) = (𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ↦ (𝑒 ∘ if(𝑎 = 0, ( I ↾ (0..^3)), ((pmTrsp‘(0..^3))‘{𝑎, 0}))))
212	176, 1, 210, 86, 211	hgt750lema 32637	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
213		2z 12352	. . . . . . . . 9 ⊢ 2 ∈ ℤ
214	213	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℤ)
215	70, 214	rpexpcld 13962	. . . . . . 7 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ⁺)
216	215, 80	rpmulcld 12788	. . . . . 6 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ⁺)
217	169, 171, 216	lemul2d 12816	. . . . 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))))))))
218	212, 217	mpbid 231	. . . 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)))))))
219	53, 170, 172, 175, 218	letrd 11132	. . 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)))))))
220	154	recnd 11003	. . . . . 6 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℂ)
221	220	sqcld 13862	. . . . 5 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℂ)
222	165	recnd 11003	. . . . 5 ⊢ (𝜑 → (1._4_14) ∈ ℂ)
223	221, 222	mulcld 10995	. . . 4 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℂ)
224		3cn 12054	. . . . 5 ⊢ 3 ∈ ℂ
225	224	a1i 11	. . . 4 ⊢ (𝜑 → 3 ∈ ℂ)
226	108	recnd 11003	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℂ)
227	223, 225, 226	mul12d 11184	. . 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)))))))
228	219, 227	breqtrd 5100	. 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)))))))
229		fzfi 13692	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ Fin
230		diffi 8962	. . . . . . . . . . 11 ⊢ ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
231	229, 230	ax-mp 5	. . . . . . . . . 10 ⊢ ((1...𝑁) ∖ ℙ) ∈ Fin
232		snfi 8834	. . . . . . . . . 10 ⊢ {2} ∈ Fin
233		unfi 8955	. . . . . . . . . 10 ⊢ ((((1...𝑁) ∖ ℙ) ∈ Fin ∧ {2} ∈ Fin) → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
234	231, 232, 233	mp2an 689	. . . . . . . . 9 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin
235	234	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
236	9	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → Λ:ℕ⟶ℝ)
237		fz1ssnn 13287	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ ℕ
238	237	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
239	238	ssdifssd 4077	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ ℕ)
240	200	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℕ)
241	240	snssd 4742	. . . . . . . . . . 11 ⊢ (𝜑 → {2} ⊆ ℕ)
242	239, 241	unssd 4120	. . . . . . . . . 10 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
243	242	sselda 3921	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 𝑖 ∈ ℕ)
244	236, 243	ffvelrnd 6962	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℝ)
245	235, 244	fsumrecl 15446	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) ∈ ℝ)
246		chpvalz 32608	. . . . . . . . 9 ⊢ (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
247	12, 246	syl 17	. . . . . . . 8 ⊢ (𝜑 → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
248		chpf 26272	. . . . . . . . . 10 ⊢ ψ:ℝ⟶ℝ
249	248	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ψ:ℝ⟶ℝ)
250	249, 124	ffvelrnd 6962	. . . . . . . 8 ⊢ (𝜑 → (ψ‘𝑁) ∈ ℝ)
251	247, 250	eqeltrrd 2840	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℝ)
252	245, 251	remulcld 11005	. . . . . 6 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ∈ ℝ)
253	123, 252	remulcld 11005	. . . . 5 ⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ∈ ℝ)
254	82, 253	remulcld 11005	. . . 4 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ∈ ℝ)
255	55, 254	remulcld 11005	. . 3 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ∈ ℝ)
256	176, 1, 210, 86	hgt750lemb 32636	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
257	108, 253, 216	lemul2d 12816	. . . . 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...𝑁)(Λ‘𝑗))))))
258	256, 257	mpbid 231	. . . 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...𝑁)(Λ‘𝑗)))))
259		3rp 12736	. . . . . 6 ⊢ 3 ∈ ℝ⁺
260	259	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℝ⁺)
261	109, 254, 260	lemul2d 12816	. . . 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...𝑁)(Λ‘𝑗)))))))
262	258, 261	mpbid 231	. . 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...𝑁)(Λ‘𝑗))))))
263		6re 12063	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℝ
264	263, 54	pm3.2i 471	. . . . . . . . . . . . . . . 16 ⊢ (6 ∈ ℝ ∧ 3 ∈ ℝ)
265		dp2cl 31154	. . . . . . . . . . . . . . . 16 ⊢ ((6 ∈ ℝ ∧ 3 ∈ ℝ) → _63 ∈ ℝ)
266	264, 265	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _63 ∈ ℝ
267	177, 266	pm3.2i 471	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℝ ∧ _63 ∈ ℝ)
268		dp2cl 31154	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ _63 ∈ ℝ) → _2_63 ∈ ℝ)
269	267, 268	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _2_63 ∈ ℝ
270	111, 269	pm3.2i 471	. . . . . . . . . . . 12 ⊢ (4 ∈ ℝ ∧ _2_63 ∈ ℝ)
271		dp2cl 31154	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ ∧ _2_63 ∈ ℝ) → _4_2_63 ∈ ℝ)
272	270, 271	ax-mp 5	. . . . . . . . . . 11 ⊢ _4_2_63 ∈ ℝ
273		dpcl 31165	. . . . . . . . . . 11 ⊢ ((1 ∈ ℕ₀ ∧ _4_2_63 ∈ ℝ) → (1._4_2_63) ∈ ℝ)
274	56, 272, 273	mp2an 689	. . . . . . . . . 10 ⊢ (1._4_2_63) ∈ ℝ
275	274	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1._4_2_63) ∈ ℝ)
276	275, 126	remulcld 11005	. . . . . . . 8 ⊢ (𝜑 → ((1._4_2_63) · (√‘𝑁)) ∈ ℝ)
277	112, 54	pm3.2i 471	. . . . . . . . . . . . . . . . . 18 ⊢ (8 ∈ ℝ ∧ 3 ∈ ℝ)
278		dp2cl 31154	. . . . . . . . . . . . . . . . . 18 ⊢ ((8 ∈ ℝ ∧ 3 ∈ ℝ) → _83 ∈ ℝ)
279	277, 278	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ _83 ∈ ℝ
280	112, 279	pm3.2i 471	. . . . . . . . . . . . . . . 16 ⊢ (8 ∈ ℝ ∧ _83 ∈ ℝ)
281		dp2cl 31154	. . . . . . . . . . . . . . . 16 ⊢ ((8 ∈ ℝ ∧ _83 ∈ ℝ) → _8_83 ∈ ℝ)
282	280, 281	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _8_83 ∈ ℝ
283	54, 282	pm3.2i 471	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℝ ∧ _8_83 ∈ ℝ)
284		dp2cl 31154	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℝ ∧ _8_83 ∈ ℝ) → _3_8_83 ∈ ℝ)
285	283, 284	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _3_8_83 ∈ ℝ
286	133, 285	pm3.2i 471	. . . . . . . . . . . 12 ⊢ (0 ∈ ℝ ∧ _3_8_83 ∈ ℝ)
287		dp2cl 31154	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ _3_8_83 ∈ ℝ) → _0_3_8_83 ∈ ℝ)
288	286, 287	ax-mp 5	. . . . . . . . . . 11 ⊢ _0_3_8_83 ∈ ℝ
289		dpcl 31165	. . . . . . . . . . 11 ⊢ ((1 ∈ ℕ₀ ∧ _0_3_8_83 ∈ ℝ) → (1._0_3_8_83) ∈ ℝ)
290	56, 288, 289	mp2an 689	. . . . . . . . . 10 ⊢ (1._0_3_8_83) ∈ ℝ
291	290	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1._0_3_8_83) ∈ ℝ)
292	291, 124	remulcld 11005	. . . . . . . 8 ⊢ (𝜑 → ((1._0_3_8_83) · 𝑁) ∈ ℝ)
293	276, 292	remulcld 11005	. . . . . . 7 ⊢ (𝜑 → (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)) ∈ ℝ)
294	123, 293	remulcld 11005	. . . . . 6 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) ∈ ℝ)
295	82, 294	remulcld 11005	. . . . 5 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))) ∈ ℝ)
296	55, 295	remulcld 11005	. . . 4 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))))) ∈ ℝ)
297		vmage0 26270	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℕ → 0 ≤ (Λ‘𝑖))
298	243, 297	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 0 ≤ (Λ‘𝑖))
299	235, 244, 298	fsumge0 15507	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖))
300	1, 209	hgt750lemd 32628	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) < ((1._4_2_63) · (√‘𝑁)))
301		fzfid 13693	. . . . . . . . . 10 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
302	9	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
303	238	sselda 3921	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
304	302, 303	ffvelrnd 6962	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
305		vmage0 26270	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → 0 ≤ (Λ‘𝑗))
306	303, 305	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 0 ≤ (Λ‘𝑗))
307	301, 304, 306	fsumge0 15507	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
308	1	hgt750lemc 32627	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) < ((1._0_3_8_83) · 𝑁))
309	245, 276, 251, 292, 299, 300, 307, 308	ltmul12ad 11916	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) < (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))
310	252, 293, 309	ltled 11123	. . . . . . 7 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ≤ (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))
311	156	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℝ)
312		1lt2 12144	. . . . . . . . . . 11 ⊢ 1 < 2
313	312	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 < 2)
314	311, 178, 124, 313, 210	ltletrd 11135	. . . . . . . . 9 ⊢ (𝜑 → 1 < 𝑁)
315	124, 314	rplogcld 25784	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ⁺)
316	252, 293, 315	lemul2d 12816	. . . . . . 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) · 𝑁)))))
317	310, 316	mpbid 231	. . . . . 6 ⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ≤ ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))))
318	253, 294, 216	lemul2d 12816	. . . . . 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) · 𝑁))))))
319	317, 318	mpbid 231	. . . . 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) · 𝑁)))))
320	254, 295, 260	lemul2d 12816	. . . . 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) · 𝑁)))))))
321	319, 320	mpbid 231	. . . 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) · 𝑁))))))
322	153	resqcli 13903	. . . . . . . . . 10 ⊢ ((1._0_7_9_9_55)↑2) ∈ ℝ
323	322, 164	remulcli 10991	. . . . . . . . 9 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ
324	274, 290	remulcli 10991	. . . . . . . . 9 ⊢ ((1._4_2_63) · (1._0_3_8_83)) ∈ ℝ
325	323, 324	remulcli 10991	. . . . . . . 8 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) ∈ ℝ
326	54, 325	remulcli 10991	. . . . . . 7 ⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) ∈ ℝ
327		hgt750lem2 32632	. . . . . . 7 ⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) < (7._3_48)
328	326, 120, 327	ltleii 11098	. . . . . 6 ⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) ≤ (7._3_48)
329	326	a1i 11	. . . . . . 7 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) ∈ ℝ)
330	315, 127	rpdivcld 12789	. . . . . . . 8 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ⁺)
331	122, 214	rpexpcld 13962	. . . . . . . 8 ⊢ (𝜑 → (𝑁↑2) ∈ ℝ⁺)
332	330, 331	rpmulcld 12788	. . . . . . 7 ⊢ (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) ∈ ℝ⁺)
333	329, 121, 332	lemul1d 12815	. . . . . 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)))))
334	328, 333	mpbii 232	. . . . 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))))
335	275	recnd 11003	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1._4_2_63) ∈ ℂ)
336	126	recnd 11003	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (√‘𝑁) ∈ ℂ)
337	291	recnd 11003	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1._0_3_8_83) ∈ ℂ)
338	124	recnd 11003	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℂ)
339	335, 336, 337, 338	mul4d 11187	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)) = (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)))
340	339	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) = ((log‘𝑁) · (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁))))
341	123	recnd 11003	. . . . . . . . . . . . 13 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
342	335, 337	mulcld 10995	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1._4_2_63) · (1._0_3_8_83)) ∈ ℂ)
343	336, 338	mulcld 10995	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((√‘𝑁) · 𝑁) ∈ ℂ)
344	342, 343	mulcld 10995	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)) ∈ ℂ)
345	341, 344	mulcomd 10996	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁))) = ((((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)) · (log‘𝑁)))
346	340, 345	eqtrd 2778	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) = ((((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)) · (log‘𝑁)))
347	342, 343, 341	mulassd 10998	. . . . . . . . . . 11 ⊢ (𝜑 → ((((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)) · (log‘𝑁)) = (((1._4_2_63) · (1._0_3_8_83)) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
348	346, 347	eqtrd 2778	. . . . . . . . . 10 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) = (((1._4_2_63) · (1._0_3_8_83)) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
349	348	oveq2d 7291	. . . . . . . . 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‘𝑁)))))
350	82	recnd 11003	. . . . . . . . . 10 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℂ)
351	343, 341	mulcld 10995	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) ∈ ℂ)
352	350, 342, 351	mulassd 10998	. . . . . . . . 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‘𝑁)))))
353	349, 352	eqtr4d 2781	. . . . . . . 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‘𝑁))))
354	353	oveq2d 7291	. . . . . . 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‘𝑁)))))
355	55	recnd 11003	. . . . . . . 8 ⊢ (𝜑 → 3 ∈ ℂ)
356	350, 342	mulcld 10995	. . . . . . . 8 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) ∈ ℂ)
357	355, 356, 351	mulassd 10998	. . . . . . 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‘𝑁)))))
358	354, 357	eqtr4d 2781	. . . . . 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‘𝑁))))
359	131	recnd 11003	. . . . . . . . 9 ⊢ (𝜑 → (𝑁↑2) ∈ ℂ)
360	341, 336, 359, 128	div32d 11774	. . . . . . . 8 ⊢ (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) = ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))))
361	359, 336, 128	divcld 11751	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) ∈ ℂ)
362	341, 361	mulcomd 10996	. . . . . . . 8 ⊢ (𝜑 → ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))) = (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)))
363	338	sqvald 13861	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁↑2) = (𝑁 · 𝑁))
364	363	oveq1d 7290	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((𝑁 · 𝑁) / (√‘𝑁)))
365	338, 338, 336, 128	divassd 11786	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 · 𝑁) / (√‘𝑁)) = (𝑁 · (𝑁 / (√‘𝑁))))
366		divsqrtid 32574	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℝ⁺ → (𝑁 / (√‘𝑁)) = (√‘𝑁))
367	122, 366	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 / (√‘𝑁)) = (√‘𝑁))
368	367	oveq2d 7291	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · (𝑁 / (√‘𝑁))) = (𝑁 · (√‘𝑁)))
369	364, 365, 368	3eqtrd 2782	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = (𝑁 · (√‘𝑁)))
370	338, 336	mulcomd 10996	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 · (√‘𝑁)) = ((√‘𝑁) · 𝑁))
371	369, 370	eqtrd 2778	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((√‘𝑁) · 𝑁))
372	371	oveq1d 7290	. . . . . . . 8 ⊢ (𝜑 → (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)) = (((√‘𝑁) · 𝑁) · (log‘𝑁)))
373	360, 362, 372	3eqtrrd 2783	. . . . . . 7 ⊢ (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) = (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)))
374	373	oveq2d 7291	. . . . . 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))))
375	358, 374	eqtrd 2778	. . . . 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))))
376	121	recnd 11003	. . . . . 6 ⊢ (𝜑 → (7._3_48) ∈ ℂ)
377	129	recnd 11003	. . . . . 6 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℂ)
378	376, 377, 359	mulassd 10998	. . . . 5 ⊢ (𝜑 → (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) = ((7._3_48) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
379	334, 375, 378	3brtr4d 5106	. . . 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)))
380	255, 296, 132, 321, 379	letrd 11132	. . 3 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ≤ (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
381	110, 255, 132, 262, 380	letrd 11132	. 2 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ≤ (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
382	53, 110, 132, 228, 381	letrd 11132	1 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 {crab 3068 ∖ cdif 3884 ∪ cun 3885 ∩ cin 3886 ⊆ wss 3887 ifcif 4459 {csn 4561 {cpr 4563 {ctp 4565 class class class wbr 5074 ↦ cmpt 5157 I cid 5488 ↾ cres 5591 ∘ ccom 5593 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 Fincfn 8733 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 · cmul 10876 +∞cpnf 11006 < clt 11009 ≤ cle 11010 / cdiv 11632 ℕcn 11973 2c2 12028 3c3 12029 4c4 12030 5c5 12031 6c6 12032 7c7 12033 8c8 12034 9c9 12035 ℕ₀cn0 12233 ℤcz 12319 cdc 12437 ℝ⁺crp 12730 [,)cico 13081 ...cfz 13239 ..^cfzo 13382 ↑cexp 13782 √csqrt 14944 Σcsu 15397 ∥ cdvds 15963 ℙcprime 16376 pmTrspcpmtr 19049 logclog 25710 Λcvma 26241 ψcchp 26242 cdp2 31145 .cdp 31162 reprcrepr 32588

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-reg 9351 ax-inf2 9399 ax-ac2 10219 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949 ax-addf 10950 ax-mulf 10951 ax-ros335 32625 ax-ros336 32626

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-iin 4927 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-of 7533 df-om 7713 df-1st 7831 df-2nd 7832 df-supp 7978 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-2o 8298 df-oadd 8301 df-er 8498 df-map 8617 df-pm 8618 df-ixp 8686 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-fsupp 9129 df-fi 9170 df-sup 9201 df-inf 9202 df-oi 9269 df-r1 9522 df-rank 9523 df-dju 9659 df-card 9697 df-ac 9872 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-xnn0 12306 df-z 12320 df-dec 12438 df-uz 12583 df-q 12689 df-rp 12731 df-xneg 12848 df-xadd 12849 df-xmul 12850 df-ioo 13083 df-ioc 13084 df-ico 13085 df-icc 13086 df-fz 13240 df-fzo 13383 df-fl 13512 df-mod 13590 df-seq 13722 df-exp 13783 df-fac 13988 df-bc 14017 df-hash 14045 df-shft 14778 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-limsup 15180 df-clim 15197 df-rlim 15198 df-sum 15398 df-prod 15616 df-ef 15777 df-sin 15779 df-cos 15780 df-tan 15781 df-pi 15782 df-dvds 15964 df-gcd 16202 df-prm 16377 df-pc 16538 df-struct 16848 df-sets 16865 df-slot 16883 df-ndx 16895 df-base 16913 df-ress 16942 df-plusg 16975 df-mulr 16976 df-starv 16977 df-sca 16978 df-vsca 16979 df-ip 16980 df-tset 16981 df-ple 16982 df-ds 16984 df-unif 16985 df-hom 16986 df-cco 16987 df-rest 17133 df-topn 17134 df-0g 17152 df-gsum 17153 df-topgen 17154 df-pt 17155 df-prds 17158 df-xrs 17213 df-qtop 17218 df-imas 17219 df-xps 17221 df-mre 17295 df-mrc 17296 df-acs 17298 df-mgm 18326 df-sgrp 18375 df-mnd 18386 df-submnd 18431 df-mulg 18701 df-cntz 18923 df-pmtr 19050 df-cmn 19388 df-psmet 20589 df-xmet 20590 df-met 20591 df-bl 20592 df-mopn 20593 df-fbas 20594 df-fg 20595 df-cnfld 20598 df-top 22043 df-topon 22060 df-topsp 22082 df-bases 22096 df-cld 22170 df-ntr 22171 df-cls 22172 df-nei 22249 df-lp 22287 df-perf 22288 df-cn 22378 df-cnp 22379 df-haus 22466 df-cmp 22538 df-tx 22713 df-hmeo 22906 df-fil 22997 df-fm 23089 df-flim 23090 df-flf 23091 df-xms 23473 df-ms 23474 df-tms 23475 df-cncf 24041 df-limc 25030 df-dv 25031 df-ulm 25536 df-log 25712 df-atan 26017 df-cht 26246 df-vma 26247 df-chp 26248 df-dp2 31146 df-dp 31163 df-repr 32589

This theorem is referenced by: tgoldbachgtde 32640

W3C validator