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

Theorem rmydioph 27076
Description: jm2.27 27070 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 7030 . . . . . . 7  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  a : ( 1 ... 3 ) --> NN0 )
2 2nn 10125 . . . . . . . . 9  |-  2  e.  NN
32jm2.27dlem3 27073 . . . . . . . 8  |-  2  e.  ( 1 ... 2
)
4 df-3 10051 . . . . . . . 8  |-  3  =  ( 2  +  1 )
53, 4, 2jm2.27dlem2 27072 . . . . . . 7  |-  2  e.  ( 1 ... 3
)
6 ffvelrn 5860 . . . . . . 7  |-  ( ( a : ( 1 ... 3 ) --> NN0 
/\  2  e.  ( 1 ... 3 ) )  ->  ( a `  2 )  e. 
NN0 )
71, 5, 6sylancl 644 . . . . . 6  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  (
a `  2 )  e.  NN0 )
8 elnn0 10215 . . . . . 6  |-  ( ( a `  2 )  e.  NN0  <->  ( ( a `
 2 )  e.  NN  \/  ( a `
 2 )  =  0 ) )
97, 8sylib 189 . . . . 5  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  (
( a `  2
)  e.  NN  \/  ( a `  2
)  =  0 ) )
10 iba 490 . . . . . . 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 838 . . . . . . 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 253 . . . . . 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 685 . . . . 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 16 . . . 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 732 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )
16 nnz 10295 . . . . . . . . . . . . . 14  |-  ( ( a `  2 )  e.  NN  ->  (
a `  2 )  e.  ZZ )
1716adantl 453 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( a ` 
2 )  e.  ZZ )
18 frmy 26968 . . . . . . . . . . . . . 14  |- Yrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> ZZ
1918fovcl 6167 . . . . . . . . . . . . 13  |-  ( ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  2 )  e.  ZZ )  ->  (
( a `  1
) Yrm  ( a `  2
) )  e.  ZZ )
2015, 17, 19syl2anc 643 . . . . . . . . . . . 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 26983 . . . . . . . . . . . . . 14  |-  ( ( a `  1 )  e.  ( ZZ>= `  2
)  ->  ( (
a `  1 ) Yrm  0 )  =  0 )
2221ad2antlr 708 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( ( a `
 1 ) Yrm  0 )  =  0 )
23 nngt0 10021 . . . . . . . . . . . . . . 15  |-  ( ( a `  2 )  e.  NN  ->  0  <  ( a `  2
) )
2423adantl 453 . . . . . . . . . . . . . 14  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  0  <  (
a `  2 )
)
25 0z 10285 . . . . . . . . . . . . . . . 16  |-  0  e.  ZZ
2625a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  0  e.  ZZ )
27 ltrmy 27008 . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . 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 202 . . . . . . . . . . . . 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 4226 . . . . . . . . . . . 12  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  0  <  (
( a `  1
) Yrm  ( a `  2
) ) )
31 elnnz 10284 . . . . . . . . . . . 12  |-  ( ( ( a `  1
) Yrm  ( a `  2
) )  e.  NN  <->  ( ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  e.  ZZ  /\  0  < 
( ( a ` 
1 ) Yrm  ( a ` 
2 ) ) ) )
3220, 30, 31sylanbrc 646 . . . . . . . . . . 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 2495 . . . . . . . . . . 11  |-  ( ( a `  3 )  =  ( ( a `
 1 ) Yrm  ( a `
 2 ) )  ->  ( ( a `
 3 )  e.  NN  <->  ( ( a `
 1 ) Yrm  ( a `
 2 ) )  e.  NN ) )
3432, 33syl5ibrcom 214 . . . . . . . . . 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 617 . . . . . . . . 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 736 . . . . . . . . . . 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 732 . . . . . . . . . . 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 448 . . . . . . . . . . 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 27070 . . . . . . . . . . 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 1184 . . . . . . . . . 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 623 . . . . . . . . 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 245 . . . . . . . 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 424 . . . . . . 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 622 . . . . . 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 6081 . . . . . . . . . . 11  |-  ( ( a `  2 )  =  0  ->  (
( a `  1
) Yrm  ( a `  2
) )  =  ( ( a `  1
) Yrm  0 ) )
4645adantl 453 . . . . . . . . . 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 708 . . . . . . . . . 10  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  =  0 )  ->  ( (
a `  1 ) Yrm  0 )  =  0 )
4846, 47eqtrd 2467 . . . . . . . . 9  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  =  0 )  ->  ( (
a `  1 ) Yrm  ( a `  2 ) )  =  0 )
4948eqeq2d 2446 . . . . . . . 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 424 . . . . . . 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 622 . . . . . 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 691 . . . . 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 623 . . . 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 245 . . 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 2938 . 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 10231 . . . 4  |-  3  e.  NN0
57 2z 10304 . . . 4  |-  2  e.  ZZ
58 ovex 6098 . . . . 5  |-  ( 1 ... 3 )  e. 
_V
59 1nn 10003 . . . . . . . 8  |-  1  e.  NN
6059jm2.27dlem3 27073 . . . . . . 7  |-  1  e.  ( 1 ... 1
)
61 df-2 10050 . . . . . . 7  |-  2  =  ( 1  +  1 )
6260, 61, 59jm2.27dlem2 27072 . . . . . 6  |-  1  e.  ( 1 ... 2
)
6362, 4, 2jm2.27dlem2 27072 . . . . 5  |-  1  e.  ( 1 ... 3
)
64 mzpproj 26785 . . . . 5  |-  ( ( ( 1 ... 3
)  e.  _V  /\  1  e.  ( 1 ... 3 ) )  ->  ( a  e.  ( ZZ  ^m  (
1 ... 3 ) ) 
|->  ( a `  1
) )  e.  (mzPoly `  ( 1 ... 3
) ) )
6558, 63, 64mp2an 654 . . . 4  |-  ( a  e.  ( ZZ  ^m  ( 1 ... 3
) )  |->  ( a `
 1 ) )  e.  (mzPoly `  (
1 ... 3 ) )
66 eluzrabdioph 26857 . . . 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 1279 . . 3  |-  { a  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( a `  1 )  e.  ( ZZ>= `  2
) }  e.  (Dioph `  3 )
68 3nn 10126 . . . . . . . . 9  |-  3  e.  NN
6968jm2.27dlem3 27073 . . . . . . . 8  |-  3  e.  ( 1 ... 3
)
70 mzpproj 26785 . . . . . . . 8  |-  ( ( ( 1 ... 3
)  e.  _V  /\  3  e.  ( 1 ... 3 ) )  ->  ( a  e.  ( ZZ  ^m  (
1 ... 3 ) ) 
|->  ( a `  3
) )  e.  (mzPoly `  ( 1 ... 3
) ) )
7158, 69, 70mp2an 654 . . . . . . 7  |-  ( a  e.  ( ZZ  ^m  ( 1 ... 3
) )  |->  ( a `
 3 ) )  e.  (mzPoly `  (
1 ... 3 ) )
72 elnnrabdioph 26858 . . . . . . 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 654 . . . . . 6  |-  { a  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( a `  3 )  e.  NN }  e.  (Dioph `  3 )
74 fvex 5734 . . . . . . . . . . . . . . . . 17  |-  ( i `
 8 )  e. 
_V
75 fvex 5734 . . . . . . . . . . . . . . . . 17  |-  ( i `
 9 )  e. 
_V
76 fvex 5734 . . . . . . . . . . . . . . . . 17  |-  ( i `
 10 )  e. 
_V
77 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  =  ( i ` 
9 )  ->  (
g ^ 2 )  =  ( ( i `
 9 ) ^
2 ) )
78 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  ( i ` 
8 )  ->  (
f ^ 2 )  =  ( ( i `
 8 ) ^
2 ) )
7978oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  =  ( i ` 
8 )  ->  (
( ( e ^
2 )  -  1 )  x.  ( f ^ 2 ) )  =  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i ` 
8 ) ^ 2 ) ) )
8077, 79oveqan12rd 6093 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
8180eqeq1d 2443 . . . . . . . . . . . . . . . . . . . . 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 ) )
82813adant3 977 . . . . . . . . . . . . . . . . . . . 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 ) )
83 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h  =  ( i `  10 )  ->  ( h  +  1 )  =  ( ( i `  10 )  +  1
) )
8483oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h  =  ( i `  10 )  ->  ( ( h  +  1 )  x.  ( 2  x.  ( ( a ` 
3 ) ^ 2 ) ) )  =  ( ( ( i `
 10 )  +  1 )  x.  (
2  x.  ( ( a `  3 ) ^ 2 ) ) ) )
8584eqeq2d 2446 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  ( i `  10 )  ->  ( c  =  ( ( h  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  <->  c  =  ( ( ( i `
 10 )  +  1 )  x.  (
2  x.  ( ( a `  3 ) ^ 2 ) ) ) ) )
86853ad2ant3 980 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
8782, 863anbi12d 1255 . . . . . . . . . . . . . . . . . . 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 )
) ) ) )
8887anbi2d 685 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
89 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  ( i ` 
8 )  ->  (
f  -  ( a `
 3 ) )  =  ( ( i `
 8 )  -  ( a `  3
) ) )
9089breq2d 4216 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( i ` 
8 )  ->  (
d  ||  ( f  -  ( a ` 
3 ) )  <->  d  ||  ( ( i ` 
8 )  -  (
a `  3 )
) ) )
9190anbi2d 685 . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )
92 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  ( i ` 
8 )  ->  (
f  -  ( a `
 2 ) )  =  ( ( i `
 8 )  -  ( a `  2
) ) )
9392breq2d 4216 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( i ` 
8 )  ->  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  <->  ( 2  x.  ( a ` 
3 ) )  ||  ( ( i ` 
8 )  -  (
a `  2 )
) ) )
9493anbi1d 686 . . . . . . . . . . . . . . . . . . . 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
) ) ) )
9591, 94anbi12d 692 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
96953ad2ant1 978 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
9788, 96anbi12d 692 . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
9874, 75, 76, 97sbc3ie 3222 . . . . . . . . . . . . . . . 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 ) ) ) ) )
9998sbcbii 3208 . . . . . . . . . . . . . . 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
) ) ) ) )
10099sbcbii 3208 . . . . . . . . . . . . . 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
) ) ) ) )
101100sbcbii 3208 . . . . . . . . . . . . 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
) ) ) ) )
102101sbcbii 3208 . . . . . . . . . . . 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
) ) ) ) )
103102sbcbii 3208 . . . . . . . . . . 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 ) ) ) ) )
104 fvex 5734 . . . . . . . . . . . . . 14  |-  ( i `
 5 )  e. 
_V
105 fvex 5734 . . . . . . . . . . . . . 14  |-  ( i `
 6 )  e. 
_V
106 fvex 5734 . . . . . . . . . . . . . 14  |-  ( i `
 7 )  e. 
_V
107 oveq1 6080 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  =  ( i ` 
6 )  ->  (
d ^ 2 )  =  ( ( i `
 6 ) ^
2 ) )
1081073ad2ant2 979 . . . . . . . . . . . . . . . . . . 19  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( d ^
2 )  =  ( ( i `  6
) ^ 2 ) )
109 oveq1 6080 . . . . . . . . . . . . . . . . . . . . 21  |-  ( c  =  ( i ` 
5 )  ->  (
c ^ 2 )  =  ( ( i `
 5 ) ^
2 ) )
110109oveq2d 6089 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  =  ( i ` 
5 )  ->  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) )  =  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( ( i ` 
5 ) ^ 2 ) ) )
1111103ad2ant1 978 . . . . . . . . . . . . . . . . . . 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 ) ) )
112108, 111oveq12d 6091 . . . . . . . . . . . . . . . . . 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 ) ) ) )
113112eqeq1d 2443 . . . . . . . . . . . . . . . . 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 ) )
114 eleq1 2495 . . . . . . . . . . . . . . . . . 18  |-  ( e  =  ( i ` 
7 )  ->  (
e  e.  ( ZZ>= ` 
2 )  <->  ( i `  7 )  e.  ( ZZ>= `  2 )
) )
1151143ad2ant3 980 . . . . . . . . . . . . . . . . 17  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( e  e.  ( ZZ>= `  2 )  <->  ( i `  7 )  e.  ( ZZ>= `  2
) ) )
116113, 1153anbi23d 1257 . . . . . . . . . . . . . . . 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 )
) ) )
117 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( e  =  ( i ` 
7 )  ->  (
e ^ 2 )  =  ( ( i `
 7 ) ^
2 ) )
118117oveq1d 6088 . . . . . . . . . . . . . . . . . . . . 21  |-  ( e  =  ( i ` 
7 )  ->  (
( e ^ 2 )  -  1 )  =  ( ( ( i `  7 ) ^ 2 )  - 
1 ) )
119118oveq1d 6088 . . . . . . . . . . . . . . . . . . . 20  |-  ( e  =  ( i ` 
7 )  ->  (
( ( e ^
2 )  -  1 )  x.  ( ( i `  8 ) ^ 2 ) )  =  ( ( ( ( i `  7
) ^ 2 )  -  1 )  x.  ( ( i ` 
8 ) ^ 2 ) ) )
120119oveq2d 6089 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
121120eqeq1d 2443 . . . . . . . . . . . . . . . . . 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 ) )
1221213ad2ant3 980 . . . . . . . . . . . . . . . . 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 ) )
123 eqeq1 2441 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
1241233ad2ant1 978 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
125 simp2 958 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  d  =  ( i `  6 ) )
126 oveq1 6080 . . . . . . . . . . . . . . . . . . 19  |-  ( e  =  ( i ` 
7 )  ->  (
e  -  ( a `
 1 ) )  =  ( ( i `
 7 )  -  ( a `  1
) ) )
1271263ad2ant3 980 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( e  -  ( a `  1
) )  =  ( ( i `  7
)  -  ( a `
 1 ) ) )
128125, 127breq12d 4217 . . . . . . . . . . . . . . . . 17  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( d  ||  ( e  -  (
a `  1 )
)  <->  ( i ` 
6 )  ||  (
( i `  7
)  -  ( a `
 1 ) ) ) )
129122, 124, 1283anbi123d 1254 . . . . . . . . . . . . . . . 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 )
) ) ) )
130116, 129anbi12d 692 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
131 oveq1 6080 . . . . . . . . . . . . . . . . . . 19  |-  ( e  =  ( i ` 
7 )  ->  (
e  -  1 )  =  ( ( i `
 7 )  - 
1 ) )
132131breq2d 4216 . . . . . . . . . . . . . . . . . 18  |-  ( e  =  ( i ` 
7 )  ->  (
( 2  x.  (
a `  3 )
)  ||  ( e  -  1 )  <->  ( 2  x.  ( a ` 
3 ) )  ||  ( ( i ` 
7 )  -  1 ) ) )
133 breq1 4207 . . . . . . . . . . . . . . . . . 18  |-  ( d  =  ( i ` 
6 )  ->  (
d  ||  ( (
i `  8 )  -  ( a ` 
3 ) )  <->  ( i `  6 )  ||  ( ( i ` 
8 )  -  (
a `  3 )
) ) )
134132, 133bi2anan9r 845 . . . . . . . . . . . . . . . . 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 )
) ) ) )
135134anbi1d 686 . . . . . . . . . . . . . . . 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
) ) ) ) )
1361353adant1 975 . . . . . . . . . . . . . . 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
) ) ) ) )
137130, 136anbi12d 692 . . . . . . . . . . . . . 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 ) ) ) ) ) )
138104, 105, 106, 137sbc3ie 3222 . . . . . . . . . . . . 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 ) ) ) ) )
139138sbcbii 3208 . . . . . . . . . . . 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
) ) ) ) )
140139sbcbii 3208 . . . . . . . . . . 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 ) ) ) ) )
141 vex 2951 . . . . . . . . . . . . 13  |-  i  e. 
_V
142141resex 5178 . . . . . . . . . . . 12  |-  ( i  |`  ( 1 ... 3
) )  e.  _V
143 fvex 5734 . . . . . . . . . . . 12  |-  ( i `
 4 )  e. 
_V
144 oveq1 6080 . . . . . . . . . . . . . . . . 17  |-  ( b  =  ( i ` 
4 )  ->  (
b ^ 2 )  =  ( ( i `
 4 ) ^
2 ) )
14563jm2.27dlem1 27071 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
a `  1 )  =  ( i ` 
1 ) )
146145oveq1d 6088 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( a `  1
) ^ 2 )  =  ( ( i `
 1 ) ^
2 ) )
147146oveq1d 6088 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( ( a ` 
1 ) ^ 2 )  -  1 )  =  ( ( ( i `  1 ) ^ 2 )  - 
1 ) )
14869jm2.27dlem1 27071 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
a `  3 )  =  ( i ` 
3 ) )
149148oveq1d 6088 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( a `  3
) ^ 2 )  =  ( ( i `
 3 ) ^
2 ) )
150147, 149oveq12d 6091 . . . . . . . . . . . . . . . . 17  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) )  =  ( ( ( ( i `  1
) ^ 2 )  -  1 )  x.  ( ( i ` 
3 ) ^ 2 ) ) )
151144, 150oveqan12rd 6093 . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . 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 6088 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( i `  5 ) ^ 2 ) )  =  ( ( ( ( i `  1
) ^ 2 )  -  1 )  x.  ( ( i ` 
5 ) ^ 2 ) ) )
154153oveq2d 6089 . . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . 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 1255 . . . . . . . . . . . . . 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 ) ^ 2 ) ) )  =  1  /\  ( i `
 7 )  e.  ( ZZ>= `  2 )
) ) )
158149oveq2d 6089 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
2  x.  ( ( a `  3 ) ^ 2 ) )  =  ( 2  x.  ( ( i ` 
3 ) ^ 2 ) ) )
159158oveq2d 6089 . . . . . . . . . . . . . . . . 17  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( ( i `  10 )  +  1
)  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  =  ( ( ( i `  10 )