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 26413
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
StepHypRef Expression
1 2z 9986 . . . . . . . . . 10  |-  2  e.  ZZ
2 eluzelz 10170 . . . . . . . . . . 11  |-  ( A  e.  ( ZZ>= `  2
)  ->  A  e.  ZZ )
32adantr 453 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  A  e.  ZZ )
4 zmulcl 9998 . . . . . . . . . 10  |-  ( ( 2  e.  ZZ  /\  A  e.  ZZ )  ->  ( 2  x.  A
)  e.  ZZ )
51, 3, 4sylancr 647 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
2  x.  A )  e.  ZZ )
6 nn0z 9978 . . . . . . . . . 10  |-  ( K  e.  NN0  ->  K  e.  ZZ )
76adantl 454 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  K  e.  ZZ )
85, 7zmulcld 10055 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( 2  x.  A
)  x.  K )  e.  ZZ )
9 zsqcl 11105 . . . . . . . . 9  |-  ( K  e.  ZZ  ->  ( K ^ 2 )  e.  ZZ )
107, 9syl 17 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 2 )  e.  ZZ )
118, 10zsubcld 10054 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  e.  ZZ )
12 peano2zm 9994 . . . . . . 7  |-  ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  e.  ZZ  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ )
1311, 12syl 17 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ )
14 dvds0 12471 . . . . . 6  |-  ( ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  0 )
1513, 14syl 17 . . . . 5  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  0 )
16 rmx0 26342 . . . . . . . . . 10  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Xrm  0 )  =  1 )
1716adantr 453 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Xrm  0 )  =  1 )
18 rmy0 26346 . . . . . . . . . . . 12  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Yrm  0 )  =  0 )
1918adantr 453 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Yrm  0 )  =  0 )
2019oveq2d 5773 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  0 ) )  =  ( ( A  -  K )  x.  0 ) )
213, 7zsubcld 10054 . . . . . . . . . . . 12  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  K )  e.  ZZ )
2221zcnd 10050 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  K )  e.  CC )
2322mul01d 8944 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  0 )  =  0 )
2420, 23eqtrd 2288 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  0 ) )  =  0 )
2517, 24oveq12d 5775 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  =  ( 1  -  0 ) )
26 ax-1cn 8728 . . . . . . . . 9  |-  1  e.  CC
2726subid1i 9051 . . . . . . . 8  |-  ( 1  -  0 )  =  1
2825, 27syl6eq 2304 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  =  1 )
29 nn0cn 9907 . . . . . . . . 9  |-  ( K  e.  NN0  ->  K  e.  CC )
3029adantl 454 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  K  e.  CC )
3130exp0d 11170 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 0 )  =  1 )
3228, 31oveq12d 5775 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  -  ( K ^ 0 ) )  =  ( 1  -  1 ) )
33 1m1e0 9747 . . . . . 6  |-  ( 1  -  1 )  =  0
3432, 33syl6eq 2304 . . . . 5  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  -  ( K ^ 0 ) )  =  0 )
3515, 34breqtrrd 3989 . . . 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 26343 . . . . . . . . . 10  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Xrm  1 )  =  A )
3736adantr 453 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Xrm  1 )  =  A )
38 rmy1 26347 . . . . . . . . . . . 12  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Yrm  1 )  =  1 )
3938adantr 453 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Yrm  1 )  =  1 )
4039oveq2d 5773 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  1 ) )  =  ( ( A  -  K )  x.  1 ) )
4122mulid1d 8785 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  1 )  =  ( A  -  K ) )
4240, 41eqtrd 2288 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  1 ) )  =  ( A  -  K
) )
4337, 42oveq12d 5775 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  =  ( A  -  ( A  -  K
) ) )
443zcnd 10050 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  A  e.  CC )
4544, 30nncand 9095 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  ( A  -  K ) )  =  K )
4643, 45eqtrd 2288 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  =  K )
4730exp1d 11171 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 1 )  =  K )
4846, 47oveq12d 5775 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  -  ( K ^ 1 ) )  =  ( K  -  K ) )
4930subidd 9078 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K  -  K )  =  0 )
5048, 49eqtrd 2288 . . . . 5  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  -  ( K ^ 1 ) )  =  0 )
5115, 50breqtrrd 3989 . . . 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 835 . . . . 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 453 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ )
545adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  A
)  e.  ZZ )
55 simpll 733 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  A  e.  ( ZZ>= ` 
2 ) )
56 nnz 9977 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  NN  ->  b  e.  ZZ )
5756adantl 454 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  ZZ )
58 frmx 26330 . . . . . . . . . . . . . . . . . 18  |- Xrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> NN0
5958fovcl 5848 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Xrm  b )  e.  NN0 )
6055, 57, 59syl2anc 645 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  b )  e. 
NN0 )
6160nn0zd 10047 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  b )  e.  ZZ )
6221adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A  -  K
)  e.  ZZ )
63 frmy 26331 . . . . . . . . . . . . . . . . . 18  |- Yrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> ZZ
6463fovcl 5848 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Yrm  b )  e.  ZZ )
6555, 57, 64syl2anc 645 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  b )  e.  ZZ )
6662, 65zmulcld 10055 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  b ) )  e.  ZZ )
6761, 66zsubcld 10054 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  e.  ZZ )
6854, 67zmulcld 10055 . . . . . . . . . . . . 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 9994 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  ZZ  ->  (
b  -  1 )  e.  ZZ )
7057, 69syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( b  -  1 )  e.  ZZ )
7158fovcl 5848 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Xrm  ( b  - 
1 ) )  e. 
NN0 )
7255, 70, 71syl2anc 645 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  - 
1 ) )  e. 
NN0 )
7372nn0zd 10047 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  - 
1 ) )  e.  ZZ )
7463fovcl 5848 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Yrm  ( b  - 
1 ) )  e.  ZZ )
7555, 70, 74syl2anc 645 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  ( b  - 
1 ) )  e.  ZZ )
7662, 75zmulcld 10055 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) )  e.  ZZ )
7773, 76zsubcld 10054 . . . . . . . . . . . . 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 10054 . . . . . . . . . . . 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 520 . . . . . . . . . . 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 453 . . . . . . . . . 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 453 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  K  e.  ZZ )
82 nnnn0 9904 . . . . . . . . . . . . . . . 16  |-  ( b  e.  NN  ->  b  e.  NN0 )
8382adantl 454 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  NN0 )
84 zexpcl 11049 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  ZZ  /\  b  e.  NN0 )  -> 
( K ^ b
)  e.  ZZ )
8581, 83, 84syl2anc 645 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ b
)  e.  ZZ )
8654, 85zmulcld 10055 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  ( K ^ b ) )  e.  ZZ )
87 nnm1nn0 9937 . . . . . . . . . . . . . . 15  |-  ( b  e.  NN  ->  (
b  -  1 )  e.  NN0 )
8887adantl 454 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( b  -  1 )  e.  NN0 )
89 zexpcl 11049 . . . . . . . . . . . . . 14  |-  ( ( K  e.  ZZ  /\  ( b  -  1 )  e.  NN0 )  ->  ( K ^ (
b  -  1 ) )  e.  ZZ )
9081, 88, 89syl2anc 645 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  -  1 ) )  e.  ZZ )
9186, 90zsubcld 10054 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( 2  x.  A )  x.  ( K ^ b
) )  -  ( K ^ ( b  - 
1 ) ) )  e.  ZZ )
92 0z 9967 . . . . . . . . . . . . . . 15  |-  0  e.  ZZ
93 zaddcl 9991 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  ZZ  /\  ( K ^ 2 )  e.  ZZ )  -> 
( 0  +  ( K ^ 2 ) )  e.  ZZ )
9492, 10, 93sylancr 647 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
0  +  ( K ^ 2 ) )  e.  ZZ )
9594adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 0  +  ( K ^ 2 ) )  e.  ZZ )
9690, 95zmulcld 10055 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
( b  -  1 ) )  x.  (
0  +  ( K ^ 2 ) ) )  e.  ZZ )
9791, 96jca 520 . . . . . . . . . . 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 453 . . . . . . . . . 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 1137 . . . . . . . . . . . 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 453 . . . . . . . . . . 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 520 . . . . . . . . . . . 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 453 . . . . . . . . . . 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 1137 . . . . . . . . . . . . . 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 709 . . . . . . . . . . . . 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 520 . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . 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 26390 . . . . . . . . . . . . . . 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 645 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( 2  x.  A )  -  (
2  x.  A ) ) )
109108ad2antrr 709 . . . . . . . . . . . . 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 449 . . . . . . . . . . . . 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 26386 . . . . . . . . . . . . 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 1191 . . . . . . . . . . . 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 699 . . . . . . . . . . 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 735 . . . . . . . . . . 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 26389 . . . . . . . . . . 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 1191 . . . . . . . . . 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 10053 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  +  ( K ^
2 ) )  e.  ZZ )
118117adantr 453 . . . . . . . . . . . . 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 26390 . . . . . . . . . . . . . 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 645 . . . . . . . . . . . . 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 12 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  0  e.  ZZ )
122 iddvds 12469 . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . 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 10050 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  CC )
125124subid1d 9079 . . . . . . . . . . . . . . . 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 3989 . . . . . . . . . . . . . . 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 26390 . . . . . . . . . . . . . . . 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 645 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( K ^
2 )  -  ( K ^ 2 ) ) )
129 congadd 26385 . . . . . . . . . . . . . . 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 1215 . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . 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 26386 . . . . . . . . . . . . 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 1215 . . . . . . . . . . . 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 10050 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  e.  CC )
13530sqcld 11174 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 2 )  e.  CC )
13626a1i 12 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  1  e.  CC )
137134, 135, 136addsubd 9111 . . . . . . . . . . . . . . . . 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 10050 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( 2  x.  A
)  x.  K )  e.  CC )
139138, 135npcand 9094 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  +  ( K ^
2 ) )  =  ( ( 2  x.  A )  x.  K
) )
140139oveq1d 5772 . . . . . . . . . . . . . . . . 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 2290 . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . 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 5773 . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  K  e.  CC )
145144, 88expcld 11176 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  -  1 ) )  e.  CC )
146138adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  K
)  e.  CC )
14726a1i 12 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  1  e.  CC )
148145, 146, 147subdid 9168 . . . . . . . . . . . . . 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 10050 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
2  x.  A )  e.  CC )
150149adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  A
)  e.  CC )
151145, 150, 144mul12d 8954 . . . . . . . . . . . . . . . 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 449 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  NN )
153 expm1t 11061 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  CC  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
154144, 152, 153syl2anc 645 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
155154oveq2d 5773 . . . . . . . . . . . . . . . 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 2291 . . . . . . . . . . . . . . 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 8785 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
( b  -  1 ) )  x.  1 )  =  ( K ^ ( b  - 
1 ) ) )
158156, 157oveq12d 5775 . . . . . . . . . . . . . 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 2293 . . . . . . . . . . . . 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 5772 . . . . . . . . . . . 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 3989 . . . . . . . . . . 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 453 . . . . . . . . . 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 26384 . . . . . . . . . 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 1191 . . . . . . . . 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 26353 . . . . . . . . . . . . . 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 645 . . . . . . . . . . . . 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 26354 . . . . . . . . . . . . . . . 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 645 . . . . . . . . . . . . . . 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 5773 . . . . . . . . . . . . . 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 10050 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  ( ZZ>= `  2
)  ->  A  e.  CC )
171170ad2antrr 709 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  A  e.  CC )
172171, 144subcld 9090 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A  -  K
)  e.  CC )
173 2cn 9749 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
17464zcnd 10050 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Yrm  b )  e.  CC )
17555, 57, 174syl2anc 645 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  b )  e.  CC )
176175, 171mulcld 8788 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Yrm  b )  x.  A )  e.  CC )
177 mulcl 8754 . . . . . . . . . . . . . . . 16  |-  ( ( 2  e.  CC  /\  ( ( A Yrm  b )  x.  A )  e.  CC )  ->  (
2  x.  ( ( A Yrm  b )  x.  A
) )  e.  CC )
178173, 176, 177sylancr 647 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  (
( A Yrm  b )  x.  A ) )  e.  CC )
17974zcnd 10050 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Yrm  ( b  - 
1 ) )  e.  CC )
18055, 70, 179syl2anc 645 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  ( b  - 
1 ) )  e.  CC )
181172, 178, 180subdid 9168 . . . . . . . . . . . . . 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 12 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  2  e.  CC )
183182, 175, 171mul12d 8954 . . . . . . . . . . . . . . . . . 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 8789 . . . . . . . . . . . . . . . . . 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 2288 . . . . . . . . . . . . . . . . 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 5773 . . . . . . . . . . . . . . . 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 8954 . . . . . . . . . . . . . . . 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 2288 . . . . . . . . . . . . . . 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 5772 . . . . . . . . . . . . . 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 2292 . . . . . . . . . . . . 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 5775 . . . . . . . . . . . 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 9952 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Xrm  b )  e.  CC )
19355, 57, 192syl2anc 645 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  b )  e.  CC )
194150, 193mulcld 8788 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  ( A Xrm  b ) )  e.  CC )
19571nn0cnd 9952 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Xrm  ( b  - 
1 ) )  e.  CC )
19655, 70, 195syl2anc 645 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  - 
1 ) )  e.  CC )
197172, 175mulcld 8788 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  b ) )  e.  CC )
198150, 197mulcld 8788 . . . . . . . . . . . . 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 8788 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) )  e.  CC )
200194, 196, 198, 199sub4d 9139 . . . . . . . . . . . 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 9168 . . . . . . . . . . . . . 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 2261 . . . . . . . . . . . . 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 5772 . . . . . . . . . . . 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 2292 . . . . . . . . . . 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 11177 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  +  1 ) )  =  ( ( K ^ b )  x.  K ) )
206 nncn 9687 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  NN  ->  b  e.  CC )
207206adantl 454 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  CC )
208 npcan 8993 . . . . . . . . . . . . . . . 16  |-  ( ( b  e.  CC  /\  1  e.  CC )  ->  ( ( b  - 
1 )  +  1 )  =  b )
209207, 26, 208sylancl 646 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( b  - 
1 )  +  1 )  =  b )
210209oveq2d 5773 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
( b  -  1 )  +  1 ) )  =  ( K ^ b ) )
211144, 88expp1d 11177 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
( b  -  1 )  +  1 ) )  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
212210, 211eqtr3d 2290 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
213212oveq1d 5772 . . . . . . . . . . . 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 8791 . . . . . . . . . . . . 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 8946 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
0  +  ( K ^ 2 ) )  =  ( K ^
2 ) )
21630sqvald 11173 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 2 )  =  ( K  x.  K
) )
217215, 216eqtr2d 2289 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K  x.  K )  =  ( 0  +  ( K ^ 2 ) ) )
218217adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K  x.  K
)  =  ( 0  +  ( K ^
2 ) ) )
219218oveq2d 5773 . . . . . . . . . . . . 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 2288 . . . . . . . . . . . 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 2292 . . . . . . . . . . 11  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  +  1 ) )  =  ( ( K ^ ( b  -  1 ) )  x.  ( 0  +  ( K ^ 2 ) ) ) )
222204, 221oveq12d 5775 . . . . . . . . . 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 453 . . . . . . . . 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 3989 . . . . . . . 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 425 . . . . . . 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 426 . . . . . 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 25 . . . . 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 30 . . . 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 5765 . . . . . . . 8  |-  ( a  =  0  ->  ( A Xrm  a )  =  ( A Xrm  0 ) )
230 oveq2 5765 . . . . . . . . 9  |-  ( a  =  0  ->  ( A Yrm  a )  =  ( A Yrm  0 ) )
231230oveq2d 5773 . . . . . . . 8  |-  ( a  =  0  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  0 ) ) )
232229, 231oveq12d 5775 . . . . . . 7  |-  ( a  =  0  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  0 )  -  (
( A  -  K
)  x.  ( A Yrm  0 ) ) ) )
233 oveq2 5765 . . . . . . 7  |-  ( a  =  0  ->  ( K ^ a )  =  ( K ^ 0 ) )
234232, 233oveq12d 5775 . . . . . 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 3975 . . . . 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 309 . . . 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 5765 . . . . . . . 8  |-  ( a  =  1  ->  ( A Xrm  a )  =  ( A Xrm  1 ) )
238 oveq2 5765 . . . . . . . . 9  |-  ( a  =  1  ->  ( A Yrm  a )  =  ( A Yrm  1 ) )
239238oveq2d 5773 . . . . . . . 8  |-  ( a  =  1  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  1 ) ) )
240237, 239oveq12d 5775 . . . . . . 7  |-  ( a  =  1  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  1 )  -  (
( A  -  K
)  x.  ( A Yrm  1 ) ) ) )
241 oveq2 5765 . . . . . . 7  |-  ( a  =  1  ->  ( K ^ a )  =  ( K ^ 1 ) )
242240, 241oveq12d 5775 . . . . . 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 3975 . . . . 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 309 . . . 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 5765 . . . . . . . 8  |-  ( a  =  ( b  - 
1 )  ->  ( A Xrm  a )  =  ( A Xrm  ( b  -  1 ) ) )
246 oveq2 5765 . . . . . . . . 9  |-  ( a  =  ( b  - 
1 )  ->  ( A Yrm  a )  =  ( A Yrm  ( b  -  1 ) ) )
247246oveq2d 5773 . . . . . . . 8  |-  ( a  =  ( b  - 
1 )  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  ( b  -  1 ) ) ) )
248245, 247oveq12d 5775 . . . . . . 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 5765 . . . . . . 7  |-  ( a  =  ( b  - 
1 )  ->  ( K ^ a )  =  ( K ^ (
b  -  1 ) ) )
250248, 249oveq12d 5775 . . . . . 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 3975 . . . . 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 309 . . . 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 5765 . . . . . . . 8  |-  ( a  =  b  ->  ( A Xrm  a )  =  ( A Xrm  b ) )
254 oveq2 5765 . . . . . . . . 9  |-  ( a  =  b  ->  ( A Yrm  a )  =  ( A Yrm  b ) )
255254oveq2d 5773 . . . . . . . 8  |-  ( a  =  b  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  b ) ) )
256253, 255oveq12d 5775 . . . . . . 7  |-  ( a  =  b  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )
257 oveq2 5765 . . . . . . 7  |-  ( a  =  b  ->  ( K ^ a )  =  ( K ^ b
) )
258256, 257oveq12d 5775 . . . . . 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 3975 . . . . 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 309 . . . 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 5765 . . . . . . . 8  |-  ( a  =  ( b  +  1 )  ->  ( A Xrm  a )  =  ( A Xrm  ( b  +  1 ) ) )
262 oveq2 5765 . . . . . . . . 9  |-  ( a  =  ( b  +  1 )  ->  ( A Yrm  a )  =  ( A Yrm  ( b  +  1 ) ) )
263262oveq2d 5773 . . . . . . . 8  |-  ( a  =  ( b  +  1 )  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  ( b  +  1 ) ) ) )
264261, 263oveq12d 5775 . . . . . . 7  |-  ( a  =  ( b  +  1 )  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  ( b  +  1 ) )  -  ( ( A