Theorem jm2.23

Description: Lemma for jm2.20nn . Truncate binomial expansion p-adicly. (Contributed by Stefan O'Rear, 26-Sep-2014)

	Ref	Expression
Assertion	jm2.23	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( A rmY N ) ^ 3 ) || ( ( A rmY ( N x. J ) ) - ( J x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( A rmY N ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fzfi	|- ( 3 ... J ) e. Fin
2		ssrab2	|- { b e. ( 3 ... J ) | -. 2 || b } C_ ( 3 ... J )
3		ssfi	|- ( ( ( 3 ... J ) e. Fin /\ { b e. ( 3 ... J ) | -. 2 || b } C_ ( 3 ... J ) ) -> { b e. ( 3 ... J ) | -. 2 || b } e. Fin )
4	1 2 3	mp2an	|- { b e. ( 3 ... J ) | -. 2 || b } e. Fin
5	4	a1i	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> { b e. ( 3 ... J ) | -. 2 || b } e. Fin )
6		nnnn0	|- ( J e. NN -> J e. NN0 )
7	6	3ad2ant3	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> J e. NN0 )
8	2	sseli	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> a e. ( 3 ... J ) )
9		elfzelz	|- ( a e. ( 3 ... J ) -> a e. ZZ )
10	8 9	syl	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> a e. ZZ )
11		bccl	|- ( ( J e. NN0 /\ a e. ZZ ) -> ( J _C a ) e. NN0 )
12	7 10 11	syl2an	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( J _C a ) e. NN0 )
13	12	nn0zd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( J _C a ) e. ZZ )
14		simpl1	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> A e. ( ZZ>= ` 2 ) )
15		simpl2	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> N e. ZZ )
16		frmx	|- rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
17	16	fovcl	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
18	14 15 17	syl2anc	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( A rmX N ) e. NN0 )
19	18	nn0zd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( A rmX N ) e. ZZ )
20	8	adantl	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> a e. ( 3 ... J ) )
21		fznn0sub	|- ( a e. ( 3 ... J ) -> ( J - a ) e. NN0 )
22	20 21	syl	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( J - a ) e. NN0 )
23		zexpcl	|- ( ( ( A rmX N ) e. ZZ /\ ( J - a ) e. NN0 ) -> ( ( A rmX N ) ^ ( J - a ) ) e. ZZ )
24	19 22 23	syl2anc	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( A rmX N ) ^ ( J - a ) ) e. ZZ )
25		rmspecnonsq	|- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )
26	25	eldifad	|- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. NN )
27	26	nnzd	|- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ZZ )
28	27	3ad2ant1	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( A ^ 2 ) - 1 ) e. ZZ )
29		breq2	|- ( b = a -> ( 2 || b <-> 2 || a ) )
30	29	notbid	|- ( b = a -> ( -. 2 || b <-> -. 2 || a ) )
31	30	elrab	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } <-> ( a e. ( 3 ... J ) /\ -. 2 || a ) )
32	31	simprbi	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> -. 2 || a )
33		1zzd	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> 1 e. ZZ )
34		n2dvds1	|- -. 2 || 1
35	34	a1i	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> -. 2 || 1 )
36		omoe	|- ( ( ( a e. ZZ /\ -. 2 || a ) /\ ( 1 e. ZZ /\ -. 2 || 1 ) ) -> 2 || ( a - 1 ) )
37	10 32 33 35 36	syl22anc	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> 2 || ( a - 1 ) )
38		2z	|- 2 e. ZZ
39	38	a1i	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> 2 e. ZZ )
40		2ne0	|- 2 =/= 0
41	40	a1i	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> 2 =/= 0 )
42		peano2zm	|- ( a e. ZZ -> ( a - 1 ) e. ZZ )
43	10 42	syl	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> ( a - 1 ) e. ZZ )
44		dvdsval2	|- ( ( 2 e. ZZ /\ 2 =/= 0 /\ ( a - 1 ) e. ZZ ) -> ( 2 || ( a - 1 ) <-> ( ( a - 1 ) / 2 ) e. ZZ ) )
45	39 41 43 44	syl3anc	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> ( 2 || ( a - 1 ) <-> ( ( a - 1 ) / 2 ) e. ZZ ) )
46	37 45	mpbid	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> ( ( a - 1 ) / 2 ) e. ZZ )
47	43	zred	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> ( a - 1 ) e. RR )
48		0red	|- ( a e. ( 3 ... J ) -> 0 e. RR )
49		3re	|- 3 e. RR
50	49	a1i	|- ( a e. ( 3 ... J ) -> 3 e. RR )
51	9	zred	|- ( a e. ( 3 ... J ) -> a e. RR )
52		3pos	|- 0 < 3
53	52	a1i	|- ( a e. ( 3 ... J ) -> 0 < 3 )
54		elfzle1	|- ( a e. ( 3 ... J ) -> 3 <_ a )
55	48 50 51 53 54	ltletrd	|- ( a e. ( 3 ... J ) -> 0 < a )
56		elnnz	|- ( a e. NN <-> ( a e. ZZ /\ 0 < a ) )
57	9 55 56	sylanbrc	|- ( a e. ( 3 ... J ) -> a e. NN )
58		nnm1nn0	|- ( a e. NN -> ( a - 1 ) e. NN0 )
59	57 58	syl	|- ( a e. ( 3 ... J ) -> ( a - 1 ) e. NN0 )
60	59	nn0ge0d	|- ( a e. ( 3 ... J ) -> 0 <_ ( a - 1 ) )
61	8 60	syl	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> 0 <_ ( a - 1 ) )
62		2re	|- 2 e. RR
63	62	a1i	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> 2 e. RR )
64		2pos	|- 0 < 2
65	64	a1i	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> 0 < 2 )
66		divge0	|- ( ( ( ( a - 1 ) e. RR /\ 0 <_ ( a - 1 ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( ( a - 1 ) / 2 ) )
67	47 61 63 65 66	syl22anc	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> 0 <_ ( ( a - 1 ) / 2 ) )
68		elnn0z	|- ( ( ( a - 1 ) / 2 ) e. NN0 <-> ( ( ( a - 1 ) / 2 ) e. ZZ /\ 0 <_ ( ( a - 1 ) / 2 ) ) )
69	46 67 68	sylanbrc	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> ( ( a - 1 ) / 2 ) e. NN0 )
70		zexpcl	|- ( ( ( ( A ^ 2 ) - 1 ) e. ZZ /\ ( ( a - 1 ) / 2 ) e. NN0 ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) e. ZZ )
71	28 69 70	syl2an	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) e. ZZ )
72		frmy	|- rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
73	72	fovcl	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
74	14 15 73	syl2anc	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( A rmY N ) e. ZZ )
75		elfzel1	|- ( a e. ( 3 ... J ) -> 3 e. ZZ )
76	9 75	zsubcld	|- ( a e. ( 3 ... J ) -> ( a - 3 ) e. ZZ )
77		subge0	|- ( ( a e. RR /\ 3 e. RR ) -> ( 0 <_ ( a - 3 ) <-> 3 <_ a ) )
78	51 49 77	sylancl	|- ( a e. ( 3 ... J ) -> ( 0 <_ ( a - 3 ) <-> 3 <_ a ) )
79	54 78	mpbird	|- ( a e. ( 3 ... J ) -> 0 <_ ( a - 3 ) )
80		elnn0z	|- ( ( a - 3 ) e. NN0 <-> ( ( a - 3 ) e. ZZ /\ 0 <_ ( a - 3 ) ) )
81	76 79 80	sylanbrc	|- ( a e. ( 3 ... J ) -> ( a - 3 ) e. NN0 )
82	8 81	syl	|- ( a e. { b e. ( 3 ... J ) | -. 2 || b } -> ( a - 3 ) e. NN0 )
83	82	adantl	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( a - 3 ) e. NN0 )
84		zexpcl	|- ( ( ( A rmY N ) e. ZZ /\ ( a - 3 ) e. NN0 ) -> ( ( A rmY N ) ^ ( a - 3 ) ) e. ZZ )
85	74 83 84	syl2anc	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( A rmY N ) ^ ( a - 3 ) ) e. ZZ )
86	71 85	zmulcld	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) e. ZZ )
87	24 86	zmulcld	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) e. ZZ )
88	13 87	zmulcld	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) e. ZZ )
89	5 88	fsumzcl	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) e. ZZ )
90	73	3adant3	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( A rmY N ) e. ZZ )
91		3nn0	|- 3 e. NN0
92		zexpcl	|- ( ( ( A rmY N ) e. ZZ /\ 3 e. NN0 ) -> ( ( A rmY N ) ^ 3 ) e. ZZ )
93	90 91 92	sylancl	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( A rmY N ) ^ 3 ) e. ZZ )
94		dvdsmul2	|- ( ( sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) e. ZZ /\ ( ( A rmY N ) ^ 3 ) e. ZZ ) -> ( ( A rmY N ) ^ 3 ) || ( sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) )
95	89 93 94	syl2anc	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( A rmY N ) ^ 3 ) || ( sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) )
96		jm2.22	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A rmY ( N x. J ) ) = sum_ a e. { b e. ( 0 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) )
97	6 96	syl3an3	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( A rmY ( N x. J ) ) = sum_ a e. { b e. ( 0 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) )
98		1lt3	|- 1 < 3
99		1re	|- 1 e. RR
100	99 49	ltnlei	|- ( 1 < 3 <-> -. 3 <_ 1 )
101	98 100	mpbi	|- -. 3 <_ 1
102		elfzle1	|- ( 1 e. ( 3 ... J ) -> 3 <_ 1 )
103	101 102	mto	|- -. 1 e. ( 3 ... J )
104	103	a1i	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> -. 1 e. ( 3 ... J ) )
105	104	intnanrd	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> -. ( 1 e. ( 3 ... J ) /\ -. 2 || 1 ) )
106		breq2	|- ( b = 1 -> ( 2 || b <-> 2 || 1 ) )
107	106	notbid	|- ( b = 1 -> ( -. 2 || b <-> -. 2 || 1 ) )
108	107	elrab	|- ( 1 e. { b e. ( 3 ... J ) | -. 2 || b } <-> ( 1 e. ( 3 ... J ) /\ -. 2 || 1 ) )
109	105 108	sylnibr	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> -. 1 e. { b e. ( 3 ... J ) | -. 2 || b } )
110		disjsn	|- ( ( { b e. ( 3 ... J ) | -. 2 || b } i^i { 1 } ) = (/) <-> -. 1 e. { b e. ( 3 ... J ) | -. 2 || b } )
111	109 110	sylibr	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( { b e. ( 3 ... J ) | -. 2 || b } i^i { 1 } ) = (/) )
112		simpr	|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) /\ a = 1 ) -> a = 1 )
113	112	olcd	|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) /\ a = 1 ) -> ( ( a e. ( 3 ... J ) /\ -. 2 || a ) \/ a = 1 ) )
114		elfznn0	|- ( a e. ( 0 ... J ) -> a e. NN0 )
115	114	adantr	|- ( ( a e. ( 0 ... J ) /\ -. 2 || a ) -> a e. NN0 )
116	115	ad2antlr	|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) /\ a =/= 1 ) -> a e. NN0 )
117		simplrr	|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) /\ a =/= 1 ) -> -. 2 || a )
118		simpr	|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) /\ a =/= 1 ) -> a =/= 1 )
119		elnn1uz2	|- ( a e. NN <-> ( a = 1 \/ a e. ( ZZ>= ` 2 ) ) )
120		df-ne	|- ( a =/= 1 <-> -. a = 1 )
121	120	biimpi	|- ( a =/= 1 -> -. a = 1 )
122	121	3ad2ant3	|- ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) -> -. a = 1 )
123	122	pm2.21d	|- ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) -> ( a = 1 -> 3 <_ a ) )
124	123	imp	|- ( ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) /\ a = 1 ) -> 3 <_ a )
125		uzp1	|- ( a e. ( ZZ>= ` 2 ) -> ( a = 2 \/ a e. ( ZZ>= ` ( 2 + 1 ) ) ) )
126		1z	|- 1 e. ZZ
127		dvdsmul1	|- ( ( 2 e. ZZ /\ 1 e. ZZ ) -> 2 || ( 2 x. 1 ) )
128	38 126 127	mp2an	|- 2 || ( 2 x. 1 )
129		2t1e2	|- ( 2 x. 1 ) = 2
130	128 129	breqtri	|- 2 || 2
131		breq2	|- ( a = 2 -> ( 2 || a <-> 2 || 2 ) )
132	131	adantl	|- ( ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) /\ a = 2 ) -> ( 2 || a <-> 2 || 2 ) )
133	130 132	mpbiri	|- ( ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) /\ a = 2 ) -> 2 || a )
134		simpl2	|- ( ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) /\ a = 2 ) -> -. 2 || a )
135	133 134	pm2.21dd	|- ( ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) /\ a = 2 ) -> 3 <_ a )
136		eluzle	|- ( a e. ( ZZ>= ` 3 ) -> 3 <_ a )
137		2p1e3	|- ( 2 + 1 ) = 3
138	137	fveq2i	|- ( ZZ>= ` ( 2 + 1 ) ) = ( ZZ>= ` 3 )
139	136 138	eleq2s	|- ( a e. ( ZZ>= ` ( 2 + 1 ) ) -> 3 <_ a )
140	139	adantl	|- ( ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) /\ a e. ( ZZ>= ` ( 2 + 1 ) ) ) -> 3 <_ a )
141	135 140	jaodan	|- ( ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) /\ ( a = 2 \/ a e. ( ZZ>= ` ( 2 + 1 ) ) ) ) -> 3 <_ a )
142	125 141	sylan2	|- ( ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) /\ a e. ( ZZ>= ` 2 ) ) -> 3 <_ a )
143	124 142	jaodan	|- ( ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) /\ ( a = 1 \/ a e. ( ZZ>= ` 2 ) ) ) -> 3 <_ a )
144	119 143	sylan2b	|- ( ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) /\ a e. NN ) -> 3 <_ a )
145		dvds0	|- ( 2 e. ZZ -> 2 || 0 )
146	38 145	ax-mp	|- 2 || 0
147		breq2	|- ( a = 0 -> ( 2 || a <-> 2 || 0 ) )
148	146 147	mpbiri	|- ( a = 0 -> 2 || a )
149	148	adantl	|- ( ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) /\ a = 0 ) -> 2 || a )
150		simpl2	|- ( ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) /\ a = 0 ) -> -. 2 || a )
151	149 150	pm2.21dd	|- ( ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) /\ a = 0 ) -> 3 <_ a )
152		elnn0	|- ( a e. NN0 <-> ( a e. NN \/ a = 0 ) )
153	152	biimpi	|- ( a e. NN0 -> ( a e. NN \/ a = 0 ) )
154	153	3ad2ant1	|- ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) -> ( a e. NN \/ a = 0 ) )
155	144 151 154	mpjaodan	|- ( ( a e. NN0 /\ -. 2 || a /\ a =/= 1 ) -> 3 <_ a )
156	116 117 118 155	syl3anc	|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) /\ a =/= 1 ) -> 3 <_ a )
157		elfzle2	|- ( a e. ( 0 ... J ) -> a <_ J )
158	157	adantr	|- ( ( a e. ( 0 ... J ) /\ -. 2 || a ) -> a <_ J )
159	158	ad2antlr	|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) /\ a =/= 1 ) -> a <_ J )
160		elfzelz	|- ( a e. ( 0 ... J ) -> a e. ZZ )
161	160	adantr	|- ( ( a e. ( 0 ... J ) /\ -. 2 || a ) -> a e. ZZ )
162	161	ad2antlr	|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) /\ a =/= 1 ) -> a e. ZZ )
163		3z	|- 3 e. ZZ
164	163	a1i	|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) /\ a =/= 1 ) -> 3 e. ZZ )
165		nnz	|- ( J e. NN -> J e. ZZ )
166	165	3ad2ant3	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> J e. ZZ )
167	166	ad2antrr	|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) /\ a =/= 1 ) -> J e. ZZ )
168		elfz	|- ( ( a e. ZZ /\ 3 e. ZZ /\ J e. ZZ ) -> ( a e. ( 3 ... J ) <-> ( 3 <_ a /\ a <_ J ) ) )
169	162 164 167 168	syl3anc	|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) /\ a =/= 1 ) -> ( a e. ( 3 ... J ) <-> ( 3 <_ a /\ a <_ J ) ) )
170	156 159 169	mpbir2and	|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) /\ a =/= 1 ) -> a e. ( 3 ... J ) )
171	170 117	jca	|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) /\ a =/= 1 ) -> ( a e. ( 3 ... J ) /\ -. 2 || a ) )
172	171	orcd	|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) /\ a =/= 1 ) -> ( ( a e. ( 3 ... J ) /\ -. 2 || a ) \/ a = 1 ) )
173	113 172	pm2.61dane	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 0 ... J ) /\ -. 2 || a ) ) -> ( ( a e. ( 3 ... J ) /\ -. 2 || a ) \/ a = 1 ) )
174		nn0uz	|- NN0 = ( ZZ>= ` 0 )
175	91 174	eleqtri	|- 3 e. ( ZZ>= ` 0 )
176		fzss1	|- ( 3 e. ( ZZ>= ` 0 ) -> ( 3 ... J ) C_ ( 0 ... J ) )
177	175 176	ax-mp	|- ( 3 ... J ) C_ ( 0 ... J )
178	177	sseli	|- ( a e. ( 3 ... J ) -> a e. ( 0 ... J ) )
179	178	anim1i	|- ( ( a e. ( 3 ... J ) /\ -. 2 || a ) -> ( a e. ( 0 ... J ) /\ -. 2 || a ) )
180	179	adantl	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( a e. ( 3 ... J ) /\ -. 2 || a ) ) -> ( a e. ( 0 ... J ) /\ -. 2 || a ) )
181		0le1	|- 0 <_ 1
182	181	a1i	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a = 1 ) -> 0 <_ 1 )
183		nnge1	|- ( J e. NN -> 1 <_ J )
184	183	3ad2ant3	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> 1 <_ J )
185	184	adantr	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a = 1 ) -> 1 <_ J )
186		1zzd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a = 1 ) -> 1 e. ZZ )
187		0zd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a = 1 ) -> 0 e. ZZ )
188	166	adantr	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a = 1 ) -> J e. ZZ )
189		elfz	|- ( ( 1 e. ZZ /\ 0 e. ZZ /\ J e. ZZ ) -> ( 1 e. ( 0 ... J ) <-> ( 0 <_ 1 /\ 1 <_ J ) ) )
190	186 187 188 189	syl3anc	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a = 1 ) -> ( 1 e. ( 0 ... J ) <-> ( 0 <_ 1 /\ 1 <_ J ) ) )
191	182 185 190	mpbir2and	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a = 1 ) -> 1 e. ( 0 ... J ) )
192	34	a1i	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a = 1 ) -> -. 2 || 1 )
193		eleq1	|- ( a = 1 -> ( a e. ( 0 ... J ) <-> 1 e. ( 0 ... J ) ) )
194		breq2	|- ( a = 1 -> ( 2 || a <-> 2 || 1 ) )
195	194	notbid	|- ( a = 1 -> ( -. 2 || a <-> -. 2 || 1 ) )
196	193 195	anbi12d	|- ( a = 1 -> ( ( a e. ( 0 ... J ) /\ -. 2 || a ) <-> ( 1 e. ( 0 ... J ) /\ -. 2 || 1 ) ) )
197	196	adantl	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a = 1 ) -> ( ( a e. ( 0 ... J ) /\ -. 2 || a ) <-> ( 1 e. ( 0 ... J ) /\ -. 2 || 1 ) ) )
198	191 192 197	mpbir2and	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a = 1 ) -> ( a e. ( 0 ... J ) /\ -. 2 || a ) )
199	180 198	jaodan	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ ( ( a e. ( 3 ... J ) /\ -. 2 || a ) \/ a = 1 ) ) -> ( a e. ( 0 ... J ) /\ -. 2 || a ) )
200	173 199	impbida	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( a e. ( 0 ... J ) /\ -. 2 || a ) <-> ( ( a e. ( 3 ... J ) /\ -. 2 || a ) \/ a = 1 ) ) )
201	30	elrab	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } <-> ( a e. ( 0 ... J ) /\ -. 2 || a ) )
202		elun	|- ( a e. ( { b e. ( 3 ... J ) | -. 2 || b } u. { 1 } ) <-> ( a e. { b e. ( 3 ... J ) | -. 2 || b } \/ a e. { 1 } ) )
203		velsn	|- ( a e. { 1 } <-> a = 1 )
204	31 203	orbi12i	|- ( ( a e. { b e. ( 3 ... J ) | -. 2 || b } \/ a e. { 1 } ) <-> ( ( a e. ( 3 ... J ) /\ -. 2 || a ) \/ a = 1 ) )
205	202 204	bitri	|- ( a e. ( { b e. ( 3 ... J ) | -. 2 || b } u. { 1 } ) <-> ( ( a e. ( 3 ... J ) /\ -. 2 || a ) \/ a = 1 ) )
206	200 201 205	3bitr4g	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( a e. { b e. ( 0 ... J ) | -. 2 || b } <-> a e. ( { b e. ( 3 ... J ) | -. 2 || b } u. { 1 } ) ) )
207	206	eqrdv	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> { b e. ( 0 ... J ) | -. 2 || b } = ( { b e. ( 3 ... J ) | -. 2 || b } u. { 1 } ) )
208		fzfi	|- ( 0 ... J ) e. Fin
209		ssrab2	|- { b e. ( 0 ... J ) | -. 2 || b } C_ ( 0 ... J )
210		ssfi	|- ( ( ( 0 ... J ) e. Fin /\ { b e. ( 0 ... J ) | -. 2 || b } C_ ( 0 ... J ) ) -> { b e. ( 0 ... J ) | -. 2 || b } e. Fin )
211	208 209 210	mp2an	|- { b e. ( 0 ... J ) | -. 2 || b } e. Fin
212	211	a1i	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> { b e. ( 0 ... J ) | -. 2 || b } e. Fin )
213	209	sseli	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> a e. ( 0 ... J ) )
214	213 160	syl	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> a e. ZZ )
215	7 214 11	syl2an	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 0 ... J ) | -. 2 || b } ) -> ( J _C a ) e. NN0 )
216	215	nn0cnd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 0 ... J ) | -. 2 || b } ) -> ( J _C a ) e. CC )
217	17	3adant3	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( A rmX N ) e. NN0 )
218	217	nn0cnd	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( A rmX N ) e. CC )
219	218	adantr	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 0 ... J ) | -. 2 || b } ) -> ( A rmX N ) e. CC )
220	213	adantl	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 0 ... J ) | -. 2 || b } ) -> a e. ( 0 ... J ) )
221		fznn0sub	|- ( a e. ( 0 ... J ) -> ( J - a ) e. NN0 )
222	220 221	syl	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 0 ... J ) | -. 2 || b } ) -> ( J - a ) e. NN0 )
223	219 222	expcld	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 0 ... J ) | -. 2 || b } ) -> ( ( A rmX N ) ^ ( J - a ) ) e. CC )
224	90	zcnd	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( A rmY N ) e. CC )
225	213 114	syl	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> a e. NN0 )
226		expcl	|- ( ( ( A rmY N ) e. CC /\ a e. NN0 ) -> ( ( A rmY N ) ^ a ) e. CC )
227	224 225 226	syl2an	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 0 ... J ) | -. 2 || b } ) -> ( ( A rmY N ) ^ a ) e. CC )
228		rmspecpos	|- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. RR+ )
229	228	rpcnd	|- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. CC )
230	229	3ad2ant1	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( A ^ 2 ) - 1 ) e. CC )
231	201	simprbi	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> -. 2 || a )
232		1zzd	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> 1 e. ZZ )
233	34	a1i	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> -. 2 || 1 )
234	214 231 232 233 36	syl22anc	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> 2 || ( a - 1 ) )
235	38	a1i	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> 2 e. ZZ )
236	40	a1i	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> 2 =/= 0 )
237	214 42	syl	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> ( a - 1 ) e. ZZ )
238	235 236 237 44	syl3anc	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> ( 2 || ( a - 1 ) <-> ( ( a - 1 ) / 2 ) e. ZZ ) )
239	234 238	mpbid	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> ( ( a - 1 ) / 2 ) e. ZZ )
240	237	zred	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> ( a - 1 ) e. RR )
241	148	a1i	|- ( a e. ( 0 ... J ) -> ( a = 0 -> 2 || a ) )
242	241	con3dimp	|- ( ( a e. ( 0 ... J ) /\ -. 2 || a ) -> -. a = 0 )
243	201 242	sylbi	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> -. a = 0 )
244	225 153	syl	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> ( a e. NN \/ a = 0 ) )
245		orel2	|- ( -. a = 0 -> ( ( a e. NN \/ a = 0 ) -> a e. NN ) )
246	243 244 245	sylc	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> a e. NN )
247	246 58	syl	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> ( a - 1 ) e. NN0 )
248	247	nn0ge0d	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> 0 <_ ( a - 1 ) )
249	62	a1i	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> 2 e. RR )
250	64	a1i	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> 0 < 2 )
251	240 248 249 250 66	syl22anc	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> 0 <_ ( ( a - 1 ) / 2 ) )
252	239 251 68	sylanbrc	|- ( a e. { b e. ( 0 ... J ) | -. 2 || b } -> ( ( a - 1 ) / 2 ) e. NN0 )
253		expcl	|- ( ( ( ( A ^ 2 ) - 1 ) e. CC /\ ( ( a - 1 ) / 2 ) e. NN0 ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) e. CC )
254	230 252 253	syl2an	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 0 ... J ) | -. 2 || b } ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) e. CC )
255	227 254	mulcld	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 0 ... J ) | -. 2 || b } ) -> ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) e. CC )
256	223 255	mulcld	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 0 ... J ) | -. 2 || b } ) -> ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) e. CC )
257	216 256	mulcld	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 0 ... J ) | -. 2 || b } ) -> ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) e. CC )
258	111 207 212 257	fsumsplit	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> sum_ a e. { b e. ( 0 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) = ( sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) + sum_ a e. { 1 } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) ) )
259		expcl	|- ( ( ( A rmY N ) e. CC /\ 3 e. NN0 ) -> ( ( A rmY N ) ^ 3 ) e. CC )
260	224 91 259	sylancl	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( A rmY N ) ^ 3 ) e. CC )
261	88	zcnd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) e. CC )
262	5 260 261	fsummulc1	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) = sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) )
263	12	nn0cnd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( J _C a ) e. CC )
264	218	adantr	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( A rmX N ) e. CC )
265	264 22	expcld	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( A rmX N ) ^ ( J - a ) ) e. CC )
266	230 69 253	syl2an	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) e. CC )
267		expcl	|- ( ( ( A rmY N ) e. CC /\ ( a - 3 ) e. NN0 ) -> ( ( A rmY N ) ^ ( a - 3 ) ) e. CC )
268	224 82 267	syl2an	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( A rmY N ) ^ ( a - 3 ) ) e. CC )
269	266 268	mulcld	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) e. CC )
270	265 269	mulcld	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) e. CC )
271	260	adantr	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( A rmY N ) ^ 3 ) e. CC )
272	263 270 271	mulassd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) = ( ( J _C a ) x. ( ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) ) )
273	265 269 271	mulassd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) = ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) x. ( ( A rmY N ) ^ 3 ) ) ) )
274	266 268 271	mulassd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) x. ( ( A rmY N ) ^ 3 ) ) = ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( ( A rmY N ) ^ ( a - 3 ) ) x. ( ( A rmY N ) ^ 3 ) ) ) )
275	268 271	mulcld	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( A rmY N ) ^ ( a - 3 ) ) x. ( ( A rmY N ) ^ 3 ) ) e. CC )
276	266 275	mulcomd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( ( A rmY N ) ^ ( a - 3 ) ) x. ( ( A rmY N ) ^ 3 ) ) ) = ( ( ( ( A rmY N ) ^ ( a - 3 ) ) x. ( ( A rmY N ) ^ 3 ) ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) )
277	224	adantr	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( A rmY N ) e. CC )
278	91	a1i	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> 3 e. NN0 )
279	277 278 83	expaddd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( A rmY N ) ^ ( ( a - 3 ) + 3 ) ) = ( ( ( A rmY N ) ^ ( a - 3 ) ) x. ( ( A rmY N ) ^ 3 ) ) )
280	10	adantl	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> a e. ZZ )
281	280	zcnd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> a e. CC )
282		3cn	|- 3 e. CC
283		npcan	|- ( ( a e. CC /\ 3 e. CC ) -> ( ( a - 3 ) + 3 ) = a )
284	281 282 283	sylancl	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( a - 3 ) + 3 ) = a )
285	284	oveq2d	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( A rmY N ) ^ ( ( a - 3 ) + 3 ) ) = ( ( A rmY N ) ^ a ) )
286	279 285	eqtr3d	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( A rmY N ) ^ ( a - 3 ) ) x. ( ( A rmY N ) ^ 3 ) ) = ( ( A rmY N ) ^ a ) )
287	286	oveq1d	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( ( A rmY N ) ^ ( a - 3 ) ) x. ( ( A rmY N ) ^ 3 ) ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) = ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) )
288	274 276 287	3eqtrd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) x. ( ( A rmY N ) ^ 3 ) ) = ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) )
289	288	oveq2d	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) x. ( ( A rmY N ) ^ 3 ) ) ) = ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) )
290	273 289	eqtrd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) = ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) )
291	290	oveq2d	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( J _C a ) x. ( ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) ) = ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) )
292	272 291	eqtrd	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) /\ a e. { b e. ( 3 ... J ) | -. 2 || b } ) -> ( ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) = ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) )
293	292	sumeq2dv	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) = sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) )
294	262 293	eqtr2d	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) = ( sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) )
295		1nn	|- 1 e. NN
296		bccl	|- ( ( J e. NN0 /\ 1 e. ZZ ) -> ( J _C 1 ) e. NN0 )
297	6 126 296	sylancl	|- ( J e. NN -> ( J _C 1 ) e. NN0 )
298	297	nn0cnd	|- ( J e. NN -> ( J _C 1 ) e. CC )
299	298	3ad2ant3	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( J _C 1 ) e. CC )
300		nnm1nn0	|- ( J e. NN -> ( J - 1 ) e. NN0 )
301	300	3ad2ant3	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( J - 1 ) e. NN0 )
302	218 301	expcld	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( A rmX N ) ^ ( J - 1 ) ) e. CC )
303		1nn0	|- 1 e. NN0
304		expcl	|- ( ( ( A rmY N ) e. CC /\ 1 e. NN0 ) -> ( ( A rmY N ) ^ 1 ) e. CC )
305	224 303 304	sylancl	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( A rmY N ) ^ 1 ) e. CC )
306		1m1e0	|- ( 1 - 1 ) = 0
307	306	oveq1i	|- ( ( 1 - 1 ) / 2 ) = ( 0 / 2 )
308		2cn	|- 2 e. CC
309	308 40	div0i	|- ( 0 / 2 ) = 0
310	307 309	eqtri	|- ( ( 1 - 1 ) / 2 ) = 0
311		0nn0	|- 0 e. NN0
312	310 311	eqeltri	|- ( ( 1 - 1 ) / 2 ) e. NN0
313		expcl	|- ( ( ( ( A ^ 2 ) - 1 ) e. CC /\ ( ( 1 - 1 ) / 2 ) e. NN0 ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) e. CC )
314	230 312 313	sylancl	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) e. CC )
315	305 314	mulcld	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) e. CC )
316	302 315	mulcld	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) e. CC )
317	299 316	mulcld	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( J _C 1 ) x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) ) e. CC )
318		oveq2	|- ( a = 1 -> ( J _C a ) = ( J _C 1 ) )
319		oveq2	|- ( a = 1 -> ( J - a ) = ( J - 1 ) )
320	319	oveq2d	|- ( a = 1 -> ( ( A rmX N ) ^ ( J - a ) ) = ( ( A rmX N ) ^ ( J - 1 ) ) )
321		oveq2	|- ( a = 1 -> ( ( A rmY N ) ^ a ) = ( ( A rmY N ) ^ 1 ) )
322		oveq1	|- ( a = 1 -> ( a - 1 ) = ( 1 - 1 ) )
323	322	oveq1d	|- ( a = 1 -> ( ( a - 1 ) / 2 ) = ( ( 1 - 1 ) / 2 ) )
324	323	oveq2d	|- ( a = 1 -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) = ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) )
325	321 324	oveq12d	|- ( a = 1 -> ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) = ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) )
326	320 325	oveq12d	|- ( a = 1 -> ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) = ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) )
327	318 326	oveq12d	|- ( a = 1 -> ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) = ( ( J _C 1 ) x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) ) )
328	327	sumsn	|- ( ( 1 e. NN /\ ( ( J _C 1 ) x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) ) e. CC ) -> sum_ a e. { 1 } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) = ( ( J _C 1 ) x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) ) )
329	295 317 328	sylancr	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> sum_ a e. { 1 } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) = ( ( J _C 1 ) x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) ) )
330	294 329	oveq12d	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) + sum_ a e. { 1 } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( A rmY N ) ^ a ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) ) ) ) ) = ( ( sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) + ( ( J _C 1 ) x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) ) ) )
331	97 258 330	3eqtrd	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( A rmY ( N x. J ) ) = ( ( sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) + ( ( J _C 1 ) x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) ) ) )
332		bcn1	|- ( J e. NN0 -> ( J _C 1 ) = J )
333	7 332	syl	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( J _C 1 ) = J )
334	333	eqcomd	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> J = ( J _C 1 ) )
335	224	exp1d	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( A rmY N ) ^ 1 ) = ( A rmY N ) )
336	310	a1i	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( 1 - 1 ) / 2 ) = 0 )
337	336	oveq2d	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) = ( ( ( A ^ 2 ) - 1 ) ^ 0 ) )
338	230	exp0d	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( ( A ^ 2 ) - 1 ) ^ 0 ) = 1 )
339	337 338	eqtrd	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) = 1 )
340	335 339	oveq12d	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) = ( ( A rmY N ) x. 1 ) )
341	224	mulid1d	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( A rmY N ) x. 1 ) = ( A rmY N ) )
342	340 341	eqtr2d	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( A rmY N ) = ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) )
343	342	oveq2d	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( A rmY N ) ) = ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) )
344	334 343	oveq12d	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( J x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( A rmY N ) ) ) = ( ( J _C 1 ) x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) ) )
345	331 344	oveq12d	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( A rmY ( N x. J ) ) - ( J x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( A rmY N ) ) ) ) = ( ( ( sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) + ( ( J _C 1 ) x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) ) ) - ( ( J _C 1 ) x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) ) ) )
346	5 261	fsumcl	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) e. CC )
347	346 260	mulcld	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) e. CC )
348	347 317	pncand	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( ( sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) + ( ( J _C 1 ) x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) ) ) - ( ( J _C 1 ) x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( ( ( A rmY N ) ^ 1 ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( 1 - 1 ) / 2 ) ) ) ) ) ) = ( sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) )
349	345 348	eqtrd	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( A rmY ( N x. J ) ) - ( J x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( A rmY N ) ) ) ) = ( sum_ a e. { b e. ( 3 ... J ) | -. 2 || b } ( ( J _C a ) x. ( ( ( A rmX N ) ^ ( J - a ) ) x. ( ( ( ( A ^ 2 ) - 1 ) ^ ( ( a - 1 ) / 2 ) ) x. ( ( A rmY N ) ^ ( a - 3 ) ) ) ) ) x. ( ( A rmY N ) ^ 3 ) ) )
350	95 349	breqtrrd	|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( A rmY N ) ^ 3 ) || ( ( A rmY ( N x. J ) ) - ( J x. ( ( ( A rmX N ) ^ ( J - 1 ) ) x. ( A rmY N ) ) ) ) )