Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  jm2.18 Structured version   Unicode version

Theorem jm2.18 29363
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.)
Assertion
Ref Expression
jm2.18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0  /\  N  e. 
NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  N )  -  ( ( A  -  K )  x.  ( A Yrm  N ) ) )  -  ( K ^ N ) ) )

Proof of Theorem jm2.18
Dummy variables  a 
b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2z 10699 . . . . . . . . . 10  |-  2  e.  ZZ
2 eluzelz 10891 . . . . . . . . . . 11  |-  ( A  e.  ( ZZ>= `  2
)  ->  A  e.  ZZ )
32adantr 465 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  A  e.  ZZ )
4 zmulcl 10714 . . . . . . . . . 10  |-  ( ( 2  e.  ZZ  /\  A  e.  ZZ )  ->  ( 2  x.  A
)  e.  ZZ )
51, 3, 4sylancr 663 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
2  x.  A )  e.  ZZ )
6 nn0z 10690 . . . . . . . . . 10  |-  ( K  e.  NN0  ->  K  e.  ZZ )
76adantl 466 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  K  e.  ZZ )
85, 7zmulcld 10774 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( 2  x.  A
)  x.  K )  e.  ZZ )
9 zsqcl 11957 . . . . . . . . 9  |-  ( K  e.  ZZ  ->  ( K ^ 2 )  e.  ZZ )
107, 9syl 16 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 2 )  e.  ZZ )
118, 10zsubcld 10773 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  e.  ZZ )
12 peano2zm 10709 . . . . . . 7  |-  ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  e.  ZZ  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ )
1311, 12syl 16 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ )
14 dvds0 13569 . . . . . 6  |-  ( ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  0 )
1513, 14syl 16 . . . . 5  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  0 )
16 rmx0 29292 . . . . . . . . . 10  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Xrm  0 )  =  1 )
1716adantr 465 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Xrm  0 )  =  1 )
18 rmy0 29296 . . . . . . . . . . . 12  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Yrm  0 )  =  0 )
1918adantr 465 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Yrm  0 )  =  0 )
2019oveq2d 6128 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  0 ) )  =  ( ( A  -  K )  x.  0 ) )
213, 7zsubcld 10773 . . . . . . . . . . . 12  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  K )  e.  ZZ )
2221zcnd 10769 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  K )  e.  CC )
2322mul01d 9589 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  0 )  =  0 )
2420, 23eqtrd 2475 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  0 ) )  =  0 )
2517, 24oveq12d 6130 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  =  ( 1  -  0 ) )
26 1m0e1 10453 . . . . . . . 8  |-  ( 1  -  0 )  =  1
2725, 26syl6eq 2491 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  =  1 )
28 nn0cn 10610 . . . . . . . . 9  |-  ( K  e.  NN0  ->  K  e.  CC )
2928adantl 466 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  K  e.  CC )
3029exp0d 12023 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 0 )  =  1 )
3127, 30oveq12d 6130 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  -  ( K ^ 0 ) )  =  ( 1  -  1 ) )
32 1m1e0 10411 . . . . . 6  |-  ( 1  -  1 )  =  0
3331, 32syl6eq 2491 . . . . 5  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  -  ( K ^ 0 ) )  =  0 )
3415, 33breqtrrd 4339 . . . 4  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  0 )  -  (
( A  -  K
)  x.  ( A Yrm  0 ) ) )  -  ( K ^
0 ) ) )
35 rmx1 29293 . . . . . . . . . 10  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Xrm  1 )  =  A )
3635adantr 465 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Xrm  1 )  =  A )
37 rmy1 29297 . . . . . . . . . . . 12  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Yrm  1 )  =  1 )
3837adantr 465 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Yrm  1 )  =  1 )
3938oveq2d 6128 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  1 ) )  =  ( ( A  -  K )  x.  1 ) )
4022mulid1d 9424 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  1 )  =  ( A  -  K ) )
4139, 40eqtrd 2475 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  1 ) )  =  ( A  -  K
) )
4236, 41oveq12d 6130 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  =  ( A  -  ( A  -  K
) ) )
433zcnd 10769 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  A  e.  CC )
4443, 29nncand 9745 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  ( A  -  K ) )  =  K )
4542, 44eqtrd 2475 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  =  K )
4629exp1d 12024 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 1 )  =  K )
4745, 46oveq12d 6130 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  -  ( K ^ 1 ) )  =  ( K  -  K ) )
4829subidd 9728 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K  -  K )  =  0 )
4947, 48eqtrd 2475 . . . . 5  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  -  ( K ^ 1 ) )  =  0 )
5015, 49breqtrrd 4339 . . . 4  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  1 )  -  (
( A  -  K
)  x.  ( A Yrm  1 ) ) )  -  ( K ^
1 ) ) )
51 pm3.43 857 . . . . 5  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  ->  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) ) )  /\  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  -> 
( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) ) )
5213adantr 465 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ )
535adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  A
)  e.  ZZ )
54 simpll 753 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  A  e.  ( ZZ>= ` 
2 ) )
55 nnz 10689 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  NN  ->  b  e.  ZZ )
5655adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  ZZ )
57 frmx 29280 . . . . . . . . . . . . . . . . . 18  |- Xrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> NN0
5857fovcl 6216 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Xrm  b )  e.  NN0 )
5954, 56, 58syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  b )  e. 
NN0 )
6059nn0zd 10766 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  b )  e.  ZZ )
6121adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A  -  K
)  e.  ZZ )
62 frmy 29281 . . . . . . . . . . . . . . . . . 18  |- Yrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> ZZ
6362fovcl 6216 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Yrm  b )  e.  ZZ )
6454, 56, 63syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  b )  e.  ZZ )
6561, 64zmulcld 10774 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  b ) )  e.  ZZ )
6660, 65zsubcld 10773 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  e.  ZZ )
6753, 66zmulcld 10774 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  (
( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  e.  ZZ )
68 peano2zm 10709 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  ZZ  ->  (
b  -  1 )  e.  ZZ )
6956, 68syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( b  -  1 )  e.  ZZ )
7057fovcl 6216 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Xrm  ( b  - 
1 ) )  e. 
NN0 )
7154, 69, 70syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  - 
1 ) )  e. 
NN0 )
7271nn0zd 10766 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  - 
1 ) )  e.  ZZ )
7362fovcl 6216 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Yrm  ( b  - 
1 ) )  e.  ZZ )
7454, 69, 73syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  ( b  - 
1 ) )  e.  ZZ )
7561, 74zmulcld 10774 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) )  e.  ZZ )
7672, 75zsubcld 10773 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) )  e.  ZZ )
7767, 76zsubcld 10773 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( A Xrm  ( b  - 
1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  e.  ZZ )
7852, 77jca 532 . . . . . . . . . . 11  |-  ( ( ( 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 Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( A Xrm  ( b  - 
1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  e.  ZZ ) )
7978adantr 465 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  /\  (
( ( 2  x.  A )  x.  (
( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  (
( A  -  K
)  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  e.  ZZ ) )
807adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  K  e.  ZZ )
81 nnnn0 10607 . . . . . . . . . . . . . . . 16  |-  ( b  e.  NN  ->  b  e.  NN0 )
8281adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  NN0 )
83 zexpcl 11901 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  ZZ  /\  b  e.  NN0 )  -> 
( K ^ b
)  e.  ZZ )
8480, 82, 83syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ b
)  e.  ZZ )
8553, 84zmulcld 10774 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  ( K ^ b ) )  e.  ZZ )
86 nnm1nn0 10642 . . . . . . . . . . . . . . 15  |-  ( b  e.  NN  ->  (
b  -  1 )  e.  NN0 )
8786adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( b  -  1 )  e.  NN0 )
88 zexpcl 11901 . . . . . . . . . . . . . 14  |-  ( ( K  e.  ZZ  /\  ( b  -  1 )  e.  NN0 )  ->  ( K ^ (
b  -  1 ) )  e.  ZZ )
8980, 87, 88syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  -  1 ) )  e.  ZZ )
9085, 89zsubcld 10773 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( 2  x.  A )  x.  ( K ^ b
) )  -  ( K ^ ( b  - 
1 ) ) )  e.  ZZ )
91 0z 10678 . . . . . . . . . . . . . . 15  |-  0  e.  ZZ
92 zaddcl 10706 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  ZZ  /\  ( K ^ 2 )  e.  ZZ )  -> 
( 0  +  ( K ^ 2 ) )  e.  ZZ )
9391, 10, 92sylancr 663 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
0  +  ( K ^ 2 ) )  e.  ZZ )
9493adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 0  +  ( K ^ 2 ) )  e.  ZZ )
9589, 94zmulcld 10774 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
( b  -  1 ) )  x.  (
0  +  ( K ^ 2 ) ) )  e.  ZZ )
9690, 95jca 532 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
9796adantr 465 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  ( K ^ b
) )  -  ( K ^ ( b  - 
1 ) ) )  e.  ZZ  /\  (
( K ^ (
b  -  1 ) )  x.  ( 0  +  ( K ^
2 ) ) )  e.  ZZ ) )
9852, 67, 853jca 1168 . . . . . . . . . . . 12  |-  ( ( ( 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 Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  e.  ZZ  /\  ( ( 2  x.  A )  x.  ( K ^ b ) )  e.  ZZ ) )
9998adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  /\  (
( 2  x.  A
)  x.  ( ( A Xrm  b )  -  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )  e.  ZZ  /\  (
( 2  x.  A
)  x.  ( K ^ b ) )  e.  ZZ ) )
10076, 89jca 532 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  e.  ZZ  /\  ( K ^ (
b  -  1 ) )  e.  ZZ ) )
101100adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) )  e.  ZZ  /\  ( K ^ ( b  -  1 ) )  e.  ZZ ) )
10213, 5, 53jca 1168 . . . . . . . . . . . . . 14  |-  ( ( 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 ) )
103102ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )  ->  ( (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  /\  ( 2  x.  A )  e.  ZZ  /\  ( 2  x.  A )  e.  ZZ ) )
10466, 84jca 532 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  e.  ZZ  /\  ( K ^ b
)  e.  ZZ ) )
105104adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )  ->  ( (
( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  e.  ZZ  /\  ( K ^ b )  e.  ZZ ) )
106 congid 29340 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( 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
) ) )
10713, 5, 106syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( 2  x.  A )  -  (
2  x.  A ) ) )
108107ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( 2  x.  A )  -  (
2  x.  A ) ) )
109 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )
110 congmul 29336 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  e.  ZZ  /\  ( 2  x.  A
)  e.  ZZ  /\  ( 2  x.  A
)  e.  ZZ )  /\  ( ( ( A Xrm  b )  -  (
( A  -  K
)  x.  ( A Yrm  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 Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( 2  x.  A
)  x.  ( K ^ b ) ) ) )
111103, 105, 108, 109, 110syl112anc 1222 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( 2  x.  A
)  x.  ( K ^ b ) ) ) )
112111adantrl 715 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( 2  x.  A
)  x.  ( K ^ b ) ) ) )
113 simprl 755 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) ) )
114 congsub 29339 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  e.  ZZ  /\  ( ( 2  x.  A )  x.  (
( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  e.  ZZ  /\  ( ( 2  x.  A )  x.  ( K ^ b ) )  e.  ZZ )  /\  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  e.  ZZ  /\  ( K ^ (
b  -  1 ) )  e.  ZZ )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( 2  x.  A
)  x.  ( K ^ b ) ) )  /\  ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) ) )  -  (
( ( 2  x.  A )  x.  ( K ^ b ) )  -  ( K ^
( b  -  1 ) ) ) ) )
11599, 101, 112, 113, 114syl112anc 1222 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) ) )  -  (
( ( 2  x.  A )  x.  ( K ^ b ) )  -  ( K ^
( b  -  1 ) ) ) ) )
11613, 10zaddcld 10772 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  +  ( K ^
2 ) )  e.  ZZ )
117116adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  +  ( K ^ 2 ) )  e.  ZZ )
118 congid 29340 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( 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 ) ) ) )
11952, 89, 118syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( 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 10679 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  0  e.  ZZ )
121 iddvds 13567 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( 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 ) )
12213, 121syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) )
12313zcnd 10769 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  CC )
124123subid1d 9729 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  -  0 )  =  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) )
125122, 124breqtrrd 4339 . . . . . . . . . . . . . . 15  |-  ( ( 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 29340 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( 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 ) ) )
12713, 10, 126syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( K ^
2 )  -  ( K ^ 2 ) ) )
128 congadd 29335 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( 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 ) ) ) )
12913, 13, 120, 10, 10, 125, 127, 128syl322anc 1246 . . . . . . . . . . . . . 14  |-  ( ( 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 ) ) ) )
130129adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( 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 29336 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( 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 ) ) ) ) )
13252, 89, 89, 117, 94, 119, 130, 131syl322anc 1246 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) ) )
13311zcnd 10769 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  e.  CC )
13429sqcld 12027 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 2 )  e.  CC )
135 ax-1cn 9361 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  CC
136135a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  1  e.  CC )
137133, 134, 136addsubd 9761 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 ) ) )
1388zcnd 10769 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( 2  x.  A
)  x.  K )  e.  CC )
139138, 134npcand 9744 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  +  ( K ^
2 ) )  =  ( ( 2  x.  A )  x.  K
) )
140139oveq1d 6127 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  +  ( K ^ 2 ) )  -  1 )  =  ( ( ( 2  x.  A )  x.  K )  -  1 ) )
141137, 140eqtr3d 2477 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  +  ( K ^
2 ) )  =  ( ( ( 2  x.  A )  x.  K )  -  1 ) )
142141adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) )
143142oveq2d 6128 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) )
14428ad2antlr 726 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  K  e.  CC )
145144, 87expcld 12029 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  -  1 ) )  e.  CC )
146138adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  K
)  e.  CC )
147135a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  1  e.  CC )
148145, 146, 147subdid 9821 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) )
1495zcnd 10769 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
2  x.  A )  e.  CC )
150149adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  A
)  e.  CC )
151145, 150, 144mul12d 9599 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )
152 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  NN )
153 expm1t 11913 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  CC  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
154144, 152, 153syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
155154oveq2d 6128 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) ) )
156151, 155eqtr4d 2478 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
157145mulid1d 9424 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
( b  -  1 ) )  x.  1 )  =  ( K ^ ( b  - 
1 ) ) )
158156, 157oveq12d 6130 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) ) )
159143, 148, 1583eqtrrd 2480 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) ) )
160159oveq1d 6127 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) ) )
161132, 160breqtrrd 4339 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) ) )
162161adantr 465 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  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 ) ) ) ) )
163 congtr 29334 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  e.  ZZ  /\  ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( A Xrm  ( b  - 
1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( 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 Xrm  b )  -  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( 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 Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) ) )  -  (
( K ^ (
b  -  1 ) )  x.  ( 0  +  ( K ^
2 ) ) ) ) )
16479, 97, 115, 162, 163syl112anc 1222 . . . . . . . . 9  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) ) )  -  (
( K ^ (
b  -  1 ) )  x.  ( 0  +  ( K ^
2 ) ) ) ) )
165 rmxluc 29303 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Xrm  ( b  +  1 ) )  =  ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( A Xrm  ( b  - 
1 ) ) ) )
16654, 56, 165syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  +  1 ) )  =  ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( A Xrm  ( b  -  1 ) ) ) )
167 rmyluc 29304 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Yrm  ( b  +  1 ) )  =  ( ( 2  x.  (
( A Yrm  b )  x.  A ) )  -  ( A Yrm  ( b  - 
1 ) ) ) )
16854, 56, 167syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  ( b  +  1 ) )  =  ( ( 2  x.  ( ( A Yrm  b )  x.  A ) )  -  ( A Yrm  ( b  -  1 ) ) ) )
169168oveq2d 6128 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) )  =  ( ( A  -  K )  x.  (
( 2  x.  (
( A Yrm  b )  x.  A ) )  -  ( A Yrm  ( b  - 
1 ) ) ) ) )
1702zcnd 10769 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  ( ZZ>= `  2
)  ->  A  e.  CC )
171170ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  A  e.  CC )
172171, 144subcld 9740 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A  -  K
)  e.  CC )
173 2cn 10413 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
17463zcnd 10769 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Yrm  b )  e.  CC )
17554, 56, 174syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  b )  e.  CC )
176175, 171mulcld 9427 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Yrm  b )  x.  A )  e.  CC )
177 mulcl 9387 . . . . . . . . . . . . . . . 16  |-  ( ( 2  e.  CC  /\  ( ( A Yrm  b )  x.  A )  e.  CC )  ->  (
2  x.  ( ( A Yrm  b )  x.  A
) )  e.  CC )
178173, 176, 177sylancr 663 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  (
( A Yrm  b )  x.  A ) )  e.  CC )
17973zcnd 10769 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Yrm  ( b  - 
1 ) )  e.  CC )
18054, 69, 179syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  ( b  - 
1 ) )  e.  CC )
181172, 178, 180subdid 9821 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  (
( 2  x.  (
( A Yrm  b )  x.  A ) )  -  ( A Yrm  ( b  - 
1 ) ) ) )  =  ( ( ( A  -  K
)  x.  ( 2  x.  ( ( A Yrm  b )  x.  A ) ) )  -  (
( A  -  K
)  x.  ( A Yrm  ( b  -  1 ) ) ) ) )
182 2cnd 10415 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  2  e.  CC )
183182, 175, 171mul12d 9599 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  (
( A Yrm  b )  x.  A ) )  =  ( ( A Yrm  b )  x.  ( 2  x.  A ) ) )
184175, 150mulcomd 9428 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Yrm  b )  x.  ( 2  x.  A ) )  =  ( ( 2  x.  A )  x.  ( A Yrm  b ) ) )
185183, 184eqtrd 2475 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  (
( A Yrm  b )  x.  A ) )  =  ( ( 2  x.  A )  x.  ( A Yrm  b ) ) )
186185oveq2d 6128 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  (
2  x.  ( ( A Yrm  b )  x.  A
) ) )  =  ( ( A  -  K )  x.  (
( 2  x.  A
)  x.  ( A Yrm  b ) ) ) )
187172, 150, 175mul12d 9599 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  (
( 2  x.  A
)  x.  ( A Yrm  b ) ) )  =  ( ( 2  x.  A )  x.  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )
188186, 187eqtrd 2475 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  (
2  x.  ( ( A Yrm  b )  x.  A
) ) )  =  ( ( 2  x.  A )  x.  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )
189188oveq1d 6127 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( A  -  K )  x.  ( 2  x.  (
( A Yrm  b )  x.  A ) ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) )  =  ( ( ( 2  x.  A
)  x.  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  (
( A  -  K
)  x.  ( A Yrm  ( b  -  1 ) ) ) ) )
190169, 181, 1893eqtrd 2479 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) )  =  ( ( ( 2  x.  A )  x.  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) ) )
191166, 190oveq12d 6130 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Xrm  ( b  +  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) ) )  =  ( ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( A Xrm  ( b  - 
1 ) ) )  -  ( ( ( 2  x.  A )  x.  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) ) )
19258nn0cnd 10659 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Xrm  b )  e.  CC )
19354, 56, 192syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  b )  e.  CC )
194150, 193mulcld 9427 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  ( A Xrm  b ) )  e.  CC )
19570nn0cnd 10659 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Xrm  ( b  - 
1 ) )  e.  CC )
19654, 69, 195syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  - 
1 ) )  e.  CC )
197172, 175mulcld 9427 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  b ) )  e.  CC )
198150, 197mulcld 9427 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  (
( A  -  K
)  x.  ( A Yrm  b ) ) )  e.  CC )
199172, 180mulcld 9427 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) )  e.  CC )
200194, 196, 198, 199sub4d 9789 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( A Xrm  ( b  -  1 ) ) )  -  (
( ( 2  x.  A )  x.  (
( A  -  K
)  x.  ( A Yrm  b ) ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  =  ( ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( ( 2  x.  A )  x.  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) ) )
201150, 193, 197subdid 9821 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  (
( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  =  ( ( ( 2  x.  A
)  x.  ( A Xrm  b ) )  -  (
( 2  x.  A
)  x.  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) ) )
202201eqcomd 2448 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( ( 2  x.  A )  x.  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  =  ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) ) )
203202oveq1d 6127 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( ( 2  x.  A )  x.  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( A Xrm  ( b  - 
1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  =  ( ( ( 2  x.  A
)  x.  ( ( A Xrm  b )  -  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) ) )
204191, 200, 2033eqtrd 2479 . . . . . . . . . . 11  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Xrm  ( b  +  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) ) )  =  ( ( ( 2  x.  A
)  x.  ( ( A Xrm  b )  -  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) ) )
205144, 82expp1d 12030 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  +  1 ) )  =  ( ( K ^ b )  x.  K ) )
206 nncn 10351 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  NN  ->  b  e.  CC )
207206adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  CC )
208 npcan 9640 . . . . . . . . . . . . . . . 16  |-  ( ( b  e.  CC  /\  1  e.  CC )  ->  ( ( b  - 
1 )  +  1 )  =  b )
209207, 135, 208sylancl 662 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( b  - 
1 )  +  1 )  =  b )
210209oveq2d 6128 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
( b  -  1 )  +  1 ) )  =  ( K ^ b ) )
211144, 87expp1d 12030 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
( b  -  1 )  +  1 ) )  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
212210, 211eqtr3d 2477 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
213212oveq1d 6127 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
b )  x.  K
)  =  ( ( ( K ^ (
b  -  1 ) )  x.  K )  x.  K ) )
214145, 144, 144mulassd 9430 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( K ^ ( b  - 
1 ) )  x.  K )  x.  K
)  =  ( ( K ^ ( b  -  1 ) )  x.  ( K  x.  K ) ) )
215134addid2d 9591 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
0  +  ( K ^ 2 ) )  =  ( K ^
2 ) )
21629sqvald 12026 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 2 )  =  ( K  x.  K
) )
217215, 216eqtr2d 2476 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K  x.  K )  =  ( 0  +  ( K ^ 2 ) ) )
218217adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K  x.  K
)  =  ( 0  +  ( K ^
2 ) ) )
219218oveq2d 6128 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
( b  -  1 ) )  x.  ( K  x.  K )
)  =  ( ( K ^ ( b  -  1 ) )  x.  ( 0  +  ( K ^ 2 ) ) ) )
220214, 219eqtrd 2475 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( K ^ ( b  - 
1 ) )  x.  K )  x.  K
)  =  ( ( K ^ ( b  -  1 ) )  x.  ( 0  +  ( K ^ 2 ) ) ) )
221205, 213, 2203eqtrd 2479 . . . . . . . . . . 11  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  +  1 ) )  =  ( ( K ^ ( b  -  1 ) )  x.  ( 0  +  ( K ^ 2 ) ) ) )
222204, 221oveq12d 6130 . . . . . . . . . 10  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( A Xrm  ( b  +  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) ) )  -  ( K ^ ( b  +  1 ) ) )  =  ( ( ( ( 2  x.  A
)  x.  ( ( A Xrm  b )  -  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  -  ( ( K ^
( b  -  1 ) )  x.  (
0  +  ( K ^ 2 ) ) ) ) )
223222adantr 465 . . . . . . . . 9  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( A Xrm  ( b  +  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) ) )  -  ( K ^ ( b  +  1 ) ) )  =  ( ( ( ( 2  x.  A
)  x.  ( ( A Xrm  b )  -  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  -  ( ( K ^
( b  -  1 ) )  x.  (
0  +  ( K ^ 2 ) ) ) ) )
224164, 223breqtrrd 4339 . . . . . . . 8  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  +  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) ) )  -  ( K ^ ( b  +  1 ) ) ) )
225224ex 434 . . . . . . 7  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  +  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) ) )  -  ( K ^ ( b  +  1 ) ) ) ) )
226225expcom 435 . . . . . 6  |-  ( b  e.  NN  ->  (
( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  -> 
( ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  +  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) ) )  -  ( K ^ ( b  +  1 ) ) ) ) ) )
227226a2d 26 . . . . 5  |-  ( b  e.  NN  ->  (
( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  ->  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  -> 
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( ( A Xrm  ( b  +  1 ) )  -  (
( A  -  K
)  x.  ( A Yrm  ( b  +  1 ) ) ) )  -  ( K ^ ( b  +  1 ) ) ) ) ) )
22851, 227syl5 32 . . . 4  |-  ( b  e.  NN  ->  (
( ( ( A  e.  ( ZZ>= `  2
)  /\  K  e.  NN0 )  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) ) )  /\  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  -> 
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( ( A Xrm  ( b  +  1 ) )  -  (
( A  -  K
)  x.  ( A Yrm  ( b  +  1 ) ) ) )  -  ( K ^ ( b  +  1 ) ) ) ) ) )
229 oveq2 6120 . . . . . . . 8  |-  ( a  =  0  ->  ( A Xrm  a )  =  ( A Xrm  0 ) )
230 oveq2 6120 . . . . . . . . 9  |-  ( a  =  0  ->  ( A Yrm  a )  =  ( A Yrm  0 ) )
231230oveq2d 6128 . . . . . . . 8  |-  ( a  =  0  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  0 ) ) )
232229, 231oveq12d 6130 . . . . . . 7  |-  ( a  =  0  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  0 )  -  (
( A  -  K
)  x.  ( A Yrm  0 ) ) ) )
233 oveq2 6120 . . . . . . 7  |-  ( a  =  0  ->  ( K ^ a )  =  ( K ^ 0 ) )
234232, 233oveq12d 6130 . . . . . 6  |-  ( a  =  0  ->  (
( ( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) )  =  ( ( ( A Xrm  0 )  -  (
( A  -  K
)  x.  ( A Yrm  0 ) ) )  -  ( K ^
0 ) ) )
235234breq2d 4325 . . . . 5  |-  ( a  =  0  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( ( A Xrm  a )  -  (
( A  -  K
)  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) )  <->  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  -  ( K ^ 0 ) ) ) )
236235imbi2d 316 . . . 4  |-  ( a  =  0  ->  (
( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  ->  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) ) )  <->  ( ( A  e.  ( ZZ>= `  2
)  /\  K  e.  NN0 )  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  0 )  -  (
( A  -  K
)  x.  ( A Yrm  0 ) ) )  -  ( K ^
0 ) ) ) ) )
237 oveq2 6120 . . . . . . . 8  |-  ( a  =  1  ->  ( A Xrm  a )  =  ( A Xrm  1 ) )
238 oveq2 6120 . . . . . . . . 9  |-  ( a  =  1  ->  ( A Yrm  a )  =  ( A Yrm  1 ) )
239238oveq2d 6128 . . . . . . . 8  |-  ( a  =  1  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  1 ) ) )
240237, 239oveq12d 6130 . . . . . . 7  |-  ( a  =  1  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  1 )  -  (
( A  -  K
)  x.  ( A Yrm  1 ) ) ) )
241 oveq2 6120 . . . . . . 7  |-  ( a  =  1  ->  ( K ^ a )  =  ( K ^ 1 ) )
242240, 241oveq12d 6130 . . . . . 6  |-  ( a  =  1  ->  (
( ( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) )  =  ( ( ( A Xrm  1 )  -  (
( A  -  K
)  x.  ( A Yrm  1 ) ) )  -  ( K ^
1 ) ) )
243242breq2d 4325 . . . . 5  |-  ( a  =  1  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( ( A Xrm  a )  -  (
( A  -  K
)  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) )  <->  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  -  ( K ^ 1 ) ) ) )
244243imbi2d 316 . . . 4  |-  ( a  =  1  ->  (
( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  ->  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) ) )  <->  ( ( A  e.  ( ZZ>= `  2
)  /\  K  e.  NN0 )  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  1 )  -  (
( A  -  K
)  x.  ( A Yrm  1 ) ) )  -  ( K ^
1 ) ) ) ) )
245 oveq2 6120 . . . . . . . 8  |-  ( a  =  ( b  - 
1 )  ->  ( A Xrm  a )  =  ( A Xrm  ( b  -  1 ) ) )
246 oveq2 6120 . . . . . . . . 9  |-  ( a  =  ( b  - 
1 )  ->  ( A Yrm  a )  =  ( A Yrm  ( b  -  1 ) ) )
247246oveq2d 6128 . . . . . . . 8  |-  ( a  =  ( b  - 
1 )  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  ( b  -  1 ) ) ) )
248245, 247oveq12d 6130 . . . . . . 7  |-  ( a  =  ( b  - 
1 )  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) )
249 oveq2 6120 . . . . . . 7  |-  ( a  =  ( b  - 
1 )  ->  ( K ^ a )  =  ( K ^ (
b  -  1 ) ) )
250248, 249oveq12d 6130 . . . . . 6  |-  ( a  =  ( b  - 
1 )  ->  (
( ( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) )  =  ( ( ( A Xrm  ( b  -  1 ) )  -  (
( A  -  K
)  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  -  1 ) ) ) )
251250breq2d 4325 . . . . 5  |-  ( a  =  ( b  - 
1 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( ( A Xrm  a )  -  (
( A  -  K
)  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) )  <->  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) ) ) )
252251imbi2d 316 . . . 4  |-  ( a  =  ( b  - 
1 )  ->  (
( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  ->  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) ) )  <->  ( ( A  e.  ( ZZ>= `  2
)  /\  K  e.  NN0 )  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) ) ) ) )
253 oveq2 6120 . . . . . . . 8  |-  ( a  =  b  ->  ( A Xrm  a )  =  ( A Xrm  b ) )
254 oveq2 6120 . . . . . . . . 9  |-  ( a  =  b  ->  ( A Yrm  a )  =  ( A Yrm  b ) )
255254oveq2d 6128 . . . . . . . 8  |-  ( a  =  b  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  b ) ) )
256253, 255oveq12d 6130 . . . . . . 7  |-  ( a  =  b  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )
257 oveq2 6120 . . . . . . 7  |-  ( a  =  b  ->  ( K ^ a )  =  ( K ^ b
) )
258256, 257oveq12d 6130 . . . . . 6  |-  ( a  =  b  ->  (
( ( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) )  =  ( ( ( A Xrm  b )  -  (
( A  -  K
)  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )
259258breq2d 4325 . . . . 5  |-  ( a  =  b  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( ( A Xrm  a )  -  (
( A  -  K
)  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) )  <->  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )
260259imbi2d 316 . . . 4  |-  ( a  =  b  ->  (
( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  ->  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) ) )  <->  ( ( A  e.  ( ZZ>= `  2
)  /\  K  e.  NN0 )  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) ) )
261 oveq2 6120 . . . . . . . 8  |-  ( a  =  ( b  +  1 )  ->  ( A Xrm  a )  =  ( A Xrm  ( b  +  1 ) ) )
262 oveq2 6120 . . . . . . . . 9  |-  ( a  =  ( b  +  1 )  ->  ( A Yrm  a )  =  ( A Yrm  ( b  +  1 ) ) )
263262oveq2d 6128 . . . . . . . 8  |-  ( a  =  ( b  +  1 )  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  ( b  +  1 ) ) ) )
264261, 263oveq12d 6130 . . . . . . 7  |-  ( a  =  ( b  +  1 )  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  ( b  +  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) ) ) )
265 oveq2 6120 . . . . . . 7  |-  ( a  =  ( b  +  1 )  ->  ( K ^ a )  =  ( K ^ (
b  +  1 ) ) )
266264, 265oveq12d 6130 . . . . . 6  |-  ( a  =  ( b  +  1 )  ->  (
( ( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) )  =  ( ( ( A Xrm  ( b  +  1 ) )  -  (
( A