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

Theorem rmydioph 27107
Description: jm2.27 27101 restated in terms of Diophantine sets. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
Assertion
Ref Expression
rmydioph  |-  { a  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  3 )  =  ( ( a `
 1 ) Yrm  ( a `
 2 ) ) ) }  e.  (Dioph `  3 )

Proof of Theorem rmydioph
Dummy variables  b 
c  d  e  f  g  h  i are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elmapi 6792 . . . . . . 7  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  a : ( 1 ... 3 ) --> NN0 )
2 2nn 9877 . . . . . . . . 9  |-  2  e.  NN
32jm2.27dlem3 27104 . . . . . . . 8  |-  2  e.  ( 1 ... 2
)
4 df-3 9805 . . . . . . . 8  |-  3  =  ( 2  +  1 )
53, 4, 2jm2.27dlem2 27103 . . . . . . 7  |-  2  e.  ( 1 ... 3
)
6 ffvelrn 5663 . . . . . . 7  |-  ( ( a : ( 1 ... 3 ) --> NN0 
/\  2  e.  ( 1 ... 3 ) )  ->  ( a `  2 )  e. 
NN0 )
71, 5, 6sylancl 643 . . . . . 6  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  (
a `  2 )  e.  NN0 )
8 elnn0 9967 . . . . . 6  |-  ( ( a `  2 )  e.  NN0  <->  ( ( a `
 2 )  e.  NN  \/  ( a `
 2 )  =  0 ) )
97, 8sylib 188 . . . . 5  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  (
( a `  2
)  e.  NN  \/  ( a `  2
)  =  0 ) )
10 iba 489 . . . . . . 7  |-  ( ( ( a `  2
)  e.  NN  \/  ( a `  2
)  =  0 )  ->  ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  <->  ( (
a `  3 )  =  ( ( a `
 1 ) Yrm  ( a `
 2 ) )  /\  ( ( a `
 2 )  e.  NN  \/  ( a `
 2 )  =  0 ) ) ) )
11 andi 837 . . . . . . 7  |-  ( ( ( a `  3
)  =  ( ( a `  1 ) Yrm  ( a `  2 ) )  /\  ( ( a `  2 )  e.  NN  \/  (
a `  2 )  =  0 ) )  <-> 
( ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  /\  ( a `  2
)  e.  NN )  \/  ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  /\  ( a `  2
)  =  0 ) ) )
1210, 11syl6bb 252 . . . . . 6  |-  ( ( ( a `  2
)  e.  NN  \/  ( a `  2
)  =  0 )  ->  ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  <->  ( (
( a `  3
)  =  ( ( a `  1 ) Yrm  ( a `  2 ) )  /\  ( a `
 2 )  e.  NN )  \/  (
( a `  3
)  =  ( ( a `  1 ) Yrm  ( a `  2 ) )  /\  ( a `
 2 )  =  0 ) ) ) )
1312anbi2d 684 . . . . 5  |-  ( ( ( a `  2
)  e.  NN  \/  ( a `  2
)  =  0 )  ->  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  ( a `  3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) ) )  <-> 
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  /\  ( a `  2
)  e.  NN )  \/  ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  /\  ( a `  2
)  =  0 ) ) ) ) )
149, 13syl 15 . . . 4  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  3
)  =  ( ( a `  1 ) Yrm  ( a `  2 ) ) )  <->  ( (
a `  1 )  e.  ( ZZ>= `  2 )  /\  ( ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  /\  ( a `  2
)  e.  NN )  \/  ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  /\  ( a `  2
)  =  0 ) ) ) ) )
15 simplr 731 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )
16 nnz 10045 . . . . . . . . . . . . . 14  |-  ( ( a `  2 )  e.  NN  ->  (
a `  2 )  e.  ZZ )
1716adantl 452 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( a ` 
2 )  e.  ZZ )
18 frmy 26999 . . . . . . . . . . . . . 14  |- Yrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> ZZ
1918fovcl 5949 . . . . . . . . . . . . 13  |-  ( ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  2 )  e.  ZZ )  ->  (
( a `  1
) Yrm  ( a `  2
) )  e.  ZZ )
2015, 17, 19syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( ( a `
 1 ) Yrm  ( a `
 2 ) )  e.  ZZ )
21 rmy0 27014 . . . . . . . . . . . . . 14  |-  ( ( a `  1 )  e.  ( ZZ>= `  2
)  ->  ( (
a `  1 ) Yrm  0 )  =  0 )
2221ad2antlr 707 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( ( a `
 1 ) Yrm  0 )  =  0 )
23 nngt0 9775 . . . . . . . . . . . . . . 15  |-  ( ( a `  2 )  e.  NN  ->  0  <  ( a `  2
) )
2423adantl 452 . . . . . . . . . . . . . 14  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  0  <  (
a `  2 )
)
25 0z 10035 . . . . . . . . . . . . . . . 16  |-  0  e.  ZZ
2625a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  0  e.  ZZ )
27 ltrmy 27039 . . . . . . . . . . . . . . 15  |-  ( ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  0  e.  ZZ  /\  ( a `
 2 )  e.  ZZ )  ->  (
0  <  ( a `  2 )  <->  ( (
a `  1 ) Yrm  0 )  <  ( ( a `  1 ) Yrm  ( a `  2 ) ) ) )
2815, 26, 17, 27syl3anc 1182 . . . . . . . . . . . . . 14  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( 0  < 
( a `  2
)  <->  ( ( a `
 1 ) Yrm  0 )  <  ( ( a `
 1 ) Yrm  ( a `
 2 ) ) ) )
2924, 28mpbid 201 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( ( a `
 1 ) Yrm  0 )  <  ( ( a `
 1 ) Yrm  ( a `
 2 ) ) )
3022, 29eqbrtrrd 4045 . . . . . . . . . . . 12  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  0  <  (
( a `  1
) Yrm  ( a `  2
) ) )
31 elnnz 10034 . . . . . . . . . . . 12  |-  ( ( ( a `  1
) Yrm  ( a `  2
) )  e.  NN  <->  ( ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  e.  ZZ  /\  0  < 
( ( a ` 
1 ) Yrm  ( a ` 
2 ) ) ) )
3220, 30, 31sylanbrc 645 . . . . . . . . . . 11  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( ( a `
 1 ) Yrm  ( a `
 2 ) )  e.  NN )
33 eleq1 2343 . . . . . . . . . . 11  |-  ( ( a `  3 )  =  ( ( a `
 1 ) Yrm  ( a `
 2 ) )  ->  ( ( a `
 3 )  e.  NN  <->  ( ( a `
 1 ) Yrm  ( a `
 2 ) )  e.  NN ) )
3432, 33syl5ibrcom 213 . . . . . . . . . 10  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  -> 
( a `  3
)  e.  NN ) )
3534pm4.71rd 616 . . . . . . . . 9  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  <->  ( (
a `  3 )  e.  NN  /\  ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) ) ) ) )
36 simpllr 735 . . . . . . . . . . 11  |-  ( ( ( ( a  e.  ( NN0  ^m  (
1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  /\  ( a ` 
3 )  e.  NN )  ->  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )
37 simplr 731 . . . . . . . . . . 11  |-  ( ( ( ( a  e.  ( NN0  ^m  (
1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  /\  ( a ` 
3 )  e.  NN )  ->  ( a ` 
2 )  e.  NN )
38 simpr 447 . . . . . . . . . . 11  |-  ( ( ( ( a  e.  ( NN0  ^m  (
1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  /\  ( a ` 
3 )  e.  NN )  ->  ( a ` 
3 )  e.  NN )
39 jm2.27 27101 . . . . . . . . . . 11  |-  ( ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  2 )  e.  NN  /\  ( a `
 3 )  e.  NN )  ->  (
( a `  3
)  =  ( ( a `  1 ) Yrm  ( a `  2 ) )  <->  E. b  e.  NN0  E. c  e.  NN0  E. d  e.  NN0  E. e  e. 
NN0  E. f  e.  NN0  E. g  e.  NN0  E. h  e.  NN0  ( ( ( ( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( g ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
f ^ 2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  /\  d  ||  (
e  -  ( a `
 1 ) ) ) )  /\  (
( ( 2  x.  ( a `  3
) )  ||  (
e  -  1 )  /\  d  ||  (
f  -  ( a `
 3 ) ) )  /\  ( ( 2  x.  ( a `
 3 ) ) 
||  ( f  -  ( a `  2
) )  /\  (
a `  2 )  <_  ( a `  3
) ) ) ) ) )
4036, 37, 38, 39syl3anc 1182 . . . . . . . . . 10  |-  ( ( ( ( a  e.  ( NN0  ^m  (
1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  /\  ( a ` 
3 )  e.  NN )  ->  ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  <->  E. b  e.  NN0  E. c  e. 
NN0  E. d  e.  NN0  E. e  e.  NN0  E. f  e.  NN0  E. g  e. 
NN0  E. h  e.  NN0  ( ( ( ( ( b ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( a `
 3 ) ^
2 ) ) )  =  1  /\  (
( d ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( c ^
2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( g ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( f ^
2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( f  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) ) ) )
4140pm5.32da 622 . . . . . . . . 9  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( ( ( a `  3 )  e.  NN  /\  (
a `  3 )  =  ( ( a `
 1 ) Yrm  ( a `
 2 ) ) )  <->  ( ( a `
 3 )  e.  NN  /\  E. b  e.  NN0  E. c  e. 
NN0  E. d  e.  NN0  E. e  e.  NN0  E. f  e.  NN0  E. g  e. 
NN0  E. h  e.  NN0  ( ( ( ( ( b ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( a `
 3 ) ^
2 ) ) )  =  1  /\  (
( d ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( c ^
2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( g ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( f ^
2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( f  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) ) ) ) )
4235, 41bitrd 244 . . . . . . . 8  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  <->  ( (
a `  3 )  e.  NN  /\  E. b  e.  NN0  E. c  e. 
NN0  E. d  e.  NN0  E. e  e.  NN0  E. f  e.  NN0  E. g  e. 
NN0  E. h  e.  NN0  ( ( ( ( ( b ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( a `
 3 ) ^
2 ) ) )  =  1  /\  (
( d ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( c ^
2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( g ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( f ^
2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( f  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) ) ) ) )
4342ex 423 . . . . . . 7  |-  ( ( a  e.  ( NN0 
^m  ( 1 ... 3 ) )  /\  ( a `  1
)  e.  ( ZZ>= ` 
2 ) )  -> 
( ( a ` 
2 )  e.  NN  ->  ( ( a ` 
3 )  =  ( ( a `  1
) Yrm  ( a `  2
) )  <->  ( (
a `  3 )  e.  NN  /\  E. b  e.  NN0  E. c  e. 
NN0  E. d  e.  NN0  E. e  e.  NN0  E. f  e.  NN0  E. g  e. 
NN0  E. h  e.  NN0  ( ( ( ( ( b ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( a `
 3 ) ^
2 ) ) )  =  1  /\  (
( d ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( c ^
2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( g ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( f ^
2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( f  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) ) ) ) ) )
4443pm5.32rd 621 . . . . . 6  |-  ( ( a  e.  ( NN0 
^m  ( 1 ... 3 ) )  /\  ( a `  1
)  e.  ( ZZ>= ` 
2 ) )  -> 
( ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  /\  ( a `  2
)  e.  NN )  <-> 
( ( ( a `
 3 )  e.  NN  /\  E. b  e.  NN0  E. c  e. 
NN0  E. d  e.  NN0  E. e  e.  NN0  E. f  e.  NN0  E. g  e. 
NN0  E. h  e.  NN0  ( ( ( ( ( b ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( a `
 3 ) ^
2 ) ) )  =  1  /\  (
( d ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( c ^
2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( g ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( f ^
2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( f  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) ) )  /\  ( a `  2
)  e.  NN ) ) )
45 oveq2 5866 . . . . . . . . . . 11  |-  ( ( a `  2 )  =  0  ->  (
( a `  1
) Yrm  ( a `  2
) )  =  ( ( a `  1
) Yrm  0 ) )
4645adantl 452 . . . . . . . . . 10  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  =  0 )  ->  ( (
a `  1 ) Yrm  ( a `  2 ) )  =  ( ( a `  1 ) Yrm  0 ) )
4721ad2antlr 707 . . . . . . . . . 10  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  =  0 )  ->  ( (
a `  1 ) Yrm  0 )  =  0 )
4846, 47eqtrd 2315 . . . . . . . . 9  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  =  0 )  ->  ( (
a `  1 ) Yrm  ( a `  2 ) )  =  0 )
4948eqeq2d 2294 . . . . . . . 8  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  =  0 )  ->  ( (
a `  3 )  =  ( ( a `
 1 ) Yrm  ( a `
 2 ) )  <-> 
( a `  3
)  =  0 ) )
5049ex 423 . . . . . . 7  |-  ( ( a  e.  ( NN0 
^m  ( 1 ... 3 ) )  /\  ( a `  1
)  e.  ( ZZ>= ` 
2 ) )  -> 
( ( a ` 
2 )  =  0  ->  ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  <->  ( a `  3 )  =  0 ) ) )
5150pm5.32rd 621 . . . . . 6  |-  ( ( a  e.  ( NN0 
^m  ( 1 ... 3 ) )  /\  ( a `  1
)  e.  ( ZZ>= ` 
2 ) )  -> 
( ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  /\  ( a `  2
)  =  0 )  <-> 
( ( a ` 
3 )  =  0  /\  ( a ` 
2 )  =  0 ) ) )
5244, 51orbi12d 690 . . . . 5  |-  ( ( a  e.  ( NN0 
^m  ( 1 ... 3 ) )  /\  ( a `  1
)  e.  ( ZZ>= ` 
2 ) )  -> 
( ( ( ( a `  3 )  =  ( ( a `
 1 ) Yrm  ( a `
 2 ) )  /\  ( a ` 
2 )  e.  NN )  \/  ( (
a `  3 )  =  ( ( a `
 1 ) Yrm  ( a `
 2 ) )  /\  ( a ` 
2 )  =  0 ) )  <->  ( (
( ( a ` 
3 )  e.  NN  /\ 
E. b  e.  NN0  E. c  e.  NN0  E. d  e.  NN0  E. e  e. 
NN0  E. f  e.  NN0  E. g  e.  NN0  E. h  e.  NN0  ( ( ( ( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( g ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
f ^ 2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  /\  d  ||  (
e  -  ( a `
 1 ) ) ) )  /\  (
( ( 2  x.  ( a `  3
) )  ||  (
e  -  1 )  /\  d  ||  (
f  -  ( a `
 3 ) ) )  /\  ( ( 2  x.  ( a `
 3 ) ) 
||  ( f  -  ( a `  2
) )  /\  (
a `  2 )  <_  ( a `  3
) ) ) ) )  /\  ( a `
 2 )  e.  NN )  \/  (
( a `  3
)  =  0  /\  ( a `  2
)  =  0 ) ) ) )
5352pm5.32da 622 . . . 4  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  /\  ( a `  2
)  e.  NN )  \/  ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  /\  ( a `  2
)  =  0 ) ) )  <->  ( (
a `  1 )  e.  ( ZZ>= `  2 )  /\  ( ( ( ( a `  3 )  e.  NN  /\  E. b  e.  NN0  E. c  e.  NN0  E. d  e. 
NN0  E. e  e.  NN0  E. f  e.  NN0  E. g  e.  NN0  E. h  e. 
NN0  ( ( ( ( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( g ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
f ^ 2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  /\  d  ||  (
e  -  ( a `
 1 ) ) ) )  /\  (
( ( 2  x.  ( a `  3
) )  ||  (
e  -  1 )  /\  d  ||  (
f  -  ( a `
 3 ) ) )  /\  ( ( 2  x.  ( a `
 3 ) ) 
||  ( f  -  ( a `  2
) )  /\  (
a `  2 )  <_  ( a `  3
) ) ) ) )  /\  ( a `
 2 )  e.  NN )  \/  (
( a `  3
)  =  0  /\  ( a `  2
)  =  0 ) ) ) ) )
5414, 53bitrd 244 . . 3  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  3
)  =  ( ( a `  1 ) Yrm  ( a `  2 ) ) )  <->  ( (
a `  1 )  e.  ( ZZ>= `  2 )  /\  ( ( ( ( a `  3 )  e.  NN  /\  E. b  e.  NN0  E. c  e.  NN0  E. d  e. 
NN0  E. e  e.  NN0  E. f  e.  NN0  E. g  e.  NN0  E. h  e. 
NN0  ( ( ( ( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( g ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
f ^ 2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  /\  d  ||  (
e  -  ( a `
 1 ) ) ) )  /\  (
( ( 2  x.  ( a `  3
) )  ||  (
e  -  1 )  /\  d  ||  (
f  -  ( a `
 3 ) ) )  /\  ( ( 2  x.  ( a `
 3 ) ) 
||  ( f  -  ( a `  2
) )  /\  (
a `  2 )  <_  ( a `  3
) ) ) ) )  /\  ( a `
 2 )  e.  NN )  \/  (
( a `  3
)  =  0  /\  ( a `  2
)  =  0 ) ) ) ) )
5554rabbiia 2778 . 2  |-  { a  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  3 )  =  ( ( a `
 1 ) Yrm  ( a `
 2 ) ) ) }  =  {
a  e.  ( NN0 
^m  ( 1 ... 3 ) )  |  ( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( ( ( ( a `  3 )  e.  NN  /\  E. b  e.  NN0  E. c  e.  NN0  E. d  e. 
NN0  E. e  e.  NN0  E. f  e.  NN0  E. g  e.  NN0  E. h  e. 
NN0  ( ( ( ( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( g ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
f ^ 2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  /\  d  ||  (
e  -  ( a `
 1 ) ) ) )  /\  (
( ( 2  x.  ( a `  3
) )  ||  (
e  -  1 )  /\  d  ||  (
f  -  ( a `
 3 ) ) )  /\  ( ( 2  x.  ( a `
 3 ) ) 
||  ( f  -  ( a `  2
) )  /\  (
a `  2 )  <_  ( a `  3
) ) ) ) )  /\  ( a `
 2 )  e.  NN )  \/  (
( a `  3
)  =  0  /\  ( a `  2
)  =  0 ) ) ) }
56 3nn0 9983 . . . 4  |-  3  e.  NN0
57 2z 10054 . . . 4  |-  2  e.  ZZ
58 ovex 5883 . . . . 5  |-  ( 1 ... 3 )  e. 
_V
59 1nn 9757 . . . . . . . 8  |-  1  e.  NN
6059jm2.27dlem3 27104 . . . . . . 7  |-  1  e.  ( 1 ... 1
)
61 df-2 9804 . . . . . . 7  |-  2  =  ( 1  +  1 )
6260, 61, 59jm2.27dlem2 27103 . . . . . 6  |-  1  e.  ( 1 ... 2
)
6362, 4, 2jm2.27dlem2 27103 . . . . 5  |-  1  e.  ( 1 ... 3
)
64 mzpproj 26815 . . . . 5  |-  ( ( ( 1 ... 3
)  e.  _V  /\  1  e.  ( 1 ... 3 ) )  ->  ( a  e.  ( ZZ  ^m  (
1 ... 3 ) ) 
|->  ( a `  1
) )  e.  (mzPoly `  ( 1 ... 3
) ) )
6558, 63, 64mp2an 653 . . . 4  |-  ( a  e.  ( ZZ  ^m  ( 1 ... 3
) )  |->  ( a `
 1 ) )  e.  (mzPoly `  (
1 ... 3 ) )
66 eluzrabdioph 26887 . . . 4  |-  ( ( 3  e.  NN0  /\  2  e.  ZZ  /\  (
a  e.  ( ZZ 
^m  ( 1 ... 3 ) )  |->  ( a `  1 ) )  e.  (mzPoly `  ( 1 ... 3
) ) )  ->  { a  e.  ( NN0  ^m  ( 1 ... 3 ) )  |  ( a ` 
1 )  e.  (
ZZ>= `  2 ) }  e.  (Dioph `  3
) )
6756, 57, 65, 66mp3an 1277 . . 3  |-  { a  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( a `  1 )  e.  ( ZZ>= `  2
) }  e.  (Dioph `  3 )
68 3nn 9878 . . . . . . . . 9  |-  3  e.  NN
6968jm2.27dlem3 27104 . . . . . . . 8  |-  3  e.  ( 1 ... 3
)
70 mzpproj 26815 . . . . . . . 8  |-  ( ( ( 1 ... 3
)  e.  _V  /\  3  e.  ( 1 ... 3 ) )  ->  ( a  e.  ( ZZ  ^m  (
1 ... 3 ) ) 
|->  ( a `  3
) )  e.  (mzPoly `  ( 1 ... 3
) ) )
7158, 69, 70mp2an 653 . . . . . . 7  |-  ( a  e.  ( ZZ  ^m  ( 1 ... 3
) )  |->  ( a `
 3 ) )  e.  (mzPoly `  (
1 ... 3 ) )
72 elnnrabdioph 26888 . . . . . . 7  |-  ( ( 3  e.  NN0  /\  ( a  e.  ( ZZ  ^m  ( 1 ... 3 ) ) 
|->  ( a `  3
) )  e.  (mzPoly `  ( 1 ... 3
) ) )  ->  { a  e.  ( NN0  ^m  ( 1 ... 3 ) )  |  ( a ` 
3 )  e.  NN }  e.  (Dioph `  3
) )
7356, 71, 72mp2an 653 . . . . . 6  |-  { a  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( a `  3 )  e.  NN }  e.  (Dioph `  3 )
74 vex 2791 . . . . . . . . . . . . 13  |-  i  e. 
_V
7574resex 4995 . . . . . . . . . . . 12  |-  ( i  |`  ( 1 ... 3
) )  e.  _V
76 fvex 5539 . . . . . . . . . . . . 13  |-  ( i `
 4 )  e. 
_V
77 fvex 5539 . . . . . . . . . . . . . 14  |-  ( i `
 5 )  e. 
_V
78 fvex 5539 . . . . . . . . . . . . . . 15  |-  ( i `
 6 )  e. 
_V
79 fvex 5539 . . . . . . . . . . . . . . . 16  |-  ( i `
 7 )  e. 
_V
80 fvex 5539 . . . . . . . . . . . . . . . . 17  |-  ( i `
 8 )  e. 
_V
81 fvex 5539 . . . . . . . . . . . . . . . . 17  |-  ( i `
 9 )  e. 
_V
82 fvex 5539 . . . . . . . . . . . . . . . . 17  |-  ( i `
 10 )  e. 
_V
83 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  =  ( i ` 
9 )  ->  (
g ^ 2 )  =  ( ( i `
 9 ) ^
2 ) )
84 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  ( i ` 
8 )  ->  (
f ^ 2 )  =  ( ( i `
 8 ) ^
2 ) )
8584oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  =  ( i ` 
8 )  ->  (
( ( e ^
2 )  -  1 )  x.  ( f ^ 2 ) )  =  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i ` 
8 ) ^ 2 ) ) )
8683, 85oveqan12rd 5878 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f  =  ( i `
 8 )  /\  g  =  ( i `  9 ) )  ->  ( ( g ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
f ^ 2 ) ) )  =  ( ( ( i ` 
9 ) ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i `
 8 ) ^
2 ) ) ) )
8786eqeq1d 2291 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  =  ( i `
 8 )  /\  g  =  ( i `  9 ) )  ->  ( ( ( g ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( f ^ 2 ) ) )  =  1  <->  ( ( ( i `  9 ) ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
( i `  8
) ^ 2 ) ) )  =  1 ) )
88873adant3 975 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f  =  ( i `
 8 )  /\  g  =  ( i `  9 )  /\  h  =  ( i `  10 ) )  -> 
( ( ( g ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
f ^ 2 ) ) )  =  1  <-> 
( ( ( i `
 9 ) ^
2 )  -  (
( ( e ^
2 )  -  1 )  x.  ( ( i `  8 ) ^ 2 ) ) )  =  1 ) )
89 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h  =  ( i `  10 )  ->  ( h  +  1 )  =  ( ( i `  10 )  +  1
) )
9089oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h  =  ( i `  10 )  ->  ( ( h  +  1 )  x.  ( 2  x.  ( ( a ` 
3 ) ^ 2 ) ) )  =  ( ( ( i `
 10 )  +  1 )  x.  (
2  x.  ( ( a `  3 ) ^ 2 ) ) ) )
9190eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  ( i `  10 )  ->  ( c  =  ( ( h  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  <->  c  =  ( ( ( i `
 10 )  +  1 )  x.  (
2  x.  ( ( a `  3 ) ^ 2 ) ) ) ) )
92913ad2ant3 978 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f  =  ( i `
 8 )  /\  g  =  ( i `  9 )  /\  h  =  ( i `  10 ) )  -> 
( c  =  ( ( h  +  1 )  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  <-> 
c  =  ( ( ( i `  10 )  +  1 )  x.  ( 2  x.  ( ( a ` 
3 ) ^ 2 ) ) ) ) )
9388, 923anbi12d 1253 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  =  ( i `
 8 )  /\  g  =  ( i `  9 )  /\  h  =  ( i `  10 ) )  -> 
( ( ( ( g ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( f ^ 2 ) ) )  =  1  /\  c  =  ( ( h  + 
1 )  x.  (
2  x.  ( ( a `  3 ) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) )  <->  ( (
( ( i ` 
9 ) ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i `
 8 ) ^
2 ) ) )  =  1  /\  c  =  ( ( ( i `  10 )  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) ) )
9493anbi2d 684 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  =  ( i `
 8 )  /\  g  =  ( i `  9 )  /\  h  =  ( i `  10 ) )  -> 
( ( ( ( ( b ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( a `
 3 ) ^
2 ) ) )  =  1  /\  (
( d ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( c ^
2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( g ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( f ^
2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  <->  ( (
( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( ( i `  9 ) ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
( i `  8
) ^ 2 ) ) )  =  1  /\  c  =  ( ( ( i `  10 )  +  1
)  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  /\  d  ||  (
e  -  ( a `
 1 ) ) ) ) ) )
95 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  ( i ` 
8 )  ->  (
f  -  ( a `
 3 ) )  =  ( ( i `
 8 )  -  ( a `  3
) ) )
9695breq2d 4035 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( i ` 
8 )  ->  (
d  ||  ( f  -  ( a ` 
3 ) )  <->  d  ||  ( ( i ` 
8 )  -  (
a `  3 )
) ) )
9796anbi2d 684 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( i ` 
8 )  ->  (
( ( 2  x.  ( a `  3
) )  ||  (
e  -  1 )  /\  d  ||  (
f  -  ( a `
 3 ) ) )  <->  ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( ( i ` 
8 )  -  (
a `  3 )
) ) ) )
98 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  ( i ` 
8 )  ->  (
f  -  ( a `
 2 ) )  =  ( ( i `
 8 )  -  ( a `  2
) ) )
9998breq2d 4035 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( i ` 
8 )  ->  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  <->  ( 2  x.  ( a ` 
3 ) )  ||  ( ( i ` 
8 )  -  (
a `  2 )
) ) )
10099anbi1d 685 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( i ` 
8 )  ->  (
( ( 2  x.  ( a `  3
) )  ||  (
f  -  ( a `
 2 ) )  /\  ( a ` 
2 )  <_  (
a `  3 )
)  <->  ( ( 2  x.  ( a ` 
3 ) )  ||  ( ( i ` 
8 )  -  (
a `  2 )
)  /\  ( a `  2 )  <_ 
( a `  3
) ) ) )
10197, 100anbi12d 691 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( i ` 
8 )  ->  (
( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( f  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) )  <->  ( ( ( 2  x.  ( a `
 3 ) ) 
||  ( e  - 
1 )  /\  d  ||  ( ( i ` 
8 )  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( (
i `  8 )  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) ) )
1021013ad2ant1 976 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  =  ( i `
 8 )  /\  g  =  ( i `  9 )  /\  h  =  ( i `  10 ) )  -> 
( ( ( ( 2  x.  ( a `
 3 ) ) 
||  ( e  - 
1 )  /\  d  ||  ( f  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) )  <->  ( ( ( 2  x.  ( a `
 3 ) ) 
||  ( e  - 
1 )  /\  d  ||  ( ( i ` 
8 )  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( (
i `  8 )  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) ) )
10394, 102anbi12d 691 . . . . . . . . . . . . . . . . 17  |-  ( ( f  =  ( i `
 8 )  /\  g  =  ( i `  9 )  /\  h  =  ( i `  10 ) )  -> 
( ( ( ( ( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( g ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
f ^ 2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  /\  d  ||  (
e  -  ( a `
 1 ) ) ) )  /\  (
( ( 2  x.  ( a `  3
) )  ||  (
e  -  1 )  /\  d  ||  (
f  -  ( a `
 3 ) ) )  /\  ( ( 2  x.  ( a `
 3 ) ) 
||  ( f  -  ( a `  2
) )  /\  (
a `  2 )  <_  ( a `  3
) ) ) )  <-> 
( ( ( ( ( b ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( a `
 3 ) ^
2 ) ) )  =  1  /\  (
( d ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( c ^
2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( ( i ` 
9 ) ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i `
 8 ) ^
2 ) ) )  =  1  /\  c  =  ( ( ( i `  10 )  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( ( i ` 
8 )  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( (
i `  8 )  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) ) ) )
10480, 81, 82, 103sbc3ie 3060 . . . . . . . . . . . . . . . 16  |-  ( [. ( i `  8
)  /  f ]. [. ( i `  9
)  /  g ]. [. ( i `  10 )  /  h ]. (
( ( ( ( b ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( ( a ` 
3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( g ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( f ^
2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( f  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) )  <->  ( (
( ( ( b ^ 2 )  -  ( ( ( ( a `  1 ) ^ 2 )  - 
1 )  x.  (
( a `  3
) ^ 2 ) ) )  =  1  /\  ( ( d ^ 2 )  -  ( ( ( ( a `  1 ) ^ 2 )  - 
1 )  x.  (
c ^ 2 ) ) )  =  1  /\  e  e.  (
ZZ>= `  2 ) )  /\  ( ( ( ( i `  9
) ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i ` 
8 ) ^ 2 ) ) )  =  1  /\  c  =  ( ( ( i `
 10 )  +  1 )  x.  (
2  x.  ( ( a `  3 ) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( ( i ` 
8 )  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( (
i `  8 )  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) ) )
10579, 104sbcbiiiOLD 26867 . . . . . . . . . . . . . . 15  |-  ( [. ( i `  7
)  /  e ]. [. ( i `  8
)  /  f ]. [. ( i `  9
)  /  g ]. [. ( i `  10 )  /  h ]. (
( ( ( ( b ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( ( a ` 
3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( g ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( f ^
2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( f  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) )  <->  [. ( i `
 7 )  / 
e ]. ( ( ( ( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( ( i `  9 ) ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
( i `  8
) ^ 2 ) ) )  =  1  /\  c  =  ( ( ( i `  10 )  +  1
)  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  /\  d  ||  (
e  -  ( a `
 1 ) ) ) )  /\  (
( ( 2  x.  ( a `  3
) )  ||  (
e  -  1 )  /\  d  ||  (
( i `  8
)  -  ( a `
 3 ) ) )  /\  ( ( 2  x.  ( a `
 3 ) ) 
||  ( ( i `
 8 )  -  ( a `  2
) )  /\  (
a `  2 )  <_  ( a `  3
) ) ) ) )
10678, 105sbcbiiiOLD 26867 . . . . . . . . . . . . . 14  |-  ( [. ( i `  6
)  /  d ]. [. ( i `  7
)  /  e ]. [. ( i `  8
)  /  f ]. [. ( i `  9
)  /  g ]. [. ( i `  10 )  /  h ]. (
( ( ( ( b ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( ( a ` 
3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( g ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( f ^
2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( f  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) )  <->  [. ( i `
 6 )  / 
d ]. [. ( i `
 7 )  / 
e ]. ( ( ( ( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( ( i `  9 ) ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
( i `  8
) ^ 2 ) ) )  =  1  /\  c  =  ( ( ( i `  10 )  +  1
)  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  /\  d  ||  (
e  -  ( a `
 1 ) ) ) )  /\  (
( ( 2  x.  ( a `  3
) )  ||  (
e  -  1 )  /\  d  ||  (
( i `  8
)  -  ( a `
 3 ) ) )  /\  ( ( 2  x.  ( a `
 3 ) ) 
||  ( ( i `
 8 )  -  ( a `  2
) )  /\  (
a `  2 )  <_  ( a `  3
) ) ) ) )
10777, 106sbcbiiiOLD 26867 . . . . . . . . . . . . 13  |-  ( [. ( i `  5
)  /  c ]. [. ( i `  6
)  /  d ]. [. ( i `  7
)  /  e ]. [. ( i `  8
)  /  f ]. [. ( i `  9
)  /  g ]. [. ( i `  10 )  /  h ]. (
( ( ( ( b ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( ( a ` 
3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( g ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( f ^
2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( f  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) )  <->  [. ( i `
 5 )  / 
c ]. [. ( i `
 6 )  / 
d ]. [. ( i `
 7 )  / 
e ]. ( ( ( ( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( ( i `  9 ) ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
( i `  8
) ^ 2 ) ) )  =  1  /\  c  =  ( ( ( i `  10 )  +  1
)  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  /\  d  ||  (
e  -  ( a `
 1 ) ) ) )  /\  (
( ( 2  x.  ( a `  3
) )  ||  (
e  -  1 )  /\  d  ||  (
( i `  8
)  -  ( a `
 3 ) ) )  /\  ( ( 2  x.  ( a `
 3 ) ) 
||  ( ( i `
 8 )  -  ( a `  2
) )  /\  (
a `  2 )  <_  ( a `  3
) ) ) ) )
10876, 107sbcbiiiOLD 26867 . . . . . . . . . . . 12  |-  ( [. ( i `  4
)  /  b ]. [. ( i `  5
)  /  c ]. [. ( i `  6
)  /  d ]. [. ( i `  7
)  /  e ]. [. ( i `  8
)  /  f ]. [. ( i `  9
)  /  g ]. [. ( i `  10 )  /  h ]. (
( ( ( ( b ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( ( a ` 
3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( g ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( f ^
2 ) ) )  =  1  /\  c  =  ( ( h  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( f  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) )  <->  [. ( i `
 4 )  / 
b ]. [. ( i `
 5 )  / 
c ]. [. ( i `
 6 )  / 
d ]. [. ( i `
 7 )  / 
e ]. ( ( ( ( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( ( i `  9 ) ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
( i `  8
) ^ 2 ) ) )  =  1  /\  c  =  ( ( ( i `  10 )  +  1
)  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  /\  d  ||  (
e  -  ( a `
 1 ) ) ) )  /\  (
( ( 2  x.  ( a `  3
) )  ||  (
e  -  1 )  /\  d  ||  (
( i `  8
)  -  ( a `
 3 ) ) )  /\  ( ( 2  x.  ( a `
 3 ) ) 
||  ( ( i `
 8 )  -  ( a `  2
) )  /\  (
a `  2 )  <_  ( a `  3
) ) ) ) )
10975, 108sbcbiiiOLD 26867 . . . . . . . . . . 11  |-  ( [. ( i  |`  (
1 ... 3 ) )  /  a ]. [. (
i `  4 )  /  b ]. [. (
i `  5 )  /  c ]. [. (
i `  6 )  /  d ]. [. (
i `  7 )  /  e ]. [. (
i `  8 )  /  f ]. [. (
i `  9 )  /  g ]. [. (
i `  10 )  /  h ]. ( ( ( ( ( b ^ 2 )  -  ( ( ( ( a `  1 ) ^ 2 )  - 
1 )  x.  (
( a `  3
) ^ 2 ) ) )  =  1  /\  ( ( d ^ 2 )  -  ( ( ( ( a `  1 ) ^ 2 )  - 
1 )  x.  (
c ^ 2 ) ) )  =  1  /\  e  e.  (
ZZ>= `  2 ) )  /\  ( ( ( g ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( f ^ 2 ) ) )  =  1  /\  c  =  ( ( h  + 
1 )  x.  (
2  x.  ( ( a `  3 ) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( f  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) )  <->  [. ( i  |`  ( 1 ... 3
) )  /  a ]. [. ( i ` 
4 )  /  b ]. [. ( i ` 
5 )  /  c ]. [. ( i ` 
6 )  /  d ]. [. ( i ` 
7 )  /  e ]. ( ( ( ( ( b ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( a `
 3 ) ^
2 ) ) )  =  1  /\  (
( d ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( c ^
2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( ( i ` 
9 ) ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i `
 8 ) ^
2 ) ) )  =  1  /\  c  =  ( ( ( i `  10 )  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( ( i ` 
8 )  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( (
i `  8 )  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) ) )
110 oveq1 5865 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  =  ( i ` 
6 )  ->  (
d ^ 2 )  =  ( ( i `
 6 ) ^
2 ) )
1111103ad2ant2 977 . . . . . . . . . . . . . . . . . . 19  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( d ^
2 )  =  ( ( i `  6
) ^ 2 ) )
112 oveq1 5865 . . . . . . . . . . . . . . . . . . . . 21  |-  ( c  =  ( i ` 
5 )  ->  (
c ^ 2 )  =  ( ( i `
 5 ) ^
2 ) )
113112oveq2d 5874 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  =  ( i ` 
5 )  ->  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) )  =  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( ( i ` 
5 ) ^ 2 ) ) )
1141133ad2ant1 976 . . . . . . . . . . . . . . . . . . 19  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( c ^ 2 ) )  =  ( ( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( i `  5 ) ^ 2 ) ) )
115111, 114oveq12d 5876 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( ( d ^ 2 )  -  ( ( ( ( a `  1 ) ^ 2 )  - 
1 )  x.  (
c ^ 2 ) ) )  =  ( ( ( i ` 
6 ) ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( i `
 5 ) ^
2 ) ) ) )
116115eqeq1d 2291 . . . . . . . . . . . . . . . . 17  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( ( ( d ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  <->  ( ( ( i `  6 ) ^ 2 )  -  ( ( ( ( a `  1 ) ^ 2 )  - 
1 )  x.  (
( i `  5
) ^ 2 ) ) )  =  1 ) )
117 eleq1 2343 . . . . . . . . . . . . . . . . . 18  |-  ( e  =  ( i ` 
7 )  ->  (
e  e.  ( ZZ>= ` 
2 )  <->  ( i `  7 )  e.  ( ZZ>= `  2 )
) )
1181173ad2ant3 978 . . . . . . . . . . . . . . . . 17  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( e  e.  ( ZZ>= `  2 )  <->  ( i `  7 )  e.  ( ZZ>= `  2
) ) )
119116, 1183anbi23d 1255 . . . . . . . . . . . . . . . 16  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( ( ( ( b ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( a `
 3 ) ^
2 ) ) )  =  1  /\  (
( d ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( c ^
2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  <->  ( ( ( b ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( ( a ` 
3 ) ^ 2 ) ) )  =  1  /\  ( ( ( i `  6
) ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( ( i ` 
5 ) ^ 2 ) ) )  =  1  /\  ( i `
 7 )  e.  ( ZZ>= `  2 )
) ) )
120 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( e  =  ( i ` 
7 )  ->  (
e ^ 2 )  =  ( ( i `
 7 ) ^
2 ) )
121120oveq1d 5873 . . . . . . . . . . . . . . . . . . . . 21  |-  ( e  =  ( i ` 
7 )  ->  (
( e ^ 2 )  -  1 )  =  ( ( ( i `  7 ) ^ 2 )  - 
1 ) )
122121oveq1d 5873 . . . . . . . . . . . . . . . . . . . 20  |-  ( e  =  ( i ` 
7 )  ->  (
( ( e ^
2 )  -  1 )  x.  ( ( i `  8 ) ^ 2 ) )  =  ( ( ( ( i `  7
) ^ 2 )  -  1 )  x.  ( ( i ` 
8 ) ^ 2 ) ) )
123122oveq2d 5874 . . . . . . . . . . . . . . . . . . 19  |-  ( e  =  ( i ` 
7 )  ->  (
( ( i ` 
9 ) ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i `
 8 ) ^
2 ) ) )  =  ( ( ( i `  9 ) ^ 2 )  -  ( ( ( ( i `  7 ) ^ 2 )  - 
1 )  x.  (
( i `  8
) ^ 2 ) ) ) )
124123eqeq1d 2291 . . . . . . . . . . . . . . . . . 18  |-  ( e  =  ( i ` 
7 )  ->  (
( ( ( i `
 9 ) ^
2 )  -  (
( ( e ^
2 )  -  1 )  x.  ( ( i `  8 ) ^ 2 ) ) )  =  1  <->  (
( ( i ` 
9 ) ^ 2 )  -  ( ( ( ( i ` 
7 ) ^ 2 )  -  1 )  x.  ( ( i `
 8 ) ^
2 ) ) )  =  1 ) )
1251243ad2ant3 978 . . . . . . . . . . . . . . . . 17  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( ( ( ( i `  9
) ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i ` 
8 ) ^ 2 ) ) )  =  1  <->  ( ( ( i `  9 ) ^ 2 )  -  ( ( ( ( i `  7 ) ^ 2 )  - 
1 )  x.  (
( i `  8
) ^ 2 ) ) )  =  1 ) )
126 eqeq1 2289 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  ( i ` 
5 )  ->  (
c  =  ( ( ( i `  10 )  +  1 )  x.  ( 2  x.  ( ( a ` 
3 ) ^ 2 ) ) )  <->  ( i `  5 )  =  ( ( ( i `
 10 )  +  1 )  x.  (
2  x.  ( ( a `  3 ) ^ 2 ) ) ) ) )
1271263ad2ant1 976 . . . . . . . . . . . . . . . . 17  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( c  =  ( ( ( i `
 10 )  +  1 )  x.  (
2  x.  ( ( a `  3 ) ^ 2 ) ) )  <->  ( i ` 
5 )  =  ( ( ( i `  10 )  +  1
)  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) ) ) )
128 simp2 956 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  d  =  ( i `  6 ) )
129 oveq1 5865 . . . . . . . . . . . . . . . . . . 19  |-  ( e  =  ( i ` 
7 )  ->  (
e  -  ( a `
 1 ) )  =  ( ( i `
 7 )  -  ( a `  1
) ) )
1301293ad2ant3 978 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( e  -  ( a `  1
) )  =  ( ( i `  7
)  -  ( a `
 1 ) ) )
131128, 130breq12d 4036 . . . . . . . . . . . . . . . . 17  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( d  ||  ( e  -  (
a `  1 )
)  <->  ( i ` 
6 )  ||  (
( i `  7
)  -  ( a `
 1 ) ) ) )
132125, 127, 1313anbi123d 1252 . . . . . . . . . . . . . . . 16  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( ( ( ( ( i ` 
9 ) ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i `
 8 ) ^
2 ) ) )  =  1  /\  c  =  ( ( ( i `  10 )  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) )  <->  ( (
( ( i ` 
9 ) ^ 2 )  -  ( ( ( ( i ` 
7 ) ^ 2 )  -  1 )  x.  ( ( i `
 8 ) ^
2 ) ) )  =  1  /\  (
i `  5 )  =  ( ( ( i `  10 )  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  (
i `  6 )  ||  ( ( i ` 
7 )  -  (
a `  1 )
) ) ) )
133119, 132anbi12d 691 . . . . . . . . . . . . . . 15  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( ( ( ( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( ( i `  9 ) ^ 2 )  -  ( ( ( e ^ 2 )  - 
1 )  x.  (
( i `  8
) ^ 2 ) ) )  =  1  /\  c  =  ( ( ( i `  10 )  +  1
)  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  /\  d  ||  (
e  -  ( a `
 1 ) ) ) )  <->  ( (
( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  1  /\  ( ( ( i `
 6 ) ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( i `  5 ) ^ 2 ) ) )  =  1  /\  ( i `  7
)  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( ( i `  9 ) ^ 2 )  -  ( ( ( ( i `  7 ) ^ 2 )  - 
1 )  x.  (
( i `  8
) ^ 2 ) ) )  =  1  /\  ( i ` 
5 )  =  ( ( ( i `  10 )  +  1
)  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  /\  ( i ` 
6 )  ||  (
( i `  7
)  -  ( a `
 1 ) ) ) ) ) )
134 oveq1 5865 . . . . . . . . . . . . . . . . . . 19  |-  ( e  =  ( i ` 
7 )  ->  (
e  -  1 )  =  ( ( i `
 7 )  - 
1 ) )
135134breq2d 4035 . . . . . . . . . . . . . . . . . 18  |-  ( e  =  ( i ` 
7 )  ->  (
( 2  x.  (
a `  3 )
)  ||  ( e  -  1 )  <->  ( 2  x.  ( a ` 
3 ) )  ||  ( ( i ` 
7 )  -  1 ) ) )
136 breq1 4026 . . . . . . . . . . . . . . . . . 18  |-  ( d  =  ( i ` 
6 )  ->  (
d  ||  ( (
i `  8 )  -  ( a ` 
3 ) )  <->  ( i `  6 )  ||  ( ( i ` 
8 )  -  (
a `  3 )
) ) )
137135, 136bi2anan9r 844 . . . . . . . . . . . . . . . . 17  |-  ( ( d  =  ( i `
 6 )  /\  e  =  ( i `  7 ) )  ->  ( ( ( 2  x.  ( a `
 3 ) ) 
||  ( e  - 
1 )  /\  d  ||  ( ( i ` 
8 )  -  (
a `  3 )
) )  <->  ( (
2  x.  ( a `
 3 ) ) 
||  ( ( i `
 7 )  - 
1 )  /\  (
i `  6 )  ||  ( ( i ` 
8 )  -  (
a `  3 )
) ) ) )
138137anbi1d 685 . . . . . . . . . . . . . . . 16  |-  ( ( d  =  ( i `
 6 )  /\  e  =  ( i `  7 ) )  ->  ( ( ( ( 2  x.  (
a `  3 )
)  ||  ( e  -  1 )  /\  d  ||  ( ( i `
 8 )  -  ( a `  3
) ) )  /\  ( ( 2  x.  ( a `  3
) )  ||  (
( i `  8
)  -  ( a `
 2 ) )  /\  ( a ` 
2 )  <_  (
a `  3 )
) )  <->  ( (
( 2  x.  (
a `  3 )
)  ||  ( (
i `  7 )  -  1 )  /\  ( i `  6
)  ||  ( (
i `  8 )  -  ( a ` 
3 ) ) )  /\  ( ( 2  x.  ( a ` 
3 ) )  ||  ( ( i ` 
8 )  -  (
a `  2 )
)  /\  ( a `  2 )  <_ 
( a `  3
) ) ) ) )
1391383adant1 973 . . . . . . . . . . . . . . 15  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( ( ( ( 2  x.  (
a `  3 )
)  ||  ( e  -  1 )  /\  d  ||  ( ( i `
 8 )  -  ( a `  3
) ) )  /\  ( ( 2  x.  ( a `  3
) )  ||  (
( i `  8
)  -  ( a `
 2 ) )  /\  ( a ` 
2 )  <_  (
a `  3 )
) )  <->  ( (
( 2  x.  (
a `  3 )
)  ||  ( (
i `  7 )  -  1 )  /\  ( i `  6
)  ||  ( (
i `  8 )  -  ( a ` 
3 ) ) )  /\  ( ( 2  x.  ( a ` 
3 ) )  ||  ( ( i ` 
8 )  -  (
a `  2 )
)  /\  ( a `  2 )  <_ 
( a `  3
) ) ) ) )
140133, 139anbi12d 691 . . . . . . . . . . . . . 14  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( ( ( ( ( ( b ^ 2 )  -  ( ( ( ( a `  1 ) ^ 2 )  - 
1 )  x.  (
( a `  3
) ^ 2 ) ) )  =  1  /\  ( ( d ^ 2 )  -  ( ( ( ( a `  1 ) ^ 2 )  - 
1 )  x.  (
c ^ 2 ) ) )  =  1  /\  e  e.  (
ZZ>= `  2 ) )  /\  ( ( ( ( i `  9
) ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i ` 
8 ) ^ 2 ) ) )  =  1  /\  c  =  ( ( ( i `
 10 )  +  1 )  x.  (
2  x.  ( ( a `  3 ) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( ( i ` 
8 )  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( (
i `  8 )  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) )  <->  ( (
( ( ( b ^ 2 )  -  ( ( ( ( a `  1 ) ^ 2 )  - 
1 )  x.  (
( a `  3
) ^ 2 ) ) )  =  1  /\  ( ( ( i `  6 ) ^ 2 )  -  ( ( ( ( a `  1 ) ^ 2 )  - 
1 )  x.  (
( i `  5
) ^ 2 ) ) )  =  1  /\  ( i ` 
7 )  e.  (
ZZ>= `  2 ) )  /\  ( ( ( ( i `  9
) ^ 2 )  -  ( ( ( ( i `  7
) ^ 2 )  -  1 )  x.  ( ( i ` 
8 ) ^ 2 ) ) )  =  1  /\  ( i `
 5 )  =  ( ( ( i `
 10 )  +  1 )  x.  (
2  x.  ( ( a `  3 ) ^ 2 ) ) )  /\  ( i `
 6 )  ||  ( ( i ` 
7 )  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( ( i ` 
7 )  -  1 )  /\  ( i `
 6 )  ||  ( ( i ` 
8 )  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( (
i `  8 )  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) ) ) )
14177, 78, 79, 140sbc3ie 3060 . . . . . . . . . . . . 13  |-  ( [. ( i `  5
)  /  c ]. [. ( i `  6
)  /  d ]. [. ( i `  7
)  /  e ]. ( ( ( ( ( b ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( a `
 3 ) ^
2 ) ) )  =  1  /\  (
( d ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( c ^
2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( ( i ` 
9 ) ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i `
 8 ) ^
2 ) ) )  =  1  /\  c  =  ( ( ( i `  10 )  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( ( i ` 
8 )  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( (
i `  8 )  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) )  <->  ( (
( ( ( b ^ 2 )  -  ( ( ( ( a `  1 ) ^ 2 )  - 
1 )  x.  (
( a `  3
) ^ 2 ) ) )  =  1  /\  ( ( ( i `  6 ) ^ 2 )  -  ( ( ( ( a `  1 ) ^ 2 )  - 
1 )  x.  (
( i `  5
) ^ 2 ) ) )  =  1  /\  ( i ` 
7 )  e.  (
ZZ>= `  2 ) )  /\  ( ( ( ( i `  9
) ^ 2 )  -  ( ( ( ( i `  7
) ^ 2 )  -  1 )  x.  ( ( i ` 
8 ) ^ 2 ) ) )  =  1  /\  ( i `
 5 )  =  ( ( ( i `
 10 )  +  1 )  x.  (
2  x.  ( ( a `  3 ) ^ 2 ) ) )  /\  ( i `
 6 )  ||  ( ( i ` 
7 )  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( ( i ` 
7 )  -  1 )  /\  ( i `
 6 )  ||  ( ( i ` 
8 )  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( (
i `  8 )  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) ) )
14276, 141sbcbiiiOLD 26867 . . . . . . . . . . . 12  |-  ( [. ( i `  4
)  /  b ]. [. ( i `  5
)  /  c ]. [. ( i `  6
)  /  d ]. [. ( i `  7
)  /  e ]. ( ( ( ( ( b ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( a `
 3 ) ^
2 ) ) )  =  1  /\  (
( d ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( c ^
2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( ( i ` 
9 ) ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i `
 8 ) ^
2 ) ) )  =  1  /\  c  =  ( ( ( i `  10 )  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( ( i ` 
8 )  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( (
i `  8 )  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) )  <->  [. ( i `
 4 )  / 
b ]. ( ( ( ( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  1  /\  ( ( ( i `
 6 ) ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( i `  5 ) ^ 2 ) ) )  =  1  /\  ( i `  7
)  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( ( i `  9 ) ^ 2 )  -  ( ( ( ( i `  7 ) ^ 2 )  - 
1 )  x.  (
( i `  8
) ^ 2 ) ) )  =  1  /\  ( i ` 
5 )  =  ( ( ( i `  10 )  +  1
)  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  /\  ( i ` 
6 )  ||  (
( i `  7
)  -  ( a `
 1 ) ) ) )  /\  (
( ( 2  x.  ( a `  3
) )  ||  (
( i `  7
)  -  1 )  /\  ( i ` 
6 )  ||  (
( i `  8
)  -  ( a `
 3 ) ) )  /\  ( ( 2  x.  ( a `
 3 ) ) 
||  ( ( i `
 8 )  -  ( a `  2
) )  /\  (
a `  2 )  <_  ( a `  3
) ) ) ) )
14375, 142sbcbiiiOLD 26867 . . . . . . . . . . 11  |-  ( [. ( i  |`  (
1 ... 3 ) )  /  a ]. [. (
i `  4 )  /  b ]. [. (
i `  5 )  /  c ]. [. (
i `  6 )  /  d ]. [. (
i `  7 )  /  e ]. (
( ( ( ( b ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( ( a ` 
3 ) ^ 2 ) ) )  =  1  /\  ( ( d ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( c ^ 2 ) ) )  =  1  /\  e  e.  ( ZZ>= `  2 )
)  /\  ( (
( ( i ` 
9 ) ^ 2 )  -  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i `
 8 ) ^
2 ) ) )  =  1  /\  c  =  ( ( ( i `  10 )  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  d  ||  ( e  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( e  -  1 )  /\  d  ||  ( ( i ` 
8 )  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( (
i `  8 )  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) )  <->  [. ( i  |`  ( 1 ... 3
) )  /  a ]. [. ( i ` 
4 )  /  b ]. ( ( ( ( ( b ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( a `
 3 ) ^
2 ) ) )  =  1  /\  (
( ( i ` 
6 ) ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( i `
 5 ) ^
2 ) ) )  =  1  /\  (
i `  7 )  e.  ( ZZ>= `  2 )
)  /\  ( (
( ( i ` 
9 ) ^ 2 )  -  ( ( ( ( i ` 
7 ) ^ 2 )  -  1 )  x.  ( ( i `
 8 ) ^
2 ) ) )  =  1  /\  (
i `  5 )  =  ( ( ( i `  10 )  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  /\  (
i `  6 )  ||  ( ( i ` 
7 )  -  (
a `  1 )
) ) )  /\  ( ( ( 2  x.  ( a ` 
3 ) )  ||  ( ( i ` 
7 )  -  1 )  /\  ( i `
 6 )  ||  ( ( i ` 
8 )  -  (
a `  3 )
) )  /\  (
( 2  x.  (
a `  3 )
)  ||  ( (
i `  8 )  -  ( a ` 
2 ) )  /\  ( a `  2
)  <_  ( a `  3 ) ) ) ) )
144 oveq1 5865 . . . . . . . . . . . . . . . . 17  |-  ( b  =  ( i ` 
4 )  ->  (
b ^ 2 )  =  ( ( i `
 4 ) ^
2 ) )
14563jm2.27dlem1 27102 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
a `  1 )  =  ( i ` 
1 ) )
146145oveq1d 5873 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( a `  1
) ^ 2 )  =  ( ( i `
 1 ) ^
2 ) )
147146oveq1d 5873 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( ( a ` 
1 ) ^ 2 )  -  1 )  =  ( ( ( i `  1 ) ^ 2 )  - 
1 ) )
14869jm2.27dlem1 27102 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
a `  3 )  =  ( i ` 
3 ) )
149148oveq1d 5873 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( a `  3
) ^ 2 )  =  ( ( i `
 3 ) ^
2 ) )
150147, 149oveq12d 5876 . . . . . . . . . . . . . . . . 17  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) )  =  ( ( ( ( i `  1
) ^ 2 )  -  1 )  x.  ( ( i ` 
3 ) ^ 2 ) ) )
151144, 150oveqan12rd 5878 . . . . . . . . . . . . . . . 16  |-  ( ( a  =  ( i  |`  ( 1 ... 3
) )  /\  b  =  ( i ` 
4 ) )  -> 
( ( b ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) ) )  =  ( ( ( i `  4
) ^ 2 )  -  ( ( ( ( i `  1
) ^ 2 )  -  1 )  x.  ( ( i ` 
3 ) ^ 2 ) ) ) )
152151eqeq1d 2291 . . . . . . . . . . . . . . 15  |-  ( ( a  =  ( i  |`  ( 1 ... 3
) )  /\  b  =  ( i ` 
4 ) )  -> 
( ( ( b ^ 2 )  -  ( ( ( ( a `  1 ) ^ 2 )  - 
1 )  x.  (
( a `  3
) ^ 2 ) ) )  =  1  <-> 
( ( ( i `
 4 ) ^
2 )  -  (
( ( ( i `
 1 ) ^
2 )  -  1 )  x.  ( ( i `  3 ) ^ 2 ) ) )  =  1 ) )
153147oveq1d 5873 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( i `  5 ) ^ 2 ) )  =  ( ( ( ( i `  1
) ^ 2 )  -  1 )  x.  ( ( i ` 
5 ) ^ 2 ) ) )
154153oveq2d 5874 . . . . . . . . . . . . . . . . 17  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( ( i ` 
6 ) ^ 2 )  -  ( ( ( ( a ` 
1 ) ^ 2 )  -  1 )  x.  ( ( i `
 5 ) ^
2 ) ) )  =  ( ( ( i `  6 ) ^ 2 )  -  ( ( ( ( i `  1 ) ^ 2 )  - 
1 )  x.  (
( i `  5
) ^ 2 ) ) ) )
155154eqeq1d 2291 . . . . . . . . . . . . . . . 16  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( ( ( i `
 6 ) ^
2 )  -  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( i `  5 ) ^ 2 ) ) )  =  1  <->  (
( ( i ` 
6 ) ^ 2 )  -  ( ( ( ( i ` 
1 ) ^ 2 )  -  1 )  x.  ( ( i `
 5 ) ^
2 ) ) )  =  1 ) )
156155adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( a  =  ( i  |`  ( 1 ... 3
) )  /\  b  =  ( i ` 
4 ) )  -> 
( ( ( ( i `  6 ) ^ 2 )  -  ( ( ( ( a `  1 ) ^ 2 )  - 
1 )  x.  (
( i `  5
) ^ 2 ) ) )  =  1  <-> 
( ( ( i `
 6 ) ^
2 )  -  (
( ( ( i `
 1 ) ^
2 )  -  1 )  x.  ( ( i `  5 ) ^ 2 ) ) )  =  1 ) )
157152, 1563anbi12d 1253 . . . . . . . . . . . . . 14  |-  ( ( a  =  ( i  |`  ( 1 ... 3
) )  /\  b  =  ( i ` 
4 ) )  -> 
( ( ( ( b ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( ( a ` 
3 ) ^ 2 ) ) )  =  1  /\  ( ( ( i `  6
) ^ 2 )  -  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( ( i ` 
5 ) ^ 2 ) ) )  =  1  /\  ( i `
 7 )  e.  ( ZZ>= `  2 )
)  <->  ( ( ( ( i `  4
) ^ 2 )  -  ( ( ( ( i `  1
) ^ 2 )  -  1 )  x.  ( ( i ` 
3 ) ^ 2 ) ) )  =  1  /\  ( ( ( i `  6
) ^ 2 )  -  ( ( ( ( i `  1
) ^ 2 )  -  1 )  x.  ( ( i ` 
5 )