Theorem jm2.22 29363

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

Assertion

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

Distinct variable groups:   A, i, x   i, N, x   i, J, x

Proof of Theorem jm2.22

Step	Hyp	Ref	Expression
1		nn0z 10684	. . . . 5 |- ( J e. NN0 -> J e. ZZ )
2		jm2.21 29362	. . . . 5 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. ZZ ) -> ( ( A Xrm ( N x. J ) ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm ( N x. J ) ) ) ) = ( ( ( A Xrm N ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ) ^ J ) )
3	1, 2	syl3an3 1253	. . . 4 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( A Xrm ( N x. J ) ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm ( N x. J ) ) ) ) = ( ( ( A Xrm N ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ) ^ J ) )
4		frmx 29273	. . . . . . . 8 |- Xrm : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
5	4	fovcl 6210	. . . . . . 7 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm N ) e. NN0 )
6	5	3adant3 1008	. . . . . 6 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A Xrm N ) e. NN0 )
7	6	nn0cnd 10653	. . . . 5 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A Xrm N ) e. CC )
8		eluzelz 10885	. . . . . . . . . 10 |- ( A e. ( ZZ>= ` 2 ) -> A e. ZZ )
9		zsqcl 11951	. . . . . . . . . 10 |- ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
10		peano2zm 10703	. . . . . . . . . 10 |- ( ( A ^ 2 ) e. ZZ -> ( ( A ^ 2 ) - 1 ) e. ZZ )
11	8, 9, 10	3syl 20	. . . . . . . . 9 |- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ZZ )
12	11	3ad2ant1 1009	. . . . . . . 8 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( A ^ 2 ) - 1 ) e. ZZ )
13	12	zcnd 10763	. . . . . . 7 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( A ^ 2 ) - 1 ) e. CC )
14	13	sqrcld 12938	. . . . . 6 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( sqr ` ( ( A ^ 2 ) - 1 ) ) e. CC )
15		frmy 29274	. . . . . . . . 9 |- Yrm : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
16	15	fovcl 6210	. . . . . . . 8 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm N ) e. ZZ )
17	16	3adant3 1008	. . . . . . 7 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A Yrm N ) e. ZZ )
18	17	zcnd 10763	. . . . . 6 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A Yrm N ) e. CC )
19	14, 18	mulcld 9421	. . . . 5 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) e. CC )
20		simp3 990	. . . . 5 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> J e. NN0 )
21		binom 13308	. . . . 5 |- ( ( ( A Xrm N ) e. CC /\ ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) e. CC /\ J e. NN0 ) -> ( ( ( A Xrm N ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ) ^ J ) = sum_ i e. ( 0 ... J ) ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) )
22	7, 19, 20, 21	syl3anc 1218	. . . 4 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( ( A Xrm N ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ) ^ J ) = sum_ i e. ( 0 ... J ) ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) )
23		rabnc 3676	. . . . . . 7 |- ( { x e. ( 0 ... J ) | 2 || x } i^i { x e. ( 0 ... J ) | -. 2 || x } ) = (/)
24	23	a1i 11	. . . . . 6 |- ( ( 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 3675	. . . . . . 7 |- ( 0 ... J ) = ( { x e. ( 0 ... J ) | 2 || x } u. { x e. ( 0 ... J ) | -. 2 || x } )
26	25	a1i 11	. . . . . 6 |- ( ( 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 11810	. . . . . 6 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( 0 ... J ) e. Fin )
28		simpl3 993	. . . . . . . . 9 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> J e. NN0 )
29		elfzelz 11468	. . . . . . . . . 10 |- ( i e. ( 0 ... J ) -> i e. ZZ )
30	29	adantl 466	. . . . . . . . 9 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> i e. ZZ )
31		bccl 12113	. . . . . . . . . 10 |- ( ( J e. NN0 /\ i e. ZZ ) -> ( J _C i ) e. NN0 )
32	31	nn0zd 10760	. . . . . . . . 9 |- ( ( J e. NN0 /\ i e. ZZ ) -> ( J _C i ) e. ZZ )
33	28, 30, 32	syl2anc 661	. . . . . . . 8 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( J _C i ) e. ZZ )
34	33	zcnd 10763	. . . . . . 7 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( J _C i ) e. CC )
35	6	nn0zd 10760	. . . . . . . . . . 11 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A Xrm N ) e. ZZ )
36	35	adantr 465	. . . . . . . . . 10 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( A Xrm N ) e. ZZ )
37	36	zcnd 10763	. . . . . . . . 9 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( A Xrm N ) e. CC )
38		fznn0sub 11502	. . . . . . . . . 10 |- ( i e. ( 0 ... J ) -> ( J - i ) e. NN0 )
39	38	adantl 466	. . . . . . . . 9 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( J - i ) e. NN0 )
40	37, 39	expcld 12023	. . . . . . . 8 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( A Xrm N ) ^ ( J - i ) ) e. CC )
41	12	adantr 465	. . . . . . . . . . . 12 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( A ^ 2 ) - 1 ) e. ZZ )
42	41	zcnd 10763	. . . . . . . . . . 11 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( A ^ 2 ) - 1 ) e. CC )
43	42	sqrcld 12938	. . . . . . . . . 10 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( sqr ` ( ( A ^ 2 ) - 1 ) ) e. CC )
44	17	adantr 465	. . . . . . . . . . 11 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( A Yrm N ) e. ZZ )
45	44	zcnd 10763	. . . . . . . . . 10 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( A Yrm N ) e. CC )
46	43, 45	mulcld 9421	. . . . . . . . 9 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) e. CC )
47		elfznn0 11496	. . . . . . . . . 10 |- ( i e. ( 0 ... J ) -> i e. NN0 )
48	47	adantl 466	. . . . . . . . 9 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> i e. NN0 )
49	46, 48	expcld 12023	. . . . . . . 8 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) e. CC )
50	40, 49	mulcld 9421	. . . . . . 7 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) e. CC )
51	34, 50	mulcld 9421	. . . . . 6 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) e. CC )
52	24, 26, 27, 51	fsumsplit 13231	. . . . 5 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. ( 0 ... J ) ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) = ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) + sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) ) )
53		fzfi 11809	. . . . . . . . . 10 |- ( 0 ... J ) e. Fin
54		ssrab2 3452	. . . . . . . . . 10 |- { x e. ( 0 ... J ) | -. 2 || x } C_ ( 0 ... J )
55		ssfi 7548	. . . . . . . . . 10 |- ( ( ( 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 672	. . . . . . . . 9 |- { x e. ( 0 ... J ) | -. 2 || x } e. Fin
57	56	a1i 11	. . . . . . . 8 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> { x e. ( 0 ... J ) | -. 2 || x } e. Fin )
58		breq2 4311	. . . . . . . . . . 11 |- ( x = i -> ( 2 || x <-> 2 || i ) )
59	58	notbid 294	. . . . . . . . . 10 |- ( x = i -> ( -. 2 || x <-> -. 2 || i ) )
60	59	elrab 3132	. . . . . . . . 9 |- ( i e. { x e. ( 0 ... J ) | -. 2 || x } <-> ( i e. ( 0 ... J ) /\ -. 2 || i ) )
61	34	adantrr 716	. . . . . . . . . 10 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( J _C i ) e. CC )
62	40	adantrr 716	. . . . . . . . . . 11 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( A Xrm N ) ^ ( J - i ) ) e. CC )
63		zexpcl 11895	. . . . . . . . . . . . . . 15 |- ( ( ( A Yrm N ) e. ZZ /\ i e. NN0 ) -> ( ( A Yrm N ) ^ i ) e. ZZ )
64	17, 47, 63	syl2an 477	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( A Yrm N ) ^ i ) e. ZZ )
65	64	zcnd 10763	. . . . . . . . . . . . 13 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( A Yrm N ) ^ i ) e. CC )
66	65	adantrr 716	. . . . . . . . . . . 12 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( A Yrm N ) ^ i ) e. CC )
67	42	adantrr 716	. . . . . . . . . . . . 13 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( A ^ 2 ) - 1 ) e. CC )
68	29	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> i e. ZZ )
69		simpr 461	. . . . . . . . . . . . . . . . 17 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> -. 2 || i )
70		1z 10691	. . . . . . . . . . . . . . . . . 18 |- 1 e. ZZ
71	70	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 1 e. ZZ )
72		n2dvds1 13597	. . . . . . . . . . . . . . . . . 18 |- -. 2 || 1
73	72	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> -. 2 || 1 )
74		omoe 13894	. . . . . . . . . . . . . . . . 17 |- ( ( ( i e. ZZ /\ -. 2 || i ) /\ ( 1 e. ZZ /\ -. 2 || 1 ) ) -> 2 || ( i - 1 ) )
75	68, 69, 71, 73, 74	syl22anc 1219	. . . . . . . . . . . . . . . 16 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 2 || ( i - 1 ) )
76		2z 10693	. . . . . . . . . . . . . . . . . 18 |- 2 e. ZZ
77	76	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 2 e. ZZ )
78		2ne0 10429	. . . . . . . . . . . . . . . . . 18 |- 2 =/= 0
79	78	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 2 =/= 0 )
80		peano2zm 10703	. . . . . . . . . . . . . . . . . . 19 |- ( i e. ZZ -> ( i - 1 ) e. ZZ )
81	29, 80	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( i e. ( 0 ... J ) -> ( i - 1 ) e. ZZ )
82	81	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> ( i - 1 ) e. ZZ )
83		dvdsval2 13553	. . . . . . . . . . . . . . . . 17 |- ( ( 2 e. ZZ /\ 2 =/= 0 /\ ( i - 1 ) e. ZZ ) -> ( 2 || ( i - 1 ) <-> ( ( i - 1 ) / 2 ) e. ZZ ) )
84	77, 79, 82, 83	syl3anc 1218	. . . . . . . . . . . . . . . 16 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> ( 2 || ( i - 1 ) <-> ( ( i - 1 ) / 2 ) e. ZZ ) )
85	75, 84	mpbid 210	. . . . . . . . . . . . . . 15 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> ( ( i - 1 ) / 2 ) e. ZZ )
86	81	zred 10762	. . . . . . . . . . . . . . . . 17 |- ( i e. ( 0 ... J ) -> ( i - 1 ) e. RR )
87	86	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> ( i - 1 ) e. RR )
88		dvds0 13563	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 2 e. ZZ -> 2 || 0 )
89	76, 88	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- 2 || 0
90		breq2 4311	. . . . . . . . . . . . . . . . . . . . . 22 |- ( i = 0 -> ( 2 || i <-> 2 || 0 ) )
91	89, 90	mpbiri 233	. . . . . . . . . . . . . . . . . . . . 21 |- ( i = 0 -> 2 || i )
92	91	con3i 135	. . . . . . . . . . . . . . . . . . . 20 |- ( -. 2 || i -> -. i = 0 )
93	92	adantl 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> -. i = 0 )
94	47	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> i e. NN0 )
95		elnn0 10596	. . . . . . . . . . . . . . . . . . . 20 |- ( i e. NN0 <-> ( i e. NN \/ i = 0 ) )
96	94, 95	sylib 196	. . . . . . . . . . . . . . . . . . 19 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> ( i e. NN \/ i = 0 ) )
97		orel2 383	. . . . . . . . . . . . . . . . . . 19 |- ( -. i = 0 -> ( ( i e. NN \/ i = 0 ) -> i e. NN ) )
98	93, 96, 97	sylc 60	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> i e. NN )
99		nnm1nn0 10636	. . . . . . . . . . . . . . . . . 18 |- ( i e. NN -> ( i - 1 ) e. NN0 )
100	98, 99	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> ( i - 1 ) e. NN0 )
101	100	nn0ge0d 10654	. . . . . . . . . . . . . . . 16 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 0 <_ ( i - 1 ) )
102		2re 10406	. . . . . . . . . . . . . . . . 17 |- 2 e. RR
103	102	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 2 e. RR )
104		2pos 10428	. . . . . . . . . . . . . . . . 17 |- 0 < 2
105	104	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 0 < 2 )
106		divge0 10213	. . . . . . . . . . . . . . . 16 |- ( ( ( ( i - 1 ) e. RR /\ 0 <_ ( i - 1 ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( ( i - 1 ) / 2 ) )
107	87, 101, 103, 105, 106	syl22anc 1219	. . . . . . . . . . . . . . 15 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> 0 <_ ( ( i - 1 ) / 2 ) )
108		elnn0z 10674	. . . . . . . . . . . . . . 15 |- ( ( ( i - 1 ) / 2 ) e. NN0 <-> ( ( ( i - 1 ) / 2 ) e. ZZ /\ 0 <_ ( ( i - 1 ) / 2 ) ) )
109	85, 107, 108	sylanbrc 664	. . . . . . . . . . . . . 14 |- ( ( i e. ( 0 ... J ) /\ -. 2 || i ) -> ( ( i - 1 ) / 2 ) e. NN0 )
110	109	adantl 466	. . . . . . . . . . . . 13 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( i - 1 ) / 2 ) e. NN0 )
111	67, 110	expcld 12023	. . . . . . . . . . . 12 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) e. CC )
112	66, 111	mulcld 9421	. . . . . . . . . . 11 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) e. CC )
113	62, 112	mulcld 9421	. . . . . . . . . 10 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) e. CC )
114	61, 113	mulcld 9421	. . . . . . . . 9 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) e. CC )
115	60, 114	sylan2b 475	. . . . . . . 8 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. { x e. ( 0 ... J ) | -. 2 || x } ) -> ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) e. CC )
116	57, 14, 115	fsummulc2 13266	. . . . . . 7 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) = sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) )
117	43	adantrr 716	. . . . . . . . . . 11 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( sqr ` ( ( A ^ 2 ) - 1 ) ) e. CC )
118	117, 61, 113	mul12d 9593	. . . . . . . . . 10 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) = ( ( J _C i ) x. ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) )
119	117, 62, 112	mul12d 9593	. . . . . . . . . . . 12 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) = ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) )
120	43, 48	expcld 12023	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) e. CC )
121	120	adantrr 716	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) e. CC )
122	66, 121	mulcomd 9422	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A Yrm N ) ^ i ) x. ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) ) = ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) x. ( ( A Yrm N ) ^ i ) ) )
123	117, 66, 111	mul12d 9593	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) = ( ( ( A Yrm N ) ^ i ) x. ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) )
124		2nn0 10611	. . . . . . . . . . . . . . . . . . . . 21 |- 2 e. NN0
125	124	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> 2 e. NN0 )
126	117, 110, 125	expmuld 12026	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ ( 2 x. ( ( i - 1 ) / 2 ) ) ) = ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) ^ ( ( i - 1 ) / 2 ) ) )
127	81	zcnd 10763	. . . . . . . . . . . . . . . . . . . . . 22 |- ( i e. ( 0 ... J ) -> ( i - 1 ) e. CC )
128	127	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( i - 1 ) e. CC )
129		2cnd 10409	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> 2 e. CC )
130	78	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> 2 =/= 0 )
131	128, 129, 130	divcan2d 10124	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( 2 x. ( ( i - 1 ) / 2 ) ) = ( i - 1 ) )
132	131	oveq2d 6122	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ ( 2 x. ( ( i - 1 ) / 2 ) ) ) = ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ ( i - 1 ) ) )
133	67	sqsqrd 12940	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) = ( ( A ^ 2 ) - 1 ) )
134	133	oveq1d 6121	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) ^ ( ( i - 1 ) / 2 ) ) = ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) )
135	126, 132, 134	3eqtr3rd 2484	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) = ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ ( i - 1 ) ) )
136	135	oveq1d 6121	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) x. ( sqr ` ( ( A ^ 2 ) - 1 ) ) ) = ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ ( i - 1 ) ) x. ( sqr ` ( ( A ^ 2 ) - 1 ) ) ) )
137	117, 111	mulcomd 9422	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) = ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) x. ( sqr ` ( ( A ^ 2 ) - 1 ) ) ) )
138	98	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> i e. NN )
139		expm1t 11907	. . . . . . . . . . . . . . . . . 18 |- ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) e. CC /\ i e. NN ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) = ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ ( i - 1 ) ) x. ( sqr ` ( ( A ^ 2 ) - 1 ) ) ) )
140	117, 138, 139	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) = ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ ( i - 1 ) ) x. ( sqr ` ( ( A ^ 2 ) - 1 ) ) ) )
141	136, 137, 140	3eqtr4d 2485	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) = ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) )
142	141	oveq2d 6122	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A Yrm N ) ^ i ) x. ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) = ( ( ( A Yrm N ) ^ i ) x. ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) ) )
143	123, 142	eqtrd 2475	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) = ( ( ( A Yrm N ) ^ i ) x. ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) ) )
144	43, 45, 48	mulexpd 12038	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) = ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) x. ( ( A Yrm N ) ^ i ) ) )
145	144	adantrr 716	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) = ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) x. ( ( A Yrm N ) ^ i ) ) )
146	122, 143, 145	3eqtr4d 2485	. . . . . . . . . . . . 13 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) = ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) )
147	146	oveq2d 6122	. . . . . . . . . . . 12 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) = ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) )
148	119, 147	eqtrd 2475	. . . . . . . . . . 11 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) = ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) )
149	148	oveq2d 6122	. . . . . . . . . 10 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( J _C i ) x. ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) = ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) )
150	118, 149	eqtrd 2475	. . . . . . . . 9 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) = ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) )
151	60, 150	sylan2b 475	. . . . . . . 8 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. { x e. ( 0 ... J ) | -. 2 || x } ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) = ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) )
152	151	sumeq2dv 13195	. . . . . . 7 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) = sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) )
153	116, 152	eqtr2d 2476	. . . . . 6 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) = ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) )
154	153	oveq2d 6122	. . . . 5 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) + sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) ) = ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) ) )
155	52, 154	eqtrd 2475	. . . 4 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. ( 0 ... J ) ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) = ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) ) )
156	3, 22, 155	3eqtrd 2479	. . 3 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( A Xrm ( N x. J ) ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm ( N x. J ) ) ) ) = ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) ) )
157		rmspecsqrnq 29266	. . . . 5 |- ( A e. ( ZZ>= ` 2 ) -> ( sqr ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
158	157	3ad2ant1 1009	. . . 4 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( sqr ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
159		nn0ssq 10976	. . . . 5 |- NN0 C_ QQ
160		simp1 988	. . . . . 6 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> A e. ( ZZ>= ` 2 ) )
161		simp2 989	. . . . . . 7 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> N e. ZZ )
162	1	3ad2ant3 1011	. . . . . . 7 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> J e. ZZ )
163	161, 162	zmulcld 10768	. . . . . 6 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( N x. J ) e. ZZ )
164	4	fovcl 6210	. . . . . 6 |- ( ( A e. ( ZZ>= ` 2 ) /\ ( N x. J ) e. ZZ ) -> ( A Xrm ( N x. J ) ) e. NN0 )
165	160, 163, 164	syl2anc 661	. . . . 5 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A Xrm ( N x. J ) ) e. NN0 )
166	159, 165	sseldi 3369	. . . 4 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A Xrm ( N x. J ) ) e. QQ )
167		zssq 10975	. . . . 5 |- ZZ C_ QQ
168	15	fovcl 6210	. . . . . 6 |- ( ( A e. ( ZZ>= ` 2 ) /\ ( N x. J ) e. ZZ ) -> ( A Yrm ( N x. J ) ) e. ZZ )
169	160, 163, 168	syl2anc 661	. . . . 5 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A Yrm ( N x. J ) ) e. ZZ )
170	167, 169	sseldi 3369	. . . 4 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A Yrm ( N x. J ) ) e. QQ )
171		ssrab2 3452	. . . . . . . 8 |- { x e. ( 0 ... J ) | 2 || x } C_ ( 0 ... J )
172		ssfi 7548	. . . . . . . 8 |- ( ( ( 0 ... J ) e. Fin /\ { x e. ( 0 ... J ) | 2 || x } C_ ( 0 ... J ) ) -> { x e. ( 0 ... J ) | 2 || x } e. Fin )
173	53, 171, 172	mp2an 672	. . . . . . 7 |- { x e. ( 0 ... J ) | 2 || x } e. Fin
174	173	a1i 11	. . . . . 6 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> { x e. ( 0 ... J ) | 2 || x } e. Fin )
175	58	elrab 3132	. . . . . . 7 |- ( i e. { x e. ( 0 ... J ) | 2 || x } <-> ( i e. ( 0 ... J ) /\ 2 || i ) )
176	33	adantrr 716	. . . . . . . 8 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( J _C i ) e. ZZ )
177		zexpcl 11895	. . . . . . . . . . 11 |- ( ( ( A Xrm N ) e. ZZ /\ ( J - i ) e. NN0 ) -> ( ( A Xrm N ) ^ ( J - i ) ) e. ZZ )
178	36, 39, 177	syl2anc 661	. . . . . . . . . 10 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( ( A Xrm N ) ^ ( J - i ) ) e. ZZ )
179	178	adantrr 716	. . . . . . . . 9 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( A Xrm N ) ^ ( J - i ) ) e. ZZ )
180	43	adantrr 716	. . . . . . . . . . . 12 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( sqr ` ( ( A ^ 2 ) - 1 ) ) e. CC )
181	45	adantrr 716	. . . . . . . . . . . 12 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( A Yrm N ) e. CC )
182	47	ad2antrl 727	. . . . . . . . . . . 12 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> i e. NN0 )
183	180, 181, 182	mulexpd 12038	. . . . . . . . . . 11 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) = ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) x. ( ( A Yrm N ) ^ i ) ) )
184	29	zcnd 10763	. . . . . . . . . . . . . . . . . 18 |- ( i e. ( 0 ... J ) -> i e. CC )
185	184	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> i e. CC )
186		2cnd 10409	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> 2 e. CC )
187	78	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> 2 =/= 0 )
188	185, 186, 187	divcan2d 10124	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> ( 2 x. ( i / 2 ) ) = i )
189	188	eqcomd 2448	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. ( 0 ... J ) ) -> i = ( 2 x. ( i / 2 ) ) )
190	189	adantrr 716	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> i = ( 2 x. ( i / 2 ) ) )
191	190	oveq2d 6122	. . . . . . . . . . . . 13 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) = ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ ( 2 x. ( i / 2 ) ) ) )
192	76	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( i e. NN0 -> 2 e. ZZ )
193	78	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( i e. NN0 -> 2 =/= 0 )
194		nn0z 10684	. . . . . . . . . . . . . . . . . . 19 |- ( i e. NN0 -> i e. ZZ )
195		dvdsval2 13553	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 e. ZZ /\ 2 =/= 0 /\ i e. ZZ ) -> ( 2 || i <-> ( i / 2 ) e. ZZ ) )
196	192, 193, 194, 195	syl3anc 1218	. . . . . . . . . . . . . . . . . 18 |- ( i e. NN0 -> ( 2 || i <-> ( i / 2 ) e. ZZ ) )
197	196	biimpa 484	. . . . . . . . . . . . . . . . 17 |- ( ( i e. NN0 /\ 2 || i ) -> ( i / 2 ) e. ZZ )
198		nn0re 10603	. . . . . . . . . . . . . . . . . . 19 |- ( i e. NN0 -> i e. RR )
199	198	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. NN0 /\ 2 || i ) -> i e. RR )
200		nn0ge0 10620	. . . . . . . . . . . . . . . . . . 19 |- ( i e. NN0 -> 0 <_ i )
201	200	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. NN0 /\ 2 || i ) -> 0 <_ i )
202	102	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. NN0 /\ 2 || i ) -> 2 e. RR )
203	104	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. NN0 /\ 2 || i ) -> 0 < 2 )
204		divge0 10213	. . . . . . . . . . . . . . . . . 18 |- ( ( ( i e. RR /\ 0 <_ i ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( i / 2 ) )
205	199, 201, 202, 203, 204	syl22anc 1219	. . . . . . . . . . . . . . . . 17 |- ( ( i e. NN0 /\ 2 || i ) -> 0 <_ ( i / 2 ) )
206		elnn0z 10674	. . . . . . . . . . . . . . . . 17 |- ( ( i / 2 ) e. NN0 <-> ( ( i / 2 ) e. ZZ /\ 0 <_ ( i / 2 ) ) )
207	197, 205, 206	sylanbrc 664	. . . . . . . . . . . . . . . 16 |- ( ( i e. NN0 /\ 2 || i ) -> ( i / 2 ) e. NN0 )
208	47, 207	sylan 471	. . . . . . . . . . . . . . 15 |- ( ( i e. ( 0 ... J ) /\ 2 || i ) -> ( i / 2 ) e. NN0 )
209	208	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( i / 2 ) e. NN0 )
210	124	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> 2 e. NN0 )
211	180, 209, 210	expmuld 12026	. . . . . . . . . . . . 13 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ ( 2 x. ( i / 2 ) ) ) = ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) ^ ( i / 2 ) ) )
212	42	adantrr 716	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( A ^ 2 ) - 1 ) e. CC )
213	212	sqsqrd 12940	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) = ( ( A ^ 2 ) - 1 ) )
214	213	oveq1d 6121	. . . . . . . . . . . . 13 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) ^ ( i / 2 ) ) = ( ( ( A ^ 2 ) - 1 ) ^ ( i / 2 ) ) )
215	191, 211, 214	3eqtrd 2479	. . . . . . . . . . . 12 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) = ( ( ( A ^ 2 ) - 1 ) ^ ( i / 2 ) ) )
216	215	oveq1d 6121	. . . . . . . . . . 11 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) ^ i ) x. ( ( A Yrm N ) ^ i ) ) = ( ( ( ( A ^ 2 ) - 1 ) ^ ( i / 2 ) ) x. ( ( A Yrm N ) ^ i ) ) )
217	183, 216	eqtrd 2475	. . . . . . . . . 10 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) = ( ( ( ( A ^ 2 ) - 1 ) ^ ( i / 2 ) ) x. ( ( A Yrm N ) ^ i ) ) )
218		zexpcl 11895	. . . . . . . . . . . 12 |- ( ( ( ( A ^ 2 ) - 1 ) e. ZZ /\ ( i / 2 ) e. NN0 ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( i / 2 ) ) e. ZZ )
219	12, 208, 218	syl2an 477	. . . . . . . . . . 11 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( i / 2 ) ) e. ZZ )
220	64	adantrr 716	. . . . . . . . . . 11 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( A Yrm N ) ^ i ) e. ZZ )
221	219, 220	zmulcld 10768	. . . . . . . . . 10 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( ( A ^ 2 ) - 1 ) ^ ( i / 2 ) ) x. ( ( A Yrm N ) ^ i ) ) e. ZZ )
222	217, 221	eqeltrd 2517	. . . . . . . . 9 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) e. ZZ )
223	179, 222	zmulcld 10768	. . . . . . . 8 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) e. ZZ )
224	176, 223	zmulcld 10768	. . . . . . 7 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ 2 || i ) ) -> ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) e. ZZ )
225	175, 224	sylan2b 475	. . . . . 6 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. { x e. ( 0 ... J ) | 2 || x } ) -> ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) e. ZZ )
226	174, 225	fsumzcl 13227	. . . . 5 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) e. ZZ )
227	167, 226	sseldi 3369	. . . 4 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) e. QQ )
228	33	adantrr 716	. . . . . . . 8 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( J _C i ) e. ZZ )
229	178	adantrr 716	. . . . . . . . 9 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( A Xrm N ) ^ ( J - i ) ) e. ZZ )
230	64	adantrr 716	. . . . . . . . . 10 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( A Yrm N ) ^ i ) e. ZZ )
231		zexpcl 11895	. . . . . . . . . . 11 |- ( ( ( ( A ^ 2 ) - 1 ) e. ZZ /\ ( ( i - 1 ) / 2 ) e. NN0 ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) e. ZZ )
232	12, 109, 231	syl2an 477	. . . . . . . . . 10 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) e. ZZ )
233	230, 232	zmulcld 10768	. . . . . . . . 9 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) e. ZZ )
234	229, 233	zmulcld 10768	. . . . . . . 8 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) e. ZZ )
235	228, 234	zmulcld 10768	. . . . . . 7 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ ( i e. ( 0 ... J ) /\ -. 2 || i ) ) -> ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) e. ZZ )
236	60, 235	sylan2b 475	. . . . . 6 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) /\ i e. { x e. ( 0 ... J ) | -. 2 || x } ) -> ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) e. ZZ )
237	57, 236	fsumzcl 13227	. . . . 5 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) e. ZZ )
238	167, 237	sseldi 3369	. . . 4 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) e. QQ )
239		qirropth 29268	. . . 4 |- ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) /\ ( ( A Xrm ( N x. J ) ) e. QQ /\ ( A Yrm ( N x. J ) ) e. QQ ) /\ ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) e. QQ /\ sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) e. QQ ) ) -> ( ( ( A Xrm ( N x. J ) ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm ( N x. J ) ) ) ) = ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) ) <-> ( ( A Xrm ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) /\ ( A Yrm ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) ) )
240	158, 166, 170, 227, 238, 239	syl122anc 1227	. . 3 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( ( A Xrm ( N x. J ) ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm ( N x. J ) ) ) ) = ( sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) ) <-> ( ( A Xrm ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) /\ ( A Yrm ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) ) )
241	156, 240	mpbid 210	. 2 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( ( A Xrm ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ^ i ) ) ) /\ ( A Yrm ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) ) )
242	241	simprd 463	1 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A Yrm ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 965   = wceq 1369   e. wcel 1756   =/= wne 2620   {crab 2734   \ cdif 3340   u. cun 3341   i^i cin 3342   C_ wss 3343   (/)c0 3652   class class class wbr 4307   ` cfv 5433  (class class class)co 6106   Fincfn 7325   CCcc 9295   RRcr 9296   0cc0 9297   1c1 9298   + caddc 9300   x. cmul 9302   < clt 9433   <_ cle 9434   - cmin 9610   / cdiv 10008   NNcn 10337   2c2 10386   NN0cn0 10594   ZZcz 10661   ZZ>=cuz 10876   QQcq 10968   ...cfz 11452   ^cexp 11880   _C cbc 12093   sqrcsqr 12737   sum_csu 13178   || cdivides 13550   X_rm crmx 29260   Y_rm crmy 29261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4418  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546  ax-un 6387  ax-inf2 7862  ax-cnex 9353  ax-resscn 9354  ax-1cn 9355  ax-icn 9356  ax-addcl 9357  ax-addrcl 9358  ax-mulcl 9359  ax-mulrcl 9360  ax-mulcom 9361  ax-addass 9362  ax-mulass 9363  ax-distr 9364  ax-i2m1 9365  ax-1ne0 9366  ax-1rid 9367  ax-rnegex 9368  ax-rrecex 9369  ax-cnre 9370  ax-pre-lttri 9371  ax-pre-lttrn 9372  ax-pre-ltadd 9373  ax-pre-mulgt0 9374  ax-pre-sup 9375  ax-addf 9376  ax-mulf 9377

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2735  df-rex 2736  df-reu 2737  df-rmo 2738  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-pss 3359  df-nul 3653  df-if 3807  df-pw 3877  df-sn 3893  df-pr 3895  df-tp 3897  df-op 3899  df-uni 4107  df-int 4144  df-iun 4188  df-iin 4189  df-br 4308  df-opab 4366  df-mpt 4367  df-tr 4401  df-eprel 4647  df-id 4651  df-po 4656  df-so 4657  df-fr 4694  df-se 4695  df-we 4696  df-ord 4737  df-on 4738  df-lim 4739  df-suc 4740  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-isom 5442  df-riota 6067  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-of 6335  df-om 6492  df-1st 6592  df-2nd 6593  df-supp 6706  df-recs 6847  df-rdg 6881  df-1o 6935  df-2o 6936  df-oadd 6939  df-omul 6940  df-er 7116  df-map 7231  df-pm 7232  df-ixp 7279  df-en 7326  df-dom 7327  df-sdom 7328  df-fin 7329  df-fsupp 7636  df-fi 7676  df-sup 7706  df-oi 7739  df-card 8124  df-acn 8127  df-cda 8352  df-pnf 9435  df-mnf 9436  df-xr 9437  df-ltxr 9438  df-le 9439  df-sub 9612  df-neg 9613  df-div 10009  df-nn 10338  df-2 10395  df-3 10396  df-4 10397  df-5 10398  df-6 10399  df-7 10400  df-8 10401  df-9 10402  df-10 10403  df-n0 10595  df-z 10662  df-dec 10771  df-uz 10877  df-q 10969  df-rp 11007  df-xneg 11104  df-xadd 11105  df-xmul 11106  df-ioo 11319  df-ioc 11320  df-ico 11321  df-icc 11322  df-fz 11453  df-fzo 11564  df-fl 11657  df-mod 11724  df-seq 11822  df-exp 11881  df-fac 12067  df-bc 12094  df-hash 12119  df-shft 12571  df-cj 12603  df-re 12604  df-im 12605  df-sqr 12739  df-abs 12740  df-limsup 12964  df-clim 12981  df-rlim 12982  df-sum 13179  df-ef 13368  df-sin 13370  df-cos 13371  df-pi 13373  df-dvds 13551  df-gcd 13706  df-numer 13828  df-denom 13829  df-struct 14191  df-ndx 14192  df-slot 14193  df-base 14194  df-sets 14195  df-ress 14196  df-plusg 14266  df-mulr 14267  df-starv 14268  df-sca 14269  df-vsca 14270  df-ip 14271  df-tset 14272  df-ple 14273  df-ds 14275  df-unif 14276  df-hom 14277  df-cco 14278  df-rest 14376  df-topn 14377  df-0g 14395  df-gsum 14396  df-topgen 14397  df-pt 14398  df-prds 14401  df-xrs 14455  df-qtop 14460  df-imas 14461  df-xps 14463  df-mre 14539  df-mrc 14540  df-acs 14542  df-mnd 15430  df-submnd 15480  df-mulg 15563  df-cntz 15850  df-cmn 16294  df-psmet 17824  df-xmet 17825  df-met 17826  df-bl 17827  df-mopn 17828  df-fbas 17829  df-fg 17830  df-cnfld 17834  df-top 18518  df-bases 18520  df-topon 18521  df-topsp 18522  df-cld 18638  df-ntr 18639  df-cls 18640  df-nei 18717  df-lp 18755  df-perf 18756  df-cn 18846  df-cnp 18847  df-haus 18934  df-tx 19150  df-hmeo 19343  df-fil 19434  df-fm 19526  df-flim 19527  df-flf 19528  df-xms 19910  df-ms 19911  df-tms 19912  df-cncf 20469  df-limc 21356  df-dv 21357  df-log 22023  df-squarenn 29201  df-pell1qr 29202  df-pell14qr 29203  df-pell1234qr 29204  df-pellfund 29205  df-rmx 29262  df-rmy 29263

This theorem is referenced by:  jm2.23  29364