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

Theorem jm2.18 27183
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 10070 . . . . . . . . . 10  |-  2  e.  ZZ
2 eluzelz 10254 . . . . . . . . . . 11  |-  ( A  e.  ( ZZ>= `  2
)  ->  A  e.  ZZ )
32adantr 451 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  A  e.  ZZ )
4 zmulcl 10082 . . . . . . . . . 10  |-  ( ( 2  e.  ZZ  /\  A  e.  ZZ )  ->  ( 2  x.  A
)  e.  ZZ )
51, 3, 4sylancr 644 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
2  x.  A )  e.  ZZ )
6 nn0z 10062 . . . . . . . . . 10  |-  ( K  e.  NN0  ->  K  e.  ZZ )
76adantl 452 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  K  e.  ZZ )
85, 7zmulcld 10139 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( 2  x.  A
)  x.  K )  e.  ZZ )
9 zsqcl 11190 . . . . . . . . 9  |-  ( K  e.  ZZ  ->  ( K ^ 2 )  e.  ZZ )
107, 9syl 15 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 2 )  e.  ZZ )
118, 10zsubcld 10138 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  e.  ZZ )
12 peano2zm 10078 . . . . . . 7  |-  ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  e.  ZZ  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ )
1311, 12syl 15 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ )
14 dvds0 12560 . . . . . 6  |-  ( ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  0 )
1513, 14syl 15 . . . . 5  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  0 )
16 rmx0 27112 . . . . . . . . . 10  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Xrm  0 )  =  1 )
1716adantr 451 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Xrm  0 )  =  1 )
18 rmy0 27116 . . . . . . . . . . . 12  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Yrm  0 )  =  0 )
1918adantr 451 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Yrm  0 )  =  0 )
2019oveq2d 5890 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  0 ) )  =  ( ( A  -  K )  x.  0 ) )
213, 7zsubcld 10138 . . . . . . . . . . . 12  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  K )  e.  ZZ )
2221zcnd 10134 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  K )  e.  CC )
2322mul01d 9027 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  0 )  =  0 )
2420, 23eqtrd 2328 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  0 ) )  =  0 )
2517, 24oveq12d 5892 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  =  ( 1  -  0 ) )
26 ax-1cn 8811 . . . . . . . . 9  |-  1  e.  CC
2726subid1i 9134 . . . . . . . 8  |-  ( 1  -  0 )  =  1
2825, 27syl6eq 2344 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  =  1 )
29 nn0cn 9991 . . . . . . . . 9  |-  ( K  e.  NN0  ->  K  e.  CC )
3029adantl 452 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  K  e.  CC )
3130exp0d 11255 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 0 )  =  1 )
3228, 31oveq12d 5892 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  -  ( K ^ 0 ) )  =  ( 1  -  1 ) )
33 1m1e0 9830 . . . . . 6  |-  ( 1  -  1 )  =  0
3432, 33syl6eq 2344 . . . . 5  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  -  ( K ^ 0 ) )  =  0 )
3515, 34breqtrrd 4065 . . . 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 ) ) )
36 rmx1 27113 . . . . . . . . . 10  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Xrm  1 )  =  A )
3736adantr 451 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Xrm  1 )  =  A )
38 rmy1 27117 . . . . . . . . . . . 12  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Yrm  1 )  =  1 )
3938adantr 451 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Yrm  1 )  =  1 )
4039oveq2d 5890 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  1 ) )  =  ( ( A  -  K )  x.  1 ) )
4122mulid1d 8868 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  1 )  =  ( A  -  K ) )
4240, 41eqtrd 2328 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  1 ) )  =  ( A  -  K
) )
4337, 42oveq12d 5892 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  =  ( A  -  ( A  -  K
) ) )
443zcnd 10134 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  A  e.  CC )
4544, 30nncand 9178 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  ( A  -  K ) )  =  K )
4643, 45eqtrd 2328 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  =  K )
4730exp1d 11256 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 1 )  =  K )
4846, 47oveq12d 5892 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  -  ( K ^ 1 ) )  =  ( K  -  K ) )
4930subidd 9161 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K  -  K )  =  0 )
5048, 49eqtrd 2328 . . . . 5  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  -  ( K ^ 1 ) )  =  0 )
5115, 50breqtrrd 4065 . . . 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 ) ) )
52 pm3.43 832 . . . . 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 ) ) ) ) )
5313adantr 451 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ )
545adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  A
)  e.  ZZ )
55 simpll 730 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  A  e.  ( ZZ>= ` 
2 ) )
56 nnz 10061 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  NN  ->  b  e.  ZZ )
5756adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  ZZ )
58 frmx 27100 . . . . . . . . . . . . . . . . . 18  |- Xrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> NN0
5958fovcl 5965 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Xrm  b )  e.  NN0 )
6055, 57, 59syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  b )  e. 
NN0 )
6160nn0zd 10131 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  b )  e.  ZZ )
6221adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A  -  K
)  e.  ZZ )
63 frmy 27101 . . . . . . . . . . . . . . . . . 18  |- Yrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> ZZ
6463fovcl 5965 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Yrm  b )  e.  ZZ )
6555, 57, 64syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  b )  e.  ZZ )
6662, 65zmulcld 10139 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  b ) )  e.  ZZ )
6761, 66zsubcld 10138 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  e.  ZZ )
6854, 67zmulcld 10139 . . . . . . . . . . . . 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 )
69 peano2zm 10078 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  ZZ  ->  (
b  -  1 )  e.  ZZ )
7057, 69syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( b  -  1 )  e.  ZZ )
7158fovcl 5965 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Xrm  ( b  - 
1 ) )  e. 
NN0 )
7255, 70, 71syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  - 
1 ) )  e. 
NN0 )
7372nn0zd 10131 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  - 
1 ) )  e.  ZZ )
7463fovcl 5965 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Yrm  ( b  - 
1 ) )  e.  ZZ )
7555, 70, 74syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  ( b  - 
1 ) )  e.  ZZ )
7662, 75zmulcld 10139 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) )  e.  ZZ )
7773, 76zsubcld 10138 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) )  e.  ZZ )
7868, 77zsubcld 10138 . . . . . . . . . . . 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 )
7953, 78jca 518 . . . . . . . . . . 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 ) )
8079adantr 451 . . . . . . . . . 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 ) )
817adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  K  e.  ZZ )
82 nnnn0 9988 . . . . . . . . . . . . . . . 16  |-  ( b  e.  NN  ->  b  e.  NN0 )
8382adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  NN0 )
84 zexpcl 11134 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  ZZ  /\  b  e.  NN0 )  -> 
( K ^ b
)  e.  ZZ )
8581, 83, 84syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ b
)  e.  ZZ )
8654, 85zmulcld 10139 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  ( K ^ b ) )  e.  ZZ )
87 nnm1nn0 10021 . . . . . . . . . . . . . . 15  |-  ( b  e.  NN  ->  (
b  -  1 )  e.  NN0 )
8887adantl 452 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( b  -  1 )  e.  NN0 )
89 zexpcl 11134 . . . . . . . . . . . . . 14  |-  ( ( K  e.  ZZ  /\  ( b  -  1 )  e.  NN0 )  ->  ( K ^ (
b  -  1 ) )  e.  ZZ )
9081, 88, 89syl2anc 642 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  -  1 ) )  e.  ZZ )
9186, 90zsubcld 10138 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( 2  x.  A )  x.  ( K ^ b
) )  -  ( K ^ ( b  - 
1 ) ) )  e.  ZZ )
92 0z 10051 . . . . . . . . . . . . . . 15  |-  0  e.  ZZ
93 zaddcl 10075 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  ZZ  /\  ( K ^ 2 )  e.  ZZ )  -> 
( 0  +  ( K ^ 2 ) )  e.  ZZ )
9492, 10, 93sylancr 644 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
0  +  ( K ^ 2 ) )  e.  ZZ )
9594adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 0  +  ( K ^ 2 ) )  e.  ZZ )
9690, 95zmulcld 10139 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
( b  -  1 ) )  x.  (
0  +  ( K ^ 2 ) ) )  e.  ZZ )
9791, 96jca 518 . . . . . . . . . . 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 ) )
9897adantr 451 . . . . . . . . . 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 ) )
9953, 68, 863jca 1132 . . . . . . . . . . . 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 ) )
10099adantr 451 . . . . . . . . . . 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 ) )
10177, 90jca 518 . . . . . . . . . . . 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 ) )
102101adantr 451 . . . . . . . . . . 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 ) )
10313, 5, 53jca 1132 . . . . . . . . . . . . . 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 ) )
104103ad2antrr 706 . . . . . . . . . . . . 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 ) )
10567, 85jca 518 . . . . . . . . . . . . . 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 ) )
106105adantr 451 . . . . . . . . . . . . 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 ) )
107 congid 27160 . . . . . . . . . . . . . . 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
) ) )
10813, 5, 107syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( 2  x.  A )  -  (
2  x.  A ) ) )
109108ad2antrr 706 . . . . . . . . . . . . 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 ) ) )
110 simpr 447 . . . . . . . . . . . . 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 ) ) )
111 congmul 27156 . . . . . . . . . . . . 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 ) ) ) )
112104, 106, 109, 110, 111syl112anc 1186 . . . . . . . . . . . 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 ) ) ) )
113112adantrl 696 . . . . . . . . . . 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 ) ) ) )
114 simprl 732 . . . . . . . . . . 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 ) ) ) )
115 congsub 27159 . . . . . . . . . . 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 ) ) ) ) )
116100, 102, 113, 114, 115syl112anc 1186 . . . . . . . . . 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 ) ) ) ) )
11713, 10zaddcld 10137 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  +  ( K ^
2 ) )  e.  ZZ )
118117adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  +  ( K ^ 2 ) )  e.  ZZ )
119 congid 27160 . . . . . . . . . . . . . 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 ) ) ) )
12053, 90, 119syl2anc 642 . . . . . . . . . . . . 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 ) ) ) )
12192a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  0  e.  ZZ )
122 iddvds 12558 . . . . . . . . . . . . . . . . 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 ) )
12313, 122syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) )
12413zcnd 10134 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  CC )
125124subid1d 9162 . . . . . . . . . . . . . . . 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 ) )
126123, 125breqtrrd 4065 . . . . . . . . . . . . . . 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 ) )
127 congid 27160 . . . . . . . . . . . . . . . 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 ) ) )
12813, 10, 127syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( K ^
2 )  -  ( K ^ 2 ) ) )
129 congadd 27155 . . . . . . . . . . . . . . 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 ) ) ) )
13013, 13, 121, 10, 10, 126, 128, 129syl322anc 1210 . . . . . . . . . . . . . 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 ) ) ) )
131130adantr 451 . . . . . . . . . . . . 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 ) ) ) )
132 congmul 27156 . . . . . . . . . . . . 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 ) ) ) ) )
13353, 90, 90, 118, 95, 120, 131, 132syl322anc 1210 . . . . . . . . . . . 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 ) ) ) ) )
13411zcnd 10134 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  e.  CC )
13530sqcld 11259 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 2 )  e.  CC )
13626a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  1  e.  CC )
137134, 135, 136addsubd 9194 . . . . . . . . . . . . . . . . 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 10134 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( 2  x.  A
)  x.  K )  e.  CC )
139138, 135npcand 9177 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  +  ( K ^
2 ) )  =  ( ( 2  x.  A )  x.  K
) )
140139oveq1d 5889 . . . . . . . . . . . . . . . . 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 2330 . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . 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 5890 . . . . . . . . . . . . . 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 ) ) )
14429ad2antlr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  K  e.  CC )
145144, 88expcld 11261 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  -  1 ) )  e.  CC )
146138adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  K
)  e.  CC )
14726a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  1  e.  CC )
148145, 146, 147subdid 9251 . . . . . . . . . . . . . 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 10134 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
2  x.  A )  e.  CC )
150149adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  A
)  e.  CC )
151145, 150, 144mul12d 9037 . . . . . . . . . . . . . . . 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 447 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  NN )
153 expm1t 11146 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  CC  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
154144, 152, 153syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
155154oveq2d 5890 . . . . . . . . . . . . . . . 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 2331 . . . . . . . . . . . . . . 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 8868 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
( b  -  1 ) )  x.  1 )  =  ( K ^ ( b  - 
1 ) ) )
158156, 157oveq12d 5892 . . . . . . . . . . . . . 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 2333 . . . . . . . . . . . . 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 5889 . . . . . . . . . . . 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 ) ) ) ) )
161133, 160breqtrrd 4065 . . . . . . . . . . 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 451 . . . . . . . . . 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 27154 . . . . . . . . . 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 ) ) ) ) )
16480, 98, 116, 162, 163syl112anc 1186 . . . . . . . . 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 27123 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Xrm  ( b  +  1 ) )  =  ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( A Xrm  ( b  - 
1 ) ) ) )
16655, 57, 165syl2anc 642 . . . . . . . . . . . . 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 27124 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Yrm  ( b  +  1 ) )  =  ( ( 2  x.  (
( A Yrm  b )  x.  A ) )  -  ( A Yrm  ( b  - 
1 ) ) ) )
16855, 57, 167syl2anc 642 . . . . . . . . . . . . . . 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 5890 . . . . . . . . . . . . . 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 10134 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  ( ZZ>= `  2
)  ->  A  e.  CC )
171170ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  A  e.  CC )
172171, 144subcld 9173 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A  -  K
)  e.  CC )
173 2cn 9832 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
17464zcnd 10134 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Yrm  b )  e.  CC )
17555, 57, 174syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  b )  e.  CC )
176175, 171mulcld 8871 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Yrm  b )  x.  A )  e.  CC )
177 mulcl 8837 . . . . . . . . . . . . . . . 16  |-  ( ( 2  e.  CC  /\  ( ( A Yrm  b )  x.  A )  e.  CC )  ->  (
2  x.  ( ( A Yrm  b )  x.  A
) )  e.  CC )
178173, 176, 177sylancr 644 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  (
( A Yrm  b )  x.  A ) )  e.  CC )
17974zcnd 10134 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Yrm  ( b  - 
1 ) )  e.  CC )
18055, 70, 179syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  ( b  - 
1 ) )  e.  CC )
181172, 178, 180subdid 9251 . . . . . . . . . . . . . 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 ) ) ) ) )
182173a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  2  e.  CC )
183182, 175, 171mul12d 9037 . . . . . . . . . . . . . . . . . 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 8872 . . . . . . . . . . . . . . . . . 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 2328 . . . . . . . . . . . . . . . . 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 5890 . . . . . . . . . . . . . . . 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 9037 . . . . . . . . . . . . . . . 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 2328 . . . . . . . . . . . . . . 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 5889 . . . . . . . . . . . . . 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 2332 . . . . . . . . . . . . 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 5892 . . . . . . . . . . . 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 ) ) ) ) ) )
19259nn0cnd 10036 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Xrm  b )  e.  CC )
19355, 57, 192syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  b )  e.  CC )
194150, 193mulcld 8871 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  ( A Xrm  b ) )  e.  CC )
19571nn0cnd 10036 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Xrm  ( b  - 
1 ) )  e.  CC )
19655, 70, 195syl2anc 642 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  - 
1 ) )  e.  CC )
197172, 175mulcld 8871 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  b ) )  e.  CC )
198150, 197mulcld 8871 . . . . . . . . . . . . 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 8871 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) )  e.  CC )
200194, 196, 198, 199sub4d 9222 . . . . . . . . . . . 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 9251 . . . . . . . . . . . . . 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 2301 . . . . . . . . . . . . 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 5889 . . . . . . . . . . . 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 2332 . . . . . . . . . . 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, 83expp1d 11262 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  +  1 ) )  =  ( ( K ^ b )  x.  K ) )
206 nncn 9770 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  NN  ->  b  e.  CC )
207206adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  CC )
208 npcan 9076 . . . . . . . . . . . . . . . 16  |-  ( ( b  e.  CC  /\  1  e.  CC )  ->  ( ( b  - 
1 )  +  1 )  =  b )
209207, 26, 208sylancl 643 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( b  - 
1 )  +  1 )  =  b )
210209oveq2d 5890 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
( b  -  1 )  +  1 ) )  =  ( K ^ b ) )
211144, 88expp1d 11262 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
( b  -  1 )  +  1 ) )  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
212210, 211eqtr3d 2330 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
213212oveq1d 5889 . . . . . . . . . . . 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 8874 . . . . . . . . . . . . 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 ) ) )
215135addid2d 9029 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
0  +  ( K ^ 2 ) )  =  ( K ^
2 ) )
21630sqvald 11258 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 2 )  =  ( K  x.  K
) )
217215, 216eqtr2d 2329 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K  x.  K )  =  ( 0  +  ( K ^ 2 ) ) )
218217adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K  x.  K
)  =  ( 0  +  ( K ^
2 ) ) )
219218oveq2d 5890 . . . . . . . . . . . . 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 2328 . . . . . . . . . . . 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 2332 . . . . . . . . . . 11  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  +  1 ) )  =  ( ( K ^ ( b  -  1 ) )  x.  ( 0  +  ( K ^ 2 ) ) ) )
222204, 221oveq12d 5892 . . . . . . . . . 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 451 . . . . . . . . 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 4065 . . . . . . . 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 423 . . . . . . 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 424 . . . . . 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 23 . . . . 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 ) ) ) ) ) )
22852, 227syl5 28 . . . 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 5882 . . . . . . . 8  |-  ( a  =  0  ->  ( A Xrm  a )  =  ( A Xrm  0 ) )
230 oveq2 5882 . . . . . . . . 9  |-  ( a  =  0  ->  ( A Yrm  a )  =  ( A Yrm  0 ) )
231230oveq2d 5890 . . . . . . . 8  |-  ( a  =  0  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  0 ) ) )
232229, 231oveq12d 5892 . . . . . . 7  |-  ( a  =  0  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  0 )  -  (
( A  -  K
)  x.  ( A Yrm  0 ) ) ) )
233 oveq2 5882 . . . . . . 7  |-  ( a  =  0  ->  ( K ^ a )  =  ( K ^ 0 ) )
234232, 233oveq12d 5892 . . . . . 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 4051 . . . . 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 307 . . . 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 5882 . . . . . . . 8  |-  ( a  =  1  ->  ( A Xrm  a )  =  ( A Xrm  1 ) )
238 oveq2 5882 . . . . . . . . 9  |-  ( a  =  1  ->  ( A Yrm  a )  =  ( A Yrm  1 ) )
239238oveq2d 5890 . . . . . . . 8  |-  ( a  =  1  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  1 ) ) )
240237, 239oveq12d 5892 . . . . . . 7  |-  ( a  =  1  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  1 )  -  (
( A  -  K
)  x.  ( A Yrm  1 ) ) ) )
241 oveq2 5882 . . . . . . 7  |-  ( a  =  1  ->  ( K ^ a )  =  ( K ^ 1 ) )
242240, 241oveq12d 5892 . . . . . 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 4051 . . . . 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 307 . . . 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 5882 . . . . . . . 8  |-  ( a  =  ( b  - 
1 )  ->  ( A Xrm  a )  =  ( A Xrm  ( b  -  1 ) ) )
246 oveq2 5882 . . . . . . . . 9  |-  ( a  =  ( b  - 
1 )  ->  ( A Yrm  a )  =  ( A Yrm  ( b  -  1 ) ) )
247246oveq2d 5890 . . . . . . . 8  |-  ( a  =  ( b  - 
1 )  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  ( b  -  1 ) ) ) )
248245, 247oveq12d 5892 . . . . . . 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 5882 . . . . . . 7  |-  ( a  =  ( b  - 
1 )  ->  ( K ^ a )  =  ( K ^ (
b  -  1 ) ) )
250248, 249oveq12d 5892 . . . . . 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 4051 . . . . 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 307 . . . 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 5882 . . . . . . . 8  |-  ( a  =  b  ->  ( A Xrm  a )  =  ( A Xrm  b ) )
254 oveq2 5882 . . . . . . . . 9  |-  ( a  =  b  ->  ( A Yrm  a )  =  ( A Yrm  b ) )
255254oveq2d 5890 . . . . . . . 8  |-  ( a  =  b  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  b ) ) )
256253, 255oveq12d 5892 . . . . . . 7  |-  ( a  =  b  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )
257 oveq2 5882 . . . . . . 7  |-  ( a  =  b  ->  ( K ^ a )  =  ( K ^ b
) )
258256, 257oveq12d 5892 . . . . . 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 4051 . . . . 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 307 . . . 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 5882 . . . . . . . 8  |-  ( a  =  ( b  +  1 )  ->  ( A Xrm  a )  =  ( A Xrm  ( b  +  1 ) ) )
262 oveq2 5882 . . . . . . . . 9  |-  ( a  =  ( b  +  1 )  ->  ( A Yrm  a )  =  ( A Yrm  ( b  +  1 ) ) )
263262oveq2d 5890 . . . . . . . 8  |-  ( a  =  ( b  +  1 )  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  ( b  +  1 ) ) ) )
264261, 263oveq12d 5892 . . . . . . 7  |-  ( a  =  ( b  +  1 )  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  ( b  +  1 ) )  -  (