This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) 𝑁 ) ) )