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

Proof

Step	Hyp	Ref	Expression
1		neg1z	⊢ - 1 ∈ ℤ
2		rmxadd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ - 1 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + - 1 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm - 1 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm - 1 ) ) ) ) )
3	1 2	mp3an3	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + - 1 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm - 1 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm - 1 ) ) ) ) )
4		1z	⊢ 1 ∈ ℤ
5		rmxneg	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 1 ∈ ℤ ) → ( 𝐴 Xrm - 1 ) = ( 𝐴 Xrm 1 ) )
6	4 5	mpan2	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm - 1 ) = ( 𝐴 Xrm 1 ) )
7		rmx1	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm 1 ) = 𝐴 )
8	6 7	eqtrd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm - 1 ) = 𝐴 )
9	8	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm - 1 ) = 𝐴 )
10	9	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm - 1 ) ) = ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) )
11		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
12	11	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
13	12	nn0cnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℂ )
14		eluzelcn	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℂ )
15	14	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ℂ )
16	13 15	mulcomd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) = ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) )
17	10 16	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm - 1 ) ) = ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) )
18		rmyneg	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 1 ∈ ℤ ) → ( 𝐴 Yrm - 1 ) = - ( 𝐴 Yrm 1 ) )
19	4 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	oveq2d	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm - 1 ) ) = ( ( 𝐴 Yrm 𝑁 ) · - 1 ) )
24	23	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm - 1 ) ) = ( ( 𝐴 Yrm 𝑁 ) · - 1 ) )
25		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
26	25	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
27	26	zcnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
28		ax-1cn	⊢ 1 ∈ ℂ
29		mulneg2	⊢ ( ( ( 𝐴 Yrm 𝑁 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 Yrm 𝑁 ) · - 1 ) = - ( ( 𝐴 Yrm 𝑁 ) · 1 ) )
30	27 28 29	sylancl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · - 1 ) = - ( ( 𝐴 Yrm 𝑁 ) · 1 ) )
31	27	mulid1d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · 1 ) = ( 𝐴 Yrm 𝑁 ) )
32	31	negeqd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → - ( ( 𝐴 Yrm 𝑁 ) · 1 ) = - ( 𝐴 Yrm 𝑁 ) )
33	30 32	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · - 1 ) = - ( 𝐴 Yrm 𝑁 ) )
34	24 33	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm - 1 ) ) = - ( 𝐴 Yrm 𝑁 ) )
35	34	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm - 1 ) ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · - ( 𝐴 Yrm 𝑁 ) ) )
36		rmspecnonsq	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) )
37	36	eldifad	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ )
38	37	nncnd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
39	38	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
40	39 27	mulneg2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · - ( 𝐴 Yrm 𝑁 ) ) = - ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) )
41	35 40	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm - 1 ) ) ) = - ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) )
42	17 41	oveq12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm - 1 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm - 1 ) ) ) ) = ( ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) + - ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
43	3 42	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + - 1 ) ) = ( ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) + - ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
44		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
45	44	adantl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℂ )
46		negsub	⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑁 + - 1 ) = ( 𝑁 − 1 ) )
47	45 28 46	sylancl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑁 + - 1 ) = ( 𝑁 − 1 ) )
48	47	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + - 1 ) ) = ( 𝐴 Xrm ( 𝑁 − 1 ) ) )
49	15 13	mulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) ∈ ℂ )
50	39 27	mulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℂ )
51	49 50	negsubd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) + - ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
52	43 48 51	3eqtr3d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 − 1 ) ) = ( ( 𝐴 · ( 𝐴 Xrm 𝑁 ) ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) )