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 29389
Description: jm2.27 29383 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 7255 . . . . . . 7  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  a : ( 1 ... 3 ) --> NN0 )
2 2nn 10500 . . . . . . . . 9  |-  2  e.  NN
32jm2.27dlem3 29386 . . . . . . . 8  |-  2  e.  ( 1 ... 2
)
4 df-3 10402 . . . . . . . 8  |-  3  =  ( 2  +  1 )
53, 4, 2jm2.27dlem2 29385 . . . . . . 7  |-  2  e.  ( 1 ... 3
)
6 ffvelrn 5862 . . . . . . 7  |-  ( ( a : ( 1 ... 3 ) --> NN0 
/\  2  e.  ( 1 ... 3 ) )  ->  ( a `  2 )  e. 
NN0 )
71, 5, 6sylancl 662 . . . . . 6  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  (
a `  2 )  e.  NN0 )
8 elnn0 10602 . . . . . 6  |-  ( ( a `  2 )  e.  NN0  <->  ( ( a `
 2 )  e.  NN  \/  ( a `
 2 )  =  0 ) )
97, 8sylib 196 . . . . 5  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  (
( a `  2
)  e.  NN  \/  ( a `  2
)  =  0 ) )
10 iba 503 . . . . . . 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 862 . . . . . . 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 261 . . . . . 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 703 . . . . 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 754 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )
16 nnz 10689 . . . . . . . . . . . . . 14  |-  ( ( a `  2 )  e.  NN  ->  (
a `  2 )  e.  ZZ )
1716adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( a ` 
2 )  e.  ZZ )
18 frmy 29281 . . . . . . . . . . . . . 14  |- Yrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> ZZ
1918fovcl 6216 . . . . . . . . . . . . 13  |-  ( ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  2 )  e.  ZZ )  ->  (
( a `  1
) Yrm  ( a `  2
) )  e.  ZZ )
2015, 17, 19syl2anc 661 . . . . . . . . . . . 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 29296 . . . . . . . . . . . . . 14  |-  ( ( a `  1 )  e.  ( ZZ>= `  2
)  ->  ( (
a `  1 ) Yrm  0 )  =  0 )
2221ad2antlr 726 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( ( a `
 1 ) Yrm  0 )  =  0 )
23 nngt0 10372 . . . . . . . . . . . . . . 15  |-  ( ( a `  2 )  e.  NN  ->  0  <  ( a `  2
) )
2423adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  0  <  (
a `  2 )
)
25 0zd 10679 . . . . . . . . . . . . . . 15  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  0  e.  ZZ )
26 ltrmy 29321 . . . . . . . . . . . . . . 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 ) ) ) )
2715, 25, 17, 26syl3anc 1218 . . . . . . . . . . . . . 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 ) ) ) )
2824, 27mpbid 210 . . . . . . . . . . . . 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 ) ) )
2922, 28eqbrtrrd 4335 . . . . . . . . . . . 12  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  0  <  (
( a `  1
) Yrm  ( a `  2
) ) )
30 elnnz 10677 . . . . . . . . . . . 12  |-  ( ( ( a `  1
) Yrm  ( a `  2
) )  e.  NN  <->  ( ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  e.  ZZ  /\  0  < 
( ( a ` 
1 ) Yrm  ( a ` 
2 ) ) ) )
3120, 29, 30sylanbrc 664 . . . . . . . . . . 11  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  ->  ( ( a `
 1 ) Yrm  ( a `
 2 ) )  e.  NN )
32 eleq1 2503 . . . . . . . . . . 11  |-  ( ( a `  3 )  =  ( ( a `
 1 ) Yrm  ( a `
 2 ) )  ->  ( ( a `
 3 )  e.  NN  <->  ( ( a `
 1 ) Yrm  ( a `
 2 ) )  e.  NN ) )
3331, 32syl5ibrcom 222 . . . . . . . . . 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 ) )
3433pm4.71rd 635 . . . . . . . . 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 ) ) ) ) )
35 simpllr 758 . . . . . . . . . . 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 ) )
36 simplr 754 . . . . . . . . . . 11  |-  ( ( ( ( a  e.  ( NN0  ^m  (
1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  /\  ( a ` 
3 )  e.  NN )  ->  ( a ` 
2 )  e.  NN )
37 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ( a  e.  ( NN0  ^m  (
1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  e.  NN )  /\  ( a ` 
3 )  e.  NN )  ->  ( a ` 
3 )  e.  NN )
38 jm2.27 29383 . . . . . . . . . . 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
) ) ) ) ) )
3935, 36, 37, 38syl3anc 1218 . . . . . . . . . 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 ) ) ) ) ) )
4039pm5.32da 641 . . . . . . . . 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 ) ) ) ) ) ) )
4134, 40bitrd 253 . . . . . . . 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 ) ) ) ) ) ) )
4241ex 434 . . . . . . 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 ) ) ) ) ) ) ) )
4342pm5.32rd 640 . . . . . 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 ) ) )
44 oveq2 6120 . . . . . . . . . . 11  |-  ( ( a `  2 )  =  0  ->  (
( a `  1
) Yrm  ( a `  2
) )  =  ( ( a `  1
) Yrm  0 ) )
4544adantl 466 . . . . . . . . . 10  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  =  0 )  ->  ( (
a `  1 ) Yrm  ( a `  2 ) )  =  ( ( a `  1 ) Yrm  0 ) )
4621ad2antlr 726 . . . . . . . . . 10  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  =  0 )  ->  ( (
a `  1 ) Yrm  0 )  =  0 )
4745, 46eqtrd 2475 . . . . . . . . 9  |-  ( ( ( a  e.  ( NN0  ^m  ( 1 ... 3 ) )  /\  ( a ` 
1 )  e.  (
ZZ>= `  2 ) )  /\  ( a ` 
2 )  =  0 )  ->  ( (
a `  1 ) Yrm  ( a `  2 ) )  =  0 )
4847eqeq2d 2454 . . . . . . . 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 ) )
4948ex 434 . . . . . . 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 ) ) )
5049pm5.32rd 640 . . . . . 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 ) ) )
5143, 50orbi12d 709 . . . . 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 ) ) ) )
5251pm5.32da 641 . . . 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 ) ) ) ) )
5314, 52bitrd 253 . . 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 ) ) ) ) )
5453rabbiia 2982 . 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 ) ) ) }
55 3nn0 10618 . . . 4  |-  3  e.  NN0
56 2z 10699 . . . 4  |-  2  e.  ZZ
57 ovex 6137 . . . . 5  |-  ( 1 ... 3 )  e. 
_V
58 1nn 10354 . . . . . . . 8  |-  1  e.  NN
5958jm2.27dlem3 29386 . . . . . . 7  |-  1  e.  ( 1 ... 1
)
60 df-2 10401 . . . . . . 7  |-  2  =  ( 1  +  1 )
6159, 60, 58jm2.27dlem2 29385 . . . . . 6  |-  1  e.  ( 1 ... 2
)
6261, 4, 2jm2.27dlem2 29385 . . . . 5  |-  1  e.  ( 1 ... 3
)
63 mzpproj 29099 . . . . 5  |-  ( ( ( 1 ... 3
)  e.  _V  /\  1  e.  ( 1 ... 3 ) )  ->  ( a  e.  ( ZZ  ^m  (
1 ... 3 ) ) 
|->  ( a `  1
) )  e.  (mzPoly `  ( 1 ... 3
) ) )
6457, 62, 63mp2an 672 . . . 4  |-  ( a  e.  ( ZZ  ^m  ( 1 ... 3
) )  |->  ( a `
 1 ) )  e.  (mzPoly `  (
1 ... 3 ) )
65 eluzrabdioph 29170 . . . 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
) )
6655, 56, 64, 65mp3an 1314 . . 3  |-  { a  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( a `  1 )  e.  ( ZZ>= `  2
) }  e.  (Dioph `  3 )
67 3nn 10501 . . . . . . . . 9  |-  3  e.  NN
6867jm2.27dlem3 29386 . . . . . . . 8  |-  3  e.  ( 1 ... 3
)
69 mzpproj 29099 . . . . . . . 8  |-  ( ( ( 1 ... 3
)  e.  _V  /\  3  e.  ( 1 ... 3 ) )  ->  ( a  e.  ( ZZ  ^m  (
1 ... 3 ) ) 
|->  ( a `  3
) )  e.  (mzPoly `  ( 1 ... 3
) ) )
7057, 68, 69mp2an 672 . . . . . . 7  |-  ( a  e.  ( ZZ  ^m  ( 1 ... 3
) )  |->  ( a `
 3 ) )  e.  (mzPoly `  (
1 ... 3 ) )
71 elnnrabdioph 29171 . . . . . . 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
) )
7255, 70, 71mp2an 672 . . . . . 6  |-  { a  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( a `  3 )  e.  NN }  e.  (Dioph `  3 )
73 fvex 5722 . . . . . . . . . . . . . . . . 17  |-  ( i `
 8 )  e. 
_V
74 fvex 5722 . . . . . . . . . . . . . . . . 17  |-  ( i `
 9 )  e. 
_V
75 fvex 5722 . . . . . . . . . . . . . . . . 17  |-  ( i `
 10 )  e. 
_V
76 oveq1 6119 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  =  ( i ` 
9 )  ->  (
g ^ 2 )  =  ( ( i `
 9 ) ^
2 ) )
77 oveq1 6119 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  ( i ` 
8 )  ->  (
f ^ 2 )  =  ( ( i `
 8 ) ^
2 ) )
7877oveq2d 6128 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  =  ( i ` 
8 )  ->  (
( ( e ^
2 )  -  1 )  x.  ( f ^ 2 ) )  =  ( ( ( e ^ 2 )  -  1 )  x.  ( ( i ` 
8 ) ^ 2 ) ) )
7976, 78oveqan12rd 6132 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
8079eqeq1d 2451 . . . . . . . . . . . . . . . . . . . . 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 ) )
81803adant3 1008 . . . . . . . . . . . . . . . . . . . 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 ) )
82 oveq1 6119 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h  =  ( i `  10 )  ->  ( h  +  1 )  =  ( ( i `  10 )  +  1
) )
8382oveq1d 6127 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h  =  ( i `  10 )  ->  ( ( h  +  1 )  x.  ( 2  x.  ( ( a ` 
3 ) ^ 2 ) ) )  =  ( ( ( i `
 10 )  +  1 )  x.  (
2  x.  ( ( a `  3 ) ^ 2 ) ) ) )
8483eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  ( i `  10 )  ->  ( c  =  ( ( h  +  1 )  x.  ( 2  x.  (
( a `  3
) ^ 2 ) ) )  <->  c  =  ( ( ( i `
 10 )  +  1 )  x.  (
2  x.  ( ( a `  3 ) ^ 2 ) ) ) ) )
85843ad2ant3 1011 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
8681, 853anbi12d 1290 . . . . . . . . . . . . . . . . . . 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 )
) ) ) )
8786anbi2d 703 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
88 oveq1 6119 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  ( i ` 
8 )  ->  (
f  -  ( a `
 3 ) )  =  ( ( i `
 8 )  -  ( a `  3
) ) )
8988breq2d 4325 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( i ` 
8 )  ->  (
d  ||  ( f  -  ( a ` 
3 ) )  <->  d  ||  ( ( i ` 
8 )  -  (
a `  3 )
) ) )
9089anbi2d 703 . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )
91 oveq1 6119 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  ( i ` 
8 )  ->  (
f  -  ( a `
 2 ) )  =  ( ( i `
 8 )  -  ( a `  2
) ) )
9291breq2d 4325 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( i ` 
8 )  ->  (
( 2  x.  (
a `  3 )
)  ||  ( f  -  ( a ` 
2 ) )  <->  ( 2  x.  ( a ` 
3 ) )  ||  ( ( i ` 
8 )  -  (
a `  2 )
) ) )
9392anbi1d 704 . . . . . . . . . . . . . . . . . . . 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
) ) ) )
9490, 93anbi12d 710 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
95943ad2ant1 1009 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
9687, 95anbi12d 710 . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
9773, 74, 75, 96sbc3ie 3285 . . . . . . . . . . . . . . . 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 ) ) ) ) )
9897sbcbii 3267 . . . . . . . . . . . . . . 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
) ) ) ) )
9998sbcbii 3267 . . . . . . . . . . . . . 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
) ) ) ) )
10099sbcbii 3267 . . . . . . . . . . . . 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
) ) ) ) )
101100sbcbii 3267 . . . . . . . . . . . 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
) ) ) ) )
102101sbcbii 3267 . . . . . . . . . . 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 ) ) ) ) )
103 fvex 5722 . . . . . . . . . . . . . 14  |-  ( i `
 5 )  e. 
_V
104 fvex 5722 . . . . . . . . . . . . . 14  |-  ( i `
 6 )  e. 
_V
105 fvex 5722 . . . . . . . . . . . . . 14  |-  ( i `
 7 )  e. 
_V
106 oveq1 6119 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  =  ( i ` 
6 )  ->  (
d ^ 2 )  =  ( ( i `
 6 ) ^
2 ) )
1071063ad2ant2 1010 . . . . . . . . . . . . . . . . . . 19  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( d ^
2 )  =  ( ( i `  6
) ^ 2 ) )
108 oveq1 6119 . . . . . . . . . . . . . . . . . . . . 21  |-  ( c  =  ( i ` 
5 )  ->  (
c ^ 2 )  =  ( ( i `
 5 ) ^
2 ) )
109108oveq2d 6128 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  =  ( i ` 
5 )  ->  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( c ^ 2 ) )  =  ( ( ( ( a `  1
) ^ 2 )  -  1 )  x.  ( ( i ` 
5 ) ^ 2 ) ) )
1101093ad2ant1 1009 . . . . . . . . . . . . . . . . . . 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 ) ) )
111107, 110oveq12d 6130 . . . . . . . . . . . . . . . . . 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 ) ) ) )
112111eqeq1d 2451 . . . . . . . . . . . . . . . . 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 ) )
113 eleq1 2503 . . . . . . . . . . . . . . . . . 18  |-  ( e  =  ( i ` 
7 )  ->  (
e  e.  ( ZZ>= ` 
2 )  <->  ( i `  7 )  e.  ( ZZ>= `  2 )
) )
1141133ad2ant3 1011 . . . . . . . . . . . . . . . . 17  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( e  e.  ( ZZ>= `  2 )  <->  ( i `  7 )  e.  ( ZZ>= `  2
) ) )
115112, 1143anbi23d 1292 . . . . . . . . . . . . . . . 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 )
) ) )
116 oveq1 6119 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( e  =  ( i ` 
7 )  ->  (
e ^ 2 )  =  ( ( i `
 7 ) ^
2 ) )
117116oveq1d 6127 . . . . . . . . . . . . . . . . . . . . 21  |-  ( e  =  ( i ` 
7 )  ->  (
( e ^ 2 )  -  1 )  =  ( ( ( i `  7 ) ^ 2 )  - 
1 ) )
118117oveq1d 6127 . . . . . . . . . . . . . . . . . . . 20  |-  ( e  =  ( i ` 
7 )  ->  (
( ( e ^
2 )  -  1 )  x.  ( ( i `  8 ) ^ 2 ) )  =  ( ( ( ( i `  7
) ^ 2 )  -  1 )  x.  ( ( i ` 
8 ) ^ 2 ) ) )
119118oveq2d 6128 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
120119eqeq1d 2451 . . . . . . . . . . . . . . . . . 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 ) )
1211203ad2ant3 1011 . . . . . . . . . . . . . . . . 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 ) )
122 eqeq1 2449 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
1231223ad2ant1 1009 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
124 simp2 989 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  d  =  ( i `  6 ) )
125 oveq1 6119 . . . . . . . . . . . . . . . . . . 19  |-  ( e  =  ( i ` 
7 )  ->  (
e  -  ( a `
 1 ) )  =  ( ( i `
 7 )  -  ( a `  1
) ) )
1261253ad2ant3 1011 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( e  -  ( a `  1
) )  =  ( ( i `  7
)  -  ( a `
 1 ) ) )
127124, 126breq12d 4326 . . . . . . . . . . . . . . . . 17  |-  ( ( c  =  ( i `
 5 )  /\  d  =  ( i `  6 )  /\  e  =  ( i `  7 ) )  ->  ( d  ||  ( e  -  (
a `  1 )
)  <->  ( i ` 
6 )  ||  (
( i `  7
)  -  ( a `
 1 ) ) ) )
128121, 123, 1273anbi123d 1289 . . . . . . . . . . . . . . . 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 )
) ) ) )
129115, 128anbi12d 710 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
130 oveq1 6119 . . . . . . . . . . . . . . . . . . 19  |-  ( e  =  ( i ` 
7 )  ->  (
e  -  1 )  =  ( ( i `
 7 )  - 
1 ) )
131130breq2d 4325 . . . . . . . . . . . . . . . . . 18  |-  ( e  =  ( i ` 
7 )  ->  (
( 2  x.  (
a `  3 )
)  ||  ( e  -  1 )  <->  ( 2  x.  ( a ` 
3 ) )  ||  ( ( i ` 
7 )  -  1 ) ) )
132 breq1 4316 . . . . . . . . . . . . . . . . . 18  |-  ( d  =  ( i ` 
6 )  ->  (
d  ||  ( (
i `  8 )  -  ( a ` 
3 ) )  <->  ( i `  6 )  ||  ( ( i ` 
8 )  -  (
a `  3 )
) ) )
133131, 132bi2anan9r 869 . . . . . . . . . . . . . . . . 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 )
) ) ) )
134133anbi1d 704 . . . . . . . . . . . . . . . 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
) ) ) ) )
1351343adant1 1006 . . . . . . . . . . . . . . 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
) ) ) ) )
136129, 135anbi12d 710 . . . . . . . . . . . . . 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 ) ) ) ) ) )
137103, 104, 105, 136sbc3ie 3285 . . . . . . . . . . . . 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 ) ) ) ) )
138137sbcbii 3267 . . . . . . . . . . . 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
) ) ) ) )
139138sbcbii 3267 . . . . . . . . . . 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 ) ) ) ) )
140 vex 2996 . . . . . . . . . . . . 13  |-  i  e. 
_V
141140resex 5171 . . . . . . . . . . . 12  |-  ( i  |`  ( 1 ... 3
) )  e.  _V
142 fvex 5722 . . . . . . . . . . . 12  |-  ( i `
 4 )  e. 
_V
143 oveq1 6119 . . . . . . . . . . . . . . . . 17  |-  ( b  =  ( i ` 
4 )  ->  (
b ^ 2 )  =  ( ( i `
 4 ) ^
2 ) )
14462jm2.27dlem1 29384 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
a `  1 )  =  ( i ` 
1 ) )
145144oveq1d 6127 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( a `  1
) ^ 2 )  =  ( ( i `
 1 ) ^
2 ) )
146145oveq1d 6127 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( ( a ` 
1 ) ^ 2 )  -  1 )  =  ( ( ( i `  1 ) ^ 2 )  - 
1 ) )
14768jm2.27dlem1 29384 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
a `  3 )  =  ( i ` 
3 ) )
148147oveq1d 6127 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( a `  3
) ^ 2 )  =  ( ( i `
 3 ) ^
2 ) )
149146, 148oveq12d 6130 . . . . . . . . . . . . . . . . 17  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( a `  3 ) ^ 2 ) )  =  ( ( ( ( i `  1
) ^ 2 )  -  1 )  x.  ( ( i ` 
3 ) ^ 2 ) ) )
150143, 149oveqan12rd 6132 . . . . . . . . . . . . . . . 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 ) ) ) )
151150eqeq1d 2451 . . . . . . . . . . . . . . 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 ) )
152146oveq1d 6127 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( ( ( a `
 1 ) ^
2 )  -  1 )  x.  ( ( i `  5 ) ^ 2 ) )  =  ( ( ( ( i `  1
) ^ 2 )  -  1 )  x.  ( ( i ` 
5 ) ^ 2 ) ) )
153152oveq2d 6128 . . . . . . . . . . . . . . . . 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 ) ) ) )
154153eqeq1d 2451 . . . . . . . . . . . . . . . 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 ) )
155154adantr 465 . . . . . . . . . . . . . . 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 ) )
156151, 1553anbi12d 1290 . . . . . . . . . . . . . 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 )
) ) )
157148oveq2d 6128 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
2  x.  ( ( a `  3 ) ^ 2 ) )  =  ( 2  x.  ( ( i ` 
3 ) ^ 2 ) ) )
158157oveq2d 6128 . . . . . . . . . . . . . . . . 17  |-  ( a  =  ( i  |`  ( 1 ... 3
) )  ->  (
( ( i `  10 )  +  1
)  x.  ( 2  x.  ( ( a `
 3 ) ^
2 ) ) )  =  ( ( ( i `  10 )  +  1 )  x.  ( 2  x.  (
(