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	ffvelcdmda	$⊢ (φ \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		0le0	$⊢ 0 \leq 0$
32	31	a1i	$⊢ φ \to 0 \leq 0$
33		0red	$⊢ φ \to 0 \in ℝ$
34	6	nnred	$⊢ φ \to M \in ℝ$
35	6	nngt0d	$⊢ φ \to 0 < M$
36	33 34 35	ltled	$⊢ φ \to 0 \leq M$
37	29 30 29 32 36	elfzd	$⊢ φ \to 0 \in (0 \dots M)$
38	14 37	ffvelcdmd	$⊢ φ \to V (0) \in ℝ$
39	38 3	resubcld	$⊢ φ \to V (0) - X \in ℝ$
40	25 28 37 39	fvmptd	$⊢ φ \to Q (0) = V (0) - X$
41	11	simprd	$⊢ φ \to ((V (0) = A + X \land V (M) = B + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))$
42	41	simpld	$⊢ φ \to (V (0) = A + X \land V (M) = B + X)$
43	42	simpld	$⊢ φ \to V (0) = A + X$
44	43	oveq1d	$⊢ φ \to V (0) - X = A + X - X$
45	1	recnd	$⊢ φ \to A \in ℂ$
46	3	recnd	$⊢ φ \to X \in ℂ$
47	45 46	pncand	$⊢ φ \to A + X - X = A$
48	40 44 47	3eqtrd	$⊢ φ \to Q (0) = A$
49		fveq2	$⊢ i = M \to V (i) = V (M)$
50	49	oveq1d	$⊢ i = M \to V (i) - X = V (M) - X$
51	50	adantl	$⊢ (φ \land i = M) \to V (i) - X = V (M) - X$
52	34	leidd	$⊢ φ \to M \leq M$
53	29 30 30 36 52	elfzd	$⊢ φ \to M \in (0 \dots M)$
54	14 53	ffvelcdmd	$⊢ φ \to V (M) \in ℝ$
55	54 3	resubcld	$⊢ φ \to V (M) - X \in ℝ$
56	25 51 53 55	fvmptd	$⊢ φ \to Q (M) = V (M) - X$
57	42	simprd	$⊢ φ \to V (M) = B + X$
58	57	oveq1d	$⊢ φ \to V (M) - X = B + X - X$
59	2	recnd	$⊢ φ \to B \in ℂ$
60	59 46	pncand	$⊢ φ \to B + X - X = B$
61	56 58 60	3eqtrd	$⊢ φ \to Q (M) = B$
62	48 61	jca	$⊢ φ \to (Q (0) = A \land Q (M) = B)$
63		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
64	63 15	sylan2	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \in ℝ$
65	14	adantr	$⊢ (φ \land i \in (0 ..^M)) \to V : (0 \dots M) ⟶ ℝ$
66		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
67	66	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
68	65 67	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) \in ℝ$
69	3	adantr	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℝ$
70	41	simprd	$⊢ φ \to \forall i \in (0 ..^M) V (i) < V (i + 1)$
71	70	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to V (i) < V (i + 1)$
72	64 68 69 71	ltsub1dd	$⊢ (φ \land i \in (0 ..^M)) \to V (i) - X < V (i + 1) - X$
73	63	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
74	63 17	sylan2	$⊢ (φ \land i \in (0 ..^M)) \to V (i) - X \in ℝ$
75	8	fvmpt2	$⊢ (i \in (0 \dots M) \land V (i) - X \in ℝ) \to Q (i) = V (i) - X$
76	73 74 75	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = V (i) - X$
77		fveq2	$⊢ i = j \to V (i) = V (j)$
78	77	oveq1d	$⊢ i = j \to V (i) - X = V (j) - X$
79	78	cbvmptv	$⊢ (i \in (0 \dots M) ⟼ V (i) - X) = (j \in (0 \dots M) ⟼ V (j) - X)$
80	8 79	eqtri	$⊢ Q = (j \in (0 \dots M) ⟼ V (j) - X)$
81	80	a1i	$⊢ (φ \land i \in (0 ..^M)) \to Q = (j \in (0 \dots M) ⟼ V (j) - X)$
82		fveq2	$⊢ j = i + 1 \to V (j) = V (i + 1)$
83	82	oveq1d	$⊢ j = i + 1 \to V (j) - X = V (i + 1) - X$
84	83	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land j = i + 1) \to V (j) - X = V (i + 1) - X$
85	68 69	resubcld	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) - X \in ℝ$
86	81 84 67 85	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) = V (i + 1) - X$
87	72 76 86	3brtr4d	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
88	87	ralrimiva	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
89	24 62 88	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)))$
90	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))))$
91	6 90	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))))$
92	89 91	mpbird	$⊢ φ \to Q \in O (M)$

Metamath Proof Explorer

Theorem fourierdlem14

Proof