# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({A}{X}_{\mathrm{rm}}\left({M}+{N}\right)=\left({A}{X}_{\mathrm{rm}}{M}\right)\left({A}{X}_{\mathrm{rm}}{N}\right)+\left({{A}}^{2}-1\right)\left({A}{Y}_{\mathrm{rm}}{M}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)\wedge {A}{Y}_{\mathrm{rm}}\left({M}+{N}\right)=\left({A}{Y}_{\mathrm{rm}}{M}\right)\left({A}{X}_{\mathrm{rm}}{N}\right)+\left({A}{X}_{\mathrm{rm}}{M}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)\right)$

### Proof

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