fourierdlem14

Description: Given the partition V , Q is the partition shifted to the left by X . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem14.1	$⊢ φ \to A \in ℝ$
	fourierdlem14.2	$⊢ φ \to B \in ℝ$
	fourierdlem14.x	$⊢ φ \to X \in ℝ$
	fourierdlem14.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A + X \land p (m) = B + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem14.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem14.m	$⊢ φ \to M \in ℕ$
	fourierdlem14.v	$⊢ φ \to V \in P (M)$
	fourierdlem14.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
Assertion	fourierdlem14	$⊢ φ \to Q \in O (M)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem14.1	$⊢ φ \to A \in ℝ$
2		fourierdlem14.2	$⊢ φ \to B \in ℝ$
3		fourierdlem14.x	$⊢ φ \to X \in ℝ$
4		fourierdlem14.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A + X \land p (m) = B + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
5		fourierdlem14.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
6		fourierdlem14.m	$⊢ φ \to M \in ℕ$
7		fourierdlem14.v	$⊢ φ \to V \in P (M)$
8		fourierdlem14.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
9	4	fourierdlem2	$⊢ M \in ℕ \to (V \in P (M) \leftrightarrow (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = A + X \land V (M) = B + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))))$
10	6 9	syl	$⊢ φ \to (V \in P (M) \leftrightarrow (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = A + X \land V (M) = B + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))))$
11	7 10	mpbid	$⊢ φ \to (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = A + X \land V (M) = B + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1)))$
12	11	simpld	$⊢ φ \to V \in (ℝ^{(0 \dots M)})$
13		elmapi	$⊢ V \in (ℝ^{(0 \dots M)}) \to V : (0 \dots M) ⟶ ℝ$
14	12 13	syl	$⊢ φ \to V : (0 \dots M) ⟶ ℝ$
15	14	ffvelrnda	$⊢ (φ \land i \in (0 \dots M)) \to V (i) \in ℝ$
16	3	adantr	$⊢ (φ \land i \in (0 \dots M)) \to X \in ℝ$
17	15 16	resubcld	$⊢ (φ \land i \in (0 \dots M)) \to V (i) - X \in ℝ$
18	17 8	fmptd	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
19		reex	$⊢ ℝ \in V$
20	19	a1i	$⊢ φ \to ℝ \in V$
21		ovex	$⊢ (0 \dots M) \in V$
22	21	a1i	$⊢ φ \to (0 \dots M) \in V$
23	20 22	elmapd	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \leftrightarrow Q : (0 \dots M) ⟶ ℝ)$
24	18 23	mpbird	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
25	8	a1i	$⊢ φ \to Q = (i \in (0 \dots M) ⟼ V (i) - X)$
26		fveq2	$⊢ i = 0 \to V (i) = V (0)$
27	26	oveq1d	$⊢ i = 0 \to V (i) - X = V (0) - X$
28	27	adantl	$⊢ (φ \land i = 0) \to V (i) - X = V (0) - X$
29		0zd	$⊢ φ \to 0 \in ℤ$
30	6	nnzd	$⊢ φ \to M \in ℤ$
31	29 30 29	3jca	$⊢ φ \to (0 \in ℤ \land M \in ℤ \land 0 \in ℤ)$
32		0le0	$⊢ 0 \leq 0$
33	32	a1i	$⊢ φ \to 0 \leq 0$
34		0red	$⊢ φ \to 0 \in ℝ$
35	6	nnred	$⊢ φ \to M \in ℝ$
36	6	nngt0d	$⊢ φ \to 0 < M$
37	34 35 36	ltled	$⊢ φ \to 0 \leq M$
38	31 33 37	jca32	$⊢ φ \to ((0 \in ℤ \land M \in ℤ \land 0 \in ℤ) \land (0 \leq 0 \land 0 \leq M))$
39		elfz2	$⊢ 0 \in (0 \dots M) \leftrightarrow ((0 \in ℤ \land M \in ℤ \land 0 \in ℤ) \land (0 \leq 0 \land 0 \leq M))$
40	38 39	sylibr	$⊢ φ \to 0 \in (0 \dots M)$
41	14 40	ffvelrnd	$⊢ φ \to V (0) \in ℝ$
42	41 3	resubcld	$⊢ φ \to V (0) - X \in ℝ$
43	25 28 40 42	fvmptd	$⊢ φ \to Q (0) = V (0) - X$
44	11	simprd	$⊢ φ \to ((V (0) = A + X \land V (M) = B + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))$
45	44	simpld	$⊢ φ \to (V (0) = A + X \land V (M) = B + X)$
46	45	simpld	$⊢ φ \to V (0) = A + X$
47	46	oveq1d	$⊢ φ \to V (0) - X = A + X - X$
48	1	recnd	$⊢ φ \to A \in ℂ$
49	3	recnd	$⊢ φ \to X \in ℂ$
50	48 49	pncand	$⊢ φ \to A + X - X = A$
51	43 47 50	3eqtrd	$⊢ φ \to Q (0) = A$
52		fveq2	$⊢ i = M \to V (i) = V (M)$
53	52	oveq1d	$⊢ i = M \to V (i) - X = V (M) - X$
54	53	adantl	$⊢ (φ \land i = M) \to V (i) - X = V (M) - X$
55	29 30 30	3jca	$⊢ φ \to (0 \in ℤ \land M \in ℤ \land M \in ℤ)$
56	35	leidd	$⊢ φ \to M \leq M$
57	55 37 56	jca32	$⊢ φ \to ((0 \in ℤ \land M \in ℤ \land M \in ℤ) \land (0 \leq M \land M \leq M))$
58		elfz2	$⊢ M \in (0 \dots M) \leftrightarrow ((0 \in ℤ \land M \in ℤ \land M \in ℤ) \land (0 \leq M \land M \leq M))$
59	57 58	sylibr	$⊢ φ \to M \in (0 \dots M)$
60	14 59	ffvelrnd	$⊢ φ \to V (M) \in ℝ$
61	60 3	resubcld	$⊢ φ \to V (M) - X \in ℝ$
62	25 54 59 61	fvmptd	$⊢ φ \to Q (M) = V (M) - X$
63	45	simprd	$⊢ φ \to V (M) = B + X$
64	63	oveq1d	$⊢ φ \to V (M) - X = B + X - X$
65	2	recnd	$⊢ φ \to B \in ℂ$
66	65 49	pncand	$⊢ φ \to B + X - X = B$
67	62 64 66	3eqtrd	$⊢ φ \to Q (M) = B$
68	51 67	jca	$⊢ φ \to (Q (0) = A \land Q (M) = B)$
69		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
70	69 15	sylan2	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \in ℝ$
71	14	adantr	$⊢ (φ \land i \in (0 ..^M)) \to V : (0 \dots M) ⟶ ℝ$
72		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
73	72	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
74	71 73	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) \in ℝ$
75	3	adantr	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℝ$
76	44	simprd	$⊢ φ \to \forall i \in (0 ..^M) V (i) < V (i + 1)$
77	76	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to V (i) < V (i + 1)$
78	70 74 75 77	ltsub1dd	$⊢ (φ \land i \in (0 ..^M)) \to V (i) - X < V (i + 1) - X$
79	69	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
80	69 17	sylan2	$⊢ (φ \land i \in (0 ..^M)) \to V (i) - X \in ℝ$
81	8	fvmpt2	$⊢ (i \in (0 \dots M) \land V (i) - X \in ℝ) \to Q (i) = V (i) - X$
82	79 80 81	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = V (i) - X$
83		fveq2	$⊢ i = j \to V (i) = V (j)$
84	83	oveq1d	$⊢ i = j \to V (i) - X = V (j) - X$
85	84	cbvmptv	$⊢ (i \in (0 \dots M) ⟼ V (i) - X) = (j \in (0 \dots M) ⟼ V (j) - X)$
86	8 85	eqtri	$⊢ Q = (j \in (0 \dots M) ⟼ V (j) - X)$
87	86	a1i	$⊢ (φ \land i \in (0 ..^M)) \to Q = (j \in (0 \dots M) ⟼ V (j) - X)$
88		fveq2	$⊢ j = i + 1 \to V (j) = V (i + 1)$
89	88	oveq1d	$⊢ j = i + 1 \to V (j) - X = V (i + 1) - X$
90	89	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land j = i + 1) \to V (j) - X = V (i + 1) - X$
91	74 75	resubcld	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) - X \in ℝ$
92	87 90 73 91	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) = V (i + 1) - X$
93	78 82 92	3brtr4d	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
94	93	ralrimiva	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
95	24 68 94	jca32	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
96	5	fourierdlem2	$⊢ M \in ℕ \to (Q \in O (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
97	6 96	syl	$⊢ φ \to (Q \in O (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
98	95 97	mpbird	$⊢ φ \to Q \in O (M)$

Metamath Proof Explorer

Theorem fourierdlem14

Proof