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⁡3N|¬c⁡0∈O∩ℙ
hgt750lema.f ⊢F=d∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ⟼d∘ifa=0I↾0..^3pmTrsp⁡0..^3⁡a0
Assertion hgt750lema ⊢φ→∑n∈ℕrepr⁡3N∖O∩ℙrepr⁡3NΛ⁡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⁡3N|¬c⁡0∈O∩ℙ
5 hgt750lema.f ⊢F=d∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ⟼d∘ifa=0I↾0..^3pmTrsp⁡0..^3⁡a0
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⁡3N∈Fin
13 ssrab2 ⊢c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ⊆ℕrepr⁡3N
14 13 a1i ⊢φ→c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ⊆ℕrepr⁡3N
15 12 14 ssfid ⊢φ→c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ∈Fin
16 15 adantr ⊢φ∧a∈0..^3→c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ∈Fin
17 vmaf ⊢Λ:ℕ⟶ℝ
18 17 a1i ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→Λ:ℕ⟶ℝ
19 ssidd ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→ℕ⊆ℕ
20 8 nn0zd ⊢φ→N∈ℤ
21 20 ad2antrr ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→N∈ℤ
22 9 a1i ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→3∈ℕ0
23 simpr ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ
24 13 23 sselid ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→n∈ℕrepr⁡3N
25 19 21 22 24 reprf ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→n:0..^3⟶ℕ
26 c0ex ⊢0∈V
27 26 tpid1 ⊢0∈012
28 fzo0to3tp ⊢0..^3=012
29 27 28 eleqtrri ⊢0∈0..^3
30 29 a1i ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→0∈0..^3
31 25 30 ffvelcdmd ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→n⁡0∈ℕ
32 18 31 ffvelcdmd ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→Λ⁡n⁡0∈ℝ
33 1ex ⊢1∈V
34 33 tpid2 ⊢1∈012
35 34 28 eleqtrri ⊢1∈0..^3
36 35 a1i ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→1∈0..^3
37 25 36 ffvelcdmd ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→n⁡1∈ℕ
38 18 37 ffvelcdmd ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→Λ⁡n⁡1∈ℝ
39 2ex ⊢2∈V
40 39 tpid3 ⊢2∈012
41 40 28 eleqtrri ⊢2∈0..^3
42 41 a1i ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→2∈0..^3
43 25 42 ffvelcdmd ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→n⁡2∈ℕ
44 18 43 ffvelcdmd ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→Λ⁡n⁡2∈ℝ
45 38 44 remulcld ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→Λ⁡n⁡1⁢Λ⁡n⁡2∈ℝ
46 32 45 remulcld ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬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⁡3N|¬c⁡a∈O∩ℙ→0≤Λ⁡n⁡0
49 vmage0 ⊢n⁡1∈ℕ→0≤Λ⁡n⁡1
50 37 49 syl ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→0≤Λ⁡n⁡1
51 vmage0 ⊢n⁡2∈ℕ→0≤Λ⁡n⁡2
52 43 51 syl ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→0≤Λ⁡n⁡2
53 38 44 50 52 mulge0d ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→0≤Λ⁡n⁡1⁢Λ⁡n⁡2
54 32 45 48 53 mulge0d ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→0≤Λ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2
55 7 16 46 54 fsumiunle ⊢φ→∑n∈⋃a∈0..^3c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2≤∑a∈0..^3∑n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2
56 eqid ⊢c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ=c∈ℕrepr⁡3N|¬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⁡3N∖O∩ℙrepr⁡3N=⋃a∈0..^3c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ
62 61 sumeq1d ⊢φ→∑n∈ℕrepr⁡3N∖O∩ℙrepr⁡3NΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2=∑n∈⋃a∈0..^3c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2
63 ssrab2 ⊢c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ⊆ℕrepr⁡3N
64 63 a1i ⊢φ→c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ⊆ℕrepr⁡3N
65 12 64 ssfid ⊢φ→c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ∈Fin
66 17 a1i ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→Λ:ℕ⟶ℝ
67 ssidd ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→ℕ⊆ℕ
68 20 adantr ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→N∈ℤ
69 9 a1i ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→3∈ℕ0
70 64 sselda ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→n∈ℕrepr⁡3N
71 67 68 69 70 reprf ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→n:0..^3⟶ℕ
72 29 a1i ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→0∈0..^3
73 71 72 ffvelcdmd ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→n⁡0∈ℕ
74 66 73 ffvelcdmd ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→Λ⁡n⁡0∈ℝ
75 35 a1i ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→1∈0..^3
76 71 75 ffvelcdmd ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→n⁡1∈ℕ
77 66 76 ffvelcdmd ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→Λ⁡n⁡1∈ℝ
78 41 a1i ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→2∈0..^3
79 71 78 ffvelcdmd ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→n⁡2∈ℕ
80 66 79 ffvelcdmd ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→Λ⁡n⁡2∈ℝ
81 77 80 remulcld ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→Λ⁡n⁡1⁢Λ⁡n⁡2∈ℝ
82 74 81 remulcld ⊢φ∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→Λ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2∈ℝ
83 65 82 fsumrecl ⊢φ→∑n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2∈ℝ
84 83 recnd ⊢φ→∑n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2∈ℂ
85 fsumconst ⊢0..^3∈Fin∧∑n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2∈ℂ→∑a∈0..^3∑n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2=0..^3⁢∑n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2
86 7 84 85 syl2anc ⊢φ→∑a∈0..^3∑n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2=0..^3⁢∑n∈c∈ℕrepr⁡3N|¬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..^33∈ℕ
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⁡3N|¬c⁡0∈O∩ℙ=d∈ℕrepr⁡3N|¬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⁡3N|¬c⁡a∈O∩ℙ=d∈ℕrepr⁡3N|¬d⁡a∈O∩ℙ
110 eqid ⊢ifa=0I↾0..^3pmTrsp⁡0..^3⁡a0=ifa=0I↾0..^3pmTrsp⁡0..^3⁡a0
111 98 99 100 101 105 109 110 5 reprpmtf1o ⊢φ∧a∈0..^3→F:c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ⟶1-1 ontoc∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ
112 eqidd ⊢φ∧a∈0..^3∧e∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→F⁡e=F⁡e
113 82 adantlr ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→Λ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2∈ℝ
114 113 recnd ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙ→Λ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2∈ℂ
115 94 16 111 112 114 fsumf1o ⊢φ∧a∈0..^3→∑n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2=∑e∈c∈ℕrepr⁡3N|¬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⁡3N|¬c⁡a∈O∩ℙΛ⁡F⁡e⁡0⁢Λ⁡F⁡e⁡1⁢Λ⁡F⁡e⁡2=∑n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙΛ⁡F⁡n⁡0⁢Λ⁡F⁡n⁡1⁢Λ⁡F⁡n⁡2
126 125 a1i ⊢φ∧a∈0..^3→∑e∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙΛ⁡F⁡e⁡0⁢Λ⁡F⁡e⁡1⁢Λ⁡F⁡e⁡2=∑n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙΛ⁡F⁡n⁡0⁢Λ⁡F⁡n⁡1⁢Λ⁡F⁡n⁡2
127 ovexd ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→0..^3∈V
128 101 adantr ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→a∈0..^3
129 127 128 30 110 pmtridf1o ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙ→ifa=0I↾0..^3pmTrsp⁡0..^3⁡a0:0..^3⟶1-1 onto0..^3
130 5 129 25 18 23 hgt750lemg ⊢φ∧a∈0..^3∧n∈c∈ℕrepr⁡3N|¬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⁡3N|¬c⁡a∈O∩ℙΛ⁡F⁡n⁡0⁢Λ⁡F⁡n⁡1⁢Λ⁡F⁡n⁡2=∑n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2
132 115 126 131 3eqtrrd ⊢φ∧a∈0..^3→∑n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2=∑n∈c∈ℕrepr⁡3N|¬c⁡0∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2
133 132 sumeq2dv ⊢φ→∑a∈0..^3∑n∈c∈ℕrepr⁡3N|¬c⁡a∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2=∑a∈0..^3∑n∈c∈ℕrepr⁡3N|¬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⁡3N|¬c⁡0∈O∩ℙ
139 138 sumeq1d ⊢φ→∑n∈AΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2=∑n∈c∈ℕrepr⁡3N|¬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⁡3N|¬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⁡3N|¬c⁡a∈O∩ℙΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2
142 55 62 141 3brtr4d ⊢φ→∑n∈ℕrepr⁡3N∖O∩ℙrepr⁡3NΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2≤3⁢∑n∈AΛ⁡n⁡0⁢Λ⁡n⁡1⁢Λ⁡n⁡2