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

Theorem jm2.18 35763
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 10970 . . . . . . . . . 10  |-  2  e.  ZZ
2 eluzelz 11169 . . . . . . . . . . 11  |-  ( A  e.  ( ZZ>= `  2
)  ->  A  e.  ZZ )
32adantr 466 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  A  e.  ZZ )
4 zmulcl 10986 . . . . . . . . . 10  |-  ( ( 2  e.  ZZ  /\  A  e.  ZZ )  ->  ( 2  x.  A
)  e.  ZZ )
51, 3, 4sylancr 667 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
2  x.  A )  e.  ZZ )
6 nn0z 10961 . . . . . . . . . 10  |-  ( K  e.  NN0  ->  K  e.  ZZ )
76adantl 467 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  K  e.  ZZ )
85, 7zmulcld 11047 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( 2  x.  A
)  x.  K )  e.  ZZ )
9 zsqcl 12345 . . . . . . . . 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 11046 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  e.  ZZ )
12 peano2zm 10981 . . . . . . 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 14306 . . . . . 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 35693 . . . . . . . . . 10  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Xrm  0 )  =  1 )
1716adantr 466 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Xrm  0 )  =  1 )
18 rmy0 35697 . . . . . . . . . . . 12  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Yrm  0 )  =  0 )
1918adantr 466 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Yrm  0 )  =  0 )
2019oveq2d 6318 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  0 ) )  =  ( ( A  -  K )  x.  0 ) )
213, 7zsubcld 11046 . . . . . . . . . . . 12  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  K )  e.  ZZ )
2221zcnd 11042 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  K )  e.  CC )
2322mul01d 9833 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  0 )  =  0 )
2420, 23eqtrd 2463 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  0 ) )  =  0 )
2517, 24oveq12d 6320 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  =  ( 1  -  0 ) )
26 1m0e1 10721 . . . . . . . 8  |-  ( 1  -  0 )  =  1
2725, 26syl6eq 2479 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  =  1 )
28 nn0cn 10880 . . . . . . . . 9  |-  ( K  e.  NN0  ->  K  e.  CC )
2928adantl 467 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  K  e.  CC )
3029exp0d 12410 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 0 )  =  1 )
3127, 30oveq12d 6320 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  -  ( K ^ 0 ) )  =  ( 1  -  1 ) )
32 1m1e0 10679 . . . . . 6  |-  ( 1  -  1 )  =  0
3331, 32syl6eq 2479 . . . . 5  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  0 )  -  ( ( A  -  K )  x.  ( A Yrm  0 ) ) )  -  ( K ^ 0 ) )  =  0 )
3415, 33breqtrrd 4447 . . . 4  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  0 )  -  (
( A  -  K
)  x.  ( A Yrm  0 ) ) )  -  ( K ^
0 ) ) )
35 rmx1 35694 . . . . . . . . . 10  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Xrm  1 )  =  A )
3635adantr 466 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Xrm  1 )  =  A )
37 rmy1 35698 . . . . . . . . . . . 12  |-  ( A  e.  ( ZZ>= `  2
)  ->  ( A Yrm  1 )  =  1 )
3837adantr 466 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A Yrm  1 )  =  1 )
3938oveq2d 6318 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  1 ) )  =  ( ( A  -  K )  x.  1 ) )
4022mulid1d 9661 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  1 )  =  ( A  -  K ) )
4139, 40eqtrd 2463 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A  -  K
)  x.  ( A Yrm  1 ) )  =  ( A  -  K
) )
4236, 41oveq12d 6320 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  =  ( A  -  ( A  -  K
) ) )
433zcnd 11042 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  A  e.  CC )
4443, 29nncand 9992 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( A  -  ( A  -  K ) )  =  K )
4542, 44eqtrd 2463 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  =  K )
4629exp1d 12411 . . . . . . 7  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 1 )  =  K )
4745, 46oveq12d 6320 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  -  ( K ^ 1 ) )  =  ( K  -  K ) )
4829subidd 9975 . . . . . 6  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K  -  K )  =  0 )
4947, 48eqtrd 2463 . . . . 5  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( A Xrm  1 )  -  ( ( A  -  K )  x.  ( A Yrm  1 ) ) )  -  ( K ^ 1 ) )  =  0 )
5015, 49breqtrrd 4447 . . . 4  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  1 )  -  (
( A  -  K
)  x.  ( A Yrm  1 ) ) )  -  ( K ^
1 ) ) )
51 pm3.43 870 . . . . 5  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  ->  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) ) )  /\  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  -> 
( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) ) )
5213adantr 466 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ )
535adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  A
)  e.  ZZ )
54 simpll 758 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  A  e.  ( ZZ>= ` 
2 ) )
55 nnz 10960 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  NN  ->  b  e.  ZZ )
5655adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  ZZ )
57 frmx 35681 . . . . . . . . . . . . . . . . . 18  |- Xrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> NN0
5857fovcl 6412 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Xrm  b )  e.  NN0 )
5954, 56, 58syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  b )  e. 
NN0 )
6059nn0zd 11039 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  b )  e.  ZZ )
6121adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A  -  K
)  e.  ZZ )
62 frmy 35682 . . . . . . . . . . . . . . . . . 18  |- Yrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> ZZ
6362fovcl 6412 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Yrm  b )  e.  ZZ )
6454, 56, 63syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  b )  e.  ZZ )
6561, 64zmulcld 11047 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  b ) )  e.  ZZ )
6660, 65zsubcld 11046 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  e.  ZZ )
6753, 66zmulcld 11047 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  (
( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  e.  ZZ )
68 peano2zm 10981 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  ZZ  ->  (
b  -  1 )  e.  ZZ )
6956, 68syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( b  -  1 )  e.  ZZ )
7057fovcl 6412 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Xrm  ( b  - 
1 ) )  e. 
NN0 )
7154, 69, 70syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  - 
1 ) )  e. 
NN0 )
7271nn0zd 11039 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  - 
1 ) )  e.  ZZ )
7362fovcl 6412 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Yrm  ( b  - 
1 ) )  e.  ZZ )
7454, 69, 73syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  ( b  - 
1 ) )  e.  ZZ )
7561, 74zmulcld 11047 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) )  e.  ZZ )
7672, 75zsubcld 11046 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) )  e.  ZZ )
7767, 76zsubcld 11046 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( A Xrm  ( b  - 
1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  e.  ZZ )
7852, 77jca 534 . . . . . . . . . . 11  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  e.  ZZ  /\  ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( A Xrm  ( b  - 
1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  e.  ZZ ) )
7978adantr 466 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  /\  (
( ( 2  x.  A )  x.  (
( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  (
( A  -  K
)  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  e.  ZZ ) )
807adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  K  e.  ZZ )
81 nnnn0 10877 . . . . . . . . . . . . . . . 16  |-  ( b  e.  NN  ->  b  e.  NN0 )
8281adantl 467 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  NN0 )
83 zexpcl 12287 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  ZZ  /\  b  e.  NN0 )  -> 
( K ^ b
)  e.  ZZ )
8480, 82, 83syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ b
)  e.  ZZ )
8553, 84zmulcld 11047 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  ( K ^ b ) )  e.  ZZ )
86 nnm1nn0 10912 . . . . . . . . . . . . . . 15  |-  ( b  e.  NN  ->  (
b  -  1 )  e.  NN0 )
8786adantl 467 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( b  -  1 )  e.  NN0 )
88 zexpcl 12287 . . . . . . . . . . . . . 14  |-  ( ( K  e.  ZZ  /\  ( b  -  1 )  e.  NN0 )  ->  ( K ^ (
b  -  1 ) )  e.  ZZ )
8980, 87, 88syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  -  1 ) )  e.  ZZ )
9085, 89zsubcld 11046 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( 2  x.  A )  x.  ( K ^ b
) )  -  ( K ^ ( b  - 
1 ) ) )  e.  ZZ )
91 0z 10949 . . . . . . . . . . . . . . 15  |-  0  e.  ZZ
92 zaddcl 10978 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  ZZ  /\  ( K ^ 2 )  e.  ZZ )  -> 
( 0  +  ( K ^ 2 ) )  e.  ZZ )
9391, 10, 92sylancr 667 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
0  +  ( K ^ 2 ) )  e.  ZZ )
9493adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 0  +  ( K ^ 2 ) )  e.  ZZ )
9589, 94zmulcld 11047 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
( b  -  1 ) )  x.  (
0  +  ( K ^ 2 ) ) )  e.  ZZ )
9690, 95jca 534 . . . . . . . . . . 11  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( 2  x.  A )  x.  ( K ^
b ) )  -  ( K ^ ( b  -  1 ) ) )  e.  ZZ  /\  ( ( K ^
( b  -  1 ) )  x.  (
0  +  ( K ^ 2 ) ) )  e.  ZZ ) )
9796adantr 466 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  ( K ^ b
) )  -  ( K ^ ( b  - 
1 ) ) )  e.  ZZ  /\  (
( K ^ (
b  -  1 ) )  x.  ( 0  +  ( K ^
2 ) ) )  e.  ZZ ) )
9852, 67, 853jca 1185 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  e.  ZZ  /\  ( ( 2  x.  A )  x.  (
( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  e.  ZZ  /\  ( ( 2  x.  A )  x.  ( K ^ b ) )  e.  ZZ ) )
9998adantr 466 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  /\  (
( 2  x.  A
)  x.  ( ( A Xrm  b )  -  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )  e.  ZZ  /\  (
( 2  x.  A
)  x.  ( K ^ b ) )  e.  ZZ ) )
10076, 89jca 534 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  e.  ZZ  /\  ( K ^ (
b  -  1 ) )  e.  ZZ ) )
101100adantr 466 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) )  e.  ZZ  /\  ( K ^ ( b  -  1 ) )  e.  ZZ ) )
10213, 5, 53jca 1185 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  /\  (
2  x.  A )  e.  ZZ  /\  (
2  x.  A )  e.  ZZ ) )
103102ad2antrr 730 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )  ->  ( (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  /\  ( 2  x.  A )  e.  ZZ  /\  ( 2  x.  A )  e.  ZZ ) )
10466, 84jca 534 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  e.  ZZ  /\  ( K ^ b
)  e.  ZZ ) )
105104adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )  ->  ( (
( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  e.  ZZ  /\  ( K ^ b )  e.  ZZ ) )
106 congid 35741 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  /\  (
2  x.  A )  e.  ZZ )  -> 
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( 2  x.  A )  -  ( 2  x.  A
) ) )
10713, 5, 106syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( 2  x.  A )  -  (
2  x.  A ) ) )
108107ad2antrr 730 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( 2  x.  A )  -  (
2  x.  A ) ) )
109 simpr 462 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )
110 congmul 35737 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  e.  ZZ  /\  ( 2  x.  A
)  e.  ZZ  /\  ( 2  x.  A
)  e.  ZZ )  /\  ( ( ( A Xrm  b )  -  (
( A  -  K
)  x.  ( A Yrm  b ) ) )  e.  ZZ  /\  ( K ^ b )  e.  ZZ )  /\  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( 2  x.  A )  -  ( 2  x.  A
) )  /\  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( 2  x.  A
)  x.  ( K ^ b ) ) ) )
111103, 105, 108, 109, 110syl112anc 1268 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) )  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( 2  x.  A
)  x.  ( K ^ b ) ) ) )
112111adantrl 720 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( 2  x.  A
)  x.  ( K ^ b ) ) ) )
113 simprl 762 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) ) )
114 congsub 35740 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  e.  ZZ  /\  ( ( 2  x.  A )  x.  (
( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  e.  ZZ  /\  ( ( 2  x.  A )  x.  ( K ^ b ) )  e.  ZZ )  /\  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  e.  ZZ  /\  ( K ^ (
b  -  1 ) )  e.  ZZ )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( 2  x.  A
)  x.  ( K ^ b ) ) )  /\  ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) ) )  -  (
( ( 2  x.  A )  x.  ( K ^ b ) )  -  ( K ^
( b  -  1 ) ) ) ) )
11599, 101, 112, 113, 114syl112anc 1268 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) ) )  -  (
( ( 2  x.  A )  x.  ( K ^ b ) )  -  ( K ^
( b  -  1 ) ) ) ) )
11613, 10zaddcld 11045 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  +  ( K ^
2 ) )  e.  ZZ )
117116adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  +  ( K ^ 2 ) )  e.  ZZ )
118 congid 35741 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  /\  ( K ^ ( b  - 
1 ) )  e.  ZZ )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( K ^
( b  -  1 ) )  -  ( K ^ ( b  - 
1 ) ) ) )
11952, 89, 118syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( K ^ ( b  - 
1 ) )  -  ( K ^ ( b  -  1 ) ) ) )
120 0zd 10950 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  0  e.  ZZ )
121 iddvds 14304 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  ->  ( (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) )
12213, 121syl 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 ) )
12313zcnd 11042 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  CC )
124123subid1d 9976 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  -  0 )  =  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) )
125122, 124breqtrrd 4447 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  -  0 ) )
126 congid 35741 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  /\  ( K ^ 2 )  e.  ZZ )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( K ^
2 )  -  ( K ^ 2 ) ) )
12713, 10, 126syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( K ^
2 )  -  ( K ^ 2 ) ) )
128 congadd 35736 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  e.  ZZ  /\  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  e.  ZZ  /\  0  e.  ZZ )  /\  (
( K ^ 2 )  e.  ZZ  /\  ( K ^ 2 )  e.  ZZ )  /\  ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  -  0 )  /\  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( K ^ 2 )  -  ( K ^ 2 ) ) ) )  -> 
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  +  ( K ^ 2 ) )  -  (
0  +  ( K ^ 2 ) ) ) )
12913, 13, 120, 10, 10, 125, 127, 128syl322anc 1292 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  +  ( K ^ 2 ) )  -  (
0  +  ( K ^ 2 ) ) ) )
130129adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  +  ( K ^ 2 ) )  -  (
0  +  ( K ^ 2 ) ) ) )
131 congmul 35737 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  e.  ZZ  /\  ( K ^ (
b  -  1 ) )  e.  ZZ  /\  ( K ^ ( b  -  1 ) )  e.  ZZ )  /\  ( ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  +  ( K ^ 2 ) )  e.  ZZ  /\  ( 0  +  ( K ^ 2 ) )  e.  ZZ )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( K ^
( b  -  1 ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  +  ( K ^ 2 ) )  -  ( 0  +  ( K ^
2 ) ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( K ^ ( b  - 
1 ) )  x.  ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  +  ( K ^ 2 ) ) )  -  (
( K ^ (
b  -  1 ) )  x.  ( 0  +  ( K ^
2 ) ) ) ) )
13252, 89, 89, 117, 94, 119, 130, 131syl322anc 1292 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( ( K ^ ( b  -  1 ) )  x.  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  +  ( K ^ 2 ) ) )  -  ( ( K ^
( b  -  1 ) )  x.  (
0  +  ( K ^ 2 ) ) ) ) )
13311zcnd 11042 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  e.  CC )
13429sqcld 12414 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 2 )  e.  CC )
135 1cnd 9660 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  1  e.  CC )
136133, 134, 135addsubd 10008 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  +  ( K ^ 2 ) )  -  1 )  =  ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  +  ( K ^ 2 ) ) )
1378zcnd 11042 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( 2  x.  A
)  x.  K )  e.  CC )
138137, 134npcand 9991 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  +  ( K ^
2 ) )  =  ( ( 2  x.  A )  x.  K
) )
139138oveq1d 6317 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  +  ( K ^ 2 ) )  -  1 )  =  ( ( ( 2  x.  A )  x.  K )  -  1 ) )
140136, 139eqtr3d 2465 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  +  ( K ^
2 ) )  =  ( ( ( 2  x.  A )  x.  K )  -  1 ) )
141140adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  +  ( K ^ 2 ) )  =  ( ( ( 2  x.  A
)  x.  K )  -  1 ) )
142141oveq2d 6318 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
( b  -  1 ) )  x.  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  +  ( K ^
2 ) ) )  =  ( ( K ^ ( b  - 
1 ) )  x.  ( ( ( 2  x.  A )  x.  K )  -  1 ) ) )
14328ad2antlr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  K  e.  CC )
144143, 87expcld 12416 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  -  1 ) )  e.  CC )
145137adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  K
)  e.  CC )
146 1cnd 9660 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  1  e.  CC )
147144, 145, 146subdid 10075 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
( b  -  1 ) )  x.  (
( ( 2  x.  A )  x.  K
)  -  1 ) )  =  ( ( ( K ^ (
b  -  1 ) )  x.  ( ( 2  x.  A )  x.  K ) )  -  ( ( K ^ ( b  - 
1 ) )  x.  1 ) ) )
1485zcnd 11042 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
2  x.  A )  e.  CC )
149148adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  A
)  e.  CC )
150144, 149, 143mul12d 9843 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
( b  -  1 ) )  x.  (
( 2  x.  A
)  x.  K ) )  =  ( ( 2  x.  A )  x.  ( ( K ^ ( b  - 
1 ) )  x.  K ) ) )
151 simpr 462 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  NN )
152 expm1t 12300 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  CC  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
153143, 151, 152syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
154153oveq2d 6318 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  ( K ^ b ) )  =  ( ( 2  x.  A )  x.  ( ( K ^
( b  -  1 ) )  x.  K
) ) )
155150, 154eqtr4d 2466 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
( b  -  1 ) )  x.  (
( 2  x.  A
)  x.  K ) )  =  ( ( 2  x.  A )  x.  ( K ^
b ) ) )
156144mulid1d 9661 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
( b  -  1 ) )  x.  1 )  =  ( K ^ ( b  - 
1 ) ) )
157155, 156oveq12d 6320 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( K ^ ( b  - 
1 ) )  x.  ( ( 2  x.  A )  x.  K
) )  -  (
( K ^ (
b  -  1 ) )  x.  1 ) )  =  ( ( ( 2  x.  A
)  x.  ( K ^ b ) )  -  ( K ^
( b  -  1 ) ) ) )
158142, 147, 1573eqtrrd 2468 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( 2  x.  A )  x.  ( K ^ b
) )  -  ( K ^ ( b  - 
1 ) ) )  =  ( ( K ^ ( b  - 
1 ) )  x.  ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  +  ( K ^ 2 ) ) ) )
159158oveq1d 6317 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( 2  x.  A )  x.  ( K ^
b ) )  -  ( K ^ ( b  -  1 ) ) )  -  ( ( K ^ ( b  -  1 ) )  x.  ( 0  +  ( K ^ 2 ) ) ) )  =  ( ( ( K ^ ( b  -  1 ) )  x.  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  +  ( K ^ 2 ) ) )  -  ( ( K ^
( b  -  1 ) )  x.  (
0  +  ( K ^ 2 ) ) ) ) )
160132, 159breqtrrd 4447 . . . . . . . . . . 11  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( ( ( 2  x.  A
)  x.  ( K ^ b ) )  -  ( K ^
( b  -  1 ) ) )  -  ( ( K ^
( b  -  1 ) )  x.  (
0  +  ( K ^ 2 ) ) ) ) )
161160adantr 466 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( ( 2  x.  A )  x.  ( K ^
b ) )  -  ( K ^ ( b  -  1 ) ) )  -  ( ( K ^ ( b  -  1 ) )  x.  ( 0  +  ( K ^ 2 ) ) ) ) )
162 congtr 35735 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  e.  ZZ  /\  ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( A Xrm  ( b  - 
1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  e.  ZZ )  /\  ( ( ( ( 2  x.  A
)  x.  ( K ^ b ) )  -  ( K ^
( b  -  1 ) ) )  e.  ZZ  /\  ( ( K ^ ( b  -  1 ) )  x.  ( 0  +  ( K ^ 2 ) ) )  e.  ZZ )  /\  (
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( ( ( 2  x.  A
)  x.  ( ( A Xrm  b )  -  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  -  ( ( ( 2  x.  A )  x.  ( K ^ b
) )  -  ( K ^ ( b  - 
1 ) ) ) )  /\  ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( ( 2  x.  A )  x.  ( K ^
b ) )  -  ( K ^ ( b  -  1 ) ) )  -  ( ( K ^ ( b  -  1 ) )  x.  ( 0  +  ( K ^ 2 ) ) ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) ) )  -  (
( K ^ (
b  -  1 ) )  x.  ( 0  +  ( K ^
2 ) ) ) ) )
16379, 97, 115, 161, 162syl112anc 1268 . . . . . . . . 9  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) ) )  -  (
( K ^ (
b  -  1 ) )  x.  ( 0  +  ( K ^
2 ) ) ) ) )
164 rmxluc 35704 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Xrm  ( b  +  1 ) )  =  ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( A Xrm  ( b  - 
1 ) ) ) )
16554, 56, 164syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  +  1 ) )  =  ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( A Xrm  ( b  -  1 ) ) ) )
166 rmyluc 35705 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Yrm  ( b  +  1 ) )  =  ( ( 2  x.  (
( A Yrm  b )  x.  A ) )  -  ( A Yrm  ( b  - 
1 ) ) ) )
16754, 56, 166syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  ( b  +  1 ) )  =  ( ( 2  x.  ( ( A Yrm  b )  x.  A ) )  -  ( A Yrm  ( b  -  1 ) ) ) )
168167oveq2d 6318 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) )  =  ( ( A  -  K )  x.  (
( 2  x.  (
( A Yrm  b )  x.  A ) )  -  ( A Yrm  ( b  - 
1 ) ) ) ) )
1692zcnd 11042 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  ( ZZ>= `  2
)  ->  A  e.  CC )
170169ad2antrr 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  A  e.  CC )
171170, 143subcld 9987 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A  -  K
)  e.  CC )
172 2cn 10681 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
17363zcnd 11042 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Yrm  b )  e.  CC )
17454, 56, 173syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  b )  e.  CC )
175174, 170mulcld 9664 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Yrm  b )  x.  A )  e.  CC )
176 mulcl 9624 . . . . . . . . . . . . . . . 16  |-  ( ( 2  e.  CC  /\  ( ( A Yrm  b )  x.  A )  e.  CC )  ->  (
2  x.  ( ( A Yrm  b )  x.  A
) )  e.  CC )
177172, 175, 176sylancr 667 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  (
( A Yrm  b )  x.  A ) )  e.  CC )
17873zcnd 11042 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Yrm  ( b  - 
1 ) )  e.  CC )
17954, 69, 178syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Yrm  ( b  - 
1 ) )  e.  CC )
180171, 177, 179subdid 10075 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  (
( 2  x.  (
( A Yrm  b )  x.  A ) )  -  ( A Yrm  ( b  - 
1 ) ) ) )  =  ( ( ( A  -  K
)  x.  ( 2  x.  ( ( A Yrm  b )  x.  A ) ) )  -  (
( A  -  K
)  x.  ( A Yrm  ( b  -  1 ) ) ) ) )
181 2cnd 10683 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  2  e.  CC )
182181, 174, 170mul12d 9843 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  (
( A Yrm  b )  x.  A ) )  =  ( ( A Yrm  b )  x.  ( 2  x.  A ) ) )
183174, 149mulcomd 9665 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Yrm  b )  x.  ( 2  x.  A ) )  =  ( ( 2  x.  A )  x.  ( A Yrm  b ) ) )
184182, 183eqtrd 2463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( 2  x.  (
( A Yrm  b )  x.  A ) )  =  ( ( 2  x.  A )  x.  ( A Yrm  b ) ) )
185184oveq2d 6318 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  (
2  x.  ( ( A Yrm  b )  x.  A
) ) )  =  ( ( A  -  K )  x.  (
( 2  x.  A
)  x.  ( A Yrm  b ) ) ) )
186171, 149, 174mul12d 9843 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  (
( 2  x.  A
)  x.  ( A Yrm  b ) ) )  =  ( ( 2  x.  A )  x.  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )
187185, 186eqtrd 2463 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  (
2  x.  ( ( A Yrm  b )  x.  A
) ) )  =  ( ( 2  x.  A )  x.  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )
188187oveq1d 6317 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( A  -  K )  x.  ( 2  x.  (
( A Yrm  b )  x.  A ) ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) )  =  ( ( ( 2  x.  A
)  x.  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  (
( A  -  K
)  x.  ( A Yrm  ( b  -  1 ) ) ) ) )
189168, 180, 1883eqtrd 2467 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) )  =  ( ( ( 2  x.  A )  x.  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  - 
1 ) ) ) ) )
190165, 189oveq12d 6320 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Xrm  ( b  +  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) ) )  =  ( ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( A Xrm  ( b  - 
1 ) ) )  -  ( ( ( 2  x.  A )  x.  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) ) )
19158nn0cnd 10928 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  b  e.  ZZ )  ->  ( A Xrm  b )  e.  CC )
19254, 56, 191syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  b )  e.  CC )
193149, 192mulcld 9664 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  ( A Xrm  b ) )  e.  CC )
19470nn0cnd 10928 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  (
b  -  1 )  e.  ZZ )  -> 
( A Xrm  ( b  - 
1 ) )  e.  CC )
19554, 69, 194syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( A Xrm  ( b  - 
1 ) )  e.  CC )
196171, 174mulcld 9664 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  b ) )  e.  CC )
197149, 196mulcld 9664 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  (
( A  -  K
)  x.  ( A Yrm  b ) ) )  e.  CC )
198171, 179mulcld 9664 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) )  e.  CC )
199193, 195, 197, 198sub4d 10036 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( A Xrm  ( b  -  1 ) ) )  -  (
( ( 2  x.  A )  x.  (
( A  -  K
)  x.  ( A Yrm  b ) ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  =  ( ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( ( 2  x.  A )  x.  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) ) )
200149, 192, 196subdid 10075 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( 2  x.  A )  x.  (
( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  =  ( ( ( 2  x.  A
)  x.  ( A Xrm  b ) )  -  (
( 2  x.  A
)  x.  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) ) )
201200eqcomd 2430 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( ( 2  x.  A )  x.  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  =  ( ( 2  x.  A )  x.  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) ) )
202201oveq1d 6317 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( ( 2  x.  A )  x.  ( A Xrm  b ) )  -  ( ( 2  x.  A )  x.  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )  -  (
( A Xrm  ( b  - 
1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  =  ( ( ( 2  x.  A
)  x.  ( ( A Xrm  b )  -  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) ) )
203190, 199, 2023eqtrd 2467 . . . . . . . . . . 11  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( A Xrm  ( b  +  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) ) )  =  ( ( ( 2  x.  A
)  x.  ( ( A Xrm  b )  -  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) ) )
204143, 82expp1d 12417 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  +  1 ) )  =  ( ( K ^ b )  x.  K ) )
205 nncn 10618 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  NN  ->  b  e.  CC )
206205adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  b  e.  CC )
207 ax-1cn 9598 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
208 npcan 9885 . . . . . . . . . . . . . . . 16  |-  ( ( b  e.  CC  /\  1  e.  CC )  ->  ( ( b  - 
1 )  +  1 )  =  b )
209206, 207, 208sylancl 666 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( b  - 
1 )  +  1 )  =  b )
210209oveq2d 6318 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
( b  -  1 )  +  1 ) )  =  ( K ^ b ) )
211143, 87expp1d 12417 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
( b  -  1 )  +  1 ) )  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
212210, 211eqtr3d 2465 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ b
)  =  ( ( K ^ ( b  -  1 ) )  x.  K ) )
213212oveq1d 6317 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( K ^
b )  x.  K
)  =  ( ( ( K ^ (
b  -  1 ) )  x.  K )  x.  K ) )
214144, 143, 143mulassd 9667 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( K ^ ( b  - 
1 ) )  x.  K )  x.  K
)  =  ( ( K ^ ( b  -  1 ) )  x.  ( K  x.  K ) ) )
215134addid2d 9835 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  (
0  +  ( K ^ 2 ) )  =  ( K ^
2 ) )
21629sqvald 12413 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K ^ 2 )  =  ( K  x.  K
) )
217215, 216eqtr2d 2464 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  NN0 )  ->  ( K  x.  K )  =  ( 0  +  ( K ^ 2 ) ) )
218217adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K  x.  K
)  =  ( 0  +  ( K ^
2 ) ) )
219218oveq2d 6318 . . . . . . . . . . . . 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 2463 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( ( ( K ^ ( b  - 
1 ) )  x.  K )  x.  K
)  =  ( ( K ^ ( b  -  1 ) )  x.  ( 0  +  ( K ^ 2 ) ) ) )
221204, 213, 2203eqtrd 2467 . . . . . . . . . . 11  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  ->  ( K ^ (
b  +  1 ) )  =  ( ( K ^ ( b  -  1 ) )  x.  ( 0  +  ( K ^ 2 ) ) ) )
222203, 221oveq12d 6320 . . . . . . . . . 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 466 . . . . . . . . 9  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  /\  b  e.  NN )  /\  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( ( A Xrm  ( b  +  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) ) )  -  ( K ^ ( b  +  1 ) ) )  =  ( ( ( ( 2  x.  A
)  x.  ( ( A Xrm  b )  -  (
( A  -  K
)  x.  ( A Yrm  b ) ) ) )  -  ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) ) )  -  ( ( K ^
( b  -  1 ) )  x.  (
0  +  ( K ^ 2 ) ) ) ) )
224163, 223breqtrrd 4447 . . . . . . . 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 435 . . . . . . 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 436 . . . . . 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 29 . . . . 5  |-  ( b  e.  NN  ->  (
( ( A  e.  ( ZZ>= `  2 )  /\  K  e.  NN0 )  ->  ( ( ( ( ( 2  x.  A )  x.  K
)  -  ( K ^ 2 ) )  -  1 )  ||  ( ( ( A Xrm  ( b  -  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  -  1 ) ) ) )  -  ( K ^ ( b  - 
1 ) ) )  /\  ( ( ( ( 2  x.  A
)  x.  K )  -  ( K ^
2 ) )  - 
1 )  ||  (
( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) )  -  ( K ^ b ) ) ) )  ->  (
( A  e.  (
ZZ>= `  2 )  /\  K  e.  NN0 )  -> 
( ( ( ( 2  x.  A )  x.  K )  -  ( K ^ 2 ) )  -  1 ) 
||  ( ( ( A Xrm  ( b  +  1 ) )  -  (
( A  -  K
)  x.  ( A Yrm  ( b  +  1 ) ) ) )  -  ( K ^ ( b  +  1 ) ) ) ) ) )
22851, 227syl5 33 . . . 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 6310 . . . . . . . 8  |-  ( a  =  0  ->  ( A Xrm  a )  =  ( A Xrm  0 ) )
230 oveq2 6310 . . . . . . . . 9  |-  ( a  =  0  ->  ( A Yrm  a )  =  ( A Yrm  0 ) )
231230oveq2d 6318 . . . . . . . 8  |-  ( a  =  0  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  0 ) ) )
232229, 231oveq12d 6320 . . . . . . 7  |-  ( a  =  0  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  0 )  -  (
( A  -  K
)  x.  ( A Yrm  0 ) ) ) )
233 oveq2 6310 . . . . . . 7  |-  ( a  =  0  ->  ( K ^ a )  =  ( K ^ 0 ) )
234232, 233oveq12d 6320 . . . . . 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 4432 . . . . 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 317 . . . 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 6310 . . . . . . . 8  |-  ( a  =  1  ->  ( A Xrm  a )  =  ( A Xrm  1 ) )
238 oveq2 6310 . . . . . . . . 9  |-  ( a  =  1  ->  ( A Yrm  a )  =  ( A Yrm  1 ) )
239238oveq2d 6318 . . . . . . . 8  |-  ( a  =  1  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  1 ) ) )
240237, 239oveq12d 6320 . . . . . . 7  |-  ( a  =  1  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  1 )  -  (
( A  -  K
)  x.  ( A Yrm  1 ) ) ) )
241 oveq2 6310 . . . . . . 7  |-  ( a  =  1  ->  ( K ^ a )  =  ( K ^ 1 ) )
242240, 241oveq12d 6320 . . . . . 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 4432 . . . . 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 317 . . . 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 6310 . . . . . . . 8  |-  ( a  =  ( b  - 
1 )  ->  ( A Xrm  a )  =  ( A Xrm  ( b  -  1 ) ) )
246 oveq2 6310 . . . . . . . . 9  |-  ( a  =  ( b  - 
1 )  ->  ( A Yrm  a )  =  ( A Yrm  ( b  -  1 ) ) )
247246oveq2d 6318 . . . . . . . 8  |-  ( a  =  ( b  - 
1 )  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  ( b  -  1 ) ) ) )
248245, 247oveq12d 6320 . . . . . . 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 6310 . . . . . . 7  |-  ( a  =  ( b  - 
1 )  ->  ( K ^ a )  =  ( K ^ (
b  -  1 ) ) )
250248, 249oveq12d 6320 . . . . . 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 4432 . . . . 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 317 . . . 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 6310 . . . . . . . 8  |-  ( a  =  b  ->  ( A Xrm  a )  =  ( A Xrm  b ) )
254 oveq2 6310 . . . . . . . . 9  |-  ( a  =  b  ->  ( A Yrm  a )  =  ( A Yrm  b ) )
255254oveq2d 6318 . . . . . . . 8  |-  ( a  =  b  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  b ) ) )
256253, 255oveq12d 6320 . . . . . . 7  |-  ( a  =  b  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  b )  -  ( ( A  -  K )  x.  ( A Yrm  b ) ) ) )
257 oveq2 6310 . . . . . . 7  |-  ( a  =  b  ->  ( K ^ a )  =  ( K ^ b
) )
258256, 257oveq12d 6320 . . . . . 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 4432 . . . . 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 317 . . . 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 6310 . . . . . . . 8  |-  ( a  =  ( b  +  1 )  ->  ( A Xrm  a )  =  ( A Xrm  ( b  +  1 ) ) )
262 oveq2 6310 . . . . . . . . 9  |-  ( a  =  ( b  +  1 )  ->  ( A Yrm  a )  =  ( A Yrm  ( b  +  1 ) ) )
263262oveq2d 6318 . . . . . . . 8  |-  ( a  =  ( b  +  1 )  ->  (
( A  -  K
)  x.  ( A Yrm  a ) )  =  ( ( A  -  K
)  x.  ( A Yrm  ( b  +  1 ) ) ) )
264261, 263oveq12d 6320 . . . . . . 7  |-  ( a  =  ( b  +  1 )  ->  (
( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  =  ( ( A Xrm  ( b  +  1 ) )  -  ( ( A  -  K )  x.  ( A Yrm  ( b  +  1 ) ) ) ) )
265 oveq2 6310 . . . . . . 7  |-  ( a  =  ( b  +  1 )  ->  ( K ^ a )  =  ( K ^ (
b  +  1 ) ) )
266264, 265oveq12d 6320 . . . . . 6  |-  ( a  =  ( b  +  1 )  ->  (
( ( A Xrm  a )  -  ( ( A  -  K )  x.  ( A Yrm  a ) ) )  -  ( K ^ a ) )  =  ( ( ( A Xrm  ( b  +  1 ) )  -  (
( A