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 
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX ( M + N ) ) = ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) ) /\ ( A rmY ( M + N ) ) = ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> A e. ( ZZ>= ` 2 ) )
2 zaddcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )
3 2 3adant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )
4 rmxyval 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M + N ) e. ZZ ) -> ( ( A rmX ( M + N ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY ( M + N ) ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ ( M + N ) ) )
5 1 3 4 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX ( M + N ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY ( M + N ) ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ ( M + N ) ) )
6 eluzelz 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. ZZ )
7 6 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> A e. ZZ )
8 7 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> A e. CC )
9 zq 
 |-  ( A e. ZZ -> A e. QQ )
10 qsqcl 
 |-  ( A e. QQ -> ( A ^ 2 ) e. QQ )
11 7 9 10 3syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A ^ 2 ) e. QQ )
12 zssq 
 |-  ZZ C_ QQ
13 1z 
 |-  1 e. ZZ
14 12 13 sselii 
 |-  1 e. QQ
15 14 a1i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> 1 e. QQ )
16 qsubcl 
 |-  ( ( ( A ^ 2 ) e. QQ /\ 1 e. QQ ) -> ( ( A ^ 2 ) - 1 ) e. QQ )
17 11 15 16 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A ^ 2 ) - 1 ) e. QQ )
18 qcn 
 |-  ( ( ( A ^ 2 ) - 1 ) e. QQ -> ( ( A ^ 2 ) - 1 ) e. CC )
19 17 18 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A ^ 2 ) - 1 ) e. CC )
20 19 sqrtcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. CC )
21 8 20 addcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. CC )
22 rmbaserp 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. RR+ )
23 22 rpne0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) =/= 0 )
24 23 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) =/= 0 )
25 simp2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> M e. ZZ )
26 simp3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> N e. ZZ )
27 expaddz 
 |-  ( ( ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. CC /\ ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ ( M + N ) ) = ( ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ M ) x. ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) ) )
28 21 24 25 26 27 syl22anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ ( M + N ) ) = ( ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ M ) x. ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) ) )
29 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
30 29 a1i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0 )
31 30 1 25 fovcdmd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmX M ) e. NN0 )
32 31 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmX M ) e. CC )
33 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
34 33 a1i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ )
35 34 1 25 fovcdmd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmY M ) e. ZZ )
36 35 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmY M ) e. CC )
37 20 36 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) e. CC )
38 30 1 26 fovcdmd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
39 38 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmX N ) e. CC )
40 34 1 26 fovcdmd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
41 40 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmY N ) e. CC )
42 20 41 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) e. CC )
43 32 37 39 42 muladdd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( A rmX M ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) x. ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) ) = ( ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) ) + ( ( ( A rmX M ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) + ( ( A rmX N ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) ) ) )
44 rmxyval 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( A rmX M ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ M ) )
45 1 25 44 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX M ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ M ) )
46 rmxyval 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) )
47 1 26 46 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) )
48 45 47 oveq12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( A rmX M ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) x. ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) ) = ( ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ M ) x. ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) ) )
49 43 48 eqtr3d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) ) + ( ( ( A rmX M ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) + ( ( A rmX N ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) ) ) = ( ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ M ) x. ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) ) )
50 20 41 20 36 mul4d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) = ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) x. ( ( A rmY N ) x. ( A rmY M ) ) ) )
51 19 msqsqrtd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) = ( ( A ^ 2 ) - 1 ) )
52 41 36 mulcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmY N ) x. ( A rmY M ) ) = ( ( A rmY M ) x. ( A rmY N ) ) )
53 51 52 oveq12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) x. ( ( A rmY N ) x. ( A rmY M ) ) ) = ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) )
54 50 53 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) = ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) )
55 54 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) ) = ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) ) )
56 32 20 41 mul12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX M ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( A rmX M ) x. ( A rmY N ) ) ) )
57 39 20 36 mul12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX N ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( A rmX N ) x. ( A rmY M ) ) ) )
58 56 57 oveq12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( A rmX M ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) + ( ( A rmX N ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) ) = ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( A rmX M ) x. ( A rmY N ) ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( A rmX N ) x. ( A rmY M ) ) ) ) )
59 32 41 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX M ) x. ( A rmY N ) ) e. CC )
60 39 36 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX N ) x. ( A rmY M ) ) e. CC )
61 20 59 60 adddid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmX M ) x. ( A rmY N ) ) + ( ( A rmX N ) x. ( A rmY M ) ) ) ) = ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( A rmX M ) x. ( A rmY N ) ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( A rmX N ) x. ( A rmY M ) ) ) ) )
62 59 60 addcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( A rmX M ) x. ( A rmY N ) ) + ( ( A rmX N ) x. ( A rmY M ) ) ) = ( ( ( A rmX N ) x. ( A rmY M ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) )
63 39 36 mulcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX N ) x. ( A rmY M ) ) = ( ( A rmY M ) x. ( A rmX N ) ) )
64 63 oveq1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( A rmX N ) x. ( A rmY M ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) = ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) )
65 62 64 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( A rmX M ) x. ( A rmY N ) ) + ( ( A rmX N ) x. ( A rmY M ) ) ) = ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) )
66 65 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmX M ) x. ( A rmY N ) ) + ( ( A rmX N ) x. ( A rmY M ) ) ) ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) ) )
67 58 61 66 3eqtr2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( A rmX M ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) + ( ( A rmX N ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) ) )
68 55 67 oveq12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) ) + ( ( ( A rmX M ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) + ( ( A rmX N ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY M ) ) ) ) ) = ( ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) ) ) )
69 28 49 68 3eqtr2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ ( M + N ) ) = ( ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) ) ) )
70 5 69 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX ( M + N ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY ( M + N ) ) ) ) = ( ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) ) ) )
71 rmspecsqrtnq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
72 71 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
73 nn0ssq 
 |-  NN0 C_ QQ
74 30 1 3 fovcdmd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmX ( M + N ) ) e. NN0 )
75 73 74 sselid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmX ( M + N ) ) e. QQ )
76 34 1 3 fovcdmd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmY ( M + N ) ) e. ZZ )
77 12 76 sselid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmY ( M + N ) ) e. QQ )
78 73 31 sselid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmX M ) e. QQ )
79 73 38 sselid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmX N ) e. QQ )
80 qmulcl 
 |-  ( ( ( A rmX M ) e. QQ /\ ( A rmX N ) e. QQ ) -> ( ( A rmX M ) x. ( A rmX N ) ) e. QQ )
81 78 79 80 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX M ) x. ( A rmX N ) ) e. QQ )
82 12 35 sselid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmY M ) e. QQ )
83 12 40 sselid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmY N ) e. QQ )
84 qmulcl 
 |-  ( ( ( A rmY M ) e. QQ /\ ( A rmY N ) e. QQ ) -> ( ( A rmY M ) x. ( A rmY N ) ) e. QQ )
85 82 83 84 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmY M ) x. ( A rmY N ) ) e. QQ )
86 qmulcl 
 |-  ( ( ( ( A ^ 2 ) - 1 ) e. QQ /\ ( ( A rmY M ) x. ( A rmY N ) ) e. QQ ) -> ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) e. QQ )
87 17 85 86 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) e. QQ )
88 qaddcl 
 |-  ( ( ( ( A rmX M ) x. ( A rmX N ) ) e. QQ /\ ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) e. QQ ) -> ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) ) e. QQ )
89 81 87 88 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) ) e. QQ )
90 qmulcl 
 |-  ( ( ( A rmY M ) e. QQ /\ ( A rmX N ) e. QQ ) -> ( ( A rmY M ) x. ( A rmX N ) ) e. QQ )
91 82 79 90 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmY M ) x. ( A rmX N ) ) e. QQ )
92 qmulcl 
 |-  ( ( ( A rmX M ) e. QQ /\ ( A rmY N ) e. QQ ) -> ( ( A rmX M ) x. ( A rmY N ) ) e. QQ )
93 78 83 92 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX M ) x. ( A rmY N ) ) e. QQ )
94 qaddcl 
 |-  ( ( ( ( A rmY M ) x. ( A rmX N ) ) e. QQ /\ ( ( A rmX M ) x. ( A rmY N ) ) e. QQ ) -> ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) e. QQ )
95 91 93 94 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) e. QQ )
96 qirropth 
 |-  ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) /\ ( ( A rmX ( M + N ) ) e. QQ /\ ( A rmY ( M + N ) ) e. QQ ) /\ ( ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) ) e. QQ /\ ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) e. QQ ) ) -> ( ( ( A rmX ( M + N ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY ( M + N ) ) ) ) = ( ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) ) ) <-> ( ( A rmX ( M + N ) ) = ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) ) /\ ( A rmY ( M + N ) ) = ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) ) ) )
97 72 75 77 89 95 96 syl122anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( A rmX ( M + N ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY ( M + N ) ) ) ) = ( ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) ) ) <-> ( ( A rmX ( M + N ) ) = ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) ) /\ ( A rmY ( M + N ) ) = ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) ) ) )
98 70 97 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX ( M + N ) ) = ( ( ( A rmX M ) x. ( A rmX N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY N ) ) ) ) /\ ( A rmY ( M + N ) ) = ( ( ( A rmY M ) x. ( A rmX N ) ) + ( ( A rmX M ) x. ( A rmY N ) ) ) ) )