fourierdlem13

Description: Value of V in terms of value of Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem13.a	$⊢ φ \to A \in ℝ$
	fourierdlem13.b	$⊢ φ \to B \in ℝ$
	fourierdlem13.x	$⊢ φ \to X \in ℝ$
	fourierdlem13.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))\})$
	fourierdlem13.m	$⊢ φ \to M \in ℕ$
	fourierdlem13.v	$⊢ φ \to V \in P (M)$
	fourierdlem13.i	$⊢ φ \to I \in (0 \dots M)$
	fourierdlem13.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
Assertion	fourierdlem13	$⊢ φ \to (Q (I) = V (I) - X \land V (I) = X + Q (I))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem13.a	$⊢ φ \to A \in ℝ$
2		fourierdlem13.b	$⊢ φ \to B \in ℝ$
3		fourierdlem13.x	$⊢ φ \to X \in ℝ$
4		fourierdlem13.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		fourierdlem13.m	$⊢ φ \to M \in ℕ$
6		fourierdlem13.v	$⊢ φ \to V \in P (M)$
7		fourierdlem13.i	$⊢ φ \to I \in (0 \dots M)$
8		fourierdlem13.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
9	8	a1i	$⊢ φ \to Q = (i \in (0 \dots M) ⟼ V (i) - X)$
10		simpr	$⊢ (φ \land i = I) \to i = I$
11	10	fveq2d	$⊢ (φ \land i = I) \to V (i) = V (I)$
12	11	oveq1d	$⊢ (φ \land i = I) \to V (i) - X = V (I) - X$
13	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))))$
14	5 13	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))))$
15	6 14	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)))$
16	15	simpld	$⊢ φ \to V \in (ℝ^{(0 \dots M)})$
17		elmapi	$⊢ V \in (ℝ^{(0 \dots M)}) \to V : (0 \dots M) ⟶ ℝ$
18	16 17	syl	$⊢ φ \to V : (0 \dots M) ⟶ ℝ$
19	18 7	ffvelrnd	$⊢ φ \to V (I) \in ℝ$
20	19 3	resubcld	$⊢ φ \to V (I) - X \in ℝ$
21	9 12 7 20	fvmptd	$⊢ φ \to Q (I) = V (I) - X$
22	21	oveq2d	$⊢ φ \to X + Q (I) = X + V (I) - X$
23	3	recnd	$⊢ φ \to X \in ℂ$
24	19	recnd	$⊢ φ \to V (I) \in ℂ$
25	23 24	pncan3d	$⊢ φ \to X + V (I) - X = V (I)$
26	22 25	eqtr2d	$⊢ φ \to V (I) = X + Q (I)$
27	21 26	jca	$⊢ φ \to (Q (I) = V (I) - X \land V (I) = X + Q (I))$

Metamath Proof Explorer

Theorem fourierdlem13

Proof