Metamath Proof Explorer

Theorem hgt750lema

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)

Ref Expression
Hypotheses hgt750leme.o ⊢ O = z ∈ ℤ | ¬ 2 ∥ z
hgt750leme.n ⊢ φ → N ∈ ℕ
hgt750lemb.2 ⊢ φ → 2 ≤ N
hgt750lemb.a ⊢ A = c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ
hgt750lema.f ⊢ F = d ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ ⟼ d ∘ if a = 0 I ↾ 0 ..^ 3 pmTrsp ⁡ 0 ..^ 3 ⁡ a 0
Assertion hgt750lema ⊢ φ → ∑ n ∈ ℕ repr ⁡ 3 N ∖ O ∩ ℙ repr ⁡ 3 N Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ≤ 3 ⁢ ∑ n ∈ A Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2

Proof

Step Hyp Ref Expression
1 hgt750leme.o ⊢ O = z ∈ ℤ | ¬ 2 ∥ z
2 hgt750leme.n ⊢ φ → N ∈ ℕ
3 hgt750lemb.2 ⊢ φ → 2 ≤ N
4 hgt750lemb.a ⊢ A = c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ
5 hgt750lema.f ⊢ F = d ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ ⟼ d ∘ if a = 0 I ↾ 0 ..^ 3 pmTrsp ⁡ 0 ..^ 3 ⁡ a 0
6 fzofi ⊢ 0 ..^ 3 ∈ Fin
7 6 a1i ⊢ φ → 0 ..^ 3 ∈ Fin
8 2 nnnn0d ⊢ φ → N ∈ ℕ 0
9 3nn0 ⊢ 3 ∈ ℕ 0
10 9 a1i ⊢ φ → 3 ∈ ℕ 0
11 ssidd ⊢ φ → ℕ ⊆ ℕ
12 8 10 11 reprfi2 ⊢ φ → ℕ repr ⁡ 3 N ∈ Fin
13 ssrab2 ⊢ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ ⊆ ℕ repr ⁡ 3 N
14 13 a1i ⊢ φ → c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ ⊆ ℕ repr ⁡ 3 N
15 12 14 ssfid ⊢ φ → c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ ∈ Fin
16 15 adantr ⊢ φ ∧ a ∈ 0 ..^ 3 → c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ ∈ Fin
17 vmaf ⊢ Λ : ℕ ⟶ ℝ
18 17 a1i ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → Λ : ℕ ⟶ ℝ
19 ssidd ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → ℕ ⊆ ℕ
20 8 nn0zd ⊢ φ → N ∈ ℤ
21 20 ad2antrr ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → N ∈ ℤ
22 9 a1i ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → 3 ∈ ℕ 0
23 simpr ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ
24 13 23 sselid ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → n ∈ ℕ repr ⁡ 3 N
25 19 21 22 24 reprf ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → n : 0 ..^ 3 ⟶ ℕ
26 c0ex ⊢ 0 ∈ V
27 26 tpid1 ⊢ 0 ∈ 0 1 2
28 fzo0to3tp ⊢ 0 ..^ 3 = 0 1 2
29 27 28 eleqtrri ⊢ 0 ∈ 0 ..^ 3
30 29 a1i ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → 0 ∈ 0 ..^ 3
31 25 30 ffvelcdmd ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → n ⁡ 0 ∈ ℕ
32 18 31 ffvelcdmd ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → Λ ⁡ n ⁡ 0 ∈ ℝ
33 1eltp012 ⊢ 1 ∈ 0 1 2
34 33 28 eleqtrri ⊢ 1 ∈ 0 ..^ 3
35 34 a1i ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → 1 ∈ 0 ..^ 3
36 25 35 ffvelcdmd ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → n ⁡ 1 ∈ ℕ
37 18 36 ffvelcdmd ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → Λ ⁡ n ⁡ 1 ∈ ℝ
38 2ex ⊢ 2 ∈ V
39 38 tpid3 ⊢ 2 ∈ 0 1 2
40 39 28 eleqtrri ⊢ 2 ∈ 0 ..^ 3
41 40 a1i ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → 2 ∈ 0 ..^ 3
42 25 41 ffvelcdmd ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → n ⁡ 2 ∈ ℕ
43 18 42 ffvelcdmd ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → Λ ⁡ n ⁡ 2 ∈ ℝ
44 37 43 remulcld ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ∈ ℝ
45 32 44 remulcld ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ∈ ℝ
46 vmage0 ⊢ n ⁡ 0 ∈ ℕ → 0 ≤ Λ ⁡ n ⁡ 0
47 31 46 syl ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → 0 ≤ Λ ⁡ n ⁡ 0
48 vmage0 ⊢ n ⁡ 1 ∈ ℕ → 0 ≤ Λ ⁡ n ⁡ 1
49 36 48 syl ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → 0 ≤ Λ ⁡ n ⁡ 1
50 vmage0 ⊢ n ⁡ 2 ∈ ℕ → 0 ≤ Λ ⁡ n ⁡ 2
51 42 50 syl ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → 0 ≤ Λ ⁡ n ⁡ 2
52 37 43 49 51 mulge0d ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → 0 ≤ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2
53 32 44 47 52 mulge0d ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → 0 ≤ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2
54 7 16 45 53 fsumiunle ⊢ φ → ∑ n ∈ ⋃ a ∈ 0 ..^ 3 c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ≤ ∑ a ∈ 0 ..^ 3 ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2
55 eqid ⊢ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ = c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ
56 inss2 ⊢ O ∩ ℙ ⊆ ℙ
57 prmssnn ⊢ ℙ ⊆ ℕ
58 56 57 sstri ⊢ O ∩ ℙ ⊆ ℕ
59 58 a1i ⊢ φ → O ∩ ℙ ⊆ ℕ
60 55 11 59 8 10 reprdifc ⊢ φ → ℕ repr ⁡ 3 N ∖ O ∩ ℙ repr ⁡ 3 N = ⋃ a ∈ 0 ..^ 3 c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ
61 60 sumeq1d ⊢ φ → ∑ n ∈ ℕ repr ⁡ 3 N ∖ O ∩ ℙ repr ⁡ 3 N Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 = ∑ n ∈ ⋃ a ∈ 0 ..^ 3 c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2
62 ssrab2 ⊢ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ ⊆ ℕ repr ⁡ 3 N
63 62 a1i ⊢ φ → c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ ⊆ ℕ repr ⁡ 3 N
64 12 63 ssfid ⊢ φ → c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ ∈ Fin
65 17 a1i ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → Λ : ℕ ⟶ ℝ
66 ssidd ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → ℕ ⊆ ℕ
67 20 adantr ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → N ∈ ℤ
68 9 a1i ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → 3 ∈ ℕ 0
69 63 sselda ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → n ∈ ℕ repr ⁡ 3 N
70 66 67 68 69 reprf ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → n : 0 ..^ 3 ⟶ ℕ
71 29 a1i ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → 0 ∈ 0 ..^ 3
72 70 71 ffvelcdmd ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → n ⁡ 0 ∈ ℕ
73 65 72 ffvelcdmd ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → Λ ⁡ n ⁡ 0 ∈ ℝ
74 34 a1i ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → 1 ∈ 0 ..^ 3
75 70 74 ffvelcdmd ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → n ⁡ 1 ∈ ℕ
76 65 75 ffvelcdmd ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → Λ ⁡ n ⁡ 1 ∈ ℝ
77 40 a1i ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → 2 ∈ 0 ..^ 3
78 70 77 ffvelcdmd ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → n ⁡ 2 ∈ ℕ
79 65 78 ffvelcdmd ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → Λ ⁡ n ⁡ 2 ∈ ℝ
80 76 79 remulcld ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ∈ ℝ
81 73 80 remulcld ⊢ φ ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ∈ ℝ
82 64 81 fsumrecl ⊢ φ → ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ∈ ℝ
83 82 recnd ⊢ φ → ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ∈ ℂ
84 fsumconst ⊢ 0 ..^ 3 ∈ Fin ∧ ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ∈ ℂ → ∑ a ∈ 0 ..^ 3 ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 = 0 ..^ 3 ⁢ ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2
85 7 83 84 syl2anc ⊢ φ → ∑ a ∈ 0 ..^ 3 ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 = 0 ..^ 3 ⁢ ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2
86 fveq1 ⊢ n = F ⁡ e → n ⁡ 0 = F ⁡ e ⁡ 0
87 86 fveq2d ⊢ n = F ⁡ e → Λ ⁡ n ⁡ 0 = Λ ⁡ F ⁡ e ⁡ 0
88 fveq1 ⊢ n = F ⁡ e → n ⁡ 1 = F ⁡ e ⁡ 1
89 88 fveq2d ⊢ n = F ⁡ e → Λ ⁡ n ⁡ 1 = Λ ⁡ F ⁡ e ⁡ 1
90 fveq1 ⊢ n = F ⁡ e → n ⁡ 2 = F ⁡ e ⁡ 2
91 90 fveq2d ⊢ n = F ⁡ e → Λ ⁡ n ⁡ 2 = Λ ⁡ F ⁡ e ⁡ 2
92 89 91 oveq12d ⊢ n = F ⁡ e → Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 = Λ ⁡ F ⁡ e ⁡ 1 ⁢ Λ ⁡ F ⁡ e ⁡ 2
93 87 92 oveq12d ⊢ n = F ⁡ e → Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 = Λ ⁡ F ⁡ e ⁡ 0 ⁢ Λ ⁡ F ⁡ e ⁡ 1 ⁢ Λ ⁡ F ⁡ e ⁡ 2
94 3nn ⊢ 3 ∈ ℕ
95 94 a1i ⊢ φ → 3 ∈ ℕ
96 95 ralrimivw ⊢ φ → ∀ a ∈ 0 ..^ 3 3 ∈ ℕ
97 96 r19.21bi ⊢ φ ∧ a ∈ 0 ..^ 3 → 3 ∈ ℕ
98 20 adantr ⊢ φ ∧ a ∈ 0 ..^ 3 → N ∈ ℤ
99 ssidd ⊢ φ ∧ a ∈ 0 ..^ 3 → ℕ ⊆ ℕ
100 simpr ⊢ φ ∧ a ∈ 0 ..^ 3 → a ∈ 0 ..^ 3
101 fveq1 ⊢ c = d → c ⁡ 0 = d ⁡ 0
102 101 eleq1d ⊢ c = d → c ⁡ 0 ∈ O ∩ ℙ ↔ d ⁡ 0 ∈ O ∩ ℙ
103 102 notbid ⊢ c = d → ¬ c ⁡ 0 ∈ O ∩ ℙ ↔ ¬ d ⁡ 0 ∈ O ∩ ℙ
104 103 cbvrabv ⊢ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ = d ∈ ℕ repr ⁡ 3 N | ¬ d ⁡ 0 ∈ O ∩ ℙ
105 fveq1 ⊢ c = d → c ⁡ a = d ⁡ a
106 105 eleq1d ⊢ c = d → c ⁡ a ∈ O ∩ ℙ ↔ d ⁡ a ∈ O ∩ ℙ
107 106 notbid ⊢ c = d → ¬ c ⁡ a ∈ O ∩ ℙ ↔ ¬ d ⁡ a ∈ O ∩ ℙ
108 107 cbvrabv ⊢ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ = d ∈ ℕ repr ⁡ 3 N | ¬ d ⁡ a ∈ O ∩ ℙ
109 eqid ⊢ if a = 0 I ↾ 0 ..^ 3 pmTrsp ⁡ 0 ..^ 3 ⁡ a 0 = if a = 0 I ↾ 0 ..^ 3 pmTrsp ⁡ 0 ..^ 3 ⁡ a 0
110 97 98 99 100 104 108 109 5 reprpmtf1o ⊢ φ ∧ a ∈ 0 ..^ 3 → F : c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ ⟶ 1-1 onto c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ
111 eqidd ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ e ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → F ⁡ e = F ⁡ e
112 81 adantlr ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ∈ ℝ
113 112 recnd ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ → Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ∈ ℂ
114 93 16 110 111 113 fsumf1o ⊢ φ ∧ a ∈ 0 ..^ 3 → ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 = ∑ e ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ Λ ⁡ F ⁡ e ⁡ 0 ⁢ Λ ⁡ F ⁡ e ⁡ 1 ⁢ Λ ⁡ F ⁡ e ⁡ 2
115 fveq2 ⊢ e = n → F ⁡ e = F ⁡ n
116 115 fveq1d ⊢ e = n → F ⁡ e ⁡ 0 = F ⁡ n ⁡ 0
117 116 fveq2d ⊢ e = n → Λ ⁡ F ⁡ e ⁡ 0 = Λ ⁡ F ⁡ n ⁡ 0
118 115 fveq1d ⊢ e = n → F ⁡ e ⁡ 1 = F ⁡ n ⁡ 1
119 118 fveq2d ⊢ e = n → Λ ⁡ F ⁡ e ⁡ 1 = Λ ⁡ F ⁡ n ⁡ 1
120 115 fveq1d ⊢ e = n → F ⁡ e ⁡ 2 = F ⁡ n ⁡ 2
121 120 fveq2d ⊢ e = n → Λ ⁡ F ⁡ e ⁡ 2 = Λ ⁡ F ⁡ n ⁡ 2
122 119 121 oveq12d ⊢ e = n → Λ ⁡ F ⁡ e ⁡ 1 ⁢ Λ ⁡ F ⁡ e ⁡ 2 = Λ ⁡ F ⁡ n ⁡ 1 ⁢ Λ ⁡ F ⁡ n ⁡ 2
123 117 122 oveq12d ⊢ e = n → Λ ⁡ F ⁡ e ⁡ 0 ⁢ Λ ⁡ F ⁡ e ⁡ 1 ⁢ Λ ⁡ F ⁡ e ⁡ 2 = Λ ⁡ F ⁡ n ⁡ 0 ⁢ Λ ⁡ F ⁡ n ⁡ 1 ⁢ Λ ⁡ F ⁡ n ⁡ 2
124 123 cbvsumv ⊢ ∑ e ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ Λ ⁡ F ⁡ e ⁡ 0 ⁢ Λ ⁡ F ⁡ e ⁡ 1 ⁢ Λ ⁡ F ⁡ e ⁡ 2 = ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ Λ ⁡ F ⁡ n ⁡ 0 ⁢ Λ ⁡ F ⁡ n ⁡ 1 ⁢ Λ ⁡ F ⁡ n ⁡ 2
125 124 a1i ⊢ φ ∧ a ∈ 0 ..^ 3 → ∑ e ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ Λ ⁡ F ⁡ e ⁡ 0 ⁢ Λ ⁡ F ⁡ e ⁡ 1 ⁢ Λ ⁡ F ⁡ e ⁡ 2 = ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ Λ ⁡ F ⁡ n ⁡ 0 ⁢ Λ ⁡ F ⁡ n ⁡ 1 ⁢ Λ ⁡ F ⁡ n ⁡ 2
126 ovexd ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → 0 ..^ 3 ∈ V
127 100 adantr ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → a ∈ 0 ..^ 3
128 126 127 30 109 pmtridf1o ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → if a = 0 I ↾ 0 ..^ 3 pmTrsp ⁡ 0 ..^ 3 ⁡ a 0 : 0 ..^ 3 ⟶ 1-1 onto 0 ..^ 3
129 5 128 25 18 23 hgt750lemg ⊢ φ ∧ a ∈ 0 ..^ 3 ∧ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ → Λ ⁡ F ⁡ n ⁡ 0 ⁢ Λ ⁡ F ⁡ n ⁡ 1 ⁢ Λ ⁡ F ⁡ n ⁡ 2 = Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2
130 129 sumeq2dv ⊢ φ ∧ a ∈ 0 ..^ 3 → ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ Λ ⁡ F ⁡ n ⁡ 0 ⁢ Λ ⁡ F ⁡ n ⁡ 1 ⁢ Λ ⁡ F ⁡ n ⁡ 2 = ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2
131 114 125 130 3eqtrrd ⊢ φ ∧ a ∈ 0 ..^ 3 → ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 = ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2
132 131 sumeq2dv ⊢ φ → ∑ a ∈ 0 ..^ 3 ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 = ∑ a ∈ 0 ..^ 3 ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2
133 hashfzo0 ⊢ 3 ∈ ℕ 0 → 0 ..^ 3 = 3
134 9 133 ax-mp ⊢ 0 ..^ 3 = 3
135 134 a1i ⊢ φ → 0 ..^ 3 = 3
136 135 eqcomd ⊢ φ → 3 = 0 ..^ 3
137 4 a1i ⊢ φ → A = c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ
138 137 sumeq1d ⊢ φ → ∑ n ∈ A Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 = ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2
139 136 138 oveq12d ⊢ φ → 3 ⁢ ∑ n ∈ A Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 = 0 ..^ 3 ⁢ ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ 0 ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2
140 85 132 139 3eqtr4rd ⊢ φ → 3 ⁢ ∑ n ∈ A Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 = ∑ a ∈ 0 ..^ 3 ∑ n ∈ c ∈ ℕ repr ⁡ 3 N | ¬ c ⁡ a ∈ O ∩ ℙ Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2
141 54 61 140 3brtr4d ⊢ φ → ∑ n ∈ ℕ repr ⁡ 3 N ∖ O ∩ ℙ repr ⁡ 3 N Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ≤ 3 ⁢ ∑ n ∈ A Λ ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2