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