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 34656

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 12510	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
3		3nn0 12467	. . . . . 6 ⊢ 3 ∈ ℕ₀
4	3	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ₀)
5		ssidd 3973	. . . . 5 ⊢ (𝜑 → ℕ ⊆ ℕ)
6	2, 4, 5	reprfi2 34621	. . . 4 ⊢ (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
7		diffi 9145	. . . 4 ⊢ ((ℕ(repr‘3)𝑁) ∈ Fin → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
8	6, 7	syl 17	. . 3 ⊢ (𝜑 → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
9		vmaf 27036	. . . . . . 7 ⊢ Λ:ℕ⟶ℝ
10	9	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → Λ:ℕ⟶ℝ)
11		ssidd 3973	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ℕ ⊆ ℕ)
12	1	nnzd 12563	. . . . . . . . 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 3929	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
17	11, 13, 14, 16	reprf 34610	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛:(0..^3)⟶ℕ)
18		c0ex 11175	. . . . . . . . . 10 ⊢ 0 ∈ V
19	18	tpid1 4735	. . . . . . . . 9 ⊢ 0 ∈ {0, 1, 2}
20		fzo0to3tp 13720	. . . . . . . . 9 ⊢ (0..^3) = {0, 1, 2}
21	19, 20	eleqtrri 2828	. . . . . . . 8 ⊢ 0 ∈ (0..^3)
22	21	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 0 ∈ (0..^3))
23	17, 22	ffvelcdmd 7060	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘0) ∈ ℕ)
24	10, 23	ffvelcdmd 7060	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘0)) ∈ ℝ)
25		rge0ssre 13424	. . . . . 6 ⊢ (0[,)+∞) ⊆ ℝ
26		hgt750leme.h	. . . . . . . 8 ⊢ (𝜑 → 𝐻:ℕ⟶(0[,)+∞))
27	26	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐻:ℕ⟶(0[,)+∞))
28	27, 23	ffvelcdmd 7060	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ (0[,)+∞))
29	25, 28	sselid 3947	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ ℝ)
30	24, 29	remulcld 11211	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) ∈ ℝ)
31		1ex 11177	. . . . . . . . . . 11 ⊢ 1 ∈ V
32	31	tpid2 4737	. . . . . . . . . 10 ⊢ 1 ∈ {0, 1, 2}
33	32, 20	eleqtrri 2828	. . . . . . . . 9 ⊢ 1 ∈ (0..^3)
34	33	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 1 ∈ (0..^3))
35	17, 34	ffvelcdmd 7060	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘1) ∈ ℕ)
36	10, 35	ffvelcdmd 7060	. . . . . 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 7060	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ (0[,)+∞))
40	25, 39	sselid 3947	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ ℝ)
41	36, 40	remulcld 11211	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) ∈ ℝ)
42		2ex 12270	. . . . . . . . . . 11 ⊢ 2 ∈ V
43	42	tpid3 4740	. . . . . . . . . 10 ⊢ 2 ∈ {0, 1, 2}
44	43, 20	eleqtrri 2828	. . . . . . . . 9 ⊢ 2 ∈ (0..^3)
45	44	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 2 ∈ (0..^3))
46	17, 45	ffvelcdmd 7060	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘2) ∈ ℕ)
47	10, 46	ffvelcdmd 7060	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘2)) ∈ ℝ)
48	38, 46	ffvelcdmd 7060	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ (0[,)+∞))
49	25, 48	sselid 3947	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ ℝ)
50	47, 49	remulcld 11211	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))) ∈ ℝ)
51	41, 50	remulcld 11211	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))) ∈ ℝ)
52	30, 51	remulcld 11211	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
53	8, 52	fsumrecl 15707	. 2 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
54		3re 12273	. . . 4 ⊢ 3 ∈ ℝ
55	54	a1i 11	. . 3 ⊢ (𝜑 → 3 ∈ ℝ)
56		1nn0 12465	. . . . . . . . 9 ⊢ 1 ∈ ℕ₀
57		0nn0 12464	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
58		7nn0 12471	. . . . . . . . . . 11 ⊢ 7 ∈ ℕ₀
59		9nn0 12473	. . . . . . . . . . . 12 ⊢ 9 ∈ ℕ₀
60		5nn0 12469	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℕ₀
61		5nn 12279	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℕ
62		nnrp 12970	. . . . . . . . . . . . . . 15 ⊢ (5 ∈ ℕ → 5 ∈ ℝ⁺)
63	61, 62	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℝ⁺
64	60, 63	rpdp2cl 32809	. . . . . . . . . . . . 13 ⊢ _55 ∈ ℝ⁺
65	59, 64	rpdp2cl 32809	. . . . . . . . . . . 12 ⊢ _9_55 ∈ ℝ⁺
66	59, 65	rpdp2cl 32809	. . . . . . . . . . 11 ⊢ _9_9_55 ∈ ℝ⁺
67	58, 66	rpdp2cl 32809	. . . . . . . . . 10 ⊢ _7_9_9_55 ∈ ℝ⁺
68	57, 67	rpdp2cl 32809	. . . . . . . . 9 ⊢ _0_7_9_9_55 ∈ ℝ⁺
69	56, 68	rpdpcl 32830	. . . . . . . 8 ⊢ (1._0_7_9_9_55) ∈ ℝ⁺
70	69	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℝ⁺)
71	70	rpred 13002	. . . . . 6 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℝ)
72	71	resqcld 14097	. . . . 5 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ)
73		4nn0 12468	. . . . . . . . 9 ⊢ 4 ∈ ℕ₀
74		4nn 12276	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ
75		nnrp 12970	. . . . . . . . . . 11 ⊢ (4 ∈ ℕ → 4 ∈ ℝ⁺)
76	74, 75	ax-mp 5	. . . . . . . . . 10 ⊢ 4 ∈ ℝ⁺
77	56, 76	rpdp2cl 32809	. . . . . . . . 9 ⊢ _14 ∈ ℝ⁺
78	73, 77	rpdp2cl 32809	. . . . . . . 8 ⊢ _4_14 ∈ ℝ⁺
79	56, 78	rpdpcl 32830	. . . . . . 7 ⊢ (1._4_14) ∈ ℝ⁺
80	79	a1i 11	. . . . . 6 ⊢ (𝜑 → (1._4_14) ∈ ℝ⁺)
81	80	rpred 13002	. . . . 5 ⊢ (𝜑 → (1._4_14) ∈ ℝ)
82	72, 81	remulcld 11211	. . . 4 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ)
83		fveq1 6860	. . . . . . . . . 10 ⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
84	83	eleq1d 2814	. . . . . . . . 9 ⊢ (𝑑 = 𝑐 → ((𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
85	84	notbid 318	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
86	85	cbvrabv 3419	. . . . . . 7 ⊢ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
87	86	ssrab3 4048	. . . . . 6 ⊢ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁)
88		ssfi 9143	. . . . . 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 3973	. . . . . . . . 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 3949	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
96	91, 92, 93, 95	reprf 34610	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛:(0..^3)⟶ℕ)
97	21	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 0 ∈ (0..^3))
98	96, 97	ffvelcdmd 7060	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘0) ∈ ℕ)
99	90, 98	ffvelcdmd 7060	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘0)) ∈ ℝ)
100	33	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 1 ∈ (0..^3))
101	96, 100	ffvelcdmd 7060	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘1) ∈ ℕ)
102	90, 101	ffvelcdmd 7060	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘1)) ∈ ℝ)
103	44	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 2 ∈ (0..^3))
104	96, 103	ffvelcdmd 7060	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘2) ∈ ℕ)
105	90, 104	ffvelcdmd 7060	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘2)) ∈ ℝ)
106	102, 105	remulcld 11211	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
107	99, 106	remulcld 11211	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
108	89, 107	fsumrecl 15707	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
109	82, 108	remulcld 11211	. . 3 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
110	55, 109	remulcld 11211	. 2 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ∈ ℝ)
111		4re 12277	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
112		8re 12289	. . . . . . . . . 10 ⊢ 8 ∈ ℝ
113	111, 112	pm3.2i 470	. . . . . . . . 9 ⊢ (4 ∈ ℝ ∧ 8 ∈ ℝ)
114		dp2cl 32807	. . . . . . . . 9 ⊢ ((4 ∈ ℝ ∧ 8 ∈ ℝ) → _48 ∈ ℝ)
115	113, 114	ax-mp 5	. . . . . . . 8 ⊢ _48 ∈ ℝ
116	54, 115	pm3.2i 470	. . . . . . 7 ⊢ (3 ∈ ℝ ∧ _48 ∈ ℝ)
117		dp2cl 32807	. . . . . . 7 ⊢ ((3 ∈ ℝ ∧ _48 ∈ ℝ) → _3_48 ∈ ℝ)
118	116, 117	ax-mp 5	. . . . . 6 ⊢ _3_48 ∈ ℝ
119		dpcl 32818	. . . . . 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 13000	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
123	122	relogcld 26539	. . . . 5 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
124	1	nnred 12208	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ)
125	122	rpge0d 13006	. . . . . 6 ⊢ (𝜑 → 0 ≤ 𝑁)
126	124, 125	resqrtcld 15391	. . . . 5 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ)
127	122	rpsqrtcld 15385	. . . . . 6 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
128	127	rpne0d 13007	. . . . 5 ⊢ (𝜑 → (√‘𝑁) ≠ 0)
129	123, 126, 128	redivcld 12017	. . . 4 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ)
130	121, 129	remulcld 11211	. . 3 ⊢ (𝜑 → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ∈ ℝ)
131	124	resqcld 14097	. . 3 ⊢ (𝜑 → (𝑁↑2) ∈ ℝ)
132	130, 131	remulcld 11211	. 2 ⊢ (𝜑 → (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) ∈ ℝ)
133		0re 11183	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
134		7re 12286	. . . . . . . . . . . . 13 ⊢ 7 ∈ ℝ
135		9re 12292	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℝ
136		5re 12280	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 ∈ ℝ
137	136, 136	pm3.2i 470	. . . . . . . . . . . . . . . . . 18 ⊢ (5 ∈ ℝ ∧ 5 ∈ ℝ)
138		dp2cl 32807	. . . . . . . . . . . . . . . . . 18 ⊢ ((5 ∈ ℝ ∧ 5 ∈ ℝ) → _55 ∈ ℝ)
139	137, 138	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ _55 ∈ ℝ
140	135, 139	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (9 ∈ ℝ ∧ _55 ∈ ℝ)
141		dp2cl 32807	. . . . . . . . . . . . . . . 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 32807	. . . . . . . . . . . . . 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 32807	. . . . . . . . . . . 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 32807	. . . . . . . . . 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 32818	. . . . . . . . 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 14097	. . . . . 6 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ)
156		1re 11181	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
157	156, 111	pm3.2i 470	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ ∧ 4 ∈ ℝ)
158		dp2cl 32807	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 4 ∈ ℝ) → _14 ∈ ℝ)
159	157, 158	ax-mp 5	. . . . . . . . . 10 ⊢ _14 ∈ ℝ
160	111, 159	pm3.2i 470	. . . . . . . . 9 ⊢ (4 ∈ ℝ ∧ _14 ∈ ℝ)
161		dp2cl 32807	. . . . . . . . 9 ⊢ ((4 ∈ ℝ ∧ _14 ∈ ℝ) → _4_14 ∈ ℝ)
162	160, 161	ax-mp 5	. . . . . . . 8 ⊢ _4_14 ∈ ℝ
163		dpcl 32818	. . . . . . . 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 11211	. . . . 5 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ)
167	36, 47	remulcld 11211	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
168	24, 167	remulcld 11211	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
169	8, 168	fsumrecl 15707	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
170	166, 169	remulcld 11211	. . . 4 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
171	55, 108	remulcld 11211	. . . . 5 ⊢ (𝜑 → (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
172	166, 171	remulcld 11211	. . . 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 34651	. . . 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 12267	. . . . . . . 8 ⊢ 2 ∈ ℝ
178	177	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ∈ ℝ)
179		10nn0 12674	. . . . . . . . . 10 ⊢ ;10 ∈ ℕ₀
180		2nn0 12466	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
181	180, 58	deccl 12671	. . . . . . . . . 10 ⊢ ;27 ∈ ℕ₀
182	179, 181	nn0expcli 14060	. . . . . . . . 9 ⊢ (;10↑;27) ∈ ℕ₀
183	182	nn0rei 12460	. . . . . . . 8 ⊢ (;10↑;27) ∈ ℝ
184	183	a1i 11	. . . . . . 7 ⊢ (𝜑 → (;10↑;27) ∈ ℝ)
185	179	numexp1 17054	. . . . . . . . . 10 ⊢ (;10↑1) = ;10
186	179	nn0rei 12460	. . . . . . . . . 10 ⊢ ;10 ∈ ℝ
187	185, 186	eqeltri 2825	. . . . . . . . 9 ⊢ (;10↑1) ∈ ℝ
188	187	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (;10↑1) ∈ ℝ)
189		1nn 12204	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
190		2lt9 12393	. . . . . . . . . . . 12 ⊢ 2 < 9
191	177, 135, 190	ltleii 11304	. . . . . . . . . . 11 ⊢ 2 ≤ 9
192	189, 57, 180, 191	declei 12692	. . . . . . . . . 10 ⊢ 2 ≤ ;10
193	192, 185	breqtrri 5137	. . . . . . . . 9 ⊢ 2 ≤ (;10↑1)
194	193	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≤ (;10↑1))
195		1z 12570	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
196	181	nn0zi 12565	. . . . . . . . . . . 12 ⊢ ;27 ∈ ℤ
197	186, 195, 196	3pm3.2i 1340	. . . . . . . . . . 11 ⊢ (;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ)
198		1lt10 12795	. . . . . . . . . . 11 ⊢ 1 < ;10
199	197, 198	pm3.2i 470	. . . . . . . . . 10 ⊢ ((;10 ∈ ℝ ∧ 1 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ 1 < ;10)
200		2nn 12266	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
201		1lt9 12394	. . . . . . . . . . . 12 ⊢ 1 < 9
202	156, 135, 201	ltleii 11304	. . . . . . . . . . 11 ⊢ 1 ≤ 9
203	200, 58, 56, 202	declei 12692	. . . . . . . . . 10 ⊢ 1 ≤ ;27
204		leexp2 14143	. . . . . . . . . . 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 11338	. . . . . . 7 ⊢ (𝜑 → 2 ≤ (;10↑;27))
209		hgt750leme.0	. . . . . . 7 ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)
210	178, 184, 124, 208, 209	letrd 11338	. . . . . 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 34655	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
213		2z 12572	. . . . . . . . 9 ⊢ 2 ∈ ℤ
214	213	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℤ)
215	70, 214	rpexpcld 14219	. . . . . . 7 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ⁺)
216	215, 80	rpmulcld 13018	. . . . . 6 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ⁺)
217	169, 171, 216	lemul2d 13046	. . . . 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 11338	. . 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 11209	. . . . . 6 ⊢ (𝜑 → (1._0_7_9_9_55) ∈ ℂ)
221	220	sqcld 14116	. . . . 5 ⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℂ)
222	165	recnd 11209	. . . . 5 ⊢ (𝜑 → (1._4_14) ∈ ℂ)
223	221, 222	mulcld 11201	. . . 4 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℂ)
224		3cn 12274	. . . . 5 ⊢ 3 ∈ ℂ
225	224	a1i 11	. . . 4 ⊢ (𝜑 → 3 ∈ ℂ)
226	108	recnd 11209	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℂ)
227	223, 225, 226	mul12d 11390	. . 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 5136	. 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 13944	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ Fin
230		diffi 9145	. . . . . . . . . . 11 ⊢ ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
231	229, 230	ax-mp 5	. . . . . . . . . 10 ⊢ ((1...𝑁) ∖ ℙ) ∈ Fin
232		snfi 9017	. . . . . . . . . 10 ⊢ {2} ∈ Fin
233		unfi 9141	. . . . . . . . . 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 13523	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ ℕ
238	237	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
239	238	ssdifssd 4113	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ ℕ)
240	200	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℕ)
241	240	snssd 4776	. . . . . . . . . . 11 ⊢ (𝜑 → {2} ⊆ ℕ)
242	239, 241	unssd 4158	. . . . . . . . . 10 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
243	242	sselda 3949	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 𝑖 ∈ ℕ)
244	236, 243	ffvelcdmd 7060	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℝ)
245	235, 244	fsumrecl 15707	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) ∈ ℝ)
246		chpvalz 34626	. . . . . . . . 9 ⊢ (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
247	12, 246	syl 17	. . . . . . . 8 ⊢ (𝜑 → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
248		chpf 27040	. . . . . . . . . 10 ⊢ ψ:ℝ⟶ℝ
249	248	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ψ:ℝ⟶ℝ)
250	249, 124	ffvelcdmd 7060	. . . . . . . 8 ⊢ (𝜑 → (ψ‘𝑁) ∈ ℝ)
251	247, 250	eqeltrrd 2830	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℝ)
252	245, 251	remulcld 11211	. . . . . 6 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ∈ ℝ)
253	123, 252	remulcld 11211	. . . . 5 ⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ∈ ℝ)
254	82, 253	remulcld 11211	. . . 4 ⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ∈ ℝ)
255	55, 254	remulcld 11211	. . 3 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ∈ ℝ)
256	176, 1, 210, 86	hgt750lemb 34654	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
257	108, 253, 216	lemul2d 13046	. . . . 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 12964	. . . . . 6 ⊢ 3 ∈ ℝ⁺
260	259	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℝ⁺)
261	109, 254, 260	lemul2d 13046	. . . 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 12283	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℝ
264	263, 54	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (6 ∈ ℝ ∧ 3 ∈ ℝ)
265		dp2cl 32807	. . . . . . . . . . . . . . . 16 ⊢ ((6 ∈ ℝ ∧ 3 ∈ ℝ) → _63 ∈ ℝ)
266	264, 265	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _63 ∈ ℝ
267	177, 266	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℝ ∧ _63 ∈ ℝ)
268		dp2cl 32807	. . . . . . . . . . . . . 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 32807	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ ∧ _2_63 ∈ ℝ) → _4_2_63 ∈ ℝ)
272	270, 271	ax-mp 5	. . . . . . . . . . 11 ⊢ _4_2_63 ∈ ℝ
273		dpcl 32818	. . . . . . . . . . 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 11211	. . . . . . . 8 ⊢ (𝜑 → ((1._4_2_63) · (√‘𝑁)) ∈ ℝ)
277	112, 54	pm3.2i 470	. . . . . . . . . . . . . . . . . 18 ⊢ (8 ∈ ℝ ∧ 3 ∈ ℝ)
278		dp2cl 32807	. . . . . . . . . . . . . . . . . 18 ⊢ ((8 ∈ ℝ ∧ 3 ∈ ℝ) → _83 ∈ ℝ)
279	277, 278	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ _83 ∈ ℝ
280	112, 279	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (8 ∈ ℝ ∧ _83 ∈ ℝ)
281		dp2cl 32807	. . . . . . . . . . . . . . . 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 32807	. . . . . . . . . . . . . 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 32807	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ _3_8_83 ∈ ℝ) → _0_3_8_83 ∈ ℝ)
288	286, 287	ax-mp 5	. . . . . . . . . . 11 ⊢ _0_3_8_83 ∈ ℝ
289		dpcl 32818	. . . . . . . . . . 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 11211	. . . . . . . 8 ⊢ (𝜑 → ((1._0_3_8_83) · 𝑁) ∈ ℝ)
293	276, 292	remulcld 11211	. . . . . . 7 ⊢ (𝜑 → (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)) ∈ ℝ)
294	123, 293	remulcld 11211	. . . . . 6 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) ∈ ℝ)
295	82, 294	remulcld 11211	. . . . 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 11211	. . . 4 ⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))))) ∈ ℝ)
297		vmage0 27038	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℕ → 0 ≤ (Λ‘𝑖))
298	243, 297	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 0 ≤ (Λ‘𝑖))
299	235, 244, 298	fsumge0 15768	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖))
300	1, 209	hgt750lemd 34646	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) < ((1._4_2_63) · (√‘𝑁)))
301		fzfid 13945	. . . . . . . . . 10 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
302	9	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
303	238	sselda 3949	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
304	302, 303	ffvelcdmd 7060	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
305		vmage0 27038	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → 0 ≤ (Λ‘𝑗))
306	303, 305	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 0 ≤ (Λ‘𝑗))
307	301, 304, 306	fsumge0 15768	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
308	1	hgt750lemc 34645	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) < ((1._0_3_8_83) · 𝑁))
309	245, 276, 251, 292, 299, 300, 307, 308	ltmul12ad 12131	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) < (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))
310	252, 293, 309	ltled 11329	. . . . . . 7 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ≤ (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)))
311	156	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℝ)
312		1lt2 12359	. . . . . . . . . . 11 ⊢ 1 < 2
313	312	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 < 2)
314	311, 178, 124, 313, 210	ltletrd 11341	. . . . . . . . 9 ⊢ (𝜑 → 1 < 𝑁)
315	124, 314	rplogcld 26545	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ⁺)
316	252, 293, 315	lemul2d 13046	. . . . . . 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 13046	. . . . . 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 13046	. . . . 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 14158	. . . . . . . . . 10 ⊢ ((1._0_7_9_9_55)↑2) ∈ ℝ
323	322, 164	remulcli 11197	. . . . . . . . 9 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ
324	274, 290	remulcli 11197	. . . . . . . . 9 ⊢ ((1._4_2_63) · (1._0_3_8_83)) ∈ ℝ
325	323, 324	remulcli 11197	. . . . . . . 8 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) ∈ ℝ
326	54, 325	remulcli 11197	. . . . . . 7 ⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) ∈ ℝ
327		hgt750lem2 34650	. . . . . . 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 11304	. . . . . 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 13019	. . . . . . . 8 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ⁺)
331	122, 214	rpexpcld 14219	. . . . . . . 8 ⊢ (𝜑 → (𝑁↑2) ∈ ℝ⁺)
332	330, 331	rpmulcld 13018	. . . . . . 7 ⊢ (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) ∈ ℝ⁺)
333	329, 121, 332	lemul1d 13045	. . . . . 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 11209	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1._4_2_63) ∈ ℂ)
336	126	recnd 11209	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (√‘𝑁) ∈ ℂ)
337	291	recnd 11209	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1._0_3_8_83) ∈ ℂ)
338	124	recnd 11209	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℂ)
339	335, 336, 337, 338	mul4d 11393	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁)) = (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)))
340	339	oveq2d 7406	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) = ((log‘𝑁) · (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁))))
341	123	recnd 11209	. . . . . . . . . . . . 13 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
342	335, 337	mulcld 11201	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1._4_2_63) · (1._0_3_8_83)) ∈ ℂ)
343	336, 338	mulcld 11201	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((√‘𝑁) · 𝑁) ∈ ℂ)
344	342, 343	mulcld 11201	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((1._4_2_63) · (1._0_3_8_83)) · ((√‘𝑁) · 𝑁)) ∈ ℂ)
345	341, 344	mulcomd 11202	. . . . . . . . . . . 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 2765	. . . . . . . . . . 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 11204	. . . . . . . . . . 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 2765	. . . . . . . . . 10 ⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63) · (√‘𝑁)) · ((1._0_3_8_83) · 𝑁))) = (((1._4_2_63) · (1._0_3_8_83)) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
349	348	oveq2d 7406	. . . . . . . . 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 11209	. . . . . . . . . 10 ⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℂ)
351	343, 341	mulcld 11201	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) ∈ ℂ)
352	350, 342, 351	mulassd 11204	. . . . . . . . 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 2768	. . . . . . . 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 7406	. . . . . . 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 11209	. . . . . . . 8 ⊢ (𝜑 → 3 ∈ ℂ)
356	350, 342	mulcld 11201	. . . . . . . 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 11204	. . . . . . 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 2768	. . . . . 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 11209	. . . . . . . . 9 ⊢ (𝜑 → (𝑁↑2) ∈ ℂ)
360	341, 336, 359, 128	div32d 11988	. . . . . . . 8 ⊢ (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) = ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))))
361	359, 336, 128	divcld 11965	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) ∈ ℂ)
362	341, 361	mulcomd 11202	. . . . . . . 8 ⊢ (𝜑 → ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))) = (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)))
363	338	sqvald 14115	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁↑2) = (𝑁 · 𝑁))
364	363	oveq1d 7405	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((𝑁 · 𝑁) / (√‘𝑁)))
365	338, 338, 336, 128	divassd 12000	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 · 𝑁) / (√‘𝑁)) = (𝑁 · (𝑁 / (√‘𝑁))))
366		divsqrtid 34592	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℝ⁺ → (𝑁 / (√‘𝑁)) = (√‘𝑁))
367	122, 366	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 / (√‘𝑁)) = (√‘𝑁))
368	367	oveq2d 7406	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · (𝑁 / (√‘𝑁))) = (𝑁 · (√‘𝑁)))
369	364, 365, 368	3eqtrd 2769	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = (𝑁 · (√‘𝑁)))
370	338, 336	mulcomd 11202	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 · (√‘𝑁)) = ((√‘𝑁) · 𝑁))
371	369, 370	eqtrd 2765	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((√‘𝑁) · 𝑁))
372	371	oveq1d 7405	. . . . . . . 8 ⊢ (𝜑 → (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)) = (((√‘𝑁) · 𝑁) · (log‘𝑁)))
373	360, 362, 372	3eqtrrd 2770	. . . . . . 7 ⊢ (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) = (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)))
374	373	oveq2d 7406	. . . . . 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 2765	. . . . 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 11209	. . . . . 6 ⊢ (𝜑 → (7._3_48) ∈ ℂ)
377	129	recnd 11209	. . . . . 6 ⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℂ)
378	376, 377, 359	mulassd 11204	. . . . 5 ⊢ (𝜑 → (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) = ((7._3_48) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
379	334, 375, 378	3brtr4d 5142	. . . 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 11338	. . 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 11338	. 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 11338	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 2109 {crab 3408 ∖ cdif 3914 ∪ cun 3915 ∩ cin 3916 ⊆ wss 3917 ifcif 4491 {csn 4592 {cpr 4594 {ctp 4596 class class class wbr 5110 ↦ cmpt 5191 I cid 5535 ↾ cres 5643 ∘ ccom 5645 ⟶wf 6510 ‘cfv 6514 (class class class)co 7390 Fincfn 8921 ℂcc 11073 ℝcr 11074 0cc0 11075 1c1 11076 · cmul 11080 +∞cpnf 11212 < clt 11215 ≤ cle 11216 / cdiv 11842 ℕcn 12193 2c2 12248 3c3 12249 4c4 12250 5c5 12251 6c6 12252 7c7 12253 8c8 12254 9c9 12255 ℕ₀cn0 12449 ℤcz 12536 cdc 12656 ℝ⁺crp 12958 [,)cico 13315 ...cfz 13475 ..^cfzo 13622 ↑cexp 14033 √csqrt 15206 Σcsu 15659 ∥ cdvds 16229 ℙcprime 16648 pmTrspcpmtr 19378 logclog 26470 Λcvma 27009 ψcchp 27010 cdp2 32798 .cdp 32815 reprcrepr 34606

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-reg 9552 ax-inf2 9601 ax-ac2 10423 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153 ax-addf 11154 ax-ros335 34643 ax-ros336 34644

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 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-iin 4961 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-of 7656 df-om 7846 df-1st 7971 df-2nd 7972 df-supp 8143 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-2o 8438 df-oadd 8441 df-er 8674 df-map 8804 df-pm 8805 df-ixp 8874 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-fsupp 9320 df-fi 9369 df-sup 9400 df-inf 9401 df-oi 9470 df-r1 9724 df-rank 9725 df-dju 9861 df-card 9899 df-ac 10076 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-4 12258 df-5 12259 df-6 12260 df-7 12261 df-8 12262 df-9 12263 df-n0 12450 df-xnn0 12523 df-z 12537 df-dec 12657 df-uz 12801 df-q 12915 df-rp 12959 df-xneg 13079 df-xadd 13080 df-xmul 13081 df-ioo 13317 df-ioc 13318 df-ico 13319 df-icc 13320 df-fz 13476 df-fzo 13623 df-fl 13761 df-mod 13839 df-seq 13974 df-exp 14034 df-fac 14246 df-bc 14275 df-hash 14303 df-shft 15040 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-limsup 15444 df-clim 15461 df-rlim 15462 df-sum 15660 df-prod 15877 df-ef 16040 df-sin 16042 df-cos 16043 df-tan 16044 df-pi 16045 df-dvds 16230 df-gcd 16472 df-prm 16649 df-pc 16815 df-struct 17124 df-sets 17141 df-slot 17159 df-ndx 17171 df-base 17187 df-ress 17208 df-plusg 17240 df-mulr 17241 df-starv 17242 df-sca 17243 df-vsca 17244 df-ip 17245 df-tset 17246 df-ple 17247 df-ds 17249 df-unif 17250 df-hom 17251 df-cco 17252 df-rest 17392 df-topn 17393 df-0g 17411 df-gsum 17412 df-topgen 17413 df-pt 17414 df-prds 17417 df-xrs 17472 df-qtop 17477 df-imas 17478 df-xps 17480 df-mre 17554 df-mrc 17555 df-acs 17557 df-mgm 18574 df-sgrp 18653 df-mnd 18669 df-submnd 18718 df-mulg 19007 df-cntz 19256 df-pmtr 19379 df-cmn 19719 df-psmet 21263 df-xmet 21264 df-met 21265 df-bl 21266 df-mopn 21267 df-fbas 21268 df-fg 21269 df-cnfld 21272 df-top 22788 df-topon 22805 df-topsp 22827 df-bases 22840 df-cld 22913 df-ntr 22914 df-cls 22915 df-nei 22992 df-lp 23030 df-perf 23031 df-cn 23121 df-cnp 23122 df-haus 23209 df-cmp 23281 df-tx 23456 df-hmeo 23649 df-fil 23740 df-fm 23832 df-flim 23833 df-flf 23834 df-xms 24215 df-ms 24216 df-tms 24217 df-cncf 24778 df-limc 25774 df-dv 25775 df-ulm 26293 df-log 26472 df-atan 26784 df-cht 27014 df-vma 27015 df-chp 27016 df-dp2 32799 df-dp 32816 df-repr 34607

This theorem is referenced by: tgoldbachgtde 34658

W3C validator