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

Metamath Proof Explorer

Theorem hgt749d

Description: A deduction version of ax-hgt749 . (Contributed by Thierry Arnoux, 15-Dec-2021)

Ref Expression
Hypotheses hgt749d.o ⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
hgt749d.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑂 )
hgt749d.1 ⊢ ( 𝜑 → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
Assertion 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 𝑥 ) )

Proof

Step Hyp Ref Expression
1 hgt749d.o ⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
2 hgt749d.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑂 )
3 hgt749d.1 ⊢ ( 𝜑 → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
4 breq2 ⊢ ( 𝑛 = 𝑁 → ( ( 1 0 ↑ 2 7 ) ≤ 𝑛 ↔ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) )
5 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ↑ 2 ) = ( 𝑁 ↑ 2 ) )
6 5 oveq2d ⊢ ( 𝑛 = 𝑁 → ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑛 ↑ 2 ) ) = ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) )
7 oveq2 ⊢ ( 𝑛 = 𝑁 → ( ( Λ ∘f · ℎ ) vts 𝑛 ) = ( ( Λ ∘f · ℎ ) vts 𝑁 ) )
8 7 fveq1d ⊢ ( 𝑛 = 𝑁 → ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) = ( ( ( Λ ∘f · ℎ ) vts 𝑁 ) ‘ 𝑥 ) )
9 oveq2 ⊢ ( 𝑛 = 𝑁 → ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) = ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) )
10 9 fveq1d ⊢ ( 𝑛 = 𝑁 → ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) = ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) )
11 10 oveq1d ⊢ ( 𝑛 = 𝑁 → ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) = ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) )
12 8 11 oveq12d ⊢ ( 𝑛 = 𝑁 → ( ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) ) = ( ( ( ( Λ ∘f · ℎ ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) )
13 negeq ⊢ ( 𝑛 = 𝑁 → - 𝑛 = - 𝑁 )
14 13 oveq1d ⊢ ( 𝑛 = 𝑁 → ( - 𝑛 · 𝑥 ) = ( - 𝑁 · 𝑥 ) )
15 14 oveq2d ⊢ ( 𝑛 = 𝑁 → ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) = ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) )
16 15 fveq2d ⊢ ( 𝑛 = 𝑁 → ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) ) = ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) )
17 12 16 oveq12d ⊢ ( 𝑛 = 𝑁 → ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) ) ) = ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) )
18 17 adantr ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) ) ) = ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) )
19 18 itgeq2dv ⊢ ( 𝑛 = 𝑁 → ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑛 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑛 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑛 · 𝑥 ) ) ) ) d 𝑥 = ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · ℎ ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝑘 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )
20 6 19 breq12d ⊢ ( 𝑛 = 𝑁 → ( ( ( 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 𝑥 ) )
21 20 3anbi3d ⊢ ( 𝑛 = 𝑁 → ( ( ∀ 𝑚 ∈ ℕ ( 𝑘 ‘ 𝑚 ) ≤ ( 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 ) ∧ ∀ 𝑚 ∈ ℕ ( ℎ ‘ 𝑚 ) ≤ ( 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 𝑥 ) ) )
22 21 rexbidv ⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑘 ∈ ( ( 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 [,) +∞ ) ↑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 𝑥 ) ) )
23 22 rexbidv ⊢ ( 𝑛 = 𝑁 → ( ∃ ℎ ∈ ( ( 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 [,) +∞ ) ↑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 𝑥 ) ) )
24 4 23 imbi12d ⊢ ( 𝑛 = 𝑁 → ( ( ( 1 0 ↑ 2 7 ) ≤ 𝑛 → ∃ ℎ ∈ ( ( 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 ) ≤ 𝑁 → ∃ ℎ ∈ ( ( 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 𝑥 ) ) ) )
25 ax-hgt749 ⊢ ∀ 𝑛 ∈ { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 } ( ( 1 0 ↑ 2 7 ) ≤ 𝑛 → ∃ ℎ ∈ ( ( 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 𝑥 ) )
26 25 a1i ⊢ ( 𝜑 → ∀ 𝑛 ∈ { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 } ( ( 1 0 ↑ 2 7 ) ≤ 𝑛 → ∃ ℎ ∈ ( ( 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 𝑥 ) ) )
27 2 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 } )
28 24 26 27 rspcdva ⊢ ( 𝜑 → ( ( 1 0 ↑ 2 7 ) ≤ 𝑁 → ∃ ℎ ∈ ( ( 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 𝑥 ) ) )
29 3 28 mpd ⊢ ( 𝜑 → ∃ ℎ ∈ ( ( 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 𝑥 ) )