hgt750lema - Mathbox for Thierry Arnoux

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

Theorem hgt750lema 35353

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, 1-Jan-2022.)

**Hypotheses**
Ref	Expression
hgt750leme.o	⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
hgt750leme.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
hgt750lemb.2	⊢ (𝜑 → 2 ≤ 𝑁)
hgt750lemb.a	⊢ 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
hgt750lema.f	⊢ 𝐹 = (𝑑 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ↦ (𝑑 ∘ if(𝑎 = 0, ( I ↾ (0..^3)), ((pmTrsp‘(0..^3))‘{𝑎, 0}))))

**Assertion**
Ref	Expression
hgt750lema	⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))

Distinct variable groups: 𝑧,𝑂 𝐴,𝑐,𝑑,𝑛 𝑁,𝑐,𝑛 𝜑,𝑐,𝑛 𝑛,𝐹 𝑁,𝑎,𝑑,𝑐,𝑛 𝑂,𝑎,𝑐,𝑑,𝑛 𝜑,𝑎,𝑑 Allowed substitution hints: 𝜑(𝑧) 𝐴(𝑧, 𝑎) 𝐹(𝑧, 𝑎, 𝑐, 𝑑) 𝑁(𝑧)

Proof of Theorem hgt750lema Dummy variable 𝑒 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzofi 14141	. . . 4 ⊢ (0..^3) ∈ Fin
2	1	a1i 11	. . 3 ⊢ (𝜑 → (0..^3) ∈ Fin)
3		hgt750leme.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ)
4	3	nnnn0d 12691	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
5		3nn0 12648	. . . . . . 7 ⊢ 3 ∈ ℕ₀
6	5	a1i 11	. . . . . 6 ⊢ (𝜑 → 3 ∈ ℕ₀)
7		ssidd 3936	. . . . . 6 ⊢ (𝜑 → ℕ ⊆ ℕ)
8	4, 6, 7	reprfi2 35319	. . . . 5 ⊢ (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
9		ssrab2 4008	. . . . . 6 ⊢ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁)
10	9	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁))
11	8, 10	ssfid 9285	. . . 4 ⊢ (𝜑 → {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ∈ Fin)
12	11	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ∈ Fin)
13		vmaf 27473	. . . . . 6 ⊢ Λ:ℕ⟶ℝ
14	13	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → Λ:ℕ⟶ℝ)
15		ssidd 3936	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → ℕ ⊆ ℕ)
16	4	nn0zd 12742	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
17	16	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 𝑁 ∈ ℤ)
18	5	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 3 ∈ ℕ₀)
19		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)})
20	9, 19	sselid 3911	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
21	15, 17, 18, 20	reprf 35308	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 𝑛:(0..^3)⟶ℕ)
22		c0ex 11324	. . . . . . . . 9 ⊢ 0 ∈ V
23	22	tpid1 4729	. . . . . . . 8 ⊢ 0 ∈ {0, 1, 2}
24		fzo0to3tp 13911	. . . . . . . 8 ⊢ (0..^3) = {0, 1, 2}
25	23, 24	eleqtrri 2863	. . . . . . 7 ⊢ 0 ∈ (0..^3)
26	25	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 0 ∈ (0..^3))
27	21, 26	ffvelcdmd 7106	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘0) ∈ ℕ)
28	14, 27	ffvelcdmd 7106	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘0)) ∈ ℝ)
29		1eltp012 12437	. . . . . . . . 9 ⊢ 1 ∈ {0, 1, 2}
30	29, 24	eleqtrri 2863	. . . . . . . 8 ⊢ 1 ∈ (0..^3)
31	30	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 1 ∈ (0..^3))
32	21, 31	ffvelcdmd 7106	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘1) ∈ ℕ)
33	14, 32	ffvelcdmd 7106	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘1)) ∈ ℝ)
34		2ex 12444	. . . . . . . . . 10 ⊢ 2 ∈ V
35	34	tpid3 4734	. . . . . . . . 9 ⊢ 2 ∈ {0, 1, 2}
36	35, 24	eleqtrri 2863	. . . . . . . 8 ⊢ 2 ∈ (0..^3)
37	36	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 2 ∈ (0..^3))
38	21, 37	ffvelcdmd 7106	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘2) ∈ ℕ)
39	14, 38	ffvelcdmd 7106	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘2)) ∈ ℝ)
40	33, 39	remulcld 11363	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
41	28, 40	remulcld 11363	. . 3 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
42		vmage0 27475	. . . . 5 ⊢ ((𝑛‘0) ∈ ℕ → 0 ≤ (Λ‘(𝑛‘0)))
43	27, 42	syl 18	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 0 ≤ (Λ‘(𝑛‘0)))
44		vmage0 27475	. . . . . 6 ⊢ ((𝑛‘1) ∈ ℕ → 0 ≤ (Λ‘(𝑛‘1)))
45	32, 44	syl 18	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 0 ≤ (Λ‘(𝑛‘1)))
46		vmage0 27475	. . . . . 6 ⊢ ((𝑛‘2) ∈ ℕ → 0 ≤ (Λ‘(𝑛‘2)))
47	38, 46	syl 18	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 0 ≤ (Λ‘(𝑛‘2)))
48	33, 39, 45, 47	mulge0d 11917	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 0 ≤ ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))
49	28, 40, 43, 48	mulge0d 11917	. . 3 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 0 ≤ ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))
50	2, 12, 41, 49	fsumiunle 33487	. 2 ⊢ (𝜑 → Σ𝑛 ∈ ∪ 𝑎 ∈ (0..^3){𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ Σ𝑎 ∈ (0..^3)Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))
51		eqid 2763	. . . 4 ⊢ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}
52		inss2 4137	. . . . . 6 ⊢ (𝑂 ∩ ℙ) ⊆ ℙ
53		prmssnn 16877	. . . . . 6 ⊢ ℙ ⊆ ℕ
54	52, 53	sstri 3922	. . . . 5 ⊢ (𝑂 ∩ ℙ) ⊆ ℕ
55	54	a1i 11	. . . 4 ⊢ (𝜑 → (𝑂 ∩ ℙ) ⊆ ℕ)
56	51, 7, 55, 4, 6	reprdifc 35323	. . 3 ⊢ (𝜑 → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) = ∪ 𝑎 ∈ (0..^3){𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)})
57	56	sumeq1d 15893	. 2 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) = Σ𝑛 ∈ ∪ 𝑎 ∈ (0..^3){𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))
58		ssrab2 4008	. . . . . . . 8 ⊢ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁)
59	58	a1i 11	. . . . . . 7 ⊢ (𝜑 → {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁))
60	8, 59	ssfid 9285	. . . . . 6 ⊢ (𝜑 → {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ∈ Fin)
61	13	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → Λ:ℕ⟶ℝ)
62		ssidd 3936	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → ℕ ⊆ ℕ)
63	16	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑁 ∈ ℤ)
64	5	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → 3 ∈ ℕ₀)
65	59	sselda 3913	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
66	62, 63, 64, 65	reprf 35308	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛:(0..^3)⟶ℕ)
67	25	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → 0 ∈ (0..^3))
68	66, 67	ffvelcdmd 7106	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘0) ∈ ℕ)
69	61, 68	ffvelcdmd 7106	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘0)) ∈ ℝ)
70	30	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → 1 ∈ (0..^3))
71	66, 70	ffvelcdmd 7106	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘1) ∈ ℕ)
72	61, 71	ffvelcdmd 7106	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘1)) ∈ ℝ)
73	36	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → 2 ∈ (0..^3))
74	66, 73	ffvelcdmd 7106	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘2) ∈ ℕ)
75	61, 74	ffvelcdmd 7106	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘2)) ∈ ℝ)
76	72, 75	remulcld 11363	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
77	69, 76	remulcld 11363	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
78	60, 77	fsumrecl 15926	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
79	78	recnd 11361	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℂ)
80		fsumconst 15982	. . . 4 ⊢ (((0..^3) ∈ Fin ∧ Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℂ) → Σ𝑎 ∈ (0..^3)Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) = ((♯‘(0..^3)) · Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
81	2, 79, 80	syl2anc 596	. . 3 ⊢ (𝜑 → Σ𝑎 ∈ (0..^3)Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) = ((♯‘(0..^3)) · Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
82		fveq1 6904	. . . . . . . 8 ⊢ (𝑛 = (𝐹‘𝑒) → (𝑛‘0) = ((𝐹‘𝑒)‘0))
83	82	fveq2d 6909	. . . . . . 7 ⊢ (𝑛 = (𝐹‘𝑒) → (Λ‘(𝑛‘0)) = (Λ‘((𝐹‘𝑒)‘0)))
84		fveq1 6904	. . . . . . . . 9 ⊢ (𝑛 = (𝐹‘𝑒) → (𝑛‘1) = ((𝐹‘𝑒)‘1))
85	84	fveq2d 6909	. . . . . . . 8 ⊢ (𝑛 = (𝐹‘𝑒) → (Λ‘(𝑛‘1)) = (Λ‘((𝐹‘𝑒)‘1)))
86		fveq1 6904	. . . . . . . . 9 ⊢ (𝑛 = (𝐹‘𝑒) → (𝑛‘2) = ((𝐹‘𝑒)‘2))
87	86	fveq2d 6909	. . . . . . . 8 ⊢ (𝑛 = (𝐹‘𝑒) → (Λ‘(𝑛‘2)) = (Λ‘((𝐹‘𝑒)‘2)))
88	85, 87	oveq12d 7458	. . . . . . 7 ⊢ (𝑛 = (𝐹‘𝑒) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) = ((Λ‘((𝐹‘𝑒)‘1)) · (Λ‘((𝐹‘𝑒)‘2))))
89	83, 88	oveq12d 7458	. . . . . 6 ⊢ (𝑛 = (𝐹‘𝑒) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) = ((Λ‘((𝐹‘𝑒)‘0)) · ((Λ‘((𝐹‘𝑒)‘1)) · (Λ‘((𝐹‘𝑒)‘2)))))
90		3nn 12446	. . . . . . . . . 10 ⊢ 3 ∈ ℕ
91	90	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 3 ∈ ℕ)
92	91	ralrimivw 3162	. . . . . . . 8 ⊢ (𝜑 → ∀𝑎 ∈ (0..^3)3 ∈ ℕ)
93	92	r19.21bi 3258	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → 3 ∈ ℕ)
94	16	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → 𝑁 ∈ ℤ)
95		ssidd 3936	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → ℕ ⊆ ℕ)
96		simpr 490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → 𝑎 ∈ (0..^3))
97		fveq1 6904	. . . . . . . . . 10 ⊢ (𝑐 = 𝑑 → (𝑐‘0) = (𝑑‘0))
98	97	eleq1d 2849	. . . . . . . . 9 ⊢ (𝑐 = 𝑑 → ((𝑐‘0) ∈ (𝑂 ∩ ℙ) ↔ (𝑑‘0) ∈ (𝑂 ∩ ℙ)))
99	98	notbid 321	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ) ↔ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)))
100	99	cbvrabv 3426	. . . . . . 7 ⊢ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} = {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}
101		fveq1 6904	. . . . . . . . . 10 ⊢ (𝑐 = 𝑑 → (𝑐‘𝑎) = (𝑑‘𝑎))
102	101	eleq1d 2849	. . . . . . . . 9 ⊢ (𝑐 = 𝑑 → ((𝑐‘𝑎) ∈ (𝑂 ∩ ℙ) ↔ (𝑑‘𝑎) ∈ (𝑂 ∩ ℙ)))
103	102	notbid 321	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ) ↔ ¬ (𝑑‘𝑎) ∈ (𝑂 ∩ ℙ)))
104	103	cbvrabv 3426	. . . . . . 7 ⊢ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} = {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘𝑎) ∈ (𝑂 ∩ ℙ)}
105		eqid 2763	. . . . . . 7 ⊢ if(𝑎 = 0, ( I ↾ (0..^3)), ((pmTrsp‘(0..^3))‘{𝑎, 0})) = if(𝑎 = 0, ( I ↾ (0..^3)), ((pmTrsp‘(0..^3))‘{𝑎, 0}))
106		hgt750lema.f	. . . . . . 7 ⊢ 𝐹 = (𝑑 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ↦ (𝑑 ∘ if(𝑎 = 0, ( I ↾ (0..^3)), ((pmTrsp‘(0..^3))‘{𝑎, 0}))))
107	93, 94, 95, 96, 100, 104, 105, 106	reprpmtf1o 35322	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → 𝐹:{𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}⟶1-1onto{𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)})
108		eqidd 2764	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → (𝐹‘𝑒) = (𝐹‘𝑒))
109	77	adantlr 728	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
110	109	recnd 11361	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℂ)
111	89, 12, 107, 108, 110	fsumf1o 15915	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) = Σ𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘((𝐹‘𝑒)‘0)) · ((Λ‘((𝐹‘𝑒)‘1)) · (Λ‘((𝐹‘𝑒)‘2)))))
112		fveq2 6905	. . . . . . . . . 10 ⊢ (𝑒 = 𝑛 → (𝐹‘𝑒) = (𝐹‘𝑛))
113	112	fveq1d 6907	. . . . . . . . 9 ⊢ (𝑒 = 𝑛 → ((𝐹‘𝑒)‘0) = ((𝐹‘𝑛)‘0))
114	113	fveq2d 6909	. . . . . . . 8 ⊢ (𝑒 = 𝑛 → (Λ‘((𝐹‘𝑒)‘0)) = (Λ‘((𝐹‘𝑛)‘0)))
115	112	fveq1d 6907	. . . . . . . . . 10 ⊢ (𝑒 = 𝑛 → ((𝐹‘𝑒)‘1) = ((𝐹‘𝑛)‘1))
116	115	fveq2d 6909	. . . . . . . . 9 ⊢ (𝑒 = 𝑛 → (Λ‘((𝐹‘𝑒)‘1)) = (Λ‘((𝐹‘𝑛)‘1)))
117	112	fveq1d 6907	. . . . . . . . . 10 ⊢ (𝑒 = 𝑛 → ((𝐹‘𝑒)‘2) = ((𝐹‘𝑛)‘2))
118	117	fveq2d 6909	. . . . . . . . 9 ⊢ (𝑒 = 𝑛 → (Λ‘((𝐹‘𝑒)‘2)) = (Λ‘((𝐹‘𝑛)‘2)))
119	116, 118	oveq12d 7458	. . . . . . . 8 ⊢ (𝑒 = 𝑛 → ((Λ‘((𝐹‘𝑒)‘1)) · (Λ‘((𝐹‘𝑒)‘2))) = ((Λ‘((𝐹‘𝑛)‘1)) · (Λ‘((𝐹‘𝑛)‘2))))
120	114, 119	oveq12d 7458	. . . . . . 7 ⊢ (𝑒 = 𝑛 → ((Λ‘((𝐹‘𝑒)‘0)) · ((Λ‘((𝐹‘𝑒)‘1)) · (Λ‘((𝐹‘𝑒)‘2)))) = ((Λ‘((𝐹‘𝑛)‘0)) · ((Λ‘((𝐹‘𝑛)‘1)) · (Λ‘((𝐹‘𝑛)‘2)))))
121	120	cbvsumv 15889	. . . . . 6 ⊢ Σ𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘((𝐹‘𝑒)‘0)) · ((Λ‘((𝐹‘𝑒)‘1)) · (Λ‘((𝐹‘𝑒)‘2)))) = Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘((𝐹‘𝑛)‘0)) · ((Λ‘((𝐹‘𝑛)‘1)) · (Λ‘((𝐹‘𝑛)‘2))))
122	121	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → Σ𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘((𝐹‘𝑒)‘0)) · ((Λ‘((𝐹‘𝑒)‘1)) · (Λ‘((𝐹‘𝑒)‘2)))) = Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘((𝐹‘𝑛)‘0)) · ((Λ‘((𝐹‘𝑛)‘1)) · (Λ‘((𝐹‘𝑛)‘2)))))
123		ovexd 7475	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → (0..^3) ∈ V)
124	96	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 𝑎 ∈ (0..^3))
125	123, 124, 26, 105	pmtridf1o 33722	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → if(𝑎 = 0, ( I ↾ (0..^3)), ((pmTrsp‘(0..^3))‘{𝑎, 0})):(0..^3)⟶1-1onto(0..^3))
126	106, 125, 21, 14, 19	hgt750lemg 35350	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘((𝐹‘𝑛)‘0)) · ((Λ‘((𝐹‘𝑛)‘1)) · (Λ‘((𝐹‘𝑛)‘2)))) = ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))
127	126	sumeq2dv 15895	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘((𝐹‘𝑛)‘0)) · ((Λ‘((𝐹‘𝑛)‘1)) · (Λ‘((𝐹‘𝑛)‘2)))) = Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))
128	111, 122, 127	3eqtrrd 2803	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) = Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))
129	128	sumeq2dv 15895	. . 3 ⊢ (𝜑 → Σ𝑎 ∈ (0..^3)Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) = Σ𝑎 ∈ (0..^3)Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))
130		hashfzo0 14599	. . . . . . 7 ⊢ (3 ∈ ℕ₀ → (♯‘(0..^3)) = 3)
131	5, 130	ax-mp 5	. . . . . 6 ⊢ (♯‘(0..^3)) = 3
132	131	a1i 11	. . . . 5 ⊢ (𝜑 → (♯‘(0..^3)) = 3)
133	132	eqcomd 2769	. . . 4 ⊢ (𝜑 → 3 = (♯‘(0..^3)))
134		hgt750lemb.a	. . . . . 6 ⊢ 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
135	134	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)})
136	135	sumeq1d 15893	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) = Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))
137	133, 136	oveq12d 7458	. . 3 ⊢ (𝜑 → (3 · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) = ((♯‘(0..^3)) · Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
138	81, 129, 137	3eqtr4rd 2809	. 2 ⊢ (𝜑 → (3 · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) = Σ𝑎 ∈ (0..^3)Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))
139	50, 57, 138	3brtr4d 5140	1 ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2147 {crab 3416 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ∩ cin 4092 ifcif 4485 {cpr 4590 {ctp 4592 ∪ ciun 4954 class class class wbr 5106 ↦ cmpt 5189 I cid 5549 ↾ cres 5657 ∘ ccom 5659 ⟶wf 6551 ‘cfv 6555 (class class class)co 7440 Fincfn 8998 ℂcc 11222 ℝcr 11223 0cc0 11224 1c1 11225 · cmul 11229 ≤ cle 11368 ℕcn 12359 2c2 12421 3c3 12422 ℕ₀cn0 12630 ℤcz 12717 ..^cfzo 13812 ♯chash 14498 Σcsu 15879 ∥ cdvds 16448 ℙcprime 16872 pmTrspcpmtr 19682 Λcvma 27446 reprcrepr 35304

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

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

This theorem is used by: hgt750leme 35354

W3C validator