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 33968

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 12536	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
3		3nn0 12494	. . . . . 6 ⊢ 3 ∈ ℕ₀
4	3	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ₀)
5		ssidd 4004	. . . . 5 ⊢ (𝜑 → ℕ ⊆ ℕ)
6	2, 4, 5	reprfi2 33933	. . . 4 ⊢ (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
7		diffi 9181	. . . 4 ⊢ ((ℕ(repr‘3)𝑁) ∈ Fin → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
8	6, 7	syl 17	. . 3 ⊢ (𝜑 → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
9		vmaf 26859	. . . . . . 7 ⊢ Λ:ℕ⟶ℝ
10	9	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → Λ:ℕ⟶ℝ)
11		ssidd 4004	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ℕ ⊆ ℕ)
12	1	nnzd 12589	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℤ)
13	12	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑁 ∈ ℤ)
14	3	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 3 ∈ ℕ₀)
15		simpr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)))
16	15	eldifad 3959	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
17	11, 13, 14, 16	reprf 33922	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛:(0..^3)⟶ℕ)
18		c0ex 11212	. . . . . . . . . 10 ⊢ 0 ∈ V
19	18	tpid1 4771	. . . . . . . . 9 ⊢ 0 ∈ {0, 1, 2}
20		fzo0to3tp 13722	. . . . . . . . 9 ⊢ (0..^3) = {0, 1, 2}
21	19, 20	eleqtrri 2830	. . . . . . . 8 ⊢ 0 ∈ (0..^3)
22	21	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 0 ∈ (0..^3))
23	17, 22	ffvelcdmd 7086	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘0) ∈ ℕ)
24	10, 23	ffvelcdmd 7086	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘0)) ∈ ℝ)
25		rge0ssre 13437	. . . . . 6 ⊢ (0[,)+∞) ⊆ ℝ
26		hgt750leme.h	. . . . . . . 8 ⊢ (𝜑 → 𝐻:ℕ⟶(0[,)+∞))
27	26	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐻:ℕ⟶(0[,)+∞))
28	27, 23	ffvelcdmd 7086	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ (0[,)+∞))
29	25, 28	sselid 3979	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ ℝ)
30	24, 29	remulcld 11248	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) ∈ ℝ)
31		1ex 11214	. . . . . . . . . . 11 ⊢ 1 ∈ V
32	31	tpid2 4773	. . . . . . . . . 10 ⊢ 1 ∈ {0, 1, 2}
33	32, 20	eleqtrri 2830	. . . . . . . . 9 ⊢ 1 ∈ (0..^3)
34	33	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 1 ∈ (0..^3))
35	17, 34	ffvelcdmd 7086	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘1) ∈ ℕ)
36	10, 35	ffvelcdmd 7086	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘1)) ∈ ℝ)
37		hgt750leme.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾:ℕ⟶(0[,)+∞))
38	37	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐾:ℕ⟶(0[,)+∞))
39	38, 35	ffvelcdmd 7086	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ (0[,)+∞))
40	25, 39	sselid 3979	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ ℝ)
41	36, 40	remulcld 11248	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) ∈ ℝ)
42		2ex 12293	. . . . . . . . . . 11 ⊢ 2 ∈ V
43	42	tpid3 4776	. . . . . . . . . 10 ⊢ 2 ∈ {0, 1, 2}
44	43, 20	eleqtrri 2830	. . . . . . . . 9 ⊢ 2 ∈ (0..^3)
45	44	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 2 ∈ (0..^3))
46	17, 45	ffvelcdmd 7086	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘2) ∈ ℕ)
47	10, 46	ffvelcdmd 7086	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘2)) ∈ ℝ)
48	38, 46	ffvelcdmd 7086	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ (0[,)+∞))
49	25, 48	sselid 3979	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ ℝ)
50	47, 49	remulcld 11248	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))) ∈ ℝ)
51	41, 50	remulcld 11248	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))) ∈ ℝ)
52	30, 51	remulcld 11248	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
53	8, 52	fsumrecl 15684	. 2 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
54		3re 12296	. . . 4 ⊢ 3 ∈ ℝ
55	54	a1i 11	. . 3 ⊢ (𝜑 → 3 ∈ ℝ)
56		1nn0 12492	. . . . . . . . 9 ⊢ 1 ∈ ℕ₀
57		0nn0 12491	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
58		7nn0 12498	. . . . . . . . . . 11 ⊢ 7 ∈ ℕ₀
59		9nn0 12500	. . . . . . . . . . . 12 ⊢ 9 ∈ ℕ₀
60		5nn0 12496	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℕ₀
61		5nn 12302	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℕ
62		nnrp 12989	. . . . . . . . . . . . . . 15 ⊢ (5 ∈ ℕ → 5 ∈ ℝ⁺)
63	61, 62	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℝ⁺
64	60, 63	rpdp2cl 32315	. . . . . . . . . . . . 13 ⊢ _55 ∈ ℝ⁺
65	59, 64	rpdp2cl 32315	. . . . . . . . . . . 12 ⊢ _9_55 ∈ ℝ⁺
66	59, 65	rpdp2cl 32315	. . . . . . . . . . 11 ⊢ _9_9_55 ∈ ℝ⁺
67	58, 66	rpdp2cl 32315	. . . . . . . . . 10 ⊢ _7_9_9_55 ∈ ℝ⁺
68	57, 67	rpdp2cl 32315	. . . . . . . . 9 ⊢ _0_7_9_9_55 ∈ ℝ⁺
69	56, 68	rpdpcl 32336	. . . . . . . 8 ⊢ (1._0_7_9_9_55) ∈ ℝ⁺
70	69	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℝ⁺)
71	70	rpred 13020	. . . . . 6 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℝ)
72	71	resqcld 14094	. . . . 5 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ)
73		4nn0 12495	. . . . . . . . 9 ⊢ 4 ∈ ℕ₀
74		4nn 12299	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ
75		nnrp 12989	. . . . . . . . . . 11 ⊢ (4 ∈ ℕ → 4 ∈ ℝ⁺)
76	74, 75	ax-mp 5	. . . . . . . . . 10 ⊢ 4 ∈ ℝ⁺
77	56, 76	rpdp2cl 32315	. . . . . . . . 9 ⊢ _14 ∈ ℝ⁺
78	73, 77	rpdp2cl 32315	. . . . . . . 8 ⊢ _4_14 ∈ ℝ⁺
79	56, 78	rpdpcl 32336	. . . . . . 7 ⊢ (1._4_14) ∈ ℝ⁺
80	79	a1i 11	. . . . . 6 ⊢ (𝜑 → (1._4_14) ∈ ℝ⁺)
81	80	rpred 13020	. . . . 5 ⊢ (𝜑 → (1._4_14) ∈ ℝ)
82	72, 81	remulcld 11248	. . . 4 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ)
83		fveq1 6889	. . . . . . . . . 10 ⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
84	83	eleq1d 2816	. . . . . . . . 9 ⊢ (𝑑 = 𝑐 → ((𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
85	84	notbid 317	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
86	85	cbvrabv 3440	. . . . . . 7 ⊢ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
87	86	ssrab3 4079	. . . . . 6 ⊢ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁)
88		ssfi 9175	. . . . . 6 ⊢ (((ℕ(repr‘3)𝑁) ∈ Fin ∧ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁)) → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ∈ Fin)
89	6, 87, 88	sylancl 584	. . . . 5 ⊢ (𝜑 → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ∈ Fin)
90	9	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → Λ:ℕ⟶ℝ)
91		ssidd 4004	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ℕ ⊆ ℕ)
92	12	adantr 479	. . . . . . . . 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 3981	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
96	91, 92, 93, 95	reprf 33922	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛:(0..^3)⟶ℕ)
97	21	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 0 ∈ (0..^3))
98	96, 97	ffvelcdmd 7086	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘0) ∈ ℕ)
99	90, 98	ffvelcdmd 7086	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘0)) ∈ ℝ)
100	33	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 1 ∈ (0..^3))
101	96, 100	ffvelcdmd 7086	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘1) ∈ ℕ)
102	90, 101	ffvelcdmd 7086	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘1)) ∈ ℝ)
103	44	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 2 ∈ (0..^3))
104	96, 103	ffvelcdmd 7086	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘2) ∈ ℕ)
105	90, 104	ffvelcdmd 7086	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘2)) ∈ ℝ)
106	102, 105	remulcld 11248	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
107	99, 106	remulcld 11248	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
108	89, 107	fsumrecl 15684	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
109	82, 108	remulcld 11248	. . 3 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
110	55, 109	remulcld 11248	. 2 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ∈ ℝ)
111		4re 12300	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
112		8re 12312	. . . . . . . . . 10 ⊢ 8 ∈ ℝ
113	111, 112	pm3.2i 469	. . . . . . . . 9 ⊢ (4 ∈ ℝ ∧ 8 ∈ ℝ)
114		dp2cl 32313	. . . . . . . . 9 ⊢ ((4 ∈ ℝ ∧ 8 ∈ ℝ) → _48 ∈ ℝ)
115	113, 114	ax-mp 5	. . . . . . . 8 ⊢ _48 ∈ ℝ
116	54, 115	pm3.2i 469	. . . . . . 7 ⊢ (3 ∈ ℝ ∧ _48 ∈ ℝ)
117		dp2cl 32313	. . . . . . 7 ⊢ ((3 ∈ ℝ ∧ _48 ∈ ℝ) → _3_48 ∈ ℝ)
118	116, 117	ax-mp 5	. . . . . 6 ⊢ _3_48 ∈ ℝ
119		dpcl 32324	. . . . . 6 ⊢ ((7 ∈ ℕ₀ ∧ _3_48 ∈ ℝ) → (7._3_48) ∈ ℝ)
120	58, 118, 119	mp2an 688	. . . . 5 ⊢ (7._3_48) ∈ ℝ
121	120	a1i 11	. . . 4 ⊢ (𝜑 → (7._3_48) ∈ ℝ)
122	1	nnrpd 13018	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
123	122	relogcld 26367	. . . . 5 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
124	1	nnred 12231	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ)
125	122	rpge0d 13024	. . . . . 6 ⊢ (𝜑 → 0 ≤ 𝑁)
126	124, 125	resqrtcld 15368	. . . . 5 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ)
127	122	rpsqrtcld 15362	. . . . . 6 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
128	127	rpne0d 13025	. . . . 5 ⊢ (𝜑 → (√‘𝑁) ≠ 0)
129	123, 126, 128	redivcld 12046	. . . 4 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ)
130	121, 129	remulcld 11248	. . 3 ⊢ (𝜑 → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ∈ ℝ)
131	124	resqcld 14094	. . 3 ⊢ (𝜑 → (𝑁↑2) ∈ ℝ)
132	130, 131	remulcld 11248	. 2 ⊢ (𝜑 → (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) ∈ ℝ)
133		0re 11220	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
134		7re 12309	. . . . . . . . . . . . 13 ⊢ 7 ∈ ℝ
135		9re 12315	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℝ
136		5re 12303	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 ∈ ℝ
137	136, 136	pm3.2i 469	. . . . . . . . . . . . . . . . . 18 ⊢ (5 ∈ ℝ ∧ 5 ∈ ℝ)
138		dp2cl 32313	. . . . . . . . . . . . . . . . . 18 ⊢ ((5 ∈ ℝ ∧ 5 ∈ ℝ) → _55 ∈ ℝ)
139	137, 138	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ _55 ∈ ℝ
140	135, 139	pm3.2i 469	. . . . . . . . . . . . . . . 16 ⊢ (9 ∈ ℝ ∧ _55 ∈ ℝ)
141		dp2cl 32313	. . . . . . . . . . . . . . . 16 ⊢ ((9 ∈ ℝ ∧ _55 ∈ ℝ) → _9_55 ∈ ℝ)
142	140, 141	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _9_55 ∈ ℝ
143	135, 142	pm3.2i 469	. . . . . . . . . . . . . 14 ⊢ (9 ∈ ℝ ∧ _9_55 ∈ ℝ)
144		dp2cl 32313	. . . . . . . . . . . . . 14 ⊢ ((9 ∈ ℝ ∧ _9_55 ∈ ℝ) → _9_9_55 ∈ ℝ)
145	143, 144	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _9_9_55 ∈ ℝ
146	134, 145	pm3.2i 469	. . . . . . . . . . . 12 ⊢ (7 ∈ ℝ ∧ _9_9_55 ∈ ℝ)
147		dp2cl 32313	. . . . . . . . . . . 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 469	. . . . . . . . . 10 ⊢ (0 ∈ ℝ ∧ _7_9_9_55 ∈ ℝ)
150		dp2cl 32313	. . . . . . . . . 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 32324	. . . . . . . . 9 ⊢ ((1 ∈ ℕ₀ ∧ _0_7_9_9_55 ∈ ℝ) → (1._0_7_9_9_55) ∈ ℝ)
153	56, 151, 152	mp2an 688	. . . . . . . 8 ⊢ (1._0_7_9_9_55) ∈ ℝ
154	153	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℝ)
155	154	resqcld 14094	. . . . . 6 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ)
156		1re 11218	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
157	156, 111	pm3.2i 469	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ ∧ 4 ∈ ℝ)
158		dp2cl 32313	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 4 ∈ ℝ) → _14 ∈ ℝ)
159	157, 158	ax-mp 5	. . . . . . . . . 10 ⊢ _14 ∈ ℝ
160	111, 159	pm3.2i 469	. . . . . . . . 9 ⊢ (4 ∈ ℝ ∧ _14 ∈ ℝ)
161		dp2cl 32313	. . . . . . . . 9 ⊢ ((4 ∈ ℝ ∧ _14 ∈ ℝ) → _4_14 ∈ ℝ)
162	160, 161	ax-mp 5	. . . . . . . 8 ⊢ _4_14 ∈ ℝ
163		dpcl 32324	. . . . . . . 8 ⊢ ((1 ∈ ℕ₀ ∧ _4_14 ∈ ℝ) → (1._4_14) ∈ ℝ)
164	56, 162, 163	mp2an 688	. . . . . . 7 ⊢ (1._4_14) ∈ ℝ
165	164	a1i 11	. . . . . 6 ⊢ (𝜑 → (1._4_14) ∈ ℝ)
166	155, 165	remulcld 11248	. . . . 5 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ)
167	36, 47	remulcld 11248	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
168	24, 167	remulcld 11248	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
169	8, 168	fsumrecl 15684	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
170	166, 169	remulcld 11248	. . . 4 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
171	55, 108	remulcld 11248	. . . . 5 ⊢ (𝜑 → (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
172	166, 171	remulcld 11248	. . . 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 33963	. . . 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 12290	. . . . . . . 8 ⊢ 2 ∈ ℝ
178	177	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ∈ ℝ)
179		10nn0 12699	. . . . . . . . . 10 ⊢ ;10 ∈ ℕ₀
180		2nn0 12493	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
181	180, 58	deccl 12696	. . . . . . . . . 10 ⊢ ;27 ∈ ℕ₀
182	179, 181	nn0expcli 14058	. . . . . . . . 9 ⊢ (;10↑;27) ∈ ℕ₀
183	182	nn0rei 12487	. . . . . . . 8 ⊢ (;10↑;27) ∈ ℝ
184	183	a1i 11	. . . . . . 7 ⊢ (𝜑 → (;10↑;27) ∈ ℝ)
185	179	numexp1 17014	. . . . . . . . . 10 ⊢ (;10↑1) = ;10
186	179	nn0rei 12487	. . . . . . . . . 10 ⊢ ;10 ∈ ℝ
187	185, 186	eqeltri 2827	. . . . . . . . 9 ⊢ (;10↑1) ∈ ℝ
188	187	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (;10↑1) ∈ ℝ)
189		1nn 12227	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
190		2lt9 12421	. . . . . . . . . . . 12 ⊢ 2 < 9
191	177, 135, 190	ltleii 11341	. . . . . . . . . . 11 ⊢ 2 ≤ 9
192	189, 57, 180, 191	declei 12717	. . . . . . . . . 10 ⊢ 2 ≤ ;10
193	192, 185	breqtrri 5174	. . . . . . . . 9 ⊢ 2 ≤ (;10↑1)
194	193	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≤ (;10↑1))
195		1z 12596	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
196	181	nn0zi 12591	. . . . . . . . . . . 12 ⊢ ;27 ∈ ℤ
197	186, 195, 196	3pm3.2i 1337	. . . . . . . . . . 11 ⊢ (;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ)
198		1lt10 12820	. . . . . . . . . . 11 ⊢ 1 < ;10
199	197, 198	pm3.2i 469	. . . . . . . . . 10 ⊢ ((;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ 1 < ;10)
200		2nn 12289	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
201		1lt9 12422	. . . . . . . . . . . 12 ⊢ 1 < 9
202	156, 135, 201	ltleii 11341	. . . . . . . . . . 11 ⊢ 1 ≤ 9
203	200, 58, 56, 202	declei 12717	. . . . . . . . . 10 ⊢ 1 ≤ ;27
204		leexp2 14140	. . . . . . . . . . 11 ⊢ (((;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ 1 < ;10) → (1 ≤ ;27 ↔ (;10↑1) ≤ (;10↑;27)))
205	204	biimpa 475	. . . . . . . . . 10 ⊢ ((((;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ 1 < ;10) ∧ 1 ≤ ;27) → (;10↑1) ≤ (;10↑;27))
206	199, 203, 205	mp2an 688	. . . . . . . . 9 ⊢ (;10↑1) ≤ (;10↑;27)
207	206	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (;10↑1) ≤ (;10↑;27))
208	178, 188, 184, 194, 207	letrd 11375	. . . . . . 7 ⊢ (𝜑 → 2 ≤ (;10↑;27))
209		hgt750leme.0	. . . . . . 7 ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)
210	178, 184, 124, 208, 209	letrd 11375	. . . . . 6 ⊢ (𝜑 → 2 ≤ 𝑁)
211		eqid 2730	. . . . . 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 33967	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
213		2z 12598	. . . . . . . . 9 ⊢ 2 ∈ ℤ
214	213	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℤ)
215	70, 214	rpexpcld 14214	. . . . . . 7 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ⁺)
216	215, 80	rpmulcld 13036	. . . . . 6 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ⁺)
217	169, 171, 216	lemul2d 13064	. . . . 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 11375	. . 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 11246	. . . . . 6 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℂ)
221	220	sqcld 14113	. . . . 5 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℂ)
222	165	recnd 11246	. . . . 5 ⊢ (𝜑 → (1._4_14) ∈ ℂ)
223	221, 222	mulcld 11238	. . . 4 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℂ)
224		3cn 12297	. . . . 5 ⊢ 3 ∈ ℂ
225	224	a1i 11	. . . 4 ⊢ (𝜑 → 3 ∈ ℂ)
226	108	recnd 11246	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℂ)
227	223, 225, 226	mul12d 11427	. . 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 5173	. 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 13941	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ Fin
230		diffi 9181	. . . . . . . . . . 11 ⊢ ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
231	229, 230	ax-mp 5	. . . . . . . . . 10 ⊢ ((1...𝑁) ∖ ℙ) ∈ Fin
232		snfi 9046	. . . . . . . . . 10 ⊢ {2} ∈ Fin
233		unfi 9174	. . . . . . . . . 10 ⊢ ((((1...𝑁) ∖ ℙ) ∈ Fin ∧ {2} ∈ Fin) → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
234	231, 232, 233	mp2an 688	. . . . . . . . 9 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin
235	234	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
236	9	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → Λ:ℕ⟶ℝ)
237		fz1ssnn 13536	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ ℕ
238	237	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
239	238	ssdifssd 4141	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ ℕ)
240	200	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℕ)
241	240	snssd 4811	. . . . . . . . . . 11 ⊢ (𝜑 → {2} ⊆ ℕ)
242	239, 241	unssd 4185	. . . . . . . . . 10 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
243	242	sselda 3981	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 𝑖 ∈ ℕ)
244	236, 243	ffvelcdmd 7086	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℝ)
245	235, 244	fsumrecl 15684	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) ∈ ℝ)
246		chpvalz 33938	. . . . . . . . 9 ⊢ (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
247	12, 246	syl 17	. . . . . . . 8 ⊢ (𝜑 → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
248		chpf 26863	. . . . . . . . . 10 ⊢ ψ:ℝ⟶ℝ
249	248	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ψ:ℝ⟶ℝ)
250	249, 124	ffvelcdmd 7086	. . . . . . . 8 ⊢ (𝜑 → (ψ‘𝑁) ∈ ℝ)
251	247, 250	eqeltrrd 2832	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℝ)
252	245, 251	remulcld 11248	. . . . . 6 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ∈ ℝ)
253	123, 252	remulcld 11248	. . . . 5 ⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ∈ ℝ)
254	82, 253	remulcld 11248	. . . 4 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ∈ ℝ)
255	55, 254	remulcld 11248	. . 3 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ∈ ℝ)
256	176, 1, 210, 86	hgt750lemb 33966	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
257	108, 253, 216	lemul2d 13064	. . . . 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 12984	. . . . . 6 ⊢ 3 ∈ ℝ⁺
260	259	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℝ⁺)
261	109, 254, 260	lemul2d 13064	. . . 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 12306	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℝ
264	263, 54	pm3.2i 469	. . . . . . . . . . . . . . . 16 ⊢ (6 ∈ ℝ ∧ 3 ∈ ℝ)
265		dp2cl 32313	. . . . . . . . . . . . . . . 16 ⊢ ((6 ∈ ℝ ∧ 3 ∈ ℝ) → _63 ∈ ℝ)
266	264, 265	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _63 ∈ ℝ
267	177, 266	pm3.2i 469	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℝ ∧ _63 ∈ ℝ)
268		dp2cl 32313	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ _63 ∈ ℝ) → _2_63 ∈ ℝ)
269	267, 268	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _2_63 ∈ ℝ
270	111, 269	pm3.2i 469	. . . . . . . . . . . 12 ⊢ (4 ∈ ℝ ∧ _2_63 ∈ ℝ)
271		dp2cl 32313	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ ∧ _2_63 ∈ ℝ) → _4_2_63 ∈ ℝ)
272	270, 271	ax-mp 5	. . . . . . . . . . 11 ⊢ _4_2_63 ∈ ℝ
273		dpcl 32324	. . . . . . . . . . 11 ⊢ ((1 ∈ ℕ₀ ∧ _4_2_63 ∈ ℝ) → (1._4_2_63) ∈ ℝ)
274	56, 272, 273	mp2an 688	. . . . . . . . . 10 ⊢ (1._4_2_63) ∈ ℝ
275	274	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1._4_2_63) ∈ ℝ)
276	275, 126	remulcld 11248	. . . . . . . 8 ⊢ (𝜑 → ((1._4_2_63) · (√‘𝑁)) ∈ ℝ)
277	112, 54	pm3.2i 469	. . . . . . . . . . . . . . . . . 18 ⊢ (8 ∈ ℝ ∧ 3 ∈ ℝ)
278		dp2cl 32313	. . . . . . . . . . . . . . . . . 18 ⊢ ((8 ∈ ℝ ∧ 3 ∈ ℝ) → _83 ∈ ℝ)
279	277, 278	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ _83 ∈ ℝ
280	112, 279	pm3.2i 469	. . . . . . . . . . . . . . . 16 ⊢ (8 ∈ ℝ ∧ _83 ∈ ℝ)
281		dp2cl 32313	. . . . . . . . . . . . . . . 16 ⊢ ((8 ∈ ℝ ∧ _83 ∈ ℝ) → _8_83 ∈ ℝ)
282	280, 281	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _8_83 ∈ ℝ
283	54, 282	pm3.2i 469	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℝ ∧ _8_83 ∈ ℝ)
284		dp2cl 32313	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℝ ∧ _8_83 ∈ ℝ) → _3_8_83 ∈ ℝ)
285	283, 284	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _3_8_83 ∈ ℝ
286	133, 285	pm3.2i 469	. . . . . . . . . . . 12 ⊢ (0 ∈ ℝ ∧ _3_8_83 ∈ ℝ)
287		dp2cl 32313	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ _3_8_83 ∈ ℝ) → _0_3_8_83 ∈ ℝ)
288	286, 287	ax-mp 5	. . . . . . . . . . 11 ⊢ _0_3_8_83 ∈ ℝ
289		dpcl 32324	. . . . . . . . . . 11 ⊢ ((1 ∈ ℕ₀ ∧ _0_3_8_83 ∈ ℝ) → (1._0_3_8_83) ∈ ℝ)
290	56, 288, 289	mp2an 688	. . . . . . . . . 10 ⊢ (1._0_3_8_83) ∈ ℝ
291	290	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1._0_3_8_83) ∈ ℝ)
292	291, 124	remulcld 11248	. . . . . . . 8 ⊢ (𝜑 → ((1._0_3_8_83) · 𝑁) ∈ ℝ)
293	276, 292	remulcld 11248	. . . . . . 7 ⊢ (𝜑 → (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)) ∈ ℝ)
294	123, 293	remulcld 11248	. . . . . 6 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) ∈ ℝ)
295	82, 294	remulcld 11248	. . . . 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 11248	. . . 4 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))))) ∈ ℝ)
297		vmage0 26861	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℕ → 0 ≤ (Λ‘𝑖))
298	243, 297	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 0 ≤ (Λ‘𝑖))
299	235, 244, 298	fsumge0 15745	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖))
300	1, 209	hgt750lemd 33958	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) < ((1._4_2_63) · (√‘𝑁)))
301		fzfid 13942	. . . . . . . . . 10 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
302	9	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
303	238	sselda 3981	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
304	302, 303	ffvelcdmd 7086	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
305		vmage0 26861	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → 0 ≤ (Λ‘𝑗))
306	303, 305	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 0 ≤ (Λ‘𝑗))
307	301, 304, 306	fsumge0 15745	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
308	1	hgt750lemc 33957	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) < ((1._0_3_8_83) · 𝑁))
309	245, 276, 251, 292, 299, 300, 307, 308	ltmul12ad 12159	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) < (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))
310	252, 293, 309	ltled 11366	. . . . . . 7 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ≤ (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))
311	156	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℝ)
312		1lt2 12387	. . . . . . . . . . 11 ⊢ 1 < 2
313	312	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 < 2)
314	311, 178, 124, 313, 210	ltletrd 11378	. . . . . . . . 9 ⊢ (𝜑 → 1 < 𝑁)
315	124, 314	rplogcld 26373	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ⁺)
316	252, 293, 315	lemul2d 13064	. . . . . . 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 13064	. . . . . 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 13064	. . . . 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 14154	. . . . . . . . . 10 ⊢ ((1._0_7_9_9_55)↑2) ∈ ℝ
323	322, 164	remulcli 11234	. . . . . . . . 9 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ
324	274, 290	remulcli 11234	. . . . . . . . 9 ⊢ ((1._4_2_63) · (1._0_3_8_83)) ∈ ℝ
325	323, 324	remulcli 11234	. . . . . . . 8 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) ∈ ℝ
326	54, 325	remulcli 11234	. . . . . . 7 ⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) ∈ ℝ
327		hgt750lem2 33962	. . . . . . 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 11341	. . . . . 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 13037	. . . . . . . 8 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ⁺)
331	122, 214	rpexpcld 14214	. . . . . . . 8 ⊢ (𝜑 → (𝑁↑2) ∈ ℝ⁺)
332	330, 331	rpmulcld 13036	. . . . . . 7 ⊢ (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) ∈ ℝ⁺)
333	329, 121, 332	lemul1d 13063	. . . . . 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 11246	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1._4_2_63) ∈ ℂ)
336	126	recnd 11246	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (√‘𝑁) ∈ ℂ)
337	291	recnd 11246	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1._0_3_8_83) ∈ ℂ)
338	124	recnd 11246	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℂ)
339	335, 336, 337, 338	mul4d 11430	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)) = (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)))
340	339	oveq2d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) = ((log‘𝑁) · (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁))))
341	123	recnd 11246	. . . . . . . . . . . . 13 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
342	335, 337	mulcld 11238	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1._4_2_63) · (1._0_3_8_83)) ∈ ℂ)
343	336, 338	mulcld 11238	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((√‘𝑁) · 𝑁) ∈ ℂ)
344	342, 343	mulcld 11238	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)) ∈ ℂ)
345	341, 344	mulcomd 11239	. . . . . . . . . . . 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 11241	. . . . . . . . . . 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 7427	. . . . . . . . 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 11246	. . . . . . . . . 10 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℂ)
351	343, 341	mulcld 11238	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) ∈ ℂ)
352	350, 342, 351	mulassd 11241	. . . . . . . . 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 7427	. . . . . . 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 11246	. . . . . . . 8 ⊢ (𝜑 → 3 ∈ ℂ)
356	350, 342	mulcld 11238	. . . . . . . 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 11241	. . . . . . 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 11246	. . . . . . . . 9 ⊢ (𝜑 → (𝑁↑2) ∈ ℂ)
360	341, 336, 359, 128	div32d 12017	. . . . . . . 8 ⊢ (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) = ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))))
361	359, 336, 128	divcld 11994	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) ∈ ℂ)
362	341, 361	mulcomd 11239	. . . . . . . 8 ⊢ (𝜑 → ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))) = (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)))
363	338	sqvald 14112	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁↑2) = (𝑁 · 𝑁))
364	363	oveq1d 7426	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((𝑁 · 𝑁) / (√‘𝑁)))
365	338, 338, 336, 128	divassd 12029	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 · 𝑁) / (√‘𝑁)) = (𝑁 · (𝑁 / (√‘𝑁))))
366		divsqrtid 33904	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℝ⁺ → (𝑁 / (√‘𝑁)) = (√‘𝑁))
367	122, 366	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 / (√‘𝑁)) = (√‘𝑁))
368	367	oveq2d 7427	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · (𝑁 / (√‘𝑁))) = (𝑁 · (√‘𝑁)))
369	364, 365, 368	3eqtrd 2774	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = (𝑁 · (√‘𝑁)))
370	338, 336	mulcomd 11239	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 · (√‘𝑁)) = ((√‘𝑁) · 𝑁))
371	369, 370	eqtrd 2770	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((√‘𝑁) · 𝑁))
372	371	oveq1d 7426	. . . . . . . 8 ⊢ (𝜑 → (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)) = (((√‘𝑁) · 𝑁) · (log‘𝑁)))
373	360, 362, 372	3eqtrrd 2775	. . . . . . 7 ⊢ (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) = (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)))
374	373	oveq2d 7427	. . . . . 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 11246	. . . . . 6 ⊢ (𝜑 → (7._3_48) ∈ ℂ)
377	129	recnd 11246	. . . . . 6 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℂ)
378	376, 377, 359	mulassd 11241	. . . . 5 ⊢ (𝜑 → (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) = ((7._3_48) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
379	334, 375, 378	3brtr4d 5179	. . . 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 11375	. . 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 11375	. 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 11375	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 394 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 {crab 3430 ∖ cdif 3944 ∪ cun 3945 ∩ cin 3946 ⊆ wss 3947 ifcif 4527 {csn 4627 {cpr 4629 {ctp 4631 class class class wbr 5147 ↦ cmpt 5230 I cid 5572 ↾ cres 5677 ∘ ccom 5679 ⟶wf 6538 ‘cfv 6542 (class class class)co 7411 Fincfn 8941 ℂcc 11110 ℝcr 11111 0cc0 11112 1c1 11113 · cmul 11117 +∞cpnf 11249 < clt 11252 ≤ cle 11253 / cdiv 11875 ℕcn 12216 2c2 12271 3c3 12272 4c4 12273 5c5 12274 6c6 12275 7c7 12276 8c8 12277 9c9 12278 ℕ₀cn0 12476 ℤcz 12562 cdc 12681 ℝ⁺crp 12978 [,)cico 13330 ...cfz 13488 ..^cfzo 13631 ↑cexp 14031 √csqrt 15184 Σcsu 15636 ∥ cdvds 16201 ℙcprime 16612 pmTrspcpmtr 19350 logclog 26299 Λcvma 26832 ψcchp 26833 cdp2 32304 .cdp 32321 reprcrepr 33918

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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-reg 9589 ax-inf2 9638 ax-ac2 10460 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190 ax-addf 11191 ax-mulf 11192 ax-ros335 33955 ax-ros336 33956

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-iin 4999 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7672 df-om 7858 df-1st 7977 df-2nd 7978 df-supp 8149 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-2o 8469 df-oadd 8472 df-er 8705 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9364 df-fi 9408 df-sup 9439 df-inf 9440 df-oi 9507 df-r1 9761 df-rank 9762 df-dju 9898 df-card 9936 df-ac 10113 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-5 12282 df-6 12283 df-7 12284 df-8 12285 df-9 12286 df-n0 12477 df-xnn0 12549 df-z 12563 df-dec 12682 df-uz 12827 df-q 12937 df-rp 12979 df-xneg 13096 df-xadd 13097 df-xmul 13098 df-ioo 13332 df-ioc 13333 df-ico 13334 df-icc 13335 df-fz 13489 df-fzo 13632 df-fl 13761 df-mod 13839 df-seq 13971 df-exp 14032 df-fac 14238 df-bc 14267 df-hash 14295 df-shft 15018 df-cj 15050 df-re 15051 df-im 15052 df-sqrt 15186 df-abs 15187 df-limsup 15419 df-clim 15436 df-rlim 15437 df-sum 15637 df-prod 15854 df-ef 16015 df-sin 16017 df-cos 16018 df-tan 16019 df-pi 16020 df-dvds 16202 df-gcd 16440 df-prm 16613 df-pc 16774 df-struct 17084 df-sets 17101 df-slot 17119 df-ndx 17131 df-base 17149 df-ress 17178 df-plusg 17214 df-mulr 17215 df-starv 17216 df-sca 17217 df-vsca 17218 df-ip 17219 df-tset 17220 df-ple 17221 df-ds 17223 df-unif 17224 df-hom 17225 df-cco 17226 df-rest 17372 df-topn 17373 df-0g 17391 df-gsum 17392 df-topgen 17393 df-pt 17394 df-prds 17397 df-xrs 17452 df-qtop 17457 df-imas 17458 df-xps 17460 df-mre 17534 df-mrc 17535 df-acs 17537 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-submnd 18706 df-mulg 18987 df-cntz 19222 df-pmtr 19351 df-cmn 19691 df-psmet 21136 df-xmet 21137 df-met 21138 df-bl 21139 df-mopn 21140 df-fbas 21141 df-fg 21142 df-cnfld 21145 df-top 22616 df-topon 22633 df-topsp 22655 df-bases 22669 df-cld 22743 df-ntr 22744 df-cls 22745 df-nei 22822 df-lp 22860 df-perf 22861 df-cn 22951 df-cnp 22952 df-haus 23039 df-cmp 23111 df-tx 23286 df-hmeo 23479 df-fil 23570 df-fm 23662 df-flim 23663 df-flf 23664 df-xms 24046 df-ms 24047 df-tms 24048 df-cncf 24618 df-limc 25615 df-dv 25616 df-ulm 26125 df-log 26301 df-atan 26608 df-cht 26837 df-vma 26838 df-chp 26839 df-dp2 32305 df-dp 32322 df-repr 33919

This theorem is referenced by: tgoldbachgtde 33970

W3C validator