Theorem 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	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) − ( 𝐴 Xrm 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
2	1	adantl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℂ )
3		ax-1cn	⊢ 1 ∈ ℂ
4		negsub	⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑁 + - 1 ) = ( 𝑁 − 1 ) )
5	2 3 4	sylancl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑁 + - 1 ) = ( 𝑁 − 1 ) )
6	5	eqcomd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑁 − 1 ) = ( 𝑁 + - 1 ) )
7	6	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) = ( 𝐴 Yrm ( 𝑁 + - 1 ) ) )
8		neg1z	⊢ - 1 ∈ ℤ
9		rmyadd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ - 1 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + - 1 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm - 1 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm - 1 ) ) ) )
10	8 9	mp3an3	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + - 1 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm - 1 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm - 1 ) ) ) )
11		1z	⊢ 1 ∈ ℤ
12		rmxneg	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 1 ∈ ℤ ) → ( 𝐴 Xrm - 1 ) = ( 𝐴 Xrm 1 ) )
13	11 12	mpan2	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm - 1 ) = ( 𝐴 Xrm 1 ) )
14		rmx1	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm 1 ) = 𝐴 )
15	13 14	eqtrd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm - 1 ) = 𝐴 )
16	15	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm - 1 ) = 𝐴 )
17	16	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm - 1 ) ) = ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) )
18		rmyneg	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 1 ∈ ℤ ) → ( 𝐴 Yrm - 1 ) = - ( 𝐴 Yrm 1 ) )
19	11 18	mpan2	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm - 1 ) = - ( 𝐴 Yrm 1 ) )
20		rmy1	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 1 ) = 1 )
21	20	negeqd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → - ( 𝐴 Yrm 1 ) = - 1 )
22	19 21	eqtrd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm - 1 ) = - 1 )
23	22	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm - 1 ) = - 1 )
24	23	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm - 1 ) ) = ( ( 𝐴 Xrm 𝑁 ) · - 1 ) )
25		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
26	25	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
27	26	nn0cnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℂ )
28		neg1cn	⊢ - 1 ∈ ℂ
29		mulcom	⊢ ( ( ( 𝐴 Xrm 𝑁 ) ∈ ℂ ∧ - 1 ∈ ℂ ) → ( ( 𝐴 Xrm 𝑁 ) · - 1 ) = ( - 1 · ( 𝐴 Xrm 𝑁 ) ) )
30	27 28 29	sylancl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · - 1 ) = ( - 1 · ( 𝐴 Xrm 𝑁 ) ) )
31	27	mulm1d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( - 1 · ( 𝐴 Xrm 𝑁 ) ) = - ( 𝐴 Xrm 𝑁 ) )
32	24 30 31	3eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm - 1 ) ) = - ( 𝐴 Xrm 𝑁 ) )
33	17 32	oveq12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm - 1 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm - 1 ) ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) + - ( 𝐴 Xrm 𝑁 ) ) )
34		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
35	34	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
36	35	zcnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
37		eluzelcn	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℂ )
38	37	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ℂ )
39	36 38	mulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ∈ ℂ )
40	39 27	negsubd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) + - ( 𝐴 Xrm 𝑁 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) − ( 𝐴 Xrm 𝑁 ) ) )
41	33 40	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm - 1 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm - 1 ) ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) − ( 𝐴 Xrm 𝑁 ) ) )
42	7 10 41	3eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) − ( 𝐴 Xrm 𝑁 ) ) )