jm2.18

Description: Theorem 2.18 of JonesMatijasevic p. 696. Direct relationship of the exponential function to X and Y sequences. (Contributed by Stefan O'Rear, 14-Oct-2014)

		Ref	Expression
	Assertion	jm2.18	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 /\ N e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) - ( K ^ N ) ) )

Proof

Step	Hyp	Ref	Expression
1		2z	\|- 2 e. ZZ
2		eluzelz	\|- ( A e. ( ZZ>= ` 2 ) -> A e. ZZ )
3	2	adantr	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> A e. ZZ )
4		zmulcl	\|- ( ( 2 e. ZZ /\ A e. ZZ ) -> ( 2 x. A ) e. ZZ )
5	1 3 4	sylancr	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( 2 x. A ) e. ZZ )
6		nn0z	\|- ( K e. NN0 -> K e. ZZ )
7	6	adantl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> K e. ZZ )
8	5 7	zmulcld	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( 2 x. A ) x. K ) e. ZZ )
9		zsqcl	\|- ( K e. ZZ -> ( K ^ 2 ) e. ZZ )
10	7 9	syl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( K ^ 2 ) e. ZZ )
11	8 10	zsubcld	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) e. ZZ )
12		peano2zm	\|- ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) e. ZZ -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ )
13	11 12	syl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ )
14		dvds0	\|- ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| 0 )
15	13 14	syl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| 0 )
16		rmx0	\|- ( A e. ( ZZ>= ` 2 ) -> ( A rmX 0 ) = 1 )
17	16	adantr	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( A rmX 0 ) = 1 )
18		rmy0	\|- ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) = 0 )
19	18	adantr	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( A rmY 0 ) = 0 )
20	19	oveq2d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( A - K ) x. ( A rmY 0 ) ) = ( ( A - K ) x. 0 ) )
21	3 7	zsubcld	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( A - K ) e. ZZ )
22	21	zcnd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( A - K ) e. CC )
23	22	mul01d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( A - K ) x. 0 ) = 0 )
24	20 23	eqtrd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( A - K ) x. ( A rmY 0 ) ) = 0 )
25	17 24	oveq12d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( A rmX 0 ) - ( ( A - K ) x. ( A rmY 0 ) ) ) = ( 1 - 0 ) )
26		1m0e1	\|- ( 1 - 0 ) = 1
27	25 26	eqtrdi	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( A rmX 0 ) - ( ( A - K ) x. ( A rmY 0 ) ) ) = 1 )
28		nn0cn	\|- ( K e. NN0 -> K e. CC )
29	28	adantl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> K e. CC )
30	29	exp0d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( K ^ 0 ) = 1 )
31	27 30	oveq12d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( A rmX 0 ) - ( ( A - K ) x. ( A rmY 0 ) ) ) - ( K ^ 0 ) ) = ( 1 - 1 ) )
32		1m1e0	\|- ( 1 - 1 ) = 0
33	31 32	eqtrdi	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( A rmX 0 ) - ( ( A - K ) x. ( A rmY 0 ) ) ) - ( K ^ 0 ) ) = 0 )
34	15 33	breqtrrd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX 0 ) - ( ( A - K ) x. ( A rmY 0 ) ) ) - ( K ^ 0 ) ) )
35		rmx1	\|- ( A e. ( ZZ>= ` 2 ) -> ( A rmX 1 ) = A )
36	35	adantr	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( A rmX 1 ) = A )
37		rmy1	\|- ( A e. ( ZZ>= ` 2 ) -> ( A rmY 1 ) = 1 )
38	37	adantr	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( A rmY 1 ) = 1 )
39	38	oveq2d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( A - K ) x. ( A rmY 1 ) ) = ( ( A - K ) x. 1 ) )
40	22	mulid1d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( A - K ) x. 1 ) = ( A - K ) )
41	39 40	eqtrd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( A - K ) x. ( A rmY 1 ) ) = ( A - K ) )
42	36 41	oveq12d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( A rmX 1 ) - ( ( A - K ) x. ( A rmY 1 ) ) ) = ( A - ( A - K ) ) )
43	3	zcnd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> A e. CC )
44	43 29	nncand	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( A - ( A - K ) ) = K )
45	42 44	eqtrd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( A rmX 1 ) - ( ( A - K ) x. ( A rmY 1 ) ) ) = K )
46	29	exp1d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( K ^ 1 ) = K )
47	45 46	oveq12d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( A rmX 1 ) - ( ( A - K ) x. ( A rmY 1 ) ) ) - ( K ^ 1 ) ) = ( K - K ) )
48	29	subidd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( K - K ) = 0 )
49	47 48	eqtrd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( A rmX 1 ) - ( ( A - K ) x. ( A rmY 1 ) ) ) - ( K ^ 1 ) ) = 0 )
50	15 49	breqtrrd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX 1 ) - ( ( A - K ) x. ( A rmY 1 ) ) ) - ( K ^ 1 ) ) )
51		pm3.43	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) ) /\ ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) )
52	13	adantr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ )
53	5	adantr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( 2 x. A ) e. ZZ )
54		simpll	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> A e. ( ZZ>= ` 2 ) )
55		nnz	\|- ( b e. NN -> b e. ZZ )
56	55	adantl	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> b e. ZZ )
57		frmx	\|- rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
58	57	fovcl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmX b ) e. NN0 )
59	54 56 58	syl2anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( A rmX b ) e. NN0 )
60	59	nn0zd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( A rmX b ) e. ZZ )
61	21	adantr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( A - K ) e. ZZ )
62		frmy	\|- rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
63	62	fovcl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY b ) e. ZZ )
64	54 56 63	syl2anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( A rmY b ) e. ZZ )
65	61 64	zmulcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A - K ) x. ( A rmY b ) ) e. ZZ )
66	60 65	zsubcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) e. ZZ )
67	53 66	zmulcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) e. ZZ )
68		peano2zm	\|- ( b e. ZZ -> ( b - 1 ) e. ZZ )
69	56 68	syl	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( b - 1 ) e. ZZ )
70	57	fovcl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ ( b - 1 ) e. ZZ ) -> ( A rmX ( b - 1 ) ) e. NN0 )
71	54 69 70	syl2anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( A rmX ( b - 1 ) ) e. NN0 )
72	71	nn0zd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( A rmX ( b - 1 ) ) e. ZZ )
73	62	fovcl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ ( b - 1 ) e. ZZ ) -> ( A rmY ( b - 1 ) ) e. ZZ )
74	54 69 73	syl2anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( A rmY ( b - 1 ) ) e. ZZ )
75	61 74	zmulcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) e. ZZ )
76	72 75	zsubcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) e. ZZ )
77	67 76	zsubcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) e. ZZ )
78	52 77	jca	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) e. ZZ ) )
79	78	adantr	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) e. ZZ ) )
80	7	adantr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> K e. ZZ )
81		nnnn0	\|- ( b e. NN -> b e. NN0 )
82	81	adantl	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> b e. NN0 )
83		zexpcl	\|- ( ( K e. ZZ /\ b e. NN0 ) -> ( K ^ b ) e. ZZ )
84	80 82 83	syl2anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( K ^ b ) e. ZZ )
85	53 84	zmulcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( 2 x. A ) x. ( K ^ b ) ) e. ZZ )
86		nnm1nn0	\|- ( b e. NN -> ( b - 1 ) e. NN0 )
87	86	adantl	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( b - 1 ) e. NN0 )
88		zexpcl	\|- ( ( K e. ZZ /\ ( b - 1 ) e. NN0 ) -> ( K ^ ( b - 1 ) ) e. ZZ )
89	80 87 88	syl2anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( K ^ ( b - 1 ) ) e. ZZ )
90	85 89	zsubcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( 2 x. A ) x. ( K ^ b ) ) - ( K ^ ( b - 1 ) ) ) e. ZZ )
91		0z	\|- 0 e. ZZ
92		zaddcl	\|- ( ( 0 e. ZZ /\ ( K ^ 2 ) e. ZZ ) -> ( 0 + ( K ^ 2 ) ) e. ZZ )
93	91 10 92	sylancr	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( 0 + ( K ^ 2 ) ) e. ZZ )
94	93	adantr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( 0 + ( K ^ 2 ) ) e. ZZ )
95	89 94	zmulcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) e. ZZ )
96	90 95	jca	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( ( 2 x. A ) x. ( K ^ b ) ) - ( K ^ ( b - 1 ) ) ) e. ZZ /\ ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) e. ZZ ) )
97	96	adantr	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( ( ( 2 x. A ) x. ( K ^ b ) ) - ( K ^ ( b - 1 ) ) ) e. ZZ /\ ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) e. ZZ ) )
98	52 67 85	3jca	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) e. ZZ /\ ( ( 2 x. A ) x. ( K ^ b ) ) e. ZZ ) )
99	98	adantr	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) e. ZZ /\ ( ( 2 x. A ) x. ( K ^ b ) ) e. ZZ ) )
100	76 89	jca	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) e. ZZ /\ ( K ^ ( b - 1 ) ) e. ZZ ) )
101	100	adantr	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) e. ZZ /\ ( K ^ ( b - 1 ) ) e. ZZ ) )
102	13 5 5	3jca	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ ( 2 x. A ) e. ZZ /\ ( 2 x. A ) e. ZZ ) )
103	102	ad2antrr	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ ( 2 x. A ) e. ZZ /\ ( 2 x. A ) e. ZZ ) )
104	66 84	jca	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) e. ZZ /\ ( K ^ b ) e. ZZ ) )
105	104	adantr	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) -> ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) e. ZZ /\ ( K ^ b ) e. ZZ ) )
106		congid	\|- ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ ( 2 x. A ) e. ZZ ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( 2 x. A ) - ( 2 x. A ) ) )
107	13 5 106	syl2anc	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( 2 x. A ) - ( 2 x. A ) ) )
108	107	ad2antrr	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( 2 x. A ) - ( 2 x. A ) ) )
109		simpr	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) )
110		congmul	\|- ( ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ ( 2 x. A ) e. ZZ /\ ( 2 x. A ) e. ZZ ) /\ ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) e. ZZ /\ ( K ^ b ) e. ZZ ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( 2 x. A ) - ( 2 x. A ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( 2 x. A ) x. ( K ^ b ) ) ) )
111	103 105 108 109 110	syl112anc	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( 2 x. A ) x. ( K ^ b ) ) ) )
112	111	adantrl	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( 2 x. A ) x. ( K ^ b ) ) ) )
113		simprl	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) )
114		congsub	\|- ( ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) e. ZZ /\ ( ( 2 x. A ) x. ( K ^ b ) ) e. ZZ ) /\ ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) e. ZZ /\ ( K ^ ( b - 1 ) ) e. ZZ ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( 2 x. A ) x. ( K ^ b ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) - ( ( ( 2 x. A ) x. ( K ^ b ) ) - ( K ^ ( b - 1 ) ) ) ) )
115	99 101 112 113 114	syl112anc	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) - ( ( ( 2 x. A ) x. ( K ^ b ) ) - ( K ^ ( b - 1 ) ) ) ) )
116	13 10	zaddcld	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) e. ZZ )
117	116	adantr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) e. ZZ )
118		congid	\|- ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ ( K ^ ( b - 1 ) ) e. ZZ ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( K ^ ( b - 1 ) ) - ( K ^ ( b - 1 ) ) ) )
119	52 89 118	syl2anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( K ^ ( b - 1 ) ) - ( K ^ ( b - 1 ) ) ) )
120		0zd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> 0 e. ZZ )
121		iddvds	\|- ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) )
122	13 121	syl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) )
123	13	zcnd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. CC )
124	123	subid1d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) - 0 ) = ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) )
125	122 124	breqtrrd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) - 0 ) )
126		congid	\|- ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ ( K ^ 2 ) e. ZZ ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( K ^ 2 ) - ( K ^ 2 ) ) )
127	13 10 126	syl2anc	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( K ^ 2 ) - ( K ^ 2 ) ) )
128		congadd	\|- ( ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ 0 e. ZZ ) /\ ( ( K ^ 2 ) e. ZZ /\ ( K ^ 2 ) e. ZZ ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) - 0 ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( K ^ 2 ) - ( K ^ 2 ) ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) - ( 0 + ( K ^ 2 ) ) ) )
129	13 13 120 10 10 125 127 128	syl322anc	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) - ( 0 + ( K ^ 2 ) ) ) )
130	129	adantr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) - ( 0 + ( K ^ 2 ) ) ) )
131		congmul	\|- ( ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ ( K ^ ( b - 1 ) ) e. ZZ /\ ( K ^ ( b - 1 ) ) e. ZZ ) /\ ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) e. ZZ /\ ( 0 + ( K ^ 2 ) ) e. ZZ ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( K ^ ( b - 1 ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) - ( 0 + ( K ^ 2 ) ) ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( K ^ ( b - 1 ) ) x. ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) ) - ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) ) )
132	52 89 89 117 94 119 130 131	syl322anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( K ^ ( b - 1 ) ) x. ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) ) - ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) ) )
133	11	zcnd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) e. CC )
134	29	sqcld	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( K ^ 2 ) e. CC )
135		1cnd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> 1 e. CC )
136	133 134 135	addsubd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) + ( K ^ 2 ) ) - 1 ) = ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) )
137	8	zcnd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( 2 x. A ) x. K ) e. CC )
138	137 134	npcand	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) + ( K ^ 2 ) ) = ( ( 2 x. A ) x. K ) )
139	138	oveq1d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) + ( K ^ 2 ) ) - 1 ) = ( ( ( 2 x. A ) x. K ) - 1 ) )
140	136 139	eqtr3d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) = ( ( ( 2 x. A ) x. K ) - 1 ) )
141	140	adantr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) = ( ( ( 2 x. A ) x. K ) - 1 ) )
142	141	oveq2d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( K ^ ( b - 1 ) ) x. ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) ) = ( ( K ^ ( b - 1 ) ) x. ( ( ( 2 x. A ) x. K ) - 1 ) ) )
143	28	ad2antlr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> K e. CC )
144	143 87	expcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( K ^ ( b - 1 ) ) e. CC )
145	137	adantr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( 2 x. A ) x. K ) e. CC )
146		1cnd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> 1 e. CC )
147	144 145 146	subdid	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( K ^ ( b - 1 ) ) x. ( ( ( 2 x. A ) x. K ) - 1 ) ) = ( ( ( K ^ ( b - 1 ) ) x. ( ( 2 x. A ) x. K ) ) - ( ( K ^ ( b - 1 ) ) x. 1 ) ) )
148	5	zcnd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( 2 x. A ) e. CC )
149	148	adantr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( 2 x. A ) e. CC )
150	144 149 143	mul12d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( K ^ ( b - 1 ) ) x. ( ( 2 x. A ) x. K ) ) = ( ( 2 x. A ) x. ( ( K ^ ( b - 1 ) ) x. K ) ) )
151		simpr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> b e. NN )
152		expm1t	\|- ( ( K e. CC /\ b e. NN ) -> ( K ^ b ) = ( ( K ^ ( b - 1 ) ) x. K ) )
153	143 151 152	syl2anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( K ^ b ) = ( ( K ^ ( b - 1 ) ) x. K ) )
154	153	oveq2d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( 2 x. A ) x. ( K ^ b ) ) = ( ( 2 x. A ) x. ( ( K ^ ( b - 1 ) ) x. K ) ) )
155	150 154	eqtr4d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( K ^ ( b - 1 ) ) x. ( ( 2 x. A ) x. K ) ) = ( ( 2 x. A ) x. ( K ^ b ) ) )
156	144	mulid1d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( K ^ ( b - 1 ) ) x. 1 ) = ( K ^ ( b - 1 ) ) )
157	155 156	oveq12d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( K ^ ( b - 1 ) ) x. ( ( 2 x. A ) x. K ) ) - ( ( K ^ ( b - 1 ) ) x. 1 ) ) = ( ( ( 2 x. A ) x. ( K ^ b ) ) - ( K ^ ( b - 1 ) ) ) )
158	142 147 157	3eqtrrd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( 2 x. A ) x. ( K ^ b ) ) - ( K ^ ( b - 1 ) ) ) = ( ( K ^ ( b - 1 ) ) x. ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) ) )
159	158	oveq1d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( ( 2 x. A ) x. ( K ^ b ) ) - ( K ^ ( b - 1 ) ) ) - ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) ) = ( ( ( K ^ ( b - 1 ) ) x. ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) + ( K ^ 2 ) ) ) - ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) ) )
160	132 159	breqtrrd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( 2 x. A ) x. ( K ^ b ) ) - ( K ^ ( b - 1 ) ) ) - ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) ) )
161	160	adantr	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( 2 x. A ) x. ( K ^ b ) ) - ( K ^ ( b - 1 ) ) ) - ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) ) )
162		congtr	\|- ( ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) e. ZZ ) /\ ( ( ( ( 2 x. A ) x. ( K ^ b ) ) - ( K ^ ( b - 1 ) ) ) e. ZZ /\ ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) e. ZZ ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) - ( ( ( 2 x. A ) x. ( K ^ b ) ) - ( K ^ ( b - 1 ) ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( 2 x. A ) x. ( K ^ b ) ) - ( K ^ ( b - 1 ) ) ) - ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) - ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) ) )
163	79 97 115 161 162	syl112anc	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) - ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) ) )
164		rmxluc	\|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmX ( b + 1 ) ) = ( ( ( 2 x. A ) x. ( A rmX b ) ) - ( A rmX ( b - 1 ) ) ) )
165	54 56 164	syl2anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( A rmX ( b + 1 ) ) = ( ( ( 2 x. A ) x. ( A rmX b ) ) - ( A rmX ( b - 1 ) ) ) )
166		rmyluc	\|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY ( b + 1 ) ) = ( ( 2 x. ( ( A rmY b ) x. A ) ) - ( A rmY ( b - 1 ) ) ) )
167	54 56 166	syl2anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( A rmY ( b + 1 ) ) = ( ( 2 x. ( ( A rmY b ) x. A ) ) - ( A rmY ( b - 1 ) ) ) )
168	167	oveq2d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) = ( ( A - K ) x. ( ( 2 x. ( ( A rmY b ) x. A ) ) - ( A rmY ( b - 1 ) ) ) ) )
169	2	zcnd	\|- ( A e. ( ZZ>= ` 2 ) -> A e. CC )
170	169	ad2antrr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> A e. CC )
171	170 143	subcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( A - K ) e. CC )
172		2cn	\|- 2 e. CC
173	63	zcnd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY b ) e. CC )
174	54 56 173	syl2anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( A rmY b ) e. CC )
175	174 170	mulcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A rmY b ) x. A ) e. CC )
176		mulcl	\|- ( ( 2 e. CC /\ ( ( A rmY b ) x. A ) e. CC ) -> ( 2 x. ( ( A rmY b ) x. A ) ) e. CC )
177	172 175 176	sylancr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( 2 x. ( ( A rmY b ) x. A ) ) e. CC )
178	73	zcnd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ ( b - 1 ) e. ZZ ) -> ( A rmY ( b - 1 ) ) e. CC )
179	54 69 178	syl2anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( A rmY ( b - 1 ) ) e. CC )
180	171 177 179	subdid	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A - K ) x. ( ( 2 x. ( ( A rmY b ) x. A ) ) - ( A rmY ( b - 1 ) ) ) ) = ( ( ( A - K ) x. ( 2 x. ( ( A rmY b ) x. A ) ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) )
181		2cnd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> 2 e. CC )
182	181 174 170	mul12d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( 2 x. ( ( A rmY b ) x. A ) ) = ( ( A rmY b ) x. ( 2 x. A ) ) )
183	174 149	mulcomd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A rmY b ) x. ( 2 x. A ) ) = ( ( 2 x. A ) x. ( A rmY b ) ) )
184	182 183	eqtrd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( 2 x. ( ( A rmY b ) x. A ) ) = ( ( 2 x. A ) x. ( A rmY b ) ) )
185	184	oveq2d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A - K ) x. ( 2 x. ( ( A rmY b ) x. A ) ) ) = ( ( A - K ) x. ( ( 2 x. A ) x. ( A rmY b ) ) ) )
186	171 149 174	mul12d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A - K ) x. ( ( 2 x. A ) x. ( A rmY b ) ) ) = ( ( 2 x. A ) x. ( ( A - K ) x. ( A rmY b ) ) ) )
187	185 186	eqtrd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A - K ) x. ( 2 x. ( ( A rmY b ) x. A ) ) ) = ( ( 2 x. A ) x. ( ( A - K ) x. ( A rmY b ) ) ) )
188	187	oveq1d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( A - K ) x. ( 2 x. ( ( A rmY b ) x. A ) ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) = ( ( ( 2 x. A ) x. ( ( A - K ) x. ( A rmY b ) ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) )
189	168 180 188	3eqtrd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) = ( ( ( 2 x. A ) x. ( ( A - K ) x. ( A rmY b ) ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) )
190	165 189	oveq12d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A rmX ( b + 1 ) ) - ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) ) = ( ( ( ( 2 x. A ) x. ( A rmX b ) ) - ( A rmX ( b - 1 ) ) ) - ( ( ( 2 x. A ) x. ( ( A - K ) x. ( A rmY b ) ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) )
191	58	nn0cnd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmX b ) e. CC )
192	54 56 191	syl2anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( A rmX b ) e. CC )
193	149 192	mulcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( 2 x. A ) x. ( A rmX b ) ) e. CC )
194	70	nn0cnd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ ( b - 1 ) e. ZZ ) -> ( A rmX ( b - 1 ) ) e. CC )
195	54 69 194	syl2anc	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( A rmX ( b - 1 ) ) e. CC )
196	171 174	mulcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A - K ) x. ( A rmY b ) ) e. CC )
197	149 196	mulcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( 2 x. A ) x. ( ( A - K ) x. ( A rmY b ) ) ) e. CC )
198	171 179	mulcld	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) e. CC )
199	193 195 197 198	sub4d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( ( 2 x. A ) x. ( A rmX b ) ) - ( A rmX ( b - 1 ) ) ) - ( ( ( 2 x. A ) x. ( ( A - K ) x. ( A rmY b ) ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) = ( ( ( ( 2 x. A ) x. ( A rmX b ) ) - ( ( 2 x. A ) x. ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) )
200	149 192 196	subdid	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) = ( ( ( 2 x. A ) x. ( A rmX b ) ) - ( ( 2 x. A ) x. ( ( A - K ) x. ( A rmY b ) ) ) ) )
201	200	eqcomd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( 2 x. A ) x. ( A rmX b ) ) - ( ( 2 x. A ) x. ( ( A - K ) x. ( A rmY b ) ) ) ) = ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) )
202	201	oveq1d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( ( 2 x. A ) x. ( A rmX b ) ) - ( ( 2 x. A ) x. ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) = ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) )
203	190 199 202	3eqtrd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( A rmX ( b + 1 ) ) - ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) ) = ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) )
204	143 82	expp1d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( K ^ ( b + 1 ) ) = ( ( K ^ b ) x. K ) )
205		nncn	\|- ( b e. NN -> b e. CC )
206	205	adantl	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> b e. CC )
207		ax-1cn	\|- 1 e. CC
208		npcan	\|- ( ( b e. CC /\ 1 e. CC ) -> ( ( b - 1 ) + 1 ) = b )
209	206 207 208	sylancl	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( b - 1 ) + 1 ) = b )
210	209	oveq2d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( K ^ ( ( b - 1 ) + 1 ) ) = ( K ^ b ) )
211	143 87	expp1d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( K ^ ( ( b - 1 ) + 1 ) ) = ( ( K ^ ( b - 1 ) ) x. K ) )
212	210 211	eqtr3d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( K ^ b ) = ( ( K ^ ( b - 1 ) ) x. K ) )
213	212	oveq1d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( K ^ b ) x. K ) = ( ( ( K ^ ( b - 1 ) ) x. K ) x. K ) )
214	144 143 143	mulassd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( K ^ ( b - 1 ) ) x. K ) x. K ) = ( ( K ^ ( b - 1 ) ) x. ( K x. K ) ) )
215	134	addid2d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( 0 + ( K ^ 2 ) ) = ( K ^ 2 ) )
216	29	sqvald	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( K ^ 2 ) = ( K x. K ) )
217	215 216	eqtr2d	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( K x. K ) = ( 0 + ( K ^ 2 ) ) )
218	217	adantr	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( K x. K ) = ( 0 + ( K ^ 2 ) ) )
219	218	oveq2d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( K ^ ( b - 1 ) ) x. ( K x. K ) ) = ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) )
220	214 219	eqtrd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( K ^ ( b - 1 ) ) x. K ) x. K ) = ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) )
221	204 213 220	3eqtrd	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( K ^ ( b + 1 ) ) = ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) )
222	203 221	oveq12d	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( A rmX ( b + 1 ) ) - ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) ) - ( K ^ ( b + 1 ) ) ) = ( ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) - ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) ) )
223	222	adantr	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( ( A rmX ( b + 1 ) ) - ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) ) - ( K ^ ( b + 1 ) ) ) = ( ( ( ( 2 x. A ) x. ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) ) - ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) ) - ( ( K ^ ( b - 1 ) ) x. ( 0 + ( K ^ 2 ) ) ) ) )
224	163 223	breqtrrd	\|- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) /\ ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b + 1 ) ) - ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) ) - ( K ^ ( b + 1 ) ) ) )
225	224	ex	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ b e. NN ) -> ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b + 1 ) ) - ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) ) - ( K ^ ( b + 1 ) ) ) ) )
226	225	expcom	\|- ( b e. NN -> ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b + 1 ) ) - ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) ) - ( K ^ ( b + 1 ) ) ) ) ) )
227	226	a2d	\|- ( b e. NN -> ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b + 1 ) ) - ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) ) - ( K ^ ( b + 1 ) ) ) ) ) )
228	51 227	syl5	\|- ( b e. NN -> ( ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) ) /\ ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) -> ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b + 1 ) ) - ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) ) - ( K ^ ( b + 1 ) ) ) ) ) )
229		oveq2	\|- ( a = 0 -> ( A rmX a ) = ( A rmX 0 ) )
230		oveq2	\|- ( a = 0 -> ( A rmY a ) = ( A rmY 0 ) )
231	230	oveq2d	\|- ( a = 0 -> ( ( A - K ) x. ( A rmY a ) ) = ( ( A - K ) x. ( A rmY 0 ) ) )
232	229 231	oveq12d	\|- ( a = 0 -> ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) = ( ( A rmX 0 ) - ( ( A - K ) x. ( A rmY 0 ) ) ) )
233		oveq2	\|- ( a = 0 -> ( K ^ a ) = ( K ^ 0 ) )
234	232 233	oveq12d	\|- ( a = 0 -> ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) = ( ( ( A rmX 0 ) - ( ( A - K ) x. ( A rmY 0 ) ) ) - ( K ^ 0 ) ) )
235	234	breq2d	\|- ( a = 0 -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) <-> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX 0 ) - ( ( A - K ) x. ( A rmY 0 ) ) ) - ( K ^ 0 ) ) ) )
236	235	imbi2d	\|- ( a = 0 -> ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX 0 ) - ( ( A - K ) x. ( A rmY 0 ) ) ) - ( K ^ 0 ) ) ) ) )
237		oveq2	\|- ( a = 1 -> ( A rmX a ) = ( A rmX 1 ) )
238		oveq2	\|- ( a = 1 -> ( A rmY a ) = ( A rmY 1 ) )
239	238	oveq2d	\|- ( a = 1 -> ( ( A - K ) x. ( A rmY a ) ) = ( ( A - K ) x. ( A rmY 1 ) ) )
240	237 239	oveq12d	\|- ( a = 1 -> ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) = ( ( A rmX 1 ) - ( ( A - K ) x. ( A rmY 1 ) ) ) )
241		oveq2	\|- ( a = 1 -> ( K ^ a ) = ( K ^ 1 ) )
242	240 241	oveq12d	\|- ( a = 1 -> ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) = ( ( ( A rmX 1 ) - ( ( A - K ) x. ( A rmY 1 ) ) ) - ( K ^ 1 ) ) )
243	242	breq2d	\|- ( a = 1 -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) <-> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX 1 ) - ( ( A - K ) x. ( A rmY 1 ) ) ) - ( K ^ 1 ) ) ) )
244	243	imbi2d	\|- ( a = 1 -> ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX 1 ) - ( ( A - K ) x. ( A rmY 1 ) ) ) - ( K ^ 1 ) ) ) ) )
245		oveq2	\|- ( a = ( b - 1 ) -> ( A rmX a ) = ( A rmX ( b - 1 ) ) )
246		oveq2	\|- ( a = ( b - 1 ) -> ( A rmY a ) = ( A rmY ( b - 1 ) ) )
247	246	oveq2d	\|- ( a = ( b - 1 ) -> ( ( A - K ) x. ( A rmY a ) ) = ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) )
248	245 247	oveq12d	\|- ( a = ( b - 1 ) -> ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) = ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) )
249		oveq2	\|- ( a = ( b - 1 ) -> ( K ^ a ) = ( K ^ ( b - 1 ) ) )
250	248 249	oveq12d	\|- ( a = ( b - 1 ) -> ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) = ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) )
251	250	breq2d	\|- ( a = ( b - 1 ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) <-> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) ) )
252	251	imbi2d	\|- ( a = ( b - 1 ) -> ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b - 1 ) ) - ( ( A - K ) x. ( A rmY ( b - 1 ) ) ) ) - ( K ^ ( b - 1 ) ) ) ) ) )
253		oveq2	\|- ( a = b -> ( A rmX a ) = ( A rmX b ) )
254		oveq2	\|- ( a = b -> ( A rmY a ) = ( A rmY b ) )
255	254	oveq2d	\|- ( a = b -> ( ( A - K ) x. ( A rmY a ) ) = ( ( A - K ) x. ( A rmY b ) ) )
256	253 255	oveq12d	\|- ( a = b -> ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) = ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) )
257		oveq2	\|- ( a = b -> ( K ^ a ) = ( K ^ b ) )
258	256 257	oveq12d	\|- ( a = b -> ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) = ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) )
259	258	breq2d	\|- ( a = b -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) <-> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) )
260	259	imbi2d	\|- ( a = b -> ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX b ) - ( ( A - K ) x. ( A rmY b ) ) ) - ( K ^ b ) ) ) ) )
261		oveq2	\|- ( a = ( b + 1 ) -> ( A rmX a ) = ( A rmX ( b + 1 ) ) )
262		oveq2	\|- ( a = ( b + 1 ) -> ( A rmY a ) = ( A rmY ( b + 1 ) ) )
263	262	oveq2d	\|- ( a = ( b + 1 ) -> ( ( A - K ) x. ( A rmY a ) ) = ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) )
264	261 263	oveq12d	\|- ( a = ( b + 1 ) -> ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) = ( ( A rmX ( b + 1 ) ) - ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) ) )
265		oveq2	\|- ( a = ( b + 1 ) -> ( K ^ a ) = ( K ^ ( b + 1 ) ) )
266	264 265	oveq12d	\|- ( a = ( b + 1 ) -> ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) = ( ( ( A rmX ( b + 1 ) ) - ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) ) - ( K ^ ( b + 1 ) ) ) )
267	266	breq2d	\|- ( a = ( b + 1 ) -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) <-> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b + 1 ) ) - ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) ) - ( K ^ ( b + 1 ) ) ) ) )
268	267	imbi2d	\|- ( a = ( b + 1 ) -> ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX ( b + 1 ) ) - ( ( A - K ) x. ( A rmY ( b + 1 ) ) ) ) - ( K ^ ( b + 1 ) ) ) ) ) )
269		oveq2	\|- ( a = N -> ( A rmX a ) = ( A rmX N ) )
270		oveq2	\|- ( a = N -> ( A rmY a ) = ( A rmY N ) )
271	270	oveq2d	\|- ( a = N -> ( ( A - K ) x. ( A rmY a ) ) = ( ( A - K ) x. ( A rmY N ) ) )
272	269 271	oveq12d	\|- ( a = N -> ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) = ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) )
273		oveq2	\|- ( a = N -> ( K ^ a ) = ( K ^ N ) )
274	272 273	oveq12d	\|- ( a = N -> ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) = ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) - ( K ^ N ) ) )
275	274	breq2d	\|- ( a = N -> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) <-> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) - ( K ^ N ) ) ) )
276	275	imbi2d	\|- ( a = N -> ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX a ) - ( ( A - K ) x. ( A rmY a ) ) ) - ( K ^ a ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) - ( K ^ N ) ) ) ) )
277	34 50 228 236 244 252 260 268 276	2nn0ind	\|- ( N e. NN0 -> ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) - ( K ^ N ) ) ) )
278	277	impcom	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 ) /\ N e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) - ( K ^ N ) ) )
279	278	3impa	\|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 /\ N e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) \|\| ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) - ( K ^ N ) ) )

Metamath Proof Explorer

Theorem jm2.18

Proof