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