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 30905
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 10902 . . . . . . . . . 10  |-  2  e.  ZZ
2 eluzelz 11099 . . . . . . . . . . 11  |-  ( A  e.  ( ZZ>= `  2
)  ->  A  e.  ZZ )
32adantr 465 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  A  e.  ZZ )
4 zmulcl 10918 . . . . . . . . . 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 10893 . . . . . . . . . 10  |-  ( K  e.  NN0  ->  K  e.  ZZ )
76adantl 466 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  K  e.  ZZ )
85, 7zmulcld 10980 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( 2  x.  A
)  x.  K )  e.  ZZ )
9 zsqcl 12217 . . . . . . . . 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 10979 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  e.  ZZ )
12 peano2zm 10913 . . . . . . 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 13876 . . . . . 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 30836 . . . . . . . . . 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 30840 . . . . . . . . . . . 12  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Yrm  0 )  =  0 )
1918adantr 465 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Yrm  0 )  =  0 )
2019oveq2d 6297 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  0 ) )  =  ( ( A  -  K )  x.  0 ) )
213, 7zsubcld 10979 . . . . . . . . . . . 12  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  K )  e.  ZZ )
2221zcnd 10975 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  K )  e.  CC )
2322mul01d 9782 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  0 )  =  0 )
2420, 23eqtrd 2484 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  0 ) )  =  0 )
2517, 24oveq12d 6299 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  =  ( 1  -  0 ) )
26 1m0e1 10652 . . . . . . . 8  |-  ( 1  -  0 )  =  1
2725, 26syl6eq 2500 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  =  1 )
28 nn0cn 10811 . . . . . . . . 9  |-  ( K  e.  NN0  ->  K  e.  CC )
2928adantl 466 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  K  e.  CC )
3029exp0d 12283 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 0 )  =  1 )
3127, 30oveq12d 6299 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  -  ( K ^ 0 ) )  =  ( 1  -  1 ) )
32 1m1e0 10610 . . . . . 6  |-  ( 1  -  1 )  =  0
3331, 32syl6eq 2500 . . . . 5  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  -  ( K ^ 0 ) )  =  0 )
3415, 33breqtrrd 4463 . . . 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 30837 . . . . . . . . . 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 30841 . . . . . . . . . . . 12  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Yrm  1 )  =  1 )
3837adantr 465 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Yrm  1 )  =  1 )
3938oveq2d 6297 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  1 ) )  =  ( ( A  -  K )  x.  1 ) )
4022mulid1d 9616 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  1 )  =  ( A  -  K ) )
4139, 40eqtrd 2484 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  1 ) )  =  ( A  -  K
) )
4236, 41oveq12d 6299 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  =  ( A  -  ( A  -  K
) ) )
433zcnd 10975 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  A  e.  CC )
4443, 29nncand 9941 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  ( A  -  K ) )  =  K )
4542, 44eqtrd 2484 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  =  K )
4629exp1d 12284 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 1 )  =  K )
4745, 46oveq12d 6299 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  -  ( K ^ 1 ) )  =  ( K  -  K ) )
4829subidd 9924 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K  -  K )  =  0 )
4947, 48eqtrd 2484 . . . . 5  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  -  ( K ^ 1 ) )  =  0 )
5015, 49breqtrrd 4463 . . . 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 862 . . . . 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 10892 . . . . . . . . . . . . . . . . . 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 30824 . . . . . . . . . . . . . . . . . 18  |- Xrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> NN0
5857fovcl 6392 . . . . . . . . . . . . . . . . 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 10972 . . . . . . . . . . . . . . 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 30825 . . . . . . . . . . . . . . . . . 18  |- Yrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> ZZ
6362fovcl 6392 . . . . . . . . . . . . . . . . 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 10980 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  b ) )  e.  ZZ )
6660, 65zsubcld 10979 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  e.  ZZ )
6753, 66zmulcld 10980 . . . . . . . . . . . . 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 10913 . . . . . . . . . . . . . . . . 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 6392 . . . . . . . . . . . . . . . 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 10972 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  - 
1 ) )  e.  ZZ )
7362fovcl 6392 . . . . . . . . . . . . . . . 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 10980 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) )  e.  ZZ )
7672, 75zsubcld 10979 . . . . . . . . . . . . 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 10979 . . . . . . . . . . . 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 10808 . . . . . . . . . . . . . . . 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 12160 . . . . . . . . . . . . . . 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 10980 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  ( K ^ b ) )  e.  ZZ )
86 nnm1nn0 10843 . . . . . . . . . . . . . . 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 12160 . . . . . . . . . . . . . 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 10979 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( 2  x.  A )  x.  ( K ^ b
) )  -  ( K ^ ( b  - 
1 ) ) )  e.  ZZ )
91 0z 10881 . . . . . . . . . . . . . . 15  |-  0  e.  ZZ
92 zaddcl 10910 . . . . . . . . . . . . . . 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 10980 . . . . . . . . . . . 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 1177 . . . . . . . . . . . 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 1177 . . . . . . . . . . . . . 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 30884 . . . . . . . . . . . . . . 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 30880 . . . . . . . . . . . . 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 1233 . . . . . . . . . . . 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 756 . . . . . . . . . . 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 30883 . . . . . . . . . . 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 1233 . . . . . . . . . 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 10978 . . . . . . . . . . . . . 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 30884 . . . . . . . . . . . . . 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 10882 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  0  e.  ZZ )
121 iddvds 13874 . . . . . . . . . . . . . . . . 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 10975 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  CC )
124123subid1d 9925 . . . . . . . . . . . . . . . 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 4463 . . . . . . . . . . . . . . 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 30884 . . . . . . . . . . . . . . . 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 30879 . . . . . . . . . . . . . . 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 1257 . . . . . . . . . . . . . 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 30880 . . . . . . . . . . . . 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 1257 . . . . . . . . . . . 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 10975 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  e.  CC )
13429sqcld 12287 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 2 )  e.  CC )
135 1cnd 9615 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  1  e.  CC )
136133, 134, 135addsubd 9957 . . . . . . . . . . . . . . . . 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 ) ) )
1378zcnd 10975 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( 2  x.  A
)  x.  K )  e.  CC )
138137, 134npcand 9940 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  +  ( K ^
2 ) )  =  ( ( 2  x.  A )  x.  K
) )
139138oveq1d 6296 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  +  ( K ^ 2 ) )  -  1 )  =  ( ( ( 2  x.  A )  x.  K )  -  1 ) )
140136, 139eqtr3d 2486 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  +  ( K ^
2 ) )  =  ( ( ( 2  x.  A )  x.  K )  -  1 ) )
141140adantr 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 ) )
142141oveq2d 6297 . . . . . . . . . . . . . 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 ) ) )
14328ad2antlr 726 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  K  e.  CC )
144143, 87expcld 12289 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  -  1 ) )  e.  CC )
145137adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  K
)  e.  CC )
146 1cnd 9615 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  1  e.  CC )
147144, 145, 146subdid 10018 . . . . . . . . . . . . . 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 ) ) )
1485zcnd 10975 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
2  x.  A )  e.  CC )
149148adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  A
)  e.  CC )
150144, 149, 143mul12d 9792 . . . . . . . . . . . . . . . 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 ) ) )
151 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  NN )
152 expm1t 12173 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  CC  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
153143, 151, 152syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
154153oveq2d 6297 . . . . . . . . . . . . . . . 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
) ) )
155150, 154eqtr4d 2487 . . . . . . . . . . . . . . 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 ) ) )
156144mulid1d 9616 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
( b  -  1 ) )  x.  1 )  =  ( K ^ ( b  - 
1 ) ) )
157155, 156oveq12d 6299 . . . . . . . . . . . . . 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 ) ) ) )
158142, 147, 1573eqtrrd 2489 . . . . . . . . . . . . 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 ) ) ) )
159158oveq1d 6296 . . . . . . . . . . . 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 ) ) ) ) )
160132, 159breqtrrd 4463 . . . . . . . . . . 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 ) ) ) ) )
161160adantr 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 ) ) ) ) )
162 congtr 30878 . . . . . . . . . 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 ) ) ) ) )
16379, 97, 115, 161, 162syl112anc 1233 . . . . . . . . 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 ) ) ) ) )
164 rmxluc 30847 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Xrm  ( b  +  1 ) )  =  ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( A Xrm  ( b  - 
1 ) ) ) )
16554, 56, 164syl2anc 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 ) ) ) )
166 rmyluc 30848 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Yrm  ( b  +  1 ) )  =  ( ( 2  x.  (
( A Yrm  b )  x.  A ) )  -  ( A Yrm  ( b  - 
1 ) ) ) )
16754, 56, 166syl2anc 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 ) ) ) )
168167oveq2d 6297 . . . . . . . . . . . . . 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 ) ) ) ) )
1692zcnd 10975 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  ( ZZ>= `  2
)  ->  A  e.  CC )
170169ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  A  e.  CC )
171170, 143subcld 9936 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A  -  K
)  e.  CC )
172 2cn 10612 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
17363zcnd 10975 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Yrm  b )  e.  CC )
17454, 56, 173syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  b )  e.  CC )
175174, 170mulcld 9619 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Yrm  b )  x.  A )  e.  CC )
176 mulcl 9579 . . . . . . . . . . . . . . . 16  |-  ( ( 2  e.  CC  /\  ( ( A Yrm  b )  x.  A )  e.  CC )  ->  (
2  x.  ( ( A Yrm  b )  x.  A
) )  e.  CC )
177172, 175, 176sylancr 663 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  (
( A Yrm  b )  x.  A ) )  e.  CC )
17873zcnd 10975 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Yrm  ( b  - 
1 ) )  e.  CC )
17954, 69, 178syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  ( b  - 
1 ) )  e.  CC )
180171, 177, 179subdid 10018 . . . . . . . . . . . . . 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 ) ) ) ) )
181 2cnd 10614 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  2  e.  CC )
182181, 174, 170mul12d 9792 . . . . . . . . . . . . . . . . . 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 ) ) )
183174, 149mulcomd 9620 . . . . . . . . . . . . . . . . . 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 ) ) )
184182, 183eqtrd 2484 . . . . . . . . . . . . . . . . 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 ) ) )
185184oveq2d 6297 . . . . . . . . . . . . . . . 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 ) ) ) )
186171, 149, 174mul12d 9792 . . . . . . . . . . . . . . . 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 ) ) ) )
187185, 186eqtrd 2484 . . . . . . . . . . . . . . 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 ) ) ) )
188187oveq1d 6296 . . . . . . . . . . . . . 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 ) ) ) ) )
189168, 180, 1883eqtrd 2488 . . . . . . . . . . . . 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 ) ) ) ) )
190165, 189oveq12d 6299 . . . . . . . . . . . 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 ) ) ) ) ) )
19158nn0cnd 10860 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Xrm  b )  e.  CC )
19254, 56, 191syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  b )  e.  CC )
193149, 192mulcld 9619 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  ( A Xrm  b ) )  e.  CC )
19470nn0cnd 10860 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Xrm  ( b  - 
1 ) )  e.  CC )
19554, 69, 194syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  - 
1 ) )  e.  CC )
196171, 174mulcld 9619 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  b ) )  e.  CC )
197149, 196mulcld 9619 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  (
( A  -  K
)  x.  ( A Yrm  b ) ) )  e.  CC )
198171, 179mulcld 9619 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) )  e.  CC )
199193, 195, 197, 198sub4d 9985 . . . . . . . . . . . 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 ) ) ) ) ) )
200149, 192, 196subdid 10018 . . . . . . . . . . . . . 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 ) ) ) ) )
201200eqcomd 2451 . . . . . . . . . . . . 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 ) ) ) ) )
202201oveq1d 6296 . . . . . . . . . . . 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 ) ) ) ) ) )
203190, 199, 2023eqtrd 2488 . . . . . . . . . . 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 ) ) ) ) ) )
204143, 82expp1d 12290 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  +  1 ) )  =  ( ( K ^ b )  x.  K ) )
205 nncn 10550 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  NN  ->  b  e.  CC )
206205adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  CC )
207 ax-1cn 9553 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
208 npcan 9834 . . . . . . . . . . . . . . . 16  |-  ( ( b  e.  CC  /\  1  e.  CC )  ->  ( ( b  - 
1 )  +  1 )  =  b )
209206, 207, 208sylancl 662 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( b  - 
1 )  +  1 )  =  b )
210209oveq2d 6297 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
( b  -  1 )  +  1 ) )  =  ( K ^ b ) )
211143, 87expp1d 12290 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
( b  -  1 )  +  1 ) )  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
212210, 211eqtr3d 2486 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
213212oveq1d 6296 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
b )  x.  K
)  =  ( ( ( K ^ (
b  -  1 ) )  x.  K )  x.  K ) )
214144, 143, 143mulassd 9622 . . . . . . . . . . . . 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 9784 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
0  +  ( K ^ 2 ) )  =  ( K ^
2 ) )
21629sqvald 12286 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 2 )  =  ( K  x.  K
) )
217215, 216eqtr2d 2485 . . . . . . . . . . . . . . 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 6297 . . . . . . . . . . . . 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 2484 . . . . . . . . . . . 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 ) ) ) )
221204, 213, 2203eqtrd 2488 . . . . . . . . . . 11  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  +  1 ) )  =  ( ( K ^ ( b  -  1 ) )  x.  ( 0  +  ( K ^ 2 ) ) ) )
222203, 221oveq12d 6299 . . . . . . . . . 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 ) ) ) ) )
224163, 223breqtrrd 4463 . . . . . . . 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 6289 . . . . . . . 8  |-  ( a  =  0  ->  ( A Xrm  a )  =  ( A Xrm  0 ) )
230 oveq2 6289 . . . . . . . . 9  |-  ( a  =  0  ->  ( A Yrm  a )  =  ( A Yrm  0 ) )
231230oveq2d 6297 . . . . . . . 8  |-  ( a  =  0  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  0 ) ) )
232229, 231oveq12d 6299 . . . . . . 7  |-  ( a  =  0  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  0 )  -  (
( A  -  K
)  x.  ( A Yrm  0 ) ) ) )
233 oveq2 6289 . . . . . . 7  |-  ( a  =  0  ->  ( K ^ a )  =  ( K ^ 0 ) )
234232, 233oveq12d 6299 . . . . . 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 4449 . . . . 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 6289 . . . . . . . 8  |-  ( a  =  1  ->  ( A Xrm  a )  =  ( A Xrm  1 ) )
238 oveq2 6289 . . . . . . . . 9  |-  ( a  =  1  ->  ( A Yrm  a )  =  ( A Yrm  1 ) )
239238oveq2d 6297 . . . . . . . 8  |-  ( a  =  1  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  1 ) ) )
240237, 239oveq12d 6299 . . . . . . 7  |-  ( a  =  1  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  1 )  -  (
( A  -  K
)  x.  ( A Yrm  1 ) ) ) )
241 oveq2 6289 . . . . . . 7  |-  ( a  =  1  ->  ( K ^ a )  =  ( K ^ 1 ) )
242240, 241oveq12d 6299 . . . . . 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 4449 . . . . 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 6289 . . . . . . . 8  |-  ( a  =  ( b  - 
1 )  ->  ( A Xrm  a )  =  ( A Xrm  ( b  -  1 ) ) )
246 oveq2 6289 . . . . . . . . 9  |-  ( a  =  ( b  - 
1 )  ->  ( A Yrm  a )  =  ( A Yrm  ( b  -  1 ) ) )
247246oveq2d 6297 . . . . . . . 8  |-  ( a  =  ( b  - 
1 )  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  ( b  -  1 ) ) ) )
248245, 247oveq12d 6299 . . . . . . 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 6289 . . . . . . 7  |-  ( a  =  ( b  - 
1 )  ->  ( K ^ a )  =  ( K ^ (
b  -  1 ) ) )
250248, 249oveq12d 6299 . . . . . 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 4449 . . . . 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 6289 . . . . . . . 8  |-  ( a  =  b  ->  ( A Xrm  a )  =  ( A Xrm  b ) )
254 oveq2 6289 . . . . . . . . 9  |-  ( a  =  b  ->  ( A Yrm  a )  =  ( A Yrm  b ) )
255254oveq2d 6297 . . . . . . . 8  |-  ( a  =  b  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  b ) ) )
256253, 255oveq12d 6299 . . . . . . 7  |-  ( a  =  b  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )
257 oveq2 6289 . . . . . . 7  |-  ( a  =  b  ->  ( K ^ a )  =  ( K ^ b
) )
258256, 257oveq12d 6299 . . . . . 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 4449 . . . . 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 6289 . . . . . . . 8  |-  ( a  =  ( b  +  1 )  ->  ( A Xrm  a )  =  ( A Xrm  ( b  +  1 ) ) )
262 oveq2 6289 . . . . . . . . 9  |-  ( a  =  ( b  +  1 )  ->  ( A Yrm  a )  =  ( A Yrm  ( b  +  1 ) ) )
263262oveq2d 6297 . . . . . . . 8  |-  ( a  =  ( b  +  1 )  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  ( b  +  1 ) ) ) )
264261, 263oveq12d 6299 . . . . . . 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 6289 . . . . . . 7  |-  ( a  =  ( b  +  1 )  ->  ( K ^ a )  =  ( K ^ (
b  +  1 ) ) )
266264, 265oveq12d 6299 . . . . . 6  |-  ( a  =  ( b  +  1 )  ->  (
( ( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) )  =  ( ( ( A Xrm  ( b  +  1 ) )  -  (
( A