rmym1

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

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

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ N \in ℤ \to N \in ℂ$
2	1	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to N \in ℂ$
3		ax-1cn	$⊢ 1 \in ℂ$
4		negsub	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + -1 = N - 1$
5	2 3 4	sylancl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to N + -1 = N - 1$
6	5	eqcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to N - 1 = N + -1$
7	6	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} (N - 1) = A Y_{rm} (N + -1)$
8		neg1z	$⊢ - 1 \in ℤ$
9		rmyadd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land - 1 \in ℤ) \to A Y_{rm} (N + -1) = (A Y_{rm} N) (A X_{rm} -1) + (A X_{rm} N) (A Y_{rm} -1)$
10	8 9	mp3an3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} (N + -1) = (A Y_{rm} N) (A X_{rm} -1) + (A X_{rm} N) (A Y_{rm} -1)$
11		1z	$⊢ 1 \in ℤ$
12		rmxneg	$⊢ (A \in ℤ_{\geq 2} \land 1 \in ℤ) \to A X_{rm} -1 = A X_{rm} 1$
13	11 12	mpan2	$⊢ A \in ℤ_{\geq 2} \to A X_{rm} -1 = A X_{rm} 1$
14		rmx1	$⊢ A \in ℤ_{\geq 2} \to A X_{rm} 1 = A$
15	13 14	eqtrd	$⊢ A \in ℤ_{\geq 2} \to A X_{rm} -1 = A$
16	15	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} -1 = A$
17	16	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) (A X_{rm} -1) = (A Y_{rm} N) A$
18		rmyneg	$⊢ (A \in ℤ_{\geq 2} \land 1 \in ℤ) \to A Y_{rm} -1 = - (A Y_{rm} 1)$
19	11 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	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} -1 = - 1$
24	23	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) (A Y_{rm} -1) = (A X_{rm} N) -1$
25		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
26	25	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
27	26	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℂ$
28		neg1cn	$⊢ - 1 \in ℂ$
29		mulcom	$⊢ (A X_{rm} N \in ℂ \land - 1 \in ℂ) \to (A X_{rm} N) -1 = -1 (A X_{rm} N)$
30	27 28 29	sylancl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) -1 = -1 (A X_{rm} N)$
31	27	mulm1d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to -1 (A X_{rm} N) = - (A X_{rm} N)$
32	24 30 31	3eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) (A Y_{rm} -1) = - (A X_{rm} N)$
33	17 32	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) (A X_{rm} -1) + (A X_{rm} N) (A Y_{rm} -1) = (A Y_{rm} N) A + (- (A X_{rm} N))$
34		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
35	34	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
36	35	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℂ$
37		eluzelcn	$⊢ A \in ℤ_{\geq 2} \to A \in ℂ$
38	37	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A \in ℂ$
39	36 38	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) A \in ℂ$
40	39 27	negsubd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) A + (- (A X_{rm} N)) = (A Y_{rm} N) A - (A X_{rm} N)$
41	33 40	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) (A X_{rm} -1) + (A X_{rm} N) (A Y_{rm} -1) = (A Y_{rm} N) A - (A X_{rm} N)$
42	7 10 41	3eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} (N - 1) = (A Y_{rm} N) A - (A X_{rm} N)$

Metamath Proof Explorer

Theorem rmym1

Proof