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 34636

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 12560	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
3		3nn0 12517	. . . . . 6 ⊢ 3 ∈ ℕ₀
4	3	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ₀)
5		ssidd 3982	. . . . 5 ⊢ (𝜑 → ℕ ⊆ ℕ)
6	2, 4, 5	reprfi2 34601	. . . 4 ⊢ (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
7		diffi 9187	. . . 4 ⊢ ((ℕ(repr‘3)𝑁) ∈ Fin → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
8	6, 7	syl 17	. . 3 ⊢ (𝜑 → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
9		vmaf 27079	. . . . . . 7 ⊢ Λ:ℕ⟶ℝ
10	9	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → Λ:ℕ⟶ℝ)
11		ssidd 3982	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ℕ ⊆ ℕ)
12	1	nnzd 12613	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℤ)
13	12	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑁 ∈ ℤ)
14	3	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 3 ∈ ℕ₀)
15		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)))
16	15	eldifad 3938	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
17	11, 13, 14, 16	reprf 34590	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛:(0..^3)⟶ℕ)
18		c0ex 11227	. . . . . . . . . 10 ⊢ 0 ∈ V
19	18	tpid1 4744	. . . . . . . . 9 ⊢ 0 ∈ {0, 1, 2}
20		fzo0to3tp 13766	. . . . . . . . 9 ⊢ (0..^3) = {0, 1, 2}
21	19, 20	eleqtrri 2833	. . . . . . . 8 ⊢ 0 ∈ (0..^3)
22	21	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 0 ∈ (0..^3))
23	17, 22	ffvelcdmd 7074	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘0) ∈ ℕ)
24	10, 23	ffvelcdmd 7074	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘0)) ∈ ℝ)
25		rge0ssre 13471	. . . . . 6 ⊢ (0[,)+∞) ⊆ ℝ
26		hgt750leme.h	. . . . . . . 8 ⊢ (𝜑 → 𝐻:ℕ⟶(0[,)+∞))
27	26	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐻:ℕ⟶(0[,)+∞))
28	27, 23	ffvelcdmd 7074	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ (0[,)+∞))
29	25, 28	sselid 3956	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ ℝ)
30	24, 29	remulcld 11263	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) ∈ ℝ)
31		1ex 11229	. . . . . . . . . . 11 ⊢ 1 ∈ V
32	31	tpid2 4746	. . . . . . . . . 10 ⊢ 1 ∈ {0, 1, 2}
33	32, 20	eleqtrri 2833	. . . . . . . . 9 ⊢ 1 ∈ (0..^3)
34	33	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 1 ∈ (0..^3))
35	17, 34	ffvelcdmd 7074	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘1) ∈ ℕ)
36	10, 35	ffvelcdmd 7074	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘1)) ∈ ℝ)
37		hgt750leme.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾:ℕ⟶(0[,)+∞))
38	37	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐾:ℕ⟶(0[,)+∞))
39	38, 35	ffvelcdmd 7074	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ (0[,)+∞))
40	25, 39	sselid 3956	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ ℝ)
41	36, 40	remulcld 11263	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) ∈ ℝ)
42		2ex 12315	. . . . . . . . . . 11 ⊢ 2 ∈ V
43	42	tpid3 4749	. . . . . . . . . 10 ⊢ 2 ∈ {0, 1, 2}
44	43, 20	eleqtrri 2833	. . . . . . . . 9 ⊢ 2 ∈ (0..^3)
45	44	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 2 ∈ (0..^3))
46	17, 45	ffvelcdmd 7074	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘2) ∈ ℕ)
47	10, 46	ffvelcdmd 7074	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘2)) ∈ ℝ)
48	38, 46	ffvelcdmd 7074	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ (0[,)+∞))
49	25, 48	sselid 3956	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ ℝ)
50	47, 49	remulcld 11263	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))) ∈ ℝ)
51	41, 50	remulcld 11263	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))) ∈ ℝ)
52	30, 51	remulcld 11263	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
53	8, 52	fsumrecl 15748	. 2 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
54		3re 12318	. . . 4 ⊢ 3 ∈ ℝ
55	54	a1i 11	. . 3 ⊢ (𝜑 → 3 ∈ ℝ)
56		1nn0 12515	. . . . . . . . 9 ⊢ 1 ∈ ℕ₀
57		0nn0 12514	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
58		7nn0 12521	. . . . . . . . . . 11 ⊢ 7 ∈ ℕ₀
59		9nn0 12523	. . . . . . . . . . . 12 ⊢ 9 ∈ ℕ₀
60		5nn0 12519	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℕ₀
61		5nn 12324	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℕ
62		nnrp 13018	. . . . . . . . . . . . . . 15 ⊢ (5 ∈ ℕ → 5 ∈ ℝ⁺)
63	61, 62	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℝ⁺
64	60, 63	rpdp2cl 32802	. . . . . . . . . . . . 13 ⊢ _55 ∈ ℝ⁺
65	59, 64	rpdp2cl 32802	. . . . . . . . . . . 12 ⊢ _9_55 ∈ ℝ⁺
66	59, 65	rpdp2cl 32802	. . . . . . . . . . 11 ⊢ _9_9_55 ∈ ℝ⁺
67	58, 66	rpdp2cl 32802	. . . . . . . . . 10 ⊢ _7_9_9_55 ∈ ℝ⁺
68	57, 67	rpdp2cl 32802	. . . . . . . . 9 ⊢ _0_7_9_9_55 ∈ ℝ⁺
69	56, 68	rpdpcl 32823	. . . . . . . 8 ⊢ (1._0_7_9_9_55) ∈ ℝ⁺
70	69	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℝ⁺)
71	70	rpred 13049	. . . . . 6 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℝ)
72	71	resqcld 14141	. . . . 5 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ)
73		4nn0 12518	. . . . . . . . 9 ⊢ 4 ∈ ℕ₀
74		4nn 12321	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ
75		nnrp 13018	. . . . . . . . . . 11 ⊢ (4 ∈ ℕ → 4 ∈ ℝ⁺)
76	74, 75	ax-mp 5	. . . . . . . . . 10 ⊢ 4 ∈ ℝ⁺
77	56, 76	rpdp2cl 32802	. . . . . . . . 9 ⊢ _14 ∈ ℝ⁺
78	73, 77	rpdp2cl 32802	. . . . . . . 8 ⊢ _4_14 ∈ ℝ⁺
79	56, 78	rpdpcl 32823	. . . . . . 7 ⊢ (1._4_14) ∈ ℝ⁺
80	79	a1i 11	. . . . . 6 ⊢ (𝜑 → (1._4_14) ∈ ℝ⁺)
81	80	rpred 13049	. . . . 5 ⊢ (𝜑 → (1._4_14) ∈ ℝ)
82	72, 81	remulcld 11263	. . . 4 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ)
83		fveq1 6874	. . . . . . . . . 10 ⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
84	83	eleq1d 2819	. . . . . . . . 9 ⊢ (𝑑 = 𝑐 → ((𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
85	84	notbid 318	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
86	85	cbvrabv 3426	. . . . . . 7 ⊢ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
87	86	ssrab3 4057	. . . . . 6 ⊢ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁)
88		ssfi 9185	. . . . . 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 3982	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ℕ ⊆ ℕ)
92	12	adantr 480	. . . . . . . . 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 3958	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
96	91, 92, 93, 95	reprf 34590	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛:(0..^3)⟶ℕ)
97	21	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 0 ∈ (0..^3))
98	96, 97	ffvelcdmd 7074	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘0) ∈ ℕ)
99	90, 98	ffvelcdmd 7074	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘0)) ∈ ℝ)
100	33	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 1 ∈ (0..^3))
101	96, 100	ffvelcdmd 7074	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘1) ∈ ℕ)
102	90, 101	ffvelcdmd 7074	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘1)) ∈ ℝ)
103	44	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 2 ∈ (0..^3))
104	96, 103	ffvelcdmd 7074	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘2) ∈ ℕ)
105	90, 104	ffvelcdmd 7074	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘2)) ∈ ℝ)
106	102, 105	remulcld 11263	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
107	99, 106	remulcld 11263	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
108	89, 107	fsumrecl 15748	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
109	82, 108	remulcld 11263	. . 3 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
110	55, 109	remulcld 11263	. 2 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ∈ ℝ)
111		4re 12322	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
112		8re 12334	. . . . . . . . . 10 ⊢ 8 ∈ ℝ
113	111, 112	pm3.2i 470	. . . . . . . . 9 ⊢ (4 ∈ ℝ ∧ 8 ∈ ℝ)
114		dp2cl 32800	. . . . . . . . 9 ⊢ ((4 ∈ ℝ ∧ 8 ∈ ℝ) → _48 ∈ ℝ)
115	113, 114	ax-mp 5	. . . . . . . 8 ⊢ _48 ∈ ℝ
116	54, 115	pm3.2i 470	. . . . . . 7 ⊢ (3 ∈ ℝ ∧ _48 ∈ ℝ)
117		dp2cl 32800	. . . . . . 7 ⊢ ((3 ∈ ℝ ∧ _48 ∈ ℝ) → _3_48 ∈ ℝ)
118	116, 117	ax-mp 5	. . . . . 6 ⊢ _3_48 ∈ ℝ
119		dpcl 32811	. . . . . 6 ⊢ ((7 ∈ ℕ₀ ∧ _3_48 ∈ ℝ) → (7._3_48) ∈ ℝ)
120	58, 118, 119	mp2an 692	. . . . 5 ⊢ (7._3_48) ∈ ℝ
121	120	a1i 11	. . . 4 ⊢ (𝜑 → (7._3_48) ∈ ℝ)
122	1	nnrpd 13047	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
123	122	relogcld 26582	. . . . 5 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
124	1	nnred 12253	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ)
125	122	rpge0d 13053	. . . . . 6 ⊢ (𝜑 → 0 ≤ 𝑁)
126	124, 125	resqrtcld 15434	. . . . 5 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ)
127	122	rpsqrtcld 15428	. . . . . 6 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
128	127	rpne0d 13054	. . . . 5 ⊢ (𝜑 → (√‘𝑁) ≠ 0)
129	123, 126, 128	redivcld 12067	. . . 4 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ)
130	121, 129	remulcld 11263	. . 3 ⊢ (𝜑 → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ∈ ℝ)
131	124	resqcld 14141	. . 3 ⊢ (𝜑 → (𝑁↑2) ∈ ℝ)
132	130, 131	remulcld 11263	. 2 ⊢ (𝜑 → (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) ∈ ℝ)
133		0re 11235	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
134		7re 12331	. . . . . . . . . . . . 13 ⊢ 7 ∈ ℝ
135		9re 12337	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℝ
136		5re 12325	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 ∈ ℝ
137	136, 136	pm3.2i 470	. . . . . . . . . . . . . . . . . 18 ⊢ (5 ∈ ℝ ∧ 5 ∈ ℝ)
138		dp2cl 32800	. . . . . . . . . . . . . . . . . 18 ⊢ ((5 ∈ ℝ ∧ 5 ∈ ℝ) → _55 ∈ ℝ)
139	137, 138	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ _55 ∈ ℝ
140	135, 139	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (9 ∈ ℝ ∧ _55 ∈ ℝ)
141		dp2cl 32800	. . . . . . . . . . . . . . . 16 ⊢ ((9 ∈ ℝ ∧ _55 ∈ ℝ) → _9_55 ∈ ℝ)
142	140, 141	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _9_55 ∈ ℝ
143	135, 142	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (9 ∈ ℝ ∧ _9_55 ∈ ℝ)
144		dp2cl 32800	. . . . . . . . . . . . . 14 ⊢ ((9 ∈ ℝ ∧ _9_55 ∈ ℝ) → _9_9_55 ∈ ℝ)
145	143, 144	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _9_9_55 ∈ ℝ
146	134, 145	pm3.2i 470	. . . . . . . . . . . 12 ⊢ (7 ∈ ℝ ∧ _9_9_55 ∈ ℝ)
147		dp2cl 32800	. . . . . . . . . . . 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 470	. . . . . . . . . 10 ⊢ (0 ∈ ℝ ∧ _7_9_9_55 ∈ ℝ)
150		dp2cl 32800	. . . . . . . . . 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 32811	. . . . . . . . 9 ⊢ ((1 ∈ ℕ₀ ∧ _0_7_9_9_55 ∈ ℝ) → (1._0_7_9_9_55) ∈ ℝ)
153	56, 151, 152	mp2an 692	. . . . . . . 8 ⊢ (1._0_7_9_9_55) ∈ ℝ
154	153	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℝ)
155	154	resqcld 14141	. . . . . 6 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ)
156		1re 11233	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
157	156, 111	pm3.2i 470	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ ∧ 4 ∈ ℝ)
158		dp2cl 32800	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 4 ∈ ℝ) → _14 ∈ ℝ)
159	157, 158	ax-mp 5	. . . . . . . . . 10 ⊢ _14 ∈ ℝ
160	111, 159	pm3.2i 470	. . . . . . . . 9 ⊢ (4 ∈ ℝ ∧ _14 ∈ ℝ)
161		dp2cl 32800	. . . . . . . . 9 ⊢ ((4 ∈ ℝ ∧ _14 ∈ ℝ) → _4_14 ∈ ℝ)
162	160, 161	ax-mp 5	. . . . . . . 8 ⊢ _4_14 ∈ ℝ
163		dpcl 32811	. . . . . . . 8 ⊢ ((1 ∈ ℕ₀ ∧ _4_14 ∈ ℝ) → (1._4_14) ∈ ℝ)
164	56, 162, 163	mp2an 692	. . . . . . 7 ⊢ (1._4_14) ∈ ℝ
165	164	a1i 11	. . . . . 6 ⊢ (𝜑 → (1._4_14) ∈ ℝ)
166	155, 165	remulcld 11263	. . . . 5 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ)
167	36, 47	remulcld 11263	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
168	24, 167	remulcld 11263	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
169	8, 168	fsumrecl 15748	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
170	166, 169	remulcld 11263	. . . 4 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
171	55, 108	remulcld 11263	. . . . 5 ⊢ (𝜑 → (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
172	166, 171	remulcld 11263	. . . 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 34631	. . . 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 12312	. . . . . . . 8 ⊢ 2 ∈ ℝ
178	177	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ∈ ℝ)
179		10nn0 12724	. . . . . . . . . 10 ⊢ ;10 ∈ ℕ₀
180		2nn0 12516	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
181	180, 58	deccl 12721	. . . . . . . . . 10 ⊢ ;27 ∈ ℕ₀
182	179, 181	nn0expcli 14104	. . . . . . . . 9 ⊢ (;10↑;27) ∈ ℕ₀
183	182	nn0rei 12510	. . . . . . . 8 ⊢ (;10↑;27) ∈ ℝ
184	183	a1i 11	. . . . . . 7 ⊢ (𝜑 → (;10↑;27) ∈ ℝ)
185	179	numexp1 17094	. . . . . . . . . 10 ⊢ (;10↑1) = ;10
186	179	nn0rei 12510	. . . . . . . . . 10 ⊢ ;10 ∈ ℝ
187	185, 186	eqeltri 2830	. . . . . . . . 9 ⊢ (;10↑1) ∈ ℝ
188	187	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (;10↑1) ∈ ℝ)
189		1nn 12249	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
190		2lt9 12443	. . . . . . . . . . . 12 ⊢ 2 < 9
191	177, 135, 190	ltleii 11356	. . . . . . . . . . 11 ⊢ 2 ≤ 9
192	189, 57, 180, 191	declei 12742	. . . . . . . . . 10 ⊢ 2 ≤ ;10
193	192, 185	breqtrri 5146	. . . . . . . . 9 ⊢ 2 ≤ (;10↑1)
194	193	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≤ (;10↑1))
195		1z 12620	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
196	181	nn0zi 12615	. . . . . . . . . . . 12 ⊢ ;27 ∈ ℤ
197	186, 195, 196	3pm3.2i 1340	. . . . . . . . . . 11 ⊢ (;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ)
198		1lt10 12845	. . . . . . . . . . 11 ⊢ 1 < ;10
199	197, 198	pm3.2i 470	. . . . . . . . . 10 ⊢ ((;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ 1 < ;10)
200		2nn 12311	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
201		1lt9 12444	. . . . . . . . . . . 12 ⊢ 1 < 9
202	156, 135, 201	ltleii 11356	. . . . . . . . . . 11 ⊢ 1 ≤ 9
203	200, 58, 56, 202	declei 12742	. . . . . . . . . 10 ⊢ 1 ≤ ;27
204		leexp2 14187	. . . . . . . . . . 11 ⊢ (((;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ 1 < ;10) → (1 ≤ ;27 ↔ (;10↑1) ≤ (;10↑;27)))
205	204	biimpa 476	. . . . . . . . . 10 ⊢ ((((;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ 1 < ;10) ∧ 1 ≤ ;27) → (;10↑1) ≤ (;10↑;27))
206	199, 203, 205	mp2an 692	. . . . . . . . 9 ⊢ (;10↑1) ≤ (;10↑;27)
207	206	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (;10↑1) ≤ (;10↑;27))
208	178, 188, 184, 194, 207	letrd 11390	. . . . . . 7 ⊢ (𝜑 → 2 ≤ (;10↑;27))
209		hgt750leme.0	. . . . . . 7 ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)
210	178, 184, 124, 208, 209	letrd 11390	. . . . . 6 ⊢ (𝜑 → 2 ≤ 𝑁)
211		eqid 2735	. . . . . 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 34635	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
213		2z 12622	. . . . . . . . 9 ⊢ 2 ∈ ℤ
214	213	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℤ)
215	70, 214	rpexpcld 14263	. . . . . . 7 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ⁺)
216	215, 80	rpmulcld 13065	. . . . . 6 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ⁺)
217	169, 171, 216	lemul2d 13093	. . . . 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 232	. . . 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 11390	. . 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 11261	. . . . . 6 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℂ)
221	220	sqcld 14160	. . . . 5 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℂ)
222	165	recnd 11261	. . . . 5 ⊢ (𝜑 → (1._4_14) ∈ ℂ)
223	221, 222	mulcld 11253	. . . 4 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℂ)
224		3cn 12319	. . . . 5 ⊢ 3 ∈ ℂ
225	224	a1i 11	. . . 4 ⊢ (𝜑 → 3 ∈ ℂ)
226	108	recnd 11261	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℂ)
227	223, 225, 226	mul12d 11442	. . 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 5145	. 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 13988	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ Fin
230		diffi 9187	. . . . . . . . . . 11 ⊢ ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
231	229, 230	ax-mp 5	. . . . . . . . . 10 ⊢ ((1...𝑁) ∖ ℙ) ∈ Fin
232		snfi 9055	. . . . . . . . . 10 ⊢ {2} ∈ Fin
233		unfi 9183	. . . . . . . . . 10 ⊢ ((((1...𝑁) ∖ ℙ) ∈ Fin ∧ {2} ∈ Fin) → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
234	231, 232, 233	mp2an 692	. . . . . . . . 9 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin
235	234	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
236	9	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → Λ:ℕ⟶ℝ)
237		fz1ssnn 13570	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ ℕ
238	237	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
239	238	ssdifssd 4122	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ ℕ)
240	200	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℕ)
241	240	snssd 4785	. . . . . . . . . . 11 ⊢ (𝜑 → {2} ⊆ ℕ)
242	239, 241	unssd 4167	. . . . . . . . . 10 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
243	242	sselda 3958	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 𝑖 ∈ ℕ)
244	236, 243	ffvelcdmd 7074	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℝ)
245	235, 244	fsumrecl 15748	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) ∈ ℝ)
246		chpvalz 34606	. . . . . . . . 9 ⊢ (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
247	12, 246	syl 17	. . . . . . . 8 ⊢ (𝜑 → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
248		chpf 27083	. . . . . . . . . 10 ⊢ ψ:ℝ⟶ℝ
249	248	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ψ:ℝ⟶ℝ)
250	249, 124	ffvelcdmd 7074	. . . . . . . 8 ⊢ (𝜑 → (ψ‘𝑁) ∈ ℝ)
251	247, 250	eqeltrrd 2835	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℝ)
252	245, 251	remulcld 11263	. . . . . 6 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ∈ ℝ)
253	123, 252	remulcld 11263	. . . . 5 ⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ∈ ℝ)
254	82, 253	remulcld 11263	. . . 4 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ∈ ℝ)
255	55, 254	remulcld 11263	. . 3 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ∈ ℝ)
256	176, 1, 210, 86	hgt750lemb 34634	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
257	108, 253, 216	lemul2d 13093	. . . . 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 232	. . . 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 13012	. . . . . 6 ⊢ 3 ∈ ℝ⁺
260	259	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℝ⁺)
261	109, 254, 260	lemul2d 13093	. . . 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 232	. . 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 12328	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℝ
264	263, 54	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (6 ∈ ℝ ∧ 3 ∈ ℝ)
265		dp2cl 32800	. . . . . . . . . . . . . . . 16 ⊢ ((6 ∈ ℝ ∧ 3 ∈ ℝ) → _63 ∈ ℝ)
266	264, 265	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _63 ∈ ℝ
267	177, 266	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℝ ∧ _63 ∈ ℝ)
268		dp2cl 32800	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ _63 ∈ ℝ) → _2_63 ∈ ℝ)
269	267, 268	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _2_63 ∈ ℝ
270	111, 269	pm3.2i 470	. . . . . . . . . . . 12 ⊢ (4 ∈ ℝ ∧ _2_63 ∈ ℝ)
271		dp2cl 32800	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ ∧ _2_63 ∈ ℝ) → _4_2_63 ∈ ℝ)
272	270, 271	ax-mp 5	. . . . . . . . . . 11 ⊢ _4_2_63 ∈ ℝ
273		dpcl 32811	. . . . . . . . . . 11 ⊢ ((1 ∈ ℕ₀ ∧ _4_2_63 ∈ ℝ) → (1._4_2_63) ∈ ℝ)
274	56, 272, 273	mp2an 692	. . . . . . . . . 10 ⊢ (1._4_2_63) ∈ ℝ
275	274	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1._4_2_63) ∈ ℝ)
276	275, 126	remulcld 11263	. . . . . . . 8 ⊢ (𝜑 → ((1._4_2_63) · (√‘𝑁)) ∈ ℝ)
277	112, 54	pm3.2i 470	. . . . . . . . . . . . . . . . . 18 ⊢ (8 ∈ ℝ ∧ 3 ∈ ℝ)
278		dp2cl 32800	. . . . . . . . . . . . . . . . . 18 ⊢ ((8 ∈ ℝ ∧ 3 ∈ ℝ) → _83 ∈ ℝ)
279	277, 278	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ _83 ∈ ℝ
280	112, 279	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (8 ∈ ℝ ∧ _83 ∈ ℝ)
281		dp2cl 32800	. . . . . . . . . . . . . . . 16 ⊢ ((8 ∈ ℝ ∧ _83 ∈ ℝ) → _8_83 ∈ ℝ)
282	280, 281	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _8_83 ∈ ℝ
283	54, 282	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℝ ∧ _8_83 ∈ ℝ)
284		dp2cl 32800	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℝ ∧ _8_83 ∈ ℝ) → _3_8_83 ∈ ℝ)
285	283, 284	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _3_8_83 ∈ ℝ
286	133, 285	pm3.2i 470	. . . . . . . . . . . 12 ⊢ (0 ∈ ℝ ∧ _3_8_83 ∈ ℝ)
287		dp2cl 32800	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ _3_8_83 ∈ ℝ) → _0_3_8_83 ∈ ℝ)
288	286, 287	ax-mp 5	. . . . . . . . . . 11 ⊢ _0_3_8_83 ∈ ℝ
289		dpcl 32811	. . . . . . . . . . 11 ⊢ ((1 ∈ ℕ₀ ∧ _0_3_8_83 ∈ ℝ) → (1._0_3_8_83) ∈ ℝ)
290	56, 288, 289	mp2an 692	. . . . . . . . . 10 ⊢ (1._0_3_8_83) ∈ ℝ
291	290	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1._0_3_8_83) ∈ ℝ)
292	291, 124	remulcld 11263	. . . . . . . 8 ⊢ (𝜑 → ((1._0_3_8_83) · 𝑁) ∈ ℝ)
293	276, 292	remulcld 11263	. . . . . . 7 ⊢ (𝜑 → (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)) ∈ ℝ)
294	123, 293	remulcld 11263	. . . . . 6 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) ∈ ℝ)
295	82, 294	remulcld 11263	. . . . 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 11263	. . . 4 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))))) ∈ ℝ)
297		vmage0 27081	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℕ → 0 ≤ (Λ‘𝑖))
298	243, 297	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 0 ≤ (Λ‘𝑖))
299	235, 244, 298	fsumge0 15809	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖))
300	1, 209	hgt750lemd 34626	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) < ((1._4_2_63) · (√‘𝑁)))
301		fzfid 13989	. . . . . . . . . 10 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
302	9	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
303	238	sselda 3958	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
304	302, 303	ffvelcdmd 7074	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
305		vmage0 27081	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → 0 ≤ (Λ‘𝑗))
306	303, 305	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 0 ≤ (Λ‘𝑗))
307	301, 304, 306	fsumge0 15809	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
308	1	hgt750lemc 34625	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) < ((1._0_3_8_83) · 𝑁))
309	245, 276, 251, 292, 299, 300, 307, 308	ltmul12ad 12181	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) < (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))
310	252, 293, 309	ltled 11381	. . . . . . 7 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ≤ (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))
311	156	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℝ)
312		1lt2 12409	. . . . . . . . . . 11 ⊢ 1 < 2
313	312	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 < 2)
314	311, 178, 124, 313, 210	ltletrd 11393	. . . . . . . . 9 ⊢ (𝜑 → 1 < 𝑁)
315	124, 314	rplogcld 26588	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ⁺)
316	252, 293, 315	lemul2d 13093	. . . . . . 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 232	. . . . . 6 ⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ≤ ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))))
318	253, 294, 216	lemul2d 13093	. . . . . 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 232	. . . . 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 13093	. . . . 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 232	. . . 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 14202	. . . . . . . . . 10 ⊢ ((1._0_7_9_9_55)↑2) ∈ ℝ
323	322, 164	remulcli 11249	. . . . . . . . 9 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ
324	274, 290	remulcli 11249	. . . . . . . . 9 ⊢ ((1._4_2_63) · (1._0_3_8_83)) ∈ ℝ
325	323, 324	remulcli 11249	. . . . . . . 8 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) ∈ ℝ
326	54, 325	remulcli 11249	. . . . . . 7 ⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) ∈ ℝ
327		hgt750lem2 34630	. . . . . . 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 11356	. . . . . 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 13066	. . . . . . . 8 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ⁺)
331	122, 214	rpexpcld 14263	. . . . . . . 8 ⊢ (𝜑 → (𝑁↑2) ∈ ℝ⁺)
332	330, 331	rpmulcld 13065	. . . . . . 7 ⊢ (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) ∈ ℝ⁺)
333	329, 121, 332	lemul1d 13092	. . . . . 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 233	. . . . 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 11261	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1._4_2_63) ∈ ℂ)
336	126	recnd 11261	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (√‘𝑁) ∈ ℂ)
337	291	recnd 11261	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1._0_3_8_83) ∈ ℂ)
338	124	recnd 11261	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℂ)
339	335, 336, 337, 338	mul4d 11445	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)) = (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)))
340	339	oveq2d 7419	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) = ((log‘𝑁) · (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁))))
341	123	recnd 11261	. . . . . . . . . . . . 13 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
342	335, 337	mulcld 11253	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1._4_2_63) · (1._0_3_8_83)) ∈ ℂ)
343	336, 338	mulcld 11253	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((√‘𝑁) · 𝑁) ∈ ℂ)
344	342, 343	mulcld 11253	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)) ∈ ℂ)
345	341, 344	mulcomd 11254	. . . . . . . . . . . 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 2770	. . . . . . . . . . 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 11256	. . . . . . . . . . 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 2770	. . . . . . . . . 10 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) = (((1._4_2_63) · (1._0_3_8_83)) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
349	348	oveq2d 7419	. . . . . . . . 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 11261	. . . . . . . . . 10 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℂ)
351	343, 341	mulcld 11253	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) ∈ ℂ)
352	350, 342, 351	mulassd 11256	. . . . . . . . 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 2773	. . . . . . . 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 7419	. . . . . . 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 11261	. . . . . . . 8 ⊢ (𝜑 → 3 ∈ ℂ)
356	350, 342	mulcld 11253	. . . . . . . 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 11256	. . . . . . 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 2773	. . . . . 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 11261	. . . . . . . . 9 ⊢ (𝜑 → (𝑁↑2) ∈ ℂ)
360	341, 336, 359, 128	div32d 12038	. . . . . . . 8 ⊢ (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) = ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))))
361	359, 336, 128	divcld 12015	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) ∈ ℂ)
362	341, 361	mulcomd 11254	. . . . . . . 8 ⊢ (𝜑 → ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))) = (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)))
363	338	sqvald 14159	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁↑2) = (𝑁 · 𝑁))
364	363	oveq1d 7418	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((𝑁 · 𝑁) / (√‘𝑁)))
365	338, 338, 336, 128	divassd 12050	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 · 𝑁) / (√‘𝑁)) = (𝑁 · (𝑁 / (√‘𝑁))))
366		divsqrtid 34572	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℝ⁺ → (𝑁 / (√‘𝑁)) = (√‘𝑁))
367	122, 366	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 / (√‘𝑁)) = (√‘𝑁))
368	367	oveq2d 7419	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · (𝑁 / (√‘𝑁))) = (𝑁 · (√‘𝑁)))
369	364, 365, 368	3eqtrd 2774	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = (𝑁 · (√‘𝑁)))
370	338, 336	mulcomd 11254	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 · (√‘𝑁)) = ((√‘𝑁) · 𝑁))
371	369, 370	eqtrd 2770	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((√‘𝑁) · 𝑁))
372	371	oveq1d 7418	. . . . . . . 8 ⊢ (𝜑 → (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)) = (((√‘𝑁) · 𝑁) · (log‘𝑁)))
373	360, 362, 372	3eqtrrd 2775	. . . . . . 7 ⊢ (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) = (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)))
374	373	oveq2d 7419	. . . . . 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 2770	. . . . 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 11261	. . . . . 6 ⊢ (𝜑 → (7._3_48) ∈ ℂ)
377	129	recnd 11261	. . . . . 6 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℂ)
378	376, 377, 359	mulassd 11256	. . . . 5 ⊢ (𝜑 → (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) = ((7._3_48) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
379	334, 375, 378	3brtr4d 5151	. . . 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 11390	. . 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 11390	. 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 11390	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 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 {crab 3415 ∖ cdif 3923 ∪ cun 3924 ∩ cin 3925 ⊆ wss 3926 ifcif 4500 {csn 4601 {cpr 4603 {ctp 4605 class class class wbr 5119 ↦ cmpt 5201 I cid 5547 ↾ cres 5656 ∘ ccom 5658 ⟶wf 6526 ‘cfv 6530 (class class class)co 7403 Fincfn 8957 ℂcc 11125 ℝcr 11126 0cc0 11127 1c1 11128 · cmul 11132 +∞cpnf 11264 < clt 11267 ≤ cle 11268 / cdiv 11892 ℕcn 12238 2c2 12293 3c3 12294 4c4 12295 5c5 12296 6c6 12297 7c7 12298 8c8 12299 9c9 12300 ℕ₀cn0 12499 ℤcz 12586 cdc 12706 ℝ⁺crp 13006 [,)cico 13362 ...cfz 13522 ..^cfzo 13669 ↑cexp 14077 √csqrt 15250 Σcsu 15700 ∥ cdvds 16270 ℙcprime 16688 pmTrspcpmtr 19420 logclog 26513 Λcvma 27052 ψcchp 27053 cdp2 32791 .cdp 32808 reprcrepr 34586

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7727 ax-reg 9604 ax-inf2 9653 ax-ac2 10475 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205 ax-addf 11206 ax-ros335 34623 ax-ros336 34624

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-tp 4606 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-iin 4970 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-se 5607 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6483 df-fun 6532 df-fn 6533 df-f 6534 df-f1 6535 df-fo 6536 df-f1o 6537 df-fv 6538 df-isom 6539 df-riota 7360 df-ov 7406 df-oprab 7407 df-mpo 7408 df-of 7669 df-om 7860 df-1st 7986 df-2nd 7987 df-supp 8158 df-frecs 8278 df-wrecs 8309 df-recs 8383 df-rdg 8422 df-1o 8478 df-2o 8479 df-oadd 8482 df-er 8717 df-map 8840 df-pm 8841 df-ixp 8910 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-fsupp 9372 df-fi 9421 df-sup 9452 df-inf 9453 df-oi 9522 df-r1 9776 df-rank 9777 df-dju 9913 df-card 9951 df-ac 10128 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11466 df-neg 11467 df-div 11893 df-nn 12239 df-2 12301 df-3 12302 df-4 12303 df-5 12304 df-6 12305 df-7 12306 df-8 12307 df-9 12308 df-n0 12500 df-xnn0 12573 df-z 12587 df-dec 12707 df-uz 12851 df-q 12963 df-rp 13007 df-xneg 13126 df-xadd 13127 df-xmul 13128 df-ioo 13364 df-ioc 13365 df-ico 13366 df-icc 13367 df-fz 13523 df-fzo 13670 df-fl 13807 df-mod 13885 df-seq 14018 df-exp 14078 df-fac 14290 df-bc 14319 df-hash 14347 df-shft 15084 df-cj 15116 df-re 15117 df-im 15118 df-sqrt 15252 df-abs 15253 df-limsup 15485 df-clim 15502 df-rlim 15503 df-sum 15701 df-prod 15918 df-ef 16081 df-sin 16083 df-cos 16084 df-tan 16085 df-pi 16086 df-dvds 16271 df-gcd 16512 df-prm 16689 df-pc 16855 df-struct 17164 df-sets 17181 df-slot 17199 df-ndx 17211 df-base 17227 df-ress 17250 df-plusg 17282 df-mulr 17283 df-starv 17284 df-sca 17285 df-vsca 17286 df-ip 17287 df-tset 17288 df-ple 17289 df-ds 17291 df-unif 17292 df-hom 17293 df-cco 17294 df-rest 17434 df-topn 17435 df-0g 17453 df-gsum 17454 df-topgen 17455 df-pt 17456 df-prds 17459 df-xrs 17514 df-qtop 17519 df-imas 17520 df-xps 17522 df-mre 17596 df-mrc 17597 df-acs 17599 df-mgm 18616 df-sgrp 18695 df-mnd 18711 df-submnd 18760 df-mulg 19049 df-cntz 19298 df-pmtr 19421 df-cmn 19761 df-psmet 21305 df-xmet 21306 df-met 21307 df-bl 21308 df-mopn 21309 df-fbas 21310 df-fg 21311 df-cnfld 21314 df-top 22830 df-topon 22847 df-topsp 22869 df-bases 22882 df-cld 22955 df-ntr 22956 df-cls 22957 df-nei 23034 df-lp 23072 df-perf 23073 df-cn 23163 df-cnp 23164 df-haus 23251 df-cmp 23323 df-tx 23498 df-hmeo 23691 df-fil 23782 df-fm 23874 df-flim 23875 df-flf 23876 df-xms 24257 df-ms 24258 df-tms 24259 df-cncf 24820 df-limc 25817 df-dv 25818 df-ulm 26336 df-log 26515 df-atan 26827 df-cht 27057 df-vma 27058 df-chp 27059 df-dp2 32792 df-dp 32809 df-repr 34587

This theorem is referenced by: tgoldbachgtde 34638

W3C validator