Metamath Proof Explorer


Theorem tgoldbachgtd

Description: Odd integers greater than ( ; 1 0 ^ ; 2 7 ) have at least a representation as a sum of three odd primes. Final statement in section 7.4 of Helfgott p. 70. (Contributed by Thierry Arnoux, 15-Dec-2021)

Ref Expression
Hypotheses tgoldbachgtd.o 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
tgoldbachgtd.n ( 𝜑𝑁𝑂 )
tgoldbachgtd.1 ( 𝜑 → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
Assertion tgoldbachgtd ( 𝜑 → 0 < ( ♯ ‘ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 tgoldbachgtd.o 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
2 tgoldbachgtd.n ( 𝜑𝑁𝑂 )
3 tgoldbachgtd.1 ( 𝜑 → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
4 2 ad3antrrr ( ( ( ( 𝜑 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 ) ) → 𝑁𝑂 )
5 3 ad3antrrr ( ( ( ( 𝜑 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 ) ) → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
6 elmapi ( ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) → : ℕ ⟶ ( 0 [,) +∞ ) )
7 6 ad3antlr ( ( ( ( 𝜑 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 ) ) → : ℕ ⟶ ( 0 [,) +∞ ) )
8 elmapi ( 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) → 𝑘 : ℕ ⟶ ( 0 [,) +∞ ) )
9 8 ad2antlr ( ( ( ( 𝜑 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 ) ) → 𝑘 : ℕ ⟶ ( 0 [,) +∞ ) )
10 simpr1 ( ( ( ( 𝜑 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 ) ) → ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) )
11 fveq2 ( 𝑚 = 𝑛 → ( 𝑘𝑚 ) = ( 𝑘𝑛 ) )
12 11 breq1d ( 𝑚 = 𝑛 → ( ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ↔ ( 𝑘𝑛 ) ≤ ( 1 . 0 7 9 9 5 5 ) ) )
13 12 cbvralvw ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ↔ ∀ 𝑛 ∈ ℕ ( 𝑘𝑛 ) ≤ ( 1 . 0 7 9 9 5 5 ) )
14 10 13 sylib ( ( ( ( 𝜑 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 ) ) → ∀ 𝑛 ∈ ℕ ( 𝑘𝑛 ) ≤ ( 1 . 0 7 9 9 5 5 ) )
15 14 r19.21bi ( ( ( ( ( 𝜑 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑘𝑛 ) ≤ ( 1 . 0 7 9 9 5 5 ) )
16 simpr2 ( ( ( ( 𝜑 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 ) ) → ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) )
17 fveq2 ( 𝑚 = 𝑛 → ( 𝑚 ) = ( 𝑛 ) )
18 17 breq1d ( 𝑚 = 𝑛 → ( ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ↔ ( 𝑛 ) ≤ ( 1 . 4 1 4 ) ) )
19 18 cbvralvw ( ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ↔ ∀ 𝑛 ∈ ℕ ( 𝑛 ) ≤ ( 1 . 4 1 4 ) )
20 16 19 sylib ( ( ( ( 𝜑 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 ) ) → ∀ 𝑛 ∈ ℕ ( 𝑛 ) ≤ ( 1 . 4 1 4 ) )
21 20 r19.21bi ( ( ( ( ( 𝜑 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 ) ≤ ( 1 . 4 1 4 ) )
22 simpr3 ( ( ( ( 𝜑 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 ) ) → ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )
23 fveq2 ( 𝑥 = 𝑦 → ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) = ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑦 ) )
24 fveq2 ( 𝑥 = 𝑦 → ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) = ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑦 ) )
25 24 oveq1d ( 𝑥 = 𝑦 → ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) = ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑦 ) ↑ 2 ) )
26 23 25 oveq12d ( 𝑥 = 𝑦 → ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) = ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑦 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑦 ) ↑ 2 ) ) )
27 oveq2 ( 𝑥 = 𝑦 → ( - 𝑁 · 𝑥 ) = ( - 𝑁 · 𝑦 ) )
28 27 oveq2d ( 𝑥 = 𝑦 → ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) = ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑦 ) ) )
29 28 fveq2d ( 𝑥 = 𝑦 → ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) = ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑦 ) ) ) )
30 26 29 oveq12d ( 𝑥 = 𝑦 → ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑦 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑦 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑦 ) ) ) ) )
31 30 cbvitgv ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 = ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑦 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑦 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑦 ) ) ) ) d 𝑦
32 22 31 breqtrdi ( ( ( ( 𝜑 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 ) ) → ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑦 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑦 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑦 ) ) ) ) d 𝑦 )
33 1 4 5 7 9 15 21 32 tgoldbachgtda ( ( ( ( 𝜑 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ) ∧ ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 ) ) → 0 < ( ♯ ‘ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) )
34 1 2 3 hgt749d ( 𝜑 → ∃ ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ∃ 𝑘 ∈ ( ( 0 [,) +∞ ) ↑m ℕ ) ( ∀ 𝑚 ∈ ℕ ( 𝑘𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) ∧ ∀ 𝑚 ∈ ℕ ( 𝑚 ) ≤ ( 1 . 4 1 4 ) ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 ) )
35 33 34 r19.29vva ( 𝜑 → 0 < ( ♯ ‘ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) )