Metamath Proof Explorer

Theorem jm2.22

Description: Lemma for jm2.20nn . Applying binomial theorem and taking irrational part. (Contributed by Stefan O'Rear, 26-Sep-2014) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Assertion jm2.22 
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A rmY ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nn0z 
 |-  ( J e. NN0 -> J e. ZZ )
2 jm2.21 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. ZZ ) -> ( ( A rmX ( N x. J ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY ( N x. J ) ) ) ) = ( ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) ^ J ) )
3 1 2 syl3an3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( A rmX ( N x. J ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY ( N x. J ) ) ) ) = ( ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) ^ J ) )
4 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
5 4 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
6 5 3adant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A rmX N ) e. NN0 )
7 6 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A rmX N ) e. CC )
8 eluzelz 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. ZZ )
9 zsqcl 
 |-  ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
10 peano2zm 
 |-  ( ( A ^ 2 ) e. ZZ -> ( ( A ^ 2 ) - 1 ) e. ZZ )
11 8 9 10 3syl 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ZZ )
12 11 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( A ^ 2 ) - 1 ) e. ZZ )
13 12 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( A ^ 2 ) - 1 ) e. CC )
14 13 sqrtcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. CC )
15 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
16 15 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
17 16 3adant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A rmY N ) e. ZZ )
18 17 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A rmY N ) e. CC )
19 14 18 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) e. CC )
20 simp3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> J e. NN0 )
21 binom 
 |-  ( ( ( A rmX N ) e. CC /\ ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) e. CC /\ J e. NN0 ) -> ( ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) ^ J ) = sum_ i e. ( 0 ... J ) ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) )
22 7 19 20 21 syl3anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) ^ J ) = sum_ i e. ( 0 ... J ) ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) )
23 rabnc 
 |-  ( { x e. ( 0 ... J ) | 2 || x } i^i { x e. ( 0 ... J ) | -. 2 || x } ) = (/)
24 23 a1i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( { x e. ( 0 ... J ) | 2 || x } i^i { x e. ( 0 ... J ) | -. 2 || x } ) = (/) )
25 rabxm 
 |-  ( 0 ... J ) = ( { x e. ( 0 ... J ) | 2 || x } u. { x e. ( 0 ... J ) | -. 2 || x } )
26 25 a1i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( 0 ... J ) = ( { x e. ( 0 ... J ) | 2 || x } u. { x e. ( 0 ... J ) | -. 2 || x } ) )
27 fzfid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( 0 ... J ) e. Fin )
28 simpl3 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> J e. NN0 )
29 elfzelz 
 |-  ( i e. ( 0 ... J ) -> i e. ZZ )
30 29 adantl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> i e. ZZ )
31 bccl 
 |-  ( ( J e. NN0 /\ i e. ZZ ) -> ( J _C i ) e. NN0 )
32 31 nn0zd 
 |-  ( ( J e. NN0 /\ i e. ZZ ) -> ( J _C i ) e. ZZ )
33 28 30 32 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( J _C i ) e. ZZ )
34 33 zcnd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( J _C i ) e. CC )
35 6 nn0zd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A rmX N ) e. ZZ )
36 35 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( A rmX N ) e. ZZ )
37 36 zcnd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( A rmX N ) e. CC )
38 fznn0sub 
 |-  ( i e. ( 0 ... J ) -> ( J - i ) e. NN0 )
39 38 adantl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( J - i ) e. NN0 )
40 37 39 expcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( A rmX N ) ^ ( J - i ) ) e. CC )
41 12 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( A ^ 2 ) - 1 ) e. ZZ )
42 41 zcnd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( A ^ 2 ) - 1 ) e. CC )
43 42 sqrtcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. CC )
44 17 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( A rmY N ) e. ZZ )
45 44 zcnd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( A rmY N ) e. CC )
46 43 45 mulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) e. CC )
47 elfznn0 
 |-  ( i e. ( 0 ... J ) -> i e. NN0 )
48 47 adantl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> i e. NN0 )
49 46 48 expcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) e. CC )
50 40 49 mulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) e. CC )
51 34 50 mulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) e. CC )
52 24 26 27 51 fsumsplit 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. ( 0 ... J ) ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) = ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) + sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) ) )
53 fzfi 
 |-  ( 0 ... J ) e. Fin
54 ssrab2 
 |-  { x e. ( 0 ... J ) | -. 2 || x } C_ ( 0 ... J )
55 ssfi 
 |-  ( ( ( 0 ... J ) e. Fin /\ { x e. ( 0 ... J ) | -. 2 || x } C_ ( 0 ... J ) ) -> { x e. ( 0 ... J ) | -. 2 || x } e. Fin )
56 53 54 55 mp2an 
 |-  { x e. ( 0 ... J ) | -. 2 || x } e. Fin
57 56 a1i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> { x e. ( 0 ... J ) | -. 2 || x } e. Fin )
58 breq2 
 |-  ( x = i -> ( 2 || x <-> 2 || i ) )
59 58 notbid 
 |-  ( x = i -> ( -. 2 || x <-> -. 2 || i ) )
60 59 elrab 
 |-  ( i e. { x e. ( 0 ... J ) | -. 2 || x } <-> ( i e. ( 0 ... J ) /\ -. 2 || i ) )
61 34 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( J _C i ) e. CC )
62 40 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( A rmX N ) ^ ( J - i ) ) e. CC )
63 zexpcl 
 |-  ( ( ( A rmY N ) e. ZZ /\ i e. NN0 ) -> ( ( A rmY N ) ^ i ) e. ZZ )
64 17 47 63 syl2an 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( A rmY N ) ^ i ) e. ZZ )
65 64 zcnd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( A rmY N ) ^ i ) e. CC )
66 65 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( A rmY N ) ^ i ) e. CC )
67 42 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( A ^ 2 ) - 1 ) e. CC )
68 29 adantr 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> i e. ZZ )
69 simpr 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> -. 2 || i )
70 1zzd 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 1 e. ZZ )
71 n2dvds1 
 |-  -. 2 || 1
72 71 a1i 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> -. 2 || 1 )
73 omoe 
 |-  ( ( ( i e. ZZ /\ -. 2 || i ) /\ ( 1 e. ZZ /\ -. 2 || 1 ) ) -> 2 || ( i - 1 ) )
74 68 69 70 72 73 syl22anc 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 2 || ( i - 1 ) )
75 2z 
 |-  2 e. ZZ
76 75 a1i 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 2 e. ZZ )
77 2ne0 
 |-  2 =/= 0
78 77 a1i 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 2 =/= 0 )
79 peano2zm 
 |-  ( i e. ZZ -> ( i - 1 ) e. ZZ )
80 29 79 syl 
 |-  ( i e. ( 0 ... J ) -> ( i - 1 ) e. ZZ )
81 80 adantr 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> ( i - 1 ) e. ZZ )
82 dvdsval2 
 |-  ( ( 2 e. ZZ /\ 2 =/= 0 /\ ( i - 1 ) e. ZZ ) -> ( 2 || ( i - 1 ) <-> ( ( i - 1 ) / 2 ) e. ZZ ) )
83 76 78 81 82 syl3anc 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> ( 2 || ( i - 1 ) <-> ( ( i - 1 ) / 2 ) e. ZZ ) )
84 74 83 mpbid 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> ( ( i - 1 ) / 2 ) e. ZZ )
85 80 zred 
 |-  ( i e. ( 0 ... J ) -> ( i - 1 ) e. RR )
86 85 adantr 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> ( i - 1 ) e. RR )
87 dvds0 
 |-  ( 2 e. ZZ -> 2 || 0 )
88 75 87 ax-mp 
 |-  2 || 0
89 breq2 
 |-  ( i = 0 -> ( 2 || i <-> 2 || 0 ) )
90 88 89 mpbiri 
 |-  ( i = 0 -> 2 || i )
91 90 con3i 
 |-  ( -. 2 || i -> -. i = 0 )
92 91 adantl 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> -. i = 0 )
93 47 adantr 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> i e. NN0 )
94 elnn0 
 |-  ( i e. NN0 <-> ( i e. NN \/ i = 0 ) )
95 93 94 sylib 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> ( i e. NN \/ i = 0 ) )
96 orel2 
 |-  ( -. i = 0 -> ( ( i e. NN \/ i = 0 ) -> i e. NN ) )
97 92 95 96 sylc 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> i e. NN )
98 nnm1nn0 
 |-  ( i e. NN -> ( i - 1 ) e. NN0 )
99 97 98 syl 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> ( i - 1 ) e. NN0 )
100 99 nn0ge0d 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 0 <_ ( i - 1 ) )
101 2re 
 |-  2 e. RR
102 101 a1i 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 2 e. RR )
103 2pos 
 |-  0 < 2
104 103 a1i 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 0 < 2 )
105 divge0 
 |-  ( ( ( ( i - 1 ) e. RR /\ 0 <_ ( i - 1 ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( ( i - 1 ) / 2 ) )
106 86 100 102 104 105 syl22anc 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 0 <_ ( ( i - 1 ) / 2 ) )
107 elnn0z 
 |-  ( ( ( i - 1 ) / 2 ) e. NN0 <-> ( ( ( i - 1 ) / 2 ) e. ZZ /\ 0 <_ ( ( i - 1 ) / 2 ) ) )
108 84 106 107 sylanbrc 
 |-  ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> ( ( i - 1 ) / 2 ) e. NN0 )
109 108 adantl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( i - 1 ) / 2 ) e. NN0 )
110 67 109 expcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) e. CC )
111 66 110 mulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) e. CC )
112 62 111 mulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) e. CC )
113 61 112 mulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) e. CC )
114 60 113 sylan2b 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. { x e. ( 0 ... J ) | -. 2 || x } ) -> ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) e. CC )
115 57 14 114 fsummulc2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) = sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) )
116 43 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. CC )
117 116 61 112 mul12d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) = ( ( J _C i ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) )
118 116 62 111 mul12d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) = ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) )
119 43 48 expcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) e. CC )
120 119 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) e. CC )
121 66 120 mulcomd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A rmY N ) ^ i ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) ) = ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) x. ( ( A rmY N ) ^ i ) ) )
122 116 66 110 mul12d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) = ( ( ( A rmY N ) ^ i ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) )
123 2nn0 
 |-  2 e. NN0
124 123 a1i 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> 2 e. NN0 )
125 116 109 124 expmuld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ ( 2 x. ( ( i - 1 ) / 2 ) ) ) = ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) ^ ( ( i - 1 ) / 2 ) ) )
126 80 zcnd 
 |-  ( i e. ( 0 ... J ) -> ( i - 1 ) e. CC )
127 126 ad2antrl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( i - 1 ) e. CC )
128 2cnd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> 2 e. CC )
129 77 a1i 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> 2 =/= 0 )
130 127 128 129 divcan2d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( 2 x. ( ( i - 1 ) / 2 ) ) = ( i - 1 ) )
131 130 oveq2d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ ( 2 x. ( ( i - 1 ) / 2 ) ) ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ ( i - 1 ) ) )
132 67 sqsqrtd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) = ( ( A ^ 2 ) - 1 ) )
133 132 oveq1d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) ^ ( ( i - 1 ) / 2 ) ) = ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) )
134 125 131 133 3eqtr3rd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ ( i - 1 ) ) )
135 134 oveq1d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) x. ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) = ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ ( i - 1 ) ) x. ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
136 116 110 mulcomd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) = ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) x. ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
137 97 adantl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> i e. NN )
138 expm1t 
 |-  ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. CC /\ i e. NN ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) = ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ ( i - 1 ) ) x. ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
139 116 137 138 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) = ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ ( i - 1 ) ) x. ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
140 135 136 139 3eqtr4d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) )
141 140 oveq2d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A rmY N ) ^ i ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) = ( ( ( A rmY N ) ^ i ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) ) )
142 122 141 eqtrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) = ( ( ( A rmY N ) ^ i ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) ) )
143 43 45 48 mulexpd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) = ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) x. ( ( A rmY N ) ^ i ) ) )
144 143 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) = ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) x. ( ( A rmY N ) ^ i ) ) )
145 121 142 144 3eqtr4d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) = ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) )
146 145 oveq2d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) = ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) )
147 118 146 eqtrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) = ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) )
148 147 oveq2d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( J _C i ) x. ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) = ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) )
149 117 148 eqtrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) = ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) )
150 60 149 sylan2b 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. { x e. ( 0 ... J ) | -. 2 || x } ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) = ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) )
151 150 sumeq2dv 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) = sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) )
152 115 151 eqtr2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) )
153 152 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) + sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) ) = ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) ) )
154 52 153 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. ( 0 ... J ) ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) = ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) ) )
155 3 22 154 3eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( A rmX ( N x. J ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY ( N x. J ) ) ) ) = ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) ) )
156 rmspecsqrtnq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
157 156 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
158 nn0ssq 
 |-  NN0 C_ QQ
159 simp1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> A e. ( ZZ>= ` 2 ) )
160 simp2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> N e. ZZ )
161 1 3ad2ant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> J e. ZZ )
162 160 161 zmulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( N x. J ) e. ZZ )
163 4 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N x. J ) e. ZZ ) -> ( A rmX ( N x. J ) ) e. NN0 )
164 159 162 163 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A rmX ( N x. J ) ) e. NN0 )
165 158 164 sseldi 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A rmX ( N x. J ) ) e. QQ )
166 zssq 
 |-  ZZ C_ QQ
167 15 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N x. J ) e. ZZ ) -> ( A rmY ( N x. J ) ) e. ZZ )
168 159 162 167 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A rmY ( N x. J ) ) e. ZZ )
169 166 168 sseldi 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A rmY ( N x. J ) ) e. QQ )
170 ssrab2 
 |-  { x e. ( 0 ... J ) | 2 || x } C_ ( 0 ... J )
171 ssfi 
 |-  ( ( ( 0 ... J ) e. Fin /\ { x e. ( 0 ... J ) | 2 || x } C_ ( 0 ... J ) ) -> { x e. ( 0 ... J ) | 2 || x } e. Fin )
172 53 170 171 mp2an 
 |-  { x e. ( 0 ... J ) | 2 || x } e. Fin
173 172 a1i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> { x e. ( 0 ... J ) | 2 || x } e. Fin )
174 58 elrab 
 |-  ( i e. { x e. ( 0 ... J ) | 2 || x } <-> ( i e. ( 0 ... J ) /\ 2 || i ) )
175 33 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( J _C i ) e. ZZ )
176 zexpcl 
 |-  ( ( ( A rmX N ) e. ZZ /\ ( J - i ) e. NN0 ) -> ( ( A rmX N ) ^ ( J - i ) ) e. ZZ )
177 36 39 176 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( A rmX N ) ^ ( J - i ) ) e. ZZ )
178 177 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( A rmX N ) ^ ( J - i ) ) e. ZZ )
179 43 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. CC )
180 45 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( A rmY N ) e. CC )
181 47 ad2antrl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> i e. NN0 )
182 179 180 181 mulexpd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) = ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) x. ( ( A rmY N ) ^ i ) ) )
183 29 zcnd 
 |-  ( i e. ( 0 ... J ) -> i e. CC )
184 183 adantl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> i e. CC )
185 2cnd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> 2 e. CC )
186 77 a1i 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> 2 =/= 0 )
187 184 185 186 divcan2d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( 2 x. ( i / 2 ) ) = i )
188 187 eqcomd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> i = ( 2 x. ( i / 2 ) ) )
189 188 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> i = ( 2 x. ( i / 2 ) ) )
190 189 oveq2d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ ( 2 x. ( i / 2 ) ) ) )
191 75 a1i 
 |-  ( i e. NN0 -> 2 e. ZZ )
192 77 a1i 
 |-  ( i e. NN0 -> 2 =/= 0 )
193 nn0z 
 |-  ( i e. NN0 -> i e. ZZ )
194 dvdsval2 
 |-  ( ( 2 e. ZZ /\ 2 =/= 0 /\ i e. ZZ ) -> ( 2 || i <-> ( i / 2 ) e. ZZ ) )
195 191 192 193 194 syl3anc 
 |-  ( i e. NN0 -> ( 2 || i <-> ( i / 2 ) e. ZZ ) )
196 195 biimpa 
 |-  ( ( i e. NN0 /\ 2 || i ) -> ( i / 2 ) e. ZZ )
197 nn0re 
 |-  ( i e. NN0 -> i e. RR )
198 197 adantr 
 |-  ( ( i e. NN0 /\ 2 || i ) -> i e. RR )
199 nn0ge0 
 |-  ( i e. NN0 -> 0 <_ i )
200 199 adantr 
 |-  ( ( i e. NN0 /\ 2 || i ) -> 0 <_ i )
201 101 a1i 
 |-  ( ( i e. NN0 /\ 2 || i ) -> 2 e. RR )
202 103 a1i 
 |-  ( ( i e. NN0 /\ 2 || i ) -> 0 < 2 )
203 divge0 
 |-  ( ( ( i e. RR /\ 0 <_ i ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( i / 2 ) )
204 198 200 201 202 203 syl22anc 
 |-  ( ( i e. NN0 /\ 2 || i ) -> 0 <_ ( i / 2 ) )
205 elnn0z 
 |-  ( ( i / 2 ) e. NN0 <-> ( ( i / 2 ) e. ZZ /\ 0 <_ ( i / 2 ) ) )
206 196 204 205 sylanbrc 
 |-  ( ( i e. NN0 /\ 2 || i ) -> ( i / 2 ) e. NN0 )
207 47 206 sylan 
 |-  ( ( i e. ( 0 ... J ) /\ 2 || i ) -> ( i / 2 ) e. NN0 )
208 207 adantl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( i / 2 ) e. NN0 )
209 123 a1i 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> 2 e. NN0 )
210 179 208 209 expmuld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ ( 2 x. ( i / 2 ) ) ) = ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) ^ ( i / 2 ) ) )
211 42 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( A ^ 2 ) - 1 ) e. CC )
212 211 sqsqrtd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) = ( ( A ^ 2 ) - 1 ) )
213 212 oveq1d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) ^ ( i / 2 ) ) = ( ( ( A ^ 2 ) - 1 ) ^ ( i / 2 ) ) )
214 190 210 213 3eqtrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) = ( ( ( A ^ 2 ) - 1 ) ^ ( i / 2 ) ) )
215 214 oveq1d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ i ) x. ( ( A rmY N ) ^ i ) ) = ( ( ( ( A ^ 2 ) - 1 ) ^ ( i / 2 ) ) x. ( ( A rmY N ) ^ i ) ) )
216 182 215 eqtrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) = ( ( ( ( A ^ 2 ) - 1 ) ^ ( i / 2 ) ) x. ( ( A rmY N ) ^ i ) ) )
217 zexpcl 
 |-  ( ( ( ( A ^ 2 ) - 1 ) e. ZZ /\ ( i / 2 ) e. NN0 ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( i / 2 ) ) e. ZZ )
218 12 207 217 syl2an 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( i / 2 ) ) e. ZZ )
219 64 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( A rmY N ) ^ i ) e. ZZ )
220 218 219 zmulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( ( A ^ 2 ) - 1 ) ^ ( i / 2 ) ) x. ( ( A rmY N ) ^ i ) ) e. ZZ )
221 216 220 eqeltrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) e. ZZ )
222 178 221 zmulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) e. ZZ )
223 175 222 zmulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) e. ZZ )
224 174 223 sylan2b 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. { x e. ( 0 ... J ) | 2 || x } ) -> ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) e. ZZ )
225 173 224 fsumzcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) e. ZZ )
226 166 225 sseldi 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) e. QQ )
227 33 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( J _C i ) e. ZZ )
228 177 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( A rmX N ) ^ ( J - i ) ) e. ZZ )
229 64 adantrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( A rmY N ) ^ i ) e. ZZ )
230 zexpcl 
 |-  ( ( ( ( A ^ 2 ) - 1 ) e. ZZ /\ ( ( i - 1 ) / 2 ) e. NN0 ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) e. ZZ )
231 12 108 230 syl2an 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) e. ZZ )
232 229 231 zmulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) e. ZZ )
233 228 232 zmulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) e. ZZ )
234 227 233 zmulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) e. ZZ )
235 60 234 sylan2b 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. { x e. ( 0 ... J ) | -. 2 || x } ) -> ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) e. ZZ )
236 57 235 fsumzcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) e. ZZ )
237 166 236 sseldi 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) e. QQ )
238 qirropth 
 |-  ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) /\ ( ( A rmX ( N x. J ) ) e. QQ /\ ( A rmY ( N x. J ) ) e. QQ ) /\ ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) e. QQ /\ sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) e. QQ ) ) -> ( ( ( A rmX ( N x. J ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY ( N x. J ) ) ) ) = ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) ) <-> ( ( A rmX ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) /\ ( A rmY ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) ) )
239 157 165 169 226 237 238 syl122anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( ( A rmX ( N x. J ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY ( N x. J ) ) ) ) = ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) ) <-> ( ( A rmX ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) /\ ( A rmY ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) ) )
240 155 239 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( A rmX ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ i ) ) ) /\ ( A rmY ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) )
241 240 simprd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A rmY ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A rmX N ) ^ ( J - i ) ) x. ( ( ( A rmY N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) )