rmxm1

Description: Subtraction of 1 formula for X sequence. Part 1 of equation 2.10 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 14-Oct-2014)

		Ref	Expression
	Assertion	rmxm1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} (N - 1) = A (A X_{rm} N) - (A^{2} - 1) (A Y_{rm} N)$

Proof

Step	Hyp	Ref	Expression
1		neg1z	$⊢ - 1 \in ℤ$
2		rmxadd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land - 1 \in ℤ) \to A X_{rm} (N + -1) = (A X_{rm} N) (A X_{rm} -1) + (A^{2} - 1) (A Y_{rm} N) (A Y_{rm} -1)$
3	1 2	mp3an3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} (N + -1) = (A X_{rm} N) (A X_{rm} -1) + (A^{2} - 1) (A Y_{rm} N) (A Y_{rm} -1)$
4		1z	$⊢ 1 \in ℤ$
5		rmxneg	$⊢ (A \in ℤ_{\geq 2} \land 1 \in ℤ) \to A X_{rm} -1 = A X_{rm} 1$
6	4 5	mpan2	$⊢ A \in ℤ_{\geq 2} \to A X_{rm} -1 = A X_{rm} 1$
7		rmx1	$⊢ A \in ℤ_{\geq 2} \to A X_{rm} 1 = A$
8	6 7	eqtrd	$⊢ A \in ℤ_{\geq 2} \to A X_{rm} -1 = A$
9	8	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} -1 = A$
10	9	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) (A X_{rm} -1) = (A X_{rm} N) A$
11		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
12	11	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
13	12	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℂ$
14		eluzelcn	$⊢ A \in ℤ_{\geq 2} \to A \in ℂ$
15	14	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A \in ℂ$
16	13 15	mulcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) A = A (A X_{rm} N)$
17	10 16	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) (A X_{rm} -1) = A (A X_{rm} N)$
18		rmyneg	$⊢ (A \in ℤ_{\geq 2} \land 1 \in ℤ) \to A Y_{rm} -1 = - (A Y_{rm} 1)$
19	4 18	mpan2	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} -1 = - (A Y_{rm} 1)$
20		rmy1	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} 1 = 1$
21	20	negeqd	$⊢ A \in ℤ_{\geq 2} \to - (A Y_{rm} 1) = - 1$
22	19 21	eqtrd	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} -1 = - 1$
23	22	oveq2d	$⊢ A \in ℤ_{\geq 2} \to (A Y_{rm} N) (A Y_{rm} -1) = (A Y_{rm} N) -1$
24	23	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) (A Y_{rm} -1) = (A Y_{rm} N) -1$
25		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
26	25	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
27	26	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℂ$
28		ax-1cn	$⊢ 1 \in ℂ$
29		mulneg2	$⊢ (A Y_{rm} N \in ℂ \land 1 \in ℂ) \to (A Y_{rm} N) -1 = - (A Y_{rm} N) \cdot 1$
30	27 28 29	sylancl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) -1 = - (A Y_{rm} N) \cdot 1$
31	27	mulridd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) \cdot 1 = A Y_{rm} N$
32	31	negeqd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to - (A Y_{rm} N) \cdot 1 = - (A Y_{rm} N)$
33	30 32	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) -1 = - (A Y_{rm} N)$
34	24 33	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) (A Y_{rm} -1) = - (A Y_{rm} N)$
35	34	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A^{2} - 1) (A Y_{rm} N) (A Y_{rm} -1) = (A^{2} - 1) (- (A Y_{rm} N))$
36		rmspecnonsq	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in (ℕ ∖ ◻_{ℕ})$
37	36	eldifad	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℕ$
38	37	nncnd	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℂ$
39	38	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A^{2} - 1 \in ℂ$
40	39 27	mulneg2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A^{2} - 1) (- (A Y_{rm} N)) = - (A^{2} - 1) (A Y_{rm} N)$
41	35 40	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A^{2} - 1) (A Y_{rm} N) (A Y_{rm} -1) = - (A^{2} - 1) (A Y_{rm} N)$
42	17 41	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) (A X_{rm} -1) + (A^{2} - 1) (A Y_{rm} N) (A Y_{rm} -1) = A (A X_{rm} N) + (- (A^{2} - 1) (A Y_{rm} N))$
43	3 42	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} (N + -1) = A (A X_{rm} N) + (- (A^{2} - 1) (A Y_{rm} N))$
44		zcn	$⊢ N \in ℤ \to N \in ℂ$
45	44	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to N \in ℂ$
46		negsub	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + -1 = N - 1$
47	45 28 46	sylancl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to N + -1 = N - 1$
48	47	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} (N + -1) = A X_{rm} (N - 1)$
49	15 13	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A (A X_{rm} N) \in ℂ$
50	39 27	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A^{2} - 1) (A Y_{rm} N) \in ℂ$
51	49 50	negsubd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A (A X_{rm} N) + (- (A^{2} - 1) (A Y_{rm} N)) = A (A X_{rm} N) - (A^{2} - 1) (A Y_{rm} N)$
52	43 48 51	3eqtr3d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} (N - 1) = A (A X_{rm} N) - (A^{2} - 1) (A Y_{rm} N)$

Metamath Proof Explorer

Theorem rmxm1

Proof