hgt749d

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

	Ref	Expression
Hypotheses	hgt749d.o	$⊢ O = \{z \in ℤ \| \neg 2 ∥ z\}$
	hgt749d.n	$⊢ φ \to N \in O$
	hgt749d.1	$⊢ φ \to 10^{27} \leq N$
Assertion	hgt749d	$⊢ φ \to \exists h \in ({[0, +∞)}^{ℕ}) \exists k \in ({[0, +∞)}^{ℕ}) (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 0.00042248 N^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2} e^{i 2 π -N x} d x)$

Proof

Step	Hyp	Ref	Expression
1		hgt749d.o	$⊢ O = \{z \in ℤ \| \neg 2 ∥ z\}$
2		hgt749d.n	$⊢ φ \to N \in O$
3		hgt749d.1	$⊢ φ \to 10^{27} \leq N$
4		breq2	$⊢ n = N \to (10^{27} \leq n \leftrightarrow 10^{27} \leq N)$
5		oveq1	$⊢ n = N \to n^{2} = N^{2}$
6	5	oveq2d	$⊢ n = N \to 0.00042248 n^{2} = 0.00042248 N^{2}$
7		oveq2	$⊢ n = N \to (Λ \times_{f} h) vts n = (Λ \times_{f} h) vts N$
8	7	fveq1d	$⊢ n = N \to ((Λ \times_{f} h) vts n) (x) = ((Λ \times_{f} h) vts N) (x)$
9		oveq2	$⊢ n = N \to (Λ \times_{f} k) vts n = (Λ \times_{f} k) vts N$
10	9	fveq1d	$⊢ n = N \to ((Λ \times_{f} k) vts n) (x) = ((Λ \times_{f} k) vts N) (x)$
11	10	oveq1d	$⊢ n = N \to {((Λ \times_{f} k) vts n) (x)}^{2} = {((Λ \times_{f} k) vts N) (x)}^{2}$
12	8 11	oveq12d	$⊢ n = N \to ((Λ \times_{f} h) vts n) (x) {((Λ \times_{f} k) vts n) (x)}^{2} = ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2}$
13		negeq	$⊢ n = N \to - n = - N$
14	13	oveq1d	$⊢ n = N \to (- n) x = -N x$
15	14	oveq2d	$⊢ n = N \to i 2 π (- n) x = i 2 π -N x$
16	15	fveq2d	$⊢ n = N \to e^{i 2 π (- n) x} = e^{i 2 π -N x}$
17	12 16	oveq12d	$⊢ n = N \to ((Λ \times_{f} h) vts n) (x) {((Λ \times_{f} k) vts n) (x)}^{2} e^{i 2 π (- n) x} = ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2} e^{i 2 π -N x}$
18	17	adantr	$⊢ (n = N \land x \in (0, 1)) \to ((Λ \times_{f} h) vts n) (x) {((Λ \times_{f} k) vts n) (x)}^{2} e^{i 2 π (- n) x} = ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2} e^{i 2 π -N x}$
19	18	itgeq2dv	$⊢ n = N \to \int_{(0, 1)} ((Λ \times_{f} h) vts n) (x) {((Λ \times_{f} k) vts n) (x)}^{2} e^{i 2 π (- n) x} d x = \int_{(0, 1)} ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2} e^{i 2 π -N x} d x$
20	6 19	breq12d	$⊢ n = N \to (0.00042248 n^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts n) (x) {((Λ \times_{f} k) vts n) (x)}^{2} e^{i 2 π (- n) x} d x \leftrightarrow 0.00042248 N^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2} e^{i 2 π -N x} d x)$
21	20	3anbi3d	$⊢ n = N \to ((\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 0.00042248 n^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts n) (x) {((Λ \times_{f} k) vts n) (x)}^{2} e^{i 2 π (- n) x} d x) \leftrightarrow (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 0.00042248 N^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2} e^{i 2 π -N x} d x))$
22	21	rexbidv	$⊢ n = N \to (\exists k \in ({[0, +∞)}^{ℕ}) (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 0.00042248 n^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts n) (x) {((Λ \times_{f} k) vts n) (x)}^{2} e^{i 2 π (- n) x} d x) \leftrightarrow \exists k \in ({[0, +∞)}^{ℕ}) (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 0.00042248 N^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2} e^{i 2 π -N x} d x))$
23	22	rexbidv	$⊢ n = N \to (\exists h \in ({[0, +∞)}^{ℕ}) \exists k \in ({[0, +∞)}^{ℕ}) (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 0.00042248 n^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts n) (x) {((Λ \times_{f} k) vts n) (x)}^{2} e^{i 2 π (- n) x} d x) \leftrightarrow \exists h \in ({[0, +∞)}^{ℕ}) \exists k \in ({[0, +∞)}^{ℕ}) (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 0.00042248 N^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2} e^{i 2 π -N x} d x))$
24	4 23	imbi12d	$⊢ n = N \to ((10^{27} \leq n \to \exists h \in ({[0, +∞)}^{ℕ}) \exists k \in ({[0, +∞)}^{ℕ}) (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 0.00042248 n^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts n) (x) {((Λ \times_{f} k) vts n) (x)}^{2} e^{i 2 π (- n) x} d x)) \leftrightarrow (10^{27} \leq N \to \exists h \in ({[0, +∞)}^{ℕ}) \exists k \in ({[0, +∞)}^{ℕ}) (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 0.00042248 N^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2} e^{i 2 π -N x} d x)))$
25		ax-hgt749	$⊢ \forall n \in \{z \in ℤ \| \neg 2 ∥ z\} (10^{27} \leq n \to \exists h \in ({[0, +∞)}^{ℕ}) \exists k \in ({[0, +∞)}^{ℕ}) (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 0.00042248 n^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts n) (x) {((Λ \times_{f} k) vts n) (x)}^{2} e^{i 2 π (- n) x} d x))$
26	25	a1i	$⊢ φ \to \forall n \in \{z \in ℤ \| \neg 2 ∥ z\} (10^{27} \leq n \to \exists h \in ({[0, +∞)}^{ℕ}) \exists k \in ({[0, +∞)}^{ℕ}) (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 0.00042248 n^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts n) (x) {((Λ \times_{f} k) vts n) (x)}^{2} e^{i 2 π (- n) x} d x))$
27	2 1	eleqtrdi	$⊢ φ \to N \in \{z \in ℤ \| \neg 2 ∥ z\}$
28	24 26 27	rspcdva	$⊢ φ \to (10^{27} \leq N \to \exists h \in ({[0, +∞)}^{ℕ}) \exists k \in ({[0, +∞)}^{ℕ}) (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 0.00042248 N^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2} e^{i 2 π -N x} d x))$
29	3 28	mpd	$⊢ φ \to \exists h \in ({[0, +∞)}^{ℕ}) \exists k \in ({[0, +∞)}^{ℕ}) (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 0.00042248 N^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2} e^{i 2 π -N x} d x)$

Metamath Proof Explorer

Theorem hgt749d

Proof