rmxyadd

Description: Addition formula for X and Y sequences. See rmxadd and rmyadd for most uses. (Contributed by Stefan O'Rear, 22-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A \in ℤ_{\geq 2}$
2		zaddcl	$⊢ (M \in ℤ \land N \in ℤ) \to M + N \in ℤ$
3	2	3adant1	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to M + N \in ℤ$
4		rmxyval	$⊢ (A \in ℤ_{\geq 2} \land M + N \in ℤ) \to (A X_{rm} (M + N)) + \sqrt{A^{2} - 1} (A Y_{rm} (M + N)) = {(A + \sqrt{A^{2} - 1})}^{M + N}$
5	1 3 4	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} (M + N)) + \sqrt{A^{2} - 1} (A Y_{rm} (M + N)) = {(A + \sqrt{A^{2} - 1})}^{M + N}$
6		eluzelz	$⊢ A \in ℤ_{\geq 2} \to A \in ℤ$
7	6	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A \in ℤ$
8	7	zcnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A \in ℂ$
9		zq	$⊢ A \in ℤ \to A \in ℚ$
10		qsqcl	$⊢ A \in ℚ \to A^{2} \in ℚ$
11	7 9 10	3syl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A^{2} \in ℚ$
12		zssq	$⊢ ℤ \subseteq ℚ$
13		1z	$⊢ 1 \in ℤ$
14	12 13	sselii	$⊢ 1 \in ℚ$
15	14	a1i	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to 1 \in ℚ$
16		qsubcl	$⊢ (A^{2} \in ℚ \land 1 \in ℚ) \to A^{2} - 1 \in ℚ$
17	11 15 16	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A^{2} - 1 \in ℚ$
18		qcn	$⊢ A^{2} - 1 \in ℚ \to A^{2} - 1 \in ℂ$
19	17 18	syl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A^{2} - 1 \in ℂ$
20	19	sqrtcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to \sqrt{A^{2} - 1} \in ℂ$
21	8 20	addcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A + \sqrt{A^{2} - 1} \in ℂ$
22		rmbaserp	$⊢ A \in ℤ_{\geq 2} \to A + \sqrt{A^{2} - 1} \in ℝ^{+}$
23	22	rpne0d	$⊢ A \in ℤ_{\geq 2} \to A + \sqrt{A^{2} - 1} \neq 0$
24	23	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A + \sqrt{A^{2} - 1} \neq 0$
25		simp2	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to M \in ℤ$
26		simp3	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to N \in ℤ$
27		expaddz	$⊢ ((A + \sqrt{A^{2} - 1} \in ℂ \land A + \sqrt{A^{2} - 1} \neq 0) \land (M \in ℤ \land N \in ℤ)) \to {(A + \sqrt{A^{2} - 1})}^{M + N} = {(A + \sqrt{A^{2} - 1})}^{M} {(A + \sqrt{A^{2} - 1})}^{N}$
28	21 24 25 26 27	syl22anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to {(A + \sqrt{A^{2} - 1})}^{M + N} = {(A + \sqrt{A^{2} - 1})}^{M} {(A + \sqrt{A^{2} - 1})}^{N}$
29		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
30	29	a1i	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
31	30 1 25	fovrnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A X_{rm} M \in ℕ_{0}$
32	31	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A X_{rm} M \in ℂ$
33		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
34	33	a1i	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
35	34 1 25	fovrnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} M \in ℤ$
36	35	zcnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} M \in ℂ$
37	20 36	mulcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to \sqrt{A^{2} - 1} (A Y_{rm} M) \in ℂ$
38	30 1 26	fovrnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
39	38	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A X_{rm} N \in ℂ$
40	34 1 26	fovrnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} N \in ℤ$
41	40	zcnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} N \in ℂ$
42	20 41	mulcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to \sqrt{A^{2} - 1} (A Y_{rm} N) \in ℂ$
43	32 37 39 42	muladdd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to ((A X_{rm} M) + \sqrt{A^{2} - 1} (A Y_{rm} M)) ((A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N)) = (A X_{rm} M) (A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N) \sqrt{A^{2} - 1} (A Y_{rm} M) + (A X_{rm} M) \sqrt{A^{2} - 1} (A Y_{rm} N) + (A X_{rm} N) \sqrt{A^{2} - 1} (A Y_{rm} M)$
44		rmxyval	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to (A X_{rm} M) + \sqrt{A^{2} - 1} (A Y_{rm} M) = {(A + \sqrt{A^{2} - 1})}^{M}$
45	1 25 44	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) + \sqrt{A^{2} - 1} (A Y_{rm} M) = {(A + \sqrt{A^{2} - 1})}^{M}$
46		rmxyval	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N) = {(A + \sqrt{A^{2} - 1})}^{N}$
47	1 26 46	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N) = {(A + \sqrt{A^{2} - 1})}^{N}$
48	45 47	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to ((A X_{rm} M) + \sqrt{A^{2} - 1} (A Y_{rm} M)) ((A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N)) = {(A + \sqrt{A^{2} - 1})}^{M} {(A + \sqrt{A^{2} - 1})}^{N}$
49	43 48	eqtr3d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) (A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N) \sqrt{A^{2} - 1} (A Y_{rm} M) + (A X_{rm} M) \sqrt{A^{2} - 1} (A Y_{rm} N) + (A X_{rm} N) \sqrt{A^{2} - 1} (A Y_{rm} M) = {(A + \sqrt{A^{2} - 1})}^{M} {(A + \sqrt{A^{2} - 1})}^{N}$
50	20 41 20 36	mul4d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to \sqrt{A^{2} - 1} (A Y_{rm} N) \sqrt{A^{2} - 1} (A Y_{rm} M) = \sqrt{A^{2} - 1} \sqrt{A^{2} - 1} (A Y_{rm} N) (A Y_{rm} M)$
51	19	msqsqrtd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to \sqrt{A^{2} - 1} \sqrt{A^{2} - 1} = A^{2} - 1$
52	41 36	mulcomd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A Y_{rm} N) (A Y_{rm} M) = (A Y_{rm} M) (A Y_{rm} N)$
53	51 52	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to \sqrt{A^{2} - 1} \sqrt{A^{2} - 1} (A Y_{rm} N) (A Y_{rm} M) = (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N)$
54	50 53	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to \sqrt{A^{2} - 1} (A Y_{rm} N) \sqrt{A^{2} - 1} (A Y_{rm} M) = (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N)$
55	54	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) (A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N) \sqrt{A^{2} - 1} (A Y_{rm} M) = (A X_{rm} M) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N)$
56	32 20 41	mul12d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) \sqrt{A^{2} - 1} (A Y_{rm} N) = \sqrt{A^{2} - 1} (A X_{rm} M) (A Y_{rm} N)$
57	39 20 36	mul12d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} N) \sqrt{A^{2} - 1} (A Y_{rm} M) = \sqrt{A^{2} - 1} (A X_{rm} N) (A Y_{rm} M)$
58	56 57	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) \sqrt{A^{2} - 1} (A Y_{rm} N) + (A X_{rm} N) \sqrt{A^{2} - 1} (A Y_{rm} M) = \sqrt{A^{2} - 1} (A X_{rm} M) (A Y_{rm} N) + \sqrt{A^{2} - 1} (A X_{rm} N) (A Y_{rm} M)$
59	32 41	mulcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) (A Y_{rm} N) \in ℂ$
60	39 36	mulcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} N) (A Y_{rm} M) \in ℂ$
61	20 59 60	adddid	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to \sqrt{A^{2} - 1} ((A X_{rm} M) (A Y_{rm} N) + (A X_{rm} N) (A Y_{rm} M)) = \sqrt{A^{2} - 1} (A X_{rm} M) (A Y_{rm} N) + \sqrt{A^{2} - 1} (A X_{rm} N) (A Y_{rm} M)$
62	59 60	addcomd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) (A Y_{rm} N) + (A X_{rm} N) (A Y_{rm} M) = (A X_{rm} N) (A Y_{rm} M) + (A X_{rm} M) (A Y_{rm} N)$
63	39 36	mulcomd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} N) (A Y_{rm} M) = (A Y_{rm} M) (A X_{rm} N)$
64	63	oveq1d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} N) (A Y_{rm} M) + (A X_{rm} M) (A Y_{rm} N) = (A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N)$
65	62 64	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) (A Y_{rm} N) + (A X_{rm} N) (A Y_{rm} M) = (A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N)$
66	65	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to \sqrt{A^{2} - 1} ((A X_{rm} M) (A Y_{rm} N) + (A X_{rm} N) (A Y_{rm} M)) = \sqrt{A^{2} - 1} ((A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N))$
67	58 61 66	3eqtr2d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) \sqrt{A^{2} - 1} (A Y_{rm} N) + (A X_{rm} N) \sqrt{A^{2} - 1} (A Y_{rm} M) = \sqrt{A^{2} - 1} ((A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N))$
68	55 67	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) (A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N) \sqrt{A^{2} - 1} (A Y_{rm} M) + (A X_{rm} M) \sqrt{A^{2} - 1} (A Y_{rm} N) + (A X_{rm} N) \sqrt{A^{2} - 1} (A Y_{rm} M) = (A X_{rm} M) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) + \sqrt{A^{2} - 1} ((A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N))$
69	28 49 68	3eqtr2d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to {(A + \sqrt{A^{2} - 1})}^{M + N} = (A X_{rm} M) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) + \sqrt{A^{2} - 1} ((A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N))$
70	5 69	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} (M + N)) + \sqrt{A^{2} - 1} (A Y_{rm} (M + N)) = (A X_{rm} M) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) + \sqrt{A^{2} - 1} ((A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N))$
71		rmspecsqrtnq	$⊢ A \in ℤ_{\geq 2} \to \sqrt{A^{2} - 1} \in (ℂ ∖ ℚ)$
72	71	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to \sqrt{A^{2} - 1} \in (ℂ ∖ ℚ)$
73		nn0ssq	$⊢ ℕ_{0} \subseteq ℚ$
74	30 1 3	fovrnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A X_{rm} (M + N) \in ℕ_{0}$
75	73 74	sseldi	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A X_{rm} (M + N) \in ℚ$
76	34 1 3	fovrnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} (M + N) \in ℤ$
77	12 76	sseldi	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} (M + N) \in ℚ$
78	73 31	sseldi	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A X_{rm} M \in ℚ$
79	73 38	sseldi	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A X_{rm} N \in ℚ$
80		qmulcl	$⊢ (A X_{rm} M \in ℚ \land A X_{rm} N \in ℚ) \to (A X_{rm} M) (A X_{rm} N) \in ℚ$
81	78 79 80	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) (A X_{rm} N) \in ℚ$
82	12 35	sseldi	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} M \in ℚ$
83	12 40	sseldi	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} N \in ℚ$
84		qmulcl	$⊢ (A Y_{rm} M \in ℚ \land A Y_{rm} N \in ℚ) \to (A Y_{rm} M) (A Y_{rm} N) \in ℚ$
85	82 83 84	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A Y_{rm} M) (A Y_{rm} N) \in ℚ$
86		qmulcl	$⊢ (A^{2} - 1 \in ℚ \land (A Y_{rm} M) (A Y_{rm} N) \in ℚ) \to (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) \in ℚ$
87	17 85 86	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) \in ℚ$
88		qaddcl	$⊢ ((A X_{rm} M) (A X_{rm} N) \in ℚ \land (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) \in ℚ) \to (A X_{rm} M) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) \in ℚ$
89	81 87 88	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) \in ℚ$
90		qmulcl	$⊢ (A Y_{rm} M \in ℚ \land A X_{rm} N \in ℚ) \to (A Y_{rm} M) (A X_{rm} N) \in ℚ$
91	82 79 90	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A Y_{rm} M) (A X_{rm} N) \in ℚ$
92		qmulcl	$⊢ (A X_{rm} M \in ℚ \land A Y_{rm} N \in ℚ) \to (A X_{rm} M) (A Y_{rm} N) \in ℚ$
93	78 83 92	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) (A Y_{rm} N) \in ℚ$
94		qaddcl	$⊢ ((A Y_{rm} M) (A X_{rm} N) \in ℚ \land (A X_{rm} M) (A Y_{rm} N) \in ℚ) \to (A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N) \in ℚ$
95	91 93 94	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N) \in ℚ$
96		qirropth	$⊢ (\sqrt{A^{2} - 1} \in (ℂ ∖ ℚ) \land (A X_{rm} (M + N) \in ℚ \land A Y_{rm} (M + N) \in ℚ) \land ((A X_{rm} M) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) \in ℚ \land (A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N) \in ℚ)) \to ((A X_{rm} (M + N)) + \sqrt{A^{2} - 1} (A Y_{rm} (M + N)) = (A X_{rm} M) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) + \sqrt{A^{2} - 1} ((A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N)) \leftrightarrow (A X_{rm} (M + N) = (A X_{rm} M) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) \land A Y_{rm} (M + N) = (A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N)))$
97	72 75 77 89 95 96	syl122anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to ((A X_{rm} (M + N)) + \sqrt{A^{2} - 1} (A Y_{rm} (M + N)) = (A X_{rm} M) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) + \sqrt{A^{2} - 1} ((A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N)) \leftrightarrow (A X_{rm} (M + N) = (A X_{rm} M) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) \land A Y_{rm} (M + N) = (A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N)))$
98	70 97	mpbid	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} (M + N) = (A X_{rm} M) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} M) (A Y_{rm} N) \land A Y_{rm} (M + N) = (A Y_{rm} M) (A X_{rm} N) + (A X_{rm} M) (A Y_{rm} N))$

Metamath Proof Explorer

Theorem rmxyadd

Proof