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

Theorem expdiophlem2 27115
Description: Lemma for expdioph 27116. Exponentiation on a restricted domain is Diophantine. (Contributed by Stefan O'Rear, 17-Oct-2014.)
Assertion
Ref Expression
expdiophlem2  |-  { a  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( ( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  /\  ( a ` 
3 )  =  ( ( a `  1
) ^ ( a `
 2 ) ) ) }  e.  (Dioph `  3 )

Proof of Theorem expdiophlem2
Dummy variables  b 
c  d  e are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elmapi 6792 . . . . 5  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  a : ( 1 ... 3 ) --> NN0 )
2 3nn 9878 . . . . . 6  |-  3  e.  NN
32jm2.27dlem3 27104 . . . . 5  |-  3  e.  ( 1 ... 3
)
4 ffvelrn 5663 . . . . 5  |-  ( ( a : ( 1 ... 3 ) --> NN0 
/\  3  e.  ( 1 ... 3 ) )  ->  ( a `  3 )  e. 
NN0 )
51, 3, 4sylancl 643 . . . 4  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  (
a `  3 )  e.  NN0 )
6 expdiophlem1 27114 . . . 4  |-  ( ( a `  3 )  e.  NN0  ->  ( ( ( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  /\  ( a ` 
3 )  =  ( ( a `  1
) ^ ( a `
 2 ) ) )  <->  E. b  e.  NN0  E. c  e.  NN0  E. d  e.  NN0  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  ( a `  2 )  e.  NN )  /\  (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  b  =  ( (
a `  1 ) Yrm  ( ( a `  2
)  +  1 ) ) )  /\  (
( b  e.  (
ZZ>= `  2 )  /\  c  =  ( b Yrm  ( a `  2 ) ) )  /\  (
( b  e.  (
ZZ>= `  2 )  /\  d  =  ( b Xrm  ( a `  2 ) ) )  /\  (
( a `  3
)  <  ( (
( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  ||  ( ( d  -  ( ( b  -  ( a `
 1 ) )  x.  c ) )  -  ( a ` 
3 ) ) ) ) ) ) ) ) )
75, 6syl 15 . . 3  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  (
( ( ( a `
 1 )  e.  ( ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  /\  ( a ` 
3 )  =  ( ( a `  1
) ^ ( a `
 2 ) ) )  <->  E. b  e.  NN0  E. c  e.  NN0  E. d  e.  NN0  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  ( a `  2 )  e.  NN )  /\  (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  b  =  ( (
a `  1 ) Yrm  ( ( a `  2
)  +  1 ) ) )  /\  (
( b  e.  (
ZZ>= `  2 )  /\  c  =  ( b Yrm  ( a `  2 ) ) )  /\  (
( b  e.  (
ZZ>= `  2 )  /\  d  =  ( b Xrm  ( a `  2 ) ) )  /\  (
( a `  3
)  <  ( (
( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  ||  ( ( d  -  ( ( b  -  ( a `
 1 ) )  x.  c ) )  -  ( a ` 
3 ) ) ) ) ) ) ) ) )
87rabbiia 2778 . 2  |-  { a  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( ( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  /\  ( a ` 
3 )  =  ( ( a `  1
) ^ ( a `
 2 ) ) ) }  =  {
a  e.  ( NN0 
^m  ( 1 ... 3 ) )  |  E. b  e.  NN0  E. c  e.  NN0  E. d  e.  NN0  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  ( a `  2 )  e.  NN )  /\  (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  b  =  ( (
a `  1 ) Yrm  ( ( a `  2
)  +  1 ) ) )  /\  (
( b  e.  (
ZZ>= `  2 )  /\  c  =  ( b Yrm  ( a `  2 ) ) )  /\  (
( b  e.  (
ZZ>= `  2 )  /\  d  =  ( b Xrm  ( a `  2 ) ) )  /\  (
( a `  3
)  <  ( (
( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  ||  ( ( d  -  ( ( b  -  ( a `
 1 ) )  x.  c ) )  -  ( a ` 
3 ) ) ) ) ) ) ) }
9 3nn0 9983 . . 3  |-  3  e.  NN0
10 vex 2791 . . . . . . . . 9  |-  e  e. 
_V
1110resex 4995 . . . . . . . 8  |-  ( e  |`  ( 1 ... 3
) )  e.  _V
12 fvex 5539 . . . . . . . . 9  |-  ( e `
 4 )  e. 
_V
13 fvex 5539 . . . . . . . . . 10  |-  ( e `
 5 )  e. 
_V
14 fvex 5539 . . . . . . . . . 10  |-  ( e `
 6 )  e. 
_V
15 eqeq1 2289 . . . . . . . . . . . . . . 15  |-  ( c  =  ( e ` 
5 )  ->  (
c  =  ( b Yrm  ( a `  2 ) )  <->  ( e ` 
5 )  =  ( b Yrm  ( a `  2
) ) ) )
1615anbi2d 684 . . . . . . . . . . . . . 14  |-  ( c  =  ( e ` 
5 )  ->  (
( b  e.  (
ZZ>= `  2 )  /\  c  =  ( b Yrm  ( a `  2 ) ) )  <->  ( b  e.  ( ZZ>= `  2 )  /\  ( e `  5
)  =  ( b Yrm  ( a `  2 ) ) ) ) )
1716adantr 451 . . . . . . . . . . . . 13  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  ( ( b  e.  ( ZZ>= `  2
)  /\  c  =  ( b Yrm  ( a ` 
2 ) ) )  <-> 
( b  e.  (
ZZ>= `  2 )  /\  ( e `  5
)  =  ( b Yrm  ( a `  2 ) ) ) ) )
18 eqeq1 2289 . . . . . . . . . . . . . . . 16  |-  ( d  =  ( e ` 
6 )  ->  (
d  =  ( b Xrm  ( a `  2 ) )  <->  ( e ` 
6 )  =  ( b Xrm  ( a `  2
) ) ) )
1918anbi2d 684 . . . . . . . . . . . . . . 15  |-  ( d  =  ( e ` 
6 )  ->  (
( b  e.  (
ZZ>= `  2 )  /\  d  =  ( b Xrm  ( a `  2 ) ) )  <->  ( b  e.  ( ZZ>= `  2 )  /\  ( e `  6
)  =  ( b Xrm  ( a `  2 ) ) ) ) )
2019adantl 452 . . . . . . . . . . . . . 14  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  ( ( b  e.  ( ZZ>= `  2
)  /\  d  =  ( b Xrm  ( a ` 
2 ) ) )  <-> 
( b  e.  (
ZZ>= `  2 )  /\  ( e `  6
)  =  ( b Xrm  ( a `  2 ) ) ) ) )
21 simpr 447 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  d  =  ( e `  6 ) )
22 oveq2 5866 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  ( e ` 
5 )  ->  (
( b  -  (
a `  1 )
)  x.  c )  =  ( ( b  -  ( a ` 
1 ) )  x.  ( e `  5
) ) )
2322adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  ( ( b  -  ( a ` 
1 ) )  x.  c )  =  ( ( b  -  (
a `  1 )
)  x.  ( e `
 5 ) ) )
2421, 23oveq12d 5876 . . . . . . . . . . . . . . . . 17  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  ( d  -  ( ( b  -  ( a `  1
) )  x.  c
) )  =  ( ( e `  6
)  -  ( ( b  -  ( a `
 1 ) )  x.  ( e ` 
5 ) ) ) )
2524oveq1d 5873 . . . . . . . . . . . . . . . 16  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  ( ( d  -  ( ( b  -  ( a ` 
1 ) )  x.  c ) )  -  ( a `  3
) )  =  ( ( ( e ` 
6 )  -  (
( b  -  (
a `  1 )
)  x.  ( e `
 5 ) ) )  -  ( a `
 3 ) ) )
2625breq2d 4035 . . . . . . . . . . . . . . 15  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  ( ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( d  -  ( ( b  -  ( a `  1
) )  x.  c
) )  -  (
a `  3 )
)  <->  ( ( ( ( 2  x.  b
)  x.  ( a `
 1 ) )  -  ( ( a `
 1 ) ^
2 ) )  - 
1 )  ||  (
( ( e ` 
6 )  -  (
( b  -  (
a `  1 )
)  x.  ( e `
 5 ) ) )  -  ( a `
 3 ) ) ) )
2726anbi2d 684 . . . . . . . . . . . . . 14  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  ( ( ( a `  3 )  <  ( ( ( ( 2  x.  b
)  x.  ( a `
 1 ) )  -  ( ( a `
 1 ) ^
2 ) )  - 
1 )  /\  (
( ( ( 2  x.  b )  x.  ( a `  1
) )  -  (
( a `  1
) ^ 2 ) )  -  1 ) 
||  ( ( d  -  ( ( b  -  ( a ` 
1 ) )  x.  c ) )  -  ( a `  3
) ) )  <->  ( (
a `  3 )  <  ( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `
 6 )  -  ( ( b  -  ( a `  1
) )  x.  (
e `  5 )
) )  -  (
a `  3 )
) ) ) )
2820, 27anbi12d 691 . . . . . . . . . . . . 13  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  ( ( ( b  e.  ( ZZ>= ` 
2 )  /\  d  =  ( b Xrm  ( a `
 2 ) ) )  /\  ( ( a `  3 )  <  ( ( ( ( 2  x.  b
)  x.  ( a `
 1 ) )  -  ( ( a `
 1 ) ^
2 ) )  - 
1 )  /\  (
( ( ( 2  x.  b )  x.  ( a `  1
) )  -  (
( a `  1
) ^ 2 ) )  -  1 ) 
||  ( ( d  -  ( ( b  -  ( a ` 
1 ) )  x.  c ) )  -  ( a `  3
) ) ) )  <-> 
( ( b  e.  ( ZZ>= `  2 )  /\  ( e `  6
)  =  ( b Xrm  ( a `  2 ) ) )  /\  (
( a `  3
)  <  ( (
( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `  6
)  -  ( ( b  -  ( a `
 1 ) )  x.  ( e ` 
5 ) ) )  -  ( a ` 
3 ) ) ) ) ) )
2917, 28anbi12d 691 . . . . . . . . . . . 12  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  ( ( ( b  e.  ( ZZ>= ` 
2 )  /\  c  =  ( b Yrm  ( a `
 2 ) ) )  /\  ( ( b  e.  ( ZZ>= ` 
2 )  /\  d  =  ( b Xrm  ( a `
 2 ) ) )  /\  ( ( a `  3 )  <  ( ( ( ( 2  x.  b
)  x.  ( a `
 1 ) )  -  ( ( a `
 1 ) ^
2 ) )  - 
1 )  /\  (
( ( ( 2  x.  b )  x.  ( a `  1
) )  -  (
( a `  1
) ^ 2 ) )  -  1 ) 
||  ( ( d  -  ( ( b  -  ( a ` 
1 ) )  x.  c ) )  -  ( a `  3
) ) ) ) )  <->  ( ( b  e.  ( ZZ>= `  2
)  /\  ( e `  5 )  =  ( b Yrm  ( a ` 
2 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  ( e `  6 )  =  ( b Xrm  ( a ` 
2 ) ) )  /\  ( ( a `
 3 )  < 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `
 6 )  -  ( ( b  -  ( a `  1
) )  x.  (
e `  5 )
) )  -  (
a `  3 )
) ) ) ) ) )
3029anbi2d 684 . . . . . . . . . . 11  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  ( ( ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  b  =  ( ( a `
 1 ) Yrm  ( ( a `  2 )  +  1 ) ) )  /\  ( ( b  e.  ( ZZ>= ` 
2 )  /\  c  =  ( b Yrm  ( a `
 2 ) ) )  /\  ( ( b  e.  ( ZZ>= ` 
2 )  /\  d  =  ( b Xrm  ( a `
 2 ) ) )  /\  ( ( a `  3 )  <  ( ( ( ( 2  x.  b
)  x.  ( a `
 1 ) )  -  ( ( a `
 1 ) ^
2 ) )  - 
1 )  /\  (
( ( ( 2  x.  b )  x.  ( a `  1
) )  -  (
( a `  1
) ^ 2 ) )  -  1 ) 
||  ( ( d  -  ( ( b  -  ( a ` 
1 ) )  x.  c ) )  -  ( a `  3
) ) ) ) ) )  <->  ( (
( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  b  =  ( ( a `
 1 ) Yrm  ( ( a `  2 )  +  1 ) ) )  /\  ( ( b  e.  ( ZZ>= ` 
2 )  /\  (
e `  5 )  =  ( b Yrm  ( a `
 2 ) ) )  /\  ( ( b  e.  ( ZZ>= ` 
2 )  /\  (
e `  6 )  =  ( b Xrm  ( a `
 2 ) ) )  /\  ( ( a `  3 )  <  ( ( ( ( 2  x.  b
)  x.  ( a `
 1 ) )  -  ( ( a `
 1 ) ^
2 ) )  - 
1 )  /\  (
( ( ( 2  x.  b )  x.  ( a `  1
) )  -  (
( a `  1
) ^ 2 ) )  -  1 ) 
||  ( ( ( e `  6 )  -  ( ( b  -  ( a ` 
1 ) )  x.  ( e `  5
) ) )  -  ( a `  3
) ) ) ) ) ) ) )
3130anbi2d 684 . . . . . . . . . 10  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  ( ( ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  2 )  e.  NN )  /\  (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  b  =  ( (
a `  1 ) Yrm  ( ( a `  2
)  +  1 ) ) )  /\  (
( b  e.  (
ZZ>= `  2 )  /\  c  =  ( b Yrm  ( a `  2 ) ) )  /\  (
( b  e.  (
ZZ>= `  2 )  /\  d  =  ( b Xrm  ( a `  2 ) ) )  /\  (
( a `  3
)  <  ( (
( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  ||  ( ( d  -  ( ( b  -  ( a `
 1 ) )  x.  c ) )  -  ( a ` 
3 ) ) ) ) ) ) )  <-> 
( ( ( a `
 1 )  e.  ( ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  /\  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  b  =  ( ( a ` 
1 ) Yrm  ( ( a `
 2 )  +  1 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  ( e `  5 )  =  ( b Yrm  ( a ` 
2 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  ( e `  6 )  =  ( b Xrm  ( a ` 
2 ) ) )  /\  ( ( a `
 3 )  < 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `
 6 )  -  ( ( b  -  ( a `  1
) )  x.  (
e `  5 )
) )  -  (
a `  3 )
) ) ) ) ) ) ) )
3213, 14, 31sbc2ie 3058 . . . . . . . . 9  |-  ( [. ( e `  5
)  /  c ]. [. ( e `  6
)  /  d ]. ( ( ( a `
 1 )  e.  ( ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  /\  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  b  =  ( ( a ` 
1 ) Yrm  ( ( a `
 2 )  +  1 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  c  =  ( b Yrm  ( a ` 
2 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  d  =  ( b Xrm  ( a ` 
2 ) ) )  /\  ( ( a `
 3 )  < 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( d  -  ( ( b  -  ( a `  1
) )  x.  c
) )  -  (
a `  3 )
) ) ) ) ) )  <->  ( (
( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  2 )  e.  NN )  /\  (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  b  =  ( (
a `  1 ) Yrm  ( ( a `  2
)  +  1 ) ) )  /\  (
( b  e.  (
ZZ>= `  2 )  /\  ( e `  5
)  =  ( b Yrm  ( a `  2 ) ) )  /\  (
( b  e.  (
ZZ>= `  2 )  /\  ( e `  6
)  =  ( b Xrm  ( a `  2 ) ) )  /\  (
( a `  3
)  <  ( (
( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `  6
)  -  ( ( b  -  ( a `
 1 ) )  x.  ( e ` 
5 ) ) )  -  ( a ` 
3 ) ) ) ) ) ) ) )
3312, 32sbcbiiiOLD 26867 . . . . . . . 8  |-  ( [. ( e `  4
)  /  b ]. [. ( e `  5
)  /  c ]. [. ( e `  6
)  /  d ]. ( ( ( a `
 1 )  e.  ( ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  /\  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  b  =  ( ( a ` 
1 ) Yrm  ( ( a `
 2 )  +  1 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  c  =  ( b Yrm  ( a ` 
2 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  d  =  ( b Xrm  ( a ` 
2 ) ) )  /\  ( ( a `
 3 )  < 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( d  -  ( ( b  -  ( a `  1
) )  x.  c
) )  -  (
a `  3 )
) ) ) ) ) )  <->  [. ( e `
 4 )  / 
b ]. ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  ( a `  2 )  e.  NN )  /\  (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  b  =  ( (
a `  1 ) Yrm  ( ( a `  2
)  +  1 ) ) )  /\  (
( b  e.  (
ZZ>= `  2 )  /\  ( e `  5
)  =  ( b Yrm  ( a `  2 ) ) )  /\  (
( b  e.  (
ZZ>= `  2 )  /\  ( e `  6
)  =  ( b Xrm  ( a `  2 ) ) )  /\  (
( a `  3
)  <  ( (
( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `  6
)  -  ( ( b  -  ( a `
 1 ) )  x.  ( e ` 
5 ) ) )  -  ( a ` 
3 ) ) ) ) ) ) ) )
3411, 33sbcbiiiOLD 26867 . . . . . . 7  |-  ( [. ( e  |`  (
1 ... 3 ) )  /  a ]. [. (
e `  4 )  /  b ]. [. (
e `  5 )  /  c ]. [. (
e `  6 )  /  d ]. (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  /\  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  b  =  ( ( a ` 
1 ) Yrm  ( ( a `
 2 )  +  1 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  c  =  ( b Yrm  ( a ` 
2 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  d  =  ( b Xrm  ( a ` 
2 ) ) )  /\  ( ( a `
 3 )  < 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( d  -  ( ( b  -  ( a `  1
) )  x.  c
) )  -  (
a `  3 )
) ) ) ) ) )  <->  [. ( e  |`  ( 1 ... 3
) )  /  a ]. [. ( e ` 
4 )  /  b ]. ( ( ( a `
 1 )  e.  ( ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  /\  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  b  =  ( ( a ` 
1 ) Yrm  ( ( a `
 2 )  +  1 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  ( e `  5 )  =  ( b Yrm  ( a ` 
2 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  ( e `  6 )  =  ( b Xrm  ( a ` 
2 ) ) )  /\  ( ( a `
 3 )  < 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `
 6 )  -  ( ( b  -  ( a `  1
) )  x.  (
e `  5 )
) )  -  (
a `  3 )
) ) ) ) ) ) )
35 df-2 9804 . . . . . . . . . . . . . . 15  |-  2  =  ( 1  +  1 )
36 df-3 9805 . . . . . . . . . . . . . . . 16  |-  3  =  ( 2  +  1 )
37 ssid 3197 . . . . . . . . . . . . . . . 16  |-  ( 1 ... 3 )  C_  ( 1 ... 3
)
3836, 37jm2.27dlem5 27106 . . . . . . . . . . . . . . 15  |-  ( 1 ... 2 )  C_  ( 1 ... 3
)
3935, 38jm2.27dlem5 27106 . . . . . . . . . . . . . 14  |-  ( 1 ... 1 )  C_  ( 1 ... 3
)
40 1nn 9757 . . . . . . . . . . . . . . 15  |-  1  e.  NN
4140jm2.27dlem3 27104 . . . . . . . . . . . . . 14  |-  1  e.  ( 1 ... 1
)
4239, 41sselii 3177 . . . . . . . . . . . . 13  |-  1  e.  ( 1 ... 3
)
4342jm2.27dlem1 27102 . . . . . . . . . . . 12  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
a `  1 )  =  ( e ` 
1 ) )
4443eleq1d 2349 . . . . . . . . . . 11  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
( a `  1
)  e.  ( ZZ>= ` 
2 )  <->  ( e `  1 )  e.  ( ZZ>= `  2 )
) )
45 2nn 9877 . . . . . . . . . . . . . . 15  |-  2  e.  NN
4645jm2.27dlem3 27104 . . . . . . . . . . . . . 14  |-  2  e.  ( 1 ... 2
)
4746, 36, 45jm2.27dlem2 27103 . . . . . . . . . . . . 13  |-  2  e.  ( 1 ... 3
)
4847jm2.27dlem1 27102 . . . . . . . . . . . 12  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
a `  2 )  =  ( e ` 
2 ) )
4948eleq1d 2349 . . . . . . . . . . 11  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
( a `  2
)  e.  NN  <->  ( e `  2 )  e.  NN ) )
5044, 49anbi12d 691 . . . . . . . . . 10  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  <-> 
( ( e ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( e `  2
)  e.  NN ) ) )
5150adantr 451 . . . . . . . . 9  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( ( a `
 1 )  e.  ( ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  <-> 
( ( e ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( e `  2
)  e.  NN ) ) )
5244adantr 451 . . . . . . . . . . 11  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  <->  ( e `  1 )  e.  ( ZZ>= `  2 )
) )
53 id 19 . . . . . . . . . . . 12  |-  ( b  =  ( e ` 
4 )  ->  b  =  ( e ` 
4 ) )
5448oveq1d 5873 . . . . . . . . . . . . 13  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
( a `  2
)  +  1 )  =  ( ( e `
 2 )  +  1 ) )
5543, 54oveq12d 5876 . . . . . . . . . . . 12  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
( a `  1
) Yrm  ( ( a ` 
2 )  +  1 ) )  =  ( ( e `  1
) Yrm  ( ( e ` 
2 )  +  1 ) ) )
5653, 55eqeqan12rd 2299 . . . . . . . . . . 11  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( b  =  ( ( a `  1
) Yrm  ( ( a ` 
2 )  +  1 ) )  <->  ( e `  4 )  =  ( ( e ` 
1 ) Yrm  ( ( e `
 2 )  +  1 ) ) ) )
5752, 56anbi12d 691 . . . . . . . . . 10  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( ( a `
 1 )  e.  ( ZZ>= `  2 )  /\  b  =  (
( a `  1
) Yrm  ( ( a ` 
2 )  +  1 ) ) )  <->  ( (
e `  1 )  e.  ( ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  ( ( e `  2
)  +  1 ) ) ) ) )
58 eleq1 2343 . . . . . . . . . . . . 13  |-  ( b  =  ( e ` 
4 )  ->  (
b  e.  ( ZZ>= ` 
2 )  <->  ( e `  4 )  e.  ( ZZ>= `  2 )
) )
5958adantl 452 . . . . . . . . . . . 12  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( b  e.  (
ZZ>= `  2 )  <->  ( e `  4 )  e.  ( ZZ>= `  2 )
) )
6053, 48oveqan12rd 5878 . . . . . . . . . . . . 13  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( b Yrm  ( a ` 
2 ) )  =  ( ( e ` 
4 ) Yrm  ( e ` 
2 ) ) )
6160eqeq2d 2294 . . . . . . . . . . . 12  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( e ` 
5 )  =  ( b Yrm  ( a `  2
) )  <->  ( e `  5 )  =  ( ( e ` 
4 ) Yrm  ( e ` 
2 ) ) ) )
6259, 61anbi12d 691 . . . . . . . . . . 11  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( b  e.  ( ZZ>= `  2 )  /\  ( e `  5
)  =  ( b Yrm  ( a `  2 ) ) )  <->  ( (
e `  4 )  e.  ( ZZ>= `  2 )  /\  ( e `  5
)  =  ( ( e `  4 ) Yrm  ( e `  2 ) ) ) ) )
6353, 48oveqan12rd 5878 . . . . . . . . . . . . . 14  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( b Xrm  ( a ` 
2 ) )  =  ( ( e ` 
4 ) Xrm  ( e ` 
2 ) ) )
6463eqeq2d 2294 . . . . . . . . . . . . 13  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( e ` 
6 )  =  ( b Xrm  ( a `  2
) )  <->  ( e `  6 )  =  ( ( e ` 
4 ) Xrm  ( e ` 
2 ) ) ) )
6559, 64anbi12d 691 . . . . . . . . . . . 12  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( b  e.  ( ZZ>= `  2 )  /\  ( e `  6
)  =  ( b Xrm  ( a `  2 ) ) )  <->  ( (
e `  4 )  e.  ( ZZ>= `  2 )  /\  ( e `  6
)  =  ( ( e `  4 ) Xrm  ( e `  2 ) ) ) ) )
663jm2.27dlem1 27102 . . . . . . . . . . . . . . 15  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
a `  3 )  =  ( e ` 
3 ) )
6766adantr 451 . . . . . . . . . . . . . 14  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( a `  3
)  =  ( e `
 3 ) )
68 oveq2 5866 . . . . . . . . . . . . . . . . 17  |-  ( b  =  ( e ` 
4 )  ->  (
2  x.  b )  =  ( 2  x.  ( e `  4
) ) )
6968, 43oveqan12rd 5878 . . . . . . . . . . . . . . . 16  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( 2  x.  b )  x.  (
a `  1 )
)  =  ( ( 2  x.  ( e `
 4 ) )  x.  ( e ` 
1 ) ) )
7043oveq1d 5873 . . . . . . . . . . . . . . . . 17  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
( a `  1
) ^ 2 )  =  ( ( e `
 1 ) ^
2 ) )
7170adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( a ` 
1 ) ^ 2 )  =  ( ( e `  1 ) ^ 2 ) )
7269, 71oveq12d 5876 . . . . . . . . . . . . . . 15  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( ( 2  x.  b )  x.  ( a `  1
) )  -  (
( a `  1
) ^ 2 ) )  =  ( ( ( 2  x.  (
e `  4 )
)  x.  ( e `
 1 ) )  -  ( ( e `
 1 ) ^
2 ) ) )
7372oveq1d 5873 . . . . . . . . . . . . . 14  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  =  ( ( ( ( 2  x.  ( e `  4
) )  x.  (
e `  1 )
)  -  ( ( e `  1 ) ^ 2 ) )  -  1 ) )
7467, 73breq12d 4036 . . . . . . . . . . . . 13  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( a ` 
3 )  <  (
( ( ( 2  x.  b )  x.  ( a `  1
) )  -  (
( a `  1
) ^ 2 ) )  -  1 )  <-> 
( e `  3
)  <  ( (
( ( 2  x.  ( e `  4
) )  x.  (
e `  1 )
)  -  ( ( e `  1 ) ^ 2 ) )  -  1 ) ) )
75 simpr 447 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
b  =  ( e `
 4 ) )
7643adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( a `  1
)  =  ( e `
 1 ) )
7775, 76oveq12d 5876 . . . . . . . . . . . . . . . . 17  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( b  -  (
a `  1 )
)  =  ( ( e `  4 )  -  ( e ` 
1 ) ) )
7877oveq1d 5873 . . . . . . . . . . . . . . . 16  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( b  -  ( a `  1
) )  x.  (
e `  5 )
)  =  ( ( ( e `  4
)  -  ( e `
 1 ) )  x.  ( e ` 
5 ) ) )
7978oveq2d 5874 . . . . . . . . . . . . . . 15  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( e ` 
6 )  -  (
( b  -  (
a `  1 )
)  x.  ( e `
 5 ) ) )  =  ( ( e `  6 )  -  ( ( ( e `  4 )  -  ( e ` 
1 ) )  x.  ( e `  5
) ) ) )
8079, 67oveq12d 5876 . . . . . . . . . . . . . 14  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( ( e `
 6 )  -  ( ( b  -  ( a `  1
) )  x.  (
e `  5 )
) )  -  (
a `  3 )
)  =  ( ( ( e `  6
)  -  ( ( ( e `  4
)  -  ( e `
 1 ) )  x.  ( e ` 
5 ) ) )  -  ( e ` 
3 ) ) )
8173, 80breq12d 4036 . . . . . . . . . . . . 13  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( ( ( ( 2  x.  b
)  x.  ( a `
 1 ) )  -  ( ( a `
 1 ) ^
2 ) )  - 
1 )  ||  (
( ( e ` 
6 )  -  (
( b  -  (
a `  1 )
)  x.  ( e `
 5 ) ) )  -  ( a `
 3 ) )  <-> 
( ( ( ( 2  x.  ( e `
 4 ) )  x.  ( e ` 
1 ) )  -  ( ( e ` 
1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `  6
)  -  ( ( ( e `  4
)  -  ( e `
 1 ) )  x.  ( e ` 
5 ) ) )  -  ( e ` 
3 ) ) ) )
8274, 81anbi12d 691 . . . . . . . . . . . 12  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( ( a `
 3 )  < 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `
 6 )  -  ( ( b  -  ( a `  1
) )  x.  (
e `  5 )
) )  -  (
a `  3 )
) )  <->  ( (
e `  3 )  <  ( ( ( ( 2  x.  ( e `
 4 ) )  x.  ( e ` 
1 ) )  -  ( ( e ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  ( e `  4
) )  x.  (
e `  1 )
)  -  ( ( e `  1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `
 6 )  -  ( ( ( e `
 4 )  -  ( e `  1
) )  x.  (
e `  5 )
) )  -  (
e `  3 )
) ) ) )
8365, 82anbi12d 691 . . . . . . . . . . 11  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( ( b  e.  ( ZZ>= `  2
)  /\  ( e `  6 )  =  ( b Xrm  ( a ` 
2 ) ) )  /\  ( ( a `
 3 )  < 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `
 6 )  -  ( ( b  -  ( a `  1
) )  x.  (
e `  5 )
) )  -  (
a `  3 )
) ) )  <->  ( (
( e `  4
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  6 )  =  ( ( e `
 4 ) Xrm  ( e `
 2 ) ) )  /\  ( ( e `  3 )  <  ( ( ( ( 2  x.  (
e `  4 )
)  x.  ( e `
 1 ) )  -  ( ( e `
 1 ) ^
2 ) )  - 
1 )  /\  (
( ( ( 2  x.  ( e ` 
4 ) )  x.  ( e `  1
) )  -  (
( e `  1
) ^ 2 ) )  -  1 ) 
||  ( ( ( e `  6 )  -  ( ( ( e `  4 )  -  ( e ` 
1 ) )  x.  ( e `  5
) ) )  -  ( e `  3
) ) ) ) ) )
8462, 83anbi12d 691 . . . . . . . . . 10  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( ( b  e.  ( ZZ>= `  2
)  /\  ( e `  5 )  =  ( b Yrm  ( a ` 
2 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  ( e `  6 )  =  ( b Xrm  ( a ` 
2 ) ) )  /\  ( ( a `
 3 )  < 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `
 6 )  -  ( ( b  -  ( a `  1
) )  x.  (
e `  5 )
) )  -  (
a `  3 )
) ) ) )  <-> 
( ( ( e `
 4 )  e.  ( ZZ>= `  2 )  /\  ( e `  5
)  =  ( ( e `  4 ) Yrm  ( e `  2 ) ) )  /\  (
( ( e ` 
4 )  e.  (
ZZ>= `  2 )  /\  ( e `  6
)  =  ( ( e `  4 ) Xrm  ( e `  2 ) ) )  /\  (
( e `  3
)  <  ( (
( ( 2  x.  ( e `  4
) )  x.  (
e `  1 )
)  -  ( ( e `  1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  ( e `
 4 ) )  x.  ( e ` 
1 ) )  -  ( ( e ` 
1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `  6
)  -  ( ( ( e `  4
)  -  ( e `
 1 ) )  x.  ( e ` 
5 ) ) )  -  ( e ` 
3 ) ) ) ) ) ) )
8557, 84anbi12d 691 . . . . . . . . 9  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  b  =  ( ( a ` 
1 ) Yrm  ( ( a `
 2 )  +  1 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  ( e `  5 )  =  ( b Yrm  ( a ` 
2 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  ( e `  6 )  =  ( b Xrm  ( a ` 
2 ) ) )  /\  ( ( a `
 3 )  < 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `
 6 )  -  ( ( b  -  ( a `  1
) )  x.  (
e `  5 )
) )  -  (
a `  3 )
) ) ) ) )  <->  ( ( ( e `  1 )  e.  ( ZZ>= `  2
)  /\  ( e `  4 )  =  ( ( e ` 
1 ) Yrm  ( ( e `
 2 )  +  1 ) ) )  /\  ( ( ( e `  4 )  e.  ( ZZ>= `  2
)  /\  ( e `  5 )  =  ( ( e ` 
4 ) Yrm  ( e ` 
2 ) ) )  /\  ( ( ( e `  4 )  e.  ( ZZ>= `  2
)  /\  ( e `  6 )  =  ( ( e ` 
4 ) Xrm  ( e ` 
2 ) ) )  /\  ( ( e `
 3 )  < 
( ( ( ( 2  x.  ( e `
 4 ) )  x.  ( e ` 
1 ) )  -  ( ( e ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  ( e `  4
) )  x.  (
e `  1 )
)  -  ( ( e `  1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `
 6 )  -  ( ( ( e `
 4 )  -  ( e `  1
) )  x.  (
e `  5 )
) )  -  (
e `  3 )
) ) ) ) ) ) )
8651, 85anbi12d 691 . . . . . . . 8  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  ( a `  2 )  e.  NN )  /\  (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  b  =  ( (
a `  1 ) Yrm  ( ( a `  2
)  +  1 ) ) )  /\  (
( b  e.  (
ZZ>= `  2 )  /\  ( e `  5
)  =  ( b Yrm  ( a `  2 ) ) )  /\  (
( b  e.  (
ZZ>= `  2 )  /\  ( e `  6
)  =  ( b Xrm  ( a `  2 ) ) )  /\  (
( a `  3
)  <  ( (
( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `  6
)  -  ( ( b  -  ( a `
 1 ) )  x.  ( e ` 
5 ) ) )  -  ( a ` 
3 ) ) ) ) ) ) )  <-> 
( ( ( e `
 1 )  e.  ( ZZ>= `  2 )  /\  ( e `  2
)  e.  NN )  /\  ( ( ( e `  1 )  e.  ( ZZ>= `  2
)  /\  ( e `  4 )  =  ( ( e ` 
1 ) Yrm  ( ( e `
 2 )  +  1 ) ) )  /\  ( ( ( e `  4 )  e.  ( ZZ>= `  2
)  /\  ( e `  5 )  =  ( ( e ` 
4 ) Yrm  ( e ` 
2 ) ) )  /\  ( ( ( e `  4 )  e.  ( ZZ>= `  2
)  /\  ( e `  6 )  =  ( ( e ` 
4 ) Xrm  ( e ` 
2 ) ) )  /\  ( ( e `
 3 )  < 
( ( ( ( 2  x.  ( e `
 4 ) )  x.  ( e ` 
1 ) )  -  ( ( e ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  ( e `  4
) )  x.  (
e `  1 )
)  -  ( ( e `  1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `
 6 )  -  ( ( ( e `
 4 )  -  ( e `  1
) )  x.  (
e `  5 )
) )  -  (
e `  3 )
) ) ) ) ) ) ) )
8711, 12, 86sbc2ie 3058 . . . . . . 7  |-  ( [. ( e  |`  (
1 ... 3 ) )  /  a ]. [. (
e `  4 )  /  b ]. (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  /\  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  b  =  ( ( a ` 
1 ) Yrm  ( ( a `
 2 )  +  1 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  ( e `  5 )  =  ( b Yrm  ( a ` 
2 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  ( e `  6 )  =  ( b Xrm  ( a ` 
2 ) ) )  /\  ( ( a `
 3 )  < 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `
 6 )  -  ( ( b  -  ( a `  1
) )  x.  (
e `  5 )
) )  -  (
a `  3 )
) ) ) ) ) )  <->  ( (
( e `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  2 )  e.  NN )  /\  (
( ( e ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  ( ( e `  2
)  +  1 ) ) )  /\  (
( ( e ` 
4 )  e.  (
ZZ>= `  2 )  /\  ( e `  5
)  =  ( ( e `  4 ) Yrm  ( e `  2 ) ) )  /\  (
( ( e ` 
4 )  e.  (
ZZ>= `  2 )  /\  ( e `  6
)  =  ( ( e `  4 ) Xrm  ( e `  2 ) ) )  /\  (
( e `  3
)  <  ( (
( ( 2  x.  ( e `  4
) )  x.  (
e `  1 )
)  -  ( ( e `  1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  ( e `
 4 ) )  x.  ( e ` 
1 ) )  -  ( ( e ` 
1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `  6
)  -  ( ( ( e `  4
)  -  ( e `
 1 ) )  x.  ( e ` 
5 ) ) )  -  ( e ` 
3 ) ) ) ) ) ) ) )
8834, 87bitri 240 . . . . . 6  |-  ( [. ( e  |`  (
1 ... 3 ) )  /  a ]. [. (
e `  4 )  /  b ]. [. (
e `  5 )  /  c ]. [. (
e `  6 )  /  d ]. (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  /\  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  b  =  ( ( a ` 
1 ) Yrm  ( ( a `
 2 )  +  1 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  c  =  ( b Yrm  ( a ` 
2 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  d  =  ( b Xrm  ( a ` 
2 ) ) )  /\  ( ( a `
 3 )  < 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( d  -  ( ( b  -  ( a `  1
) )  x.  c
) )  -  (
a `  3 )
) ) ) ) ) )  <->  ( (
( e `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  2 )  e.  NN )  /\  (
( ( e ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  ( ( e `  2
)  +  1 ) ) )  /\  (
( ( e ` 
4 )  e.  (
ZZ>= `  2 )  /\  ( e `  5
)  =  ( ( e `  4 ) Yrm  ( e `  2 ) ) )  /\  (
( ( e ` 
4 )  e.  (
ZZ>= `  2 )  /\  ( e `  6
)  =  ( ( e `  4 ) Xrm  ( e `  2 ) ) )  /\  (
( e `  3
)  <  ( (
( ( 2  x.  ( e `  4
) )  x.  (
e `  1 )
)  -  ( ( e `  1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  ( e `
 4 ) )  x.  ( e ` 
1 ) )  -  ( ( e ` 
1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `  6
)  -  ( ( ( e `  4
)  -  ( e `
 1 ) )  x.  ( e ` 
5 ) ) )  -  ( e ` 
3 ) ) ) ) ) ) ) )
8988a1i 10 . . . . 5  |-  ( e  e.  ( NN0  ^m  ( 1 ... 6
) )  ->  ( [. ( e  |`  (
1 ... 3 ) )  /  a ]. [. (
e `  4 )  /  b ]. [. (
e `  5 )  /  c ]. [. (
e `  6 )  /  d ]. (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  /\  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  b  =  ( ( a ` 
1 ) Yrm  ( ( a `
 2 )  +  1 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  c  =  ( b Yrm  ( a ` 
2 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  d  =  ( b Xrm  ( a ` 
2 ) ) )  /\  ( ( a `
 3 )  < 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( d  -  ( ( b  -  ( a `  1
) )  x.  c
) )  -  (
a `  3 )
) ) ) ) ) )  <->  ( (
( e `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  2 )  e.  NN )  /\  (
( ( e ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  ( ( e `  2
)  +  1 ) ) )  /\  (
( ( e ` 
4 )  e.  (
ZZ>= `  2 )  /\  ( e `  5
)  =  ( ( e `  4 ) Yrm  ( e `  2 ) ) )  /\  (
( ( e ` 
4 )  e.  (
ZZ>= `  2 )  /\  ( e `  6
)  =  ( ( e `  4 ) Xrm  ( e `  2 ) ) )  /\  (
( e `  3
)  <  ( (
( ( 2  x.  ( e `  4
) )  x.  (
e `  1 )
)  -  ( ( e `  1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  ( e `
 4 ) )  x.  ( e ` 
1 ) )  -  ( ( e ` 
1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `  6
)  -  ( ( ( e `  4
)  -  ( e `
 1 ) )  x.  ( e ` 
5 ) ) )  -  ( e ` 
3 ) ) ) ) ) ) ) ) )
9089rabbiia 2778 . . . 4  |-  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  [. ( e  |`  (
1 ... 3 ) )  /  a ]. [. (
e `  4 )  /  b ]. [. (
e `  5 )  /  c ]. [. (
e `  6 )  /  d ]. (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  /\  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  b  =  ( ( a ` 
1 ) Yrm  ( ( a `
 2 )  +  1 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  c  =  ( b Yrm  ( a ` 
2 ) ) )  /\  ( ( b  e.  ( ZZ>= `  2
)  /\  d  =  ( b Xrm  ( a ` 
2 ) ) )  /\  ( ( a `
 3 )  < 
( ( ( ( 2  x.  b )  x.  ( a ` 
1 ) )  -  ( ( a ` 
1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  b )  x.  (
a `  1 )
)  -  ( ( a `  1 ) ^ 2 ) )  -  1 )  ||  ( ( d  -  ( ( b  -  ( a `  1
) )  x.  c
) )  -  (
a `  3 )
) ) ) ) ) ) }  =  { e  e.  ( NN0  ^m  ( 1 ... 6 ) )  |  ( ( ( e `  1 )  e.  ( ZZ>= `  2
)  /\  ( e `  2 )  e.  NN )  /\  (
( ( e ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  ( ( e `  2
)  +  1 ) ) )  /\  (
( ( e ` 
4 )  e.  (
ZZ>= `  2 )  /\  ( e `  5
)  =  ( ( e `  4 ) Yrm  ( e `  2 ) ) )  /\  (
( ( e ` 
4 )  e.  (
ZZ>= `  2 )  /\  ( e `  6
)  =  ( ( e `  4 ) Xrm  ( e `  2 ) ) )  /\  (
( e `  3
)  <  ( (
( ( 2  x.  ( e `  4
) )  x.  (
e `  1 )
)  -  ( ( e `  1 ) ^ 2 ) )  -  1 )  /\  ( ( ( ( 2  x.  ( e `
 4 ) )  x.  ( e ` 
1 ) )  -  ( ( e ` 
1 ) ^ 2 ) )  -  1 )  ||  ( ( ( e `  6
)  -  ( ( ( e `  4
)  -  ( e `
 1 ) )  x.  ( e ` 
5 ) ) )  -  ( e ` 
3 ) ) ) ) ) ) ) }
91 6nn0 9986 . . . . . . 7  |-  6  e.  NN0
92 2z 10054 . . . . . . 7  |-  2  e.  ZZ
93 ovex 5883 . . . . . . . 8  |-  ( 1 ... 6 )  e. 
_V
94 df-4 9806 . . . . . . . . . . . 12  |-  4  =  ( 3  +  1 )
95 df-5 9807 . . . . . . . . . . . . 13  |-  5  =  ( 4  +  1 )
96 df-6 9808 . . . . . . . . . . . . . 14  |-  6  =  ( 5  +  1 )
97 ssid 3197 . . . . . . . . . . . . . 14  |-  ( 1 ... 6 )  C_  ( 1 ... 6
)
9896, 97jm2.27dlem5 27106 . . . . . . . . . . . . 13  |-  ( 1 ... 5 )  C_  ( 1 ... 6
)
9995, 98jm2.27dlem5 27106 . . . . . . . . . . . 12  |-  ( 1 ... 4 )  C_  ( 1 ... 6
)
10094, 99jm2.27dlem5 27106 . . . . . . . . . . 11  |-  ( 1 ... 3 )  C_  ( 1 ... 6
)
10136, 100jm2.27dlem5 27106 . . . . . . . . . 10  |-  ( 1 ... 2 )  C_  ( 1 ... 6
)
10235, 101jm2.27dlem5 27106 . . . . . . . . 9  |-  ( 1 ... 1 )  C_  ( 1 ... 6
)
103102, 41sselii 3177 . . . . . . . 8  |-  1  e.  ( 1 ... 6
)
104 mzpproj 26815 . . . . . . . 8  |-  ( ( ( 1 ... 6
)  e.  _V  /\  1  e.  ( 1 ... 6 ) )  ->  ( e  e.  ( ZZ  ^m  (
1 ... 6 ) ) 
|->  ( e `  1
) )  e.  (mzPoly `  ( 1 ... 6
) ) )
10593, 103, 104mp2an 653 . . . . . . 7  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  ( e `
 1 ) )  e.  (mzPoly `  (
1 ... 6 ) )
106 eluzrabdioph 26887 . . . . . . 7  |-  ( ( 6  e.  NN0  /\  2  e.  ZZ  /\  (
e  e.  ( ZZ 
^m  ( 1 ... 6 ) )  |->  ( e `  1 ) )  e.  (mzPoly `  ( 1 ... 6
) ) )  ->  { e  e.  ( NN0  ^m  ( 1 ... 6 ) )  |  ( e ` 
1 )  e.  (
ZZ>= `  2 ) }  e.  (Dioph `  6
) )
10791, 92, 105, 106mp3an 1277 . . . . . 6  |-  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  ( e `  1 )  e.  ( ZZ>= `  2
) }  e.  (Dioph `  6 )
108101, 46sselii 3177 . . . . . . . 8  |-  2  e.  ( 1 ... 6
)
109 mzpproj 26815 . . . . . . . 8  |-  ( ( ( 1 ... 6
)  e.  _V  /\  2  e.  ( 1 ... 6 ) )  ->  ( e  e.  ( ZZ  ^m  (
1 ... 6 ) ) 
|->  ( e `  2
) )  e.  (mzPoly `  ( 1 ... 6
) ) )
11093, 108, 109mp2an 653 . . . . . . 7  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  ( e `
 2 ) )  e.  (mzPoly `  (
1 ... 6 ) )
111 elnnrabdioph 26888 . . . . . . 7  |-  ( ( 6  e.  NN0  /\  ( e  e.  ( ZZ  ^m  ( 1 ... 6 ) ) 
|->  ( e `  2
) )  e.  (mzPoly `  ( 1 ... 6
) ) )  ->  { e  e.  ( NN0  ^m  ( 1 ... 6 ) )  |  ( e ` 
2 )  e.  NN }  e.  (Dioph `  6
) )
11291, 110, 111mp2an 653 . . . . . 6  |-  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  ( e `  2 )  e.  NN }  e.  (Dioph `  6 )
113 anrabdioph 26860 . . . . . 6  |-  ( ( { e  e.  ( NN0  ^m  ( 1 ... 6 ) )  |  ( e ` 
1 )  e.  (
ZZ>= `  2 ) }  e.  (Dioph `  6
)  /\  { e  e.  ( NN0  ^m  (
1 ... 6 ) )  |  ( e ` 
2 )  e.  NN }  e.  (Dioph `  6
) )  ->  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  ( ( e `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  2 )  e.  NN ) }  e.  (Dioph `  6 ) )
114107, 112, 113mp2an 653 . . . . 5  |-  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  ( ( e `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  2 )  e.  NN ) }  e.  (Dioph `  6 )
115 elmapi 6792 . . . . . . . . . . 11  |-  ( e  e.  ( NN0  ^m  ( 1 ... 6
) )  ->  e : ( 1 ... 6 ) --> NN0 )
116 ffvelrn 5663 . . . . . . . . . . 11  |-  ( ( e : ( 1 ... 6 ) --> NN0 
/\  2  e.  ( 1 ... 6 ) )  ->  ( e `  2 )  e. 
NN0 )
117115, 108, 116sylancl 643 . . . . . . . . . 10  |-  ( e  e.  ( NN0  ^m  ( 1 ... 6
) )  ->  (
e `  2 )  e.  NN0 )
118 peano2nn0 10004 . . . . . . . . . 10  |-  ( ( e `  2 )  e.  NN0  ->  ( ( e `  2 )  +  1 )  e. 
NN0 )
119 oveq2 5866 . . . . . . . . . . . . 13  |-  ( b  =  ( ( e `
 2 )  +  1 )  ->  (
( e `  1
) Yrm  b )  =  ( ( e `  1
) Yrm  ( ( e ` 
2 )  +  1 ) ) )
120119eqeq2d 2294 . . . . . . . . . . . 12  |-  ( b  =  ( ( e `
 2 )  +  1 )  ->  (
( e `  4
)  =  ( ( e `  1 ) Yrm  b )  <->  ( e ` 
4 )  =  ( ( e `  1
) Yrm  ( ( e ` 
2 )  +  1 ) ) ) )
121120anbi2d 684 . . . . . . . . . . 11  |-  ( b  =  ( ( e `
 2 )  +  1 )  ->  (
( ( e ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  b ) )  <->  ( (
e `  1 )  e.  ( ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  ( ( e `  2
)  +  1 ) ) ) ) )
122121ceqsrexv 2901 . . . . . . . . . 10  |-  ( ( ( e `  2
)  +  1 )  e.  NN0  ->  ( E. b  e.  NN0  (
b  =  ( ( e `  2 )  +  1 )  /\  ( ( e ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  b ) ) )  <->  ( (
e `  1 )  e.  ( ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  ( ( e `  2
)  +  1 ) ) ) ) )
123117, 118, 1223syl 18 . . . . . . . . 9  |-  ( e  e.  ( NN0  ^m  ( 1 ... 6
) )  ->  ( E. b  e.  NN0  ( b  =  ( ( e `  2
)  +  1 )  /\  ( ( e `
 1 )  e.  ( ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  b ) ) )  <->  ( (
e `  1 )  e.  ( ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  ( ( e `  2
)  +  1 ) ) ) ) )
124123bicomd 192 . . . . . . . 8  |-  ( e  e.  ( NN0  ^m  ( 1 ... 6
) )  ->  (
( ( e ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  ( ( e `  2
)  +  1 ) ) )  <->  E. b  e.  NN0  ( b  =  ( ( e ` 
2 )  +  1 )  /\  ( ( e `  1 )  e.  ( ZZ>= `  2
)  /\  ( e `  4 )  =  ( ( e ` 
1 ) Yrm  b ) ) ) ) )
125124rabbiia 2778 . . . . . . 7  |-  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  ( ( e `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  4 )  =  ( ( e `
 1 ) Yrm  ( ( e `  2 )  +  1 ) ) ) }  =  {
e  e.  ( NN0 
^m  ( 1 ... 6 ) )  |  E. b  e.  NN0  ( b  =  ( ( e `  2
)  +  1 )  /\  ( ( e `
 1 )  e.  ( ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  b ) ) ) }
126 vex 2791 . . . . . . . . . . . . 13  |-  a  e. 
_V
127126resex 4995 . . . . . . . . . . . 12  |-  ( a  |`  ( 1 ... 6
) )  e.  _V
128 fvex 5539 . . . . . . . . . . . 12  |-  ( a `
 7 )  e. 
_V
129 id 19 . . . . . . . . . . . . . 14  |-  ( b  =  ( a ` 
7 )  ->  b  =  ( a ` 
7 ) )
130108jm2.27dlem1 27102 . . . . . . . . . . . . . . 15  |-  ( e  =  ( a  |`  ( 1 ... 6
) )  ->  (
e `  2 )  =  ( a ` 
2 ) )
131130oveq1d 5873 . . . . . . . . . . . . . 14  |-  ( e  =  ( a  |`  ( 1 ... 6
) )  ->  (
( e `  2
)  +  1 )  =  ( ( a `
 2 )  +  1 ) )
132129, 131eqeqan12rd 2299 . . . . . . . . . . . . 13  |-  ( ( e  =  ( a  |`  ( 1 ... 6
) )  /\  b  =  ( a ` 
7 ) )  -> 
( b  =  ( ( e `  2
)  +  1 )  <-> 
( a `  7
)  =  ( ( a `  2 )  +  1 ) ) )
133103jm2.27dlem1 27102 . . . . . . . . . . . . . . . 16  |-  ( e  =  ( a  |`  ( 1 ... 6
) )  ->  (
e `  1 )  =  ( a ` 
1 ) )
134133adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( e  =  ( a  |`  ( 1 ... 6
) )  /\  b  =  ( a ` 
7 ) )  -> 
( e `  1
)  =  ( a `
 1 ) )
135134eleq1d 2349 . . . . . . . . . . . . . 14  |-  ( ( e  =  ( a  |`  ( 1 ... 6
) )  /\  b  =  ( a ` 
7 ) )  -> 
( ( e ` 
1 )  e.  (
ZZ>= `  2 )  <->  ( a `  1 )  e.  ( ZZ>= `  2 )
) )
136 4nn 9879 . . . . . . . . . . . . . . . . . . 19  |-  4  e.  NN
137136jm2.27dlem3 27104 . . . . . . . . . . . . . . . . . 18  |-  4  e.  ( 1 ... 4
)
13899, 137sselii 3177 . . . . . . . . . . . . . . . . 17  |-  4  e.  ( 1 ... 6
)
139138jm2.27dlem1 27102 . . . . . . . . . . . . . . . 16  |-  ( e  =  ( a  |`  ( 1 ... 6
) )  ->  (
e `  4 )  =  ( a ` 
4 ) )
140139adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( e  =  ( a  |`  ( 1 ... 6
) )  /\  b  =  ( a ` 
7 ) )  -> 
( e `  4
)  =  ( a `
 4 ) )
141133, 129oveqan12d 5877 . . . . . . . . . . . . . . 15  |-  ( ( e  =  ( a  |`  ( 1 ... 6
) )  /\  b  =  ( a ` 
7 ) )  -> 
( ( e ` 
1 ) Yrm  b )  =  ( ( a ` 
1 ) Yrm  ( a ` 
7 ) ) )
142140, 141eqeq12d 2297 . . . . . . . . . . . . . 14  |-  ( ( e  =  ( a  |`  ( 1 ... 6
) )  /\  b  =  ( a ` 
7 ) )  -> 
( ( e ` 
4 )  =  ( ( e `  1
) Yrm  b )  <->  ( a `  4 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
7 ) ) ) )
143135, 142anbi12d 691 . . . . . . . . . . . . 13  |-  ( ( e  =  ( a  |`  ( 1 ... 6
) )  /\  b  =  ( a ` 
7 ) )  -> 
( ( ( e `
 1 )  e.  ( ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  b ) )  <->  ( (
a `  1 )  e.  ( ZZ>= `  2 )  /\  ( a `  4
)  =  ( ( a `  1 ) Yrm  ( a `  7 ) ) ) ) )
144132, 143anbi12d 691 . . . . . . . . . . . 12  |-  ( ( e  =  ( a  |`  ( 1 ... 6
) )  /\  b  =  ( a ` 
7 ) )  -> 
( ( b  =  ( ( e ` 
2 )  +  1 )  /\  ( ( e `  1 )  e.  ( ZZ>= `  2
)  /\  ( e `  4 )  =  ( ( e ` 
1 ) Yrm  b ) ) )  <->  ( ( a `
 7 )  =  ( ( a ` 
2 )  +  1 )  /\  ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  ( a `  4 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
7 ) ) ) ) ) )
145127, 128, 144sbc2ie 3058 . . . . . . . . . . 11  |-  ( [. ( a  |`  (
1 ... 6 ) )  /  e ]. [. (
a `  7 )  /  b ]. (
b  =  ( ( e `  2 )  +  1 )  /\  ( ( e ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  b ) ) )  <->  ( (
a `  7 )  =  ( ( a `
 2 )  +  1 )  /\  (
( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  4 )  =  ( ( a `
 1 ) Yrm  ( a `
 7 ) ) ) ) )
146145a1i 10 . . . . . . . . . 10  |-  ( a  e.  ( NN0  ^m  ( 1 ... 7
) )  ->  ( [. ( a  |`  (
1 ... 6 ) )  /  e ]. [. (
a `  7 )  /  b ]. (
b  =  ( ( e `  2 )  +  1 )  /\  ( ( e ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  b ) ) )  <->  ( (
a `  7 )  =  ( ( a `
 2 )  +  1 )  /\  (
( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  4 )  =  ( ( a `
 1 ) Yrm  ( a `
 7 ) ) ) ) ) )
147146rabbiia 2778 . . . . . . . . 9  |-  { a  e.  ( NN0  ^m  ( 1 ... 7
) )  |  [. ( a  |`  (
1 ... 6 ) )  /  e ]. [. (
a `  7 )  /  b ]. (
b  =  ( ( e `  2 )  +  1 )  /\  ( ( e ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  b ) ) ) }  =  { a  e.  ( NN0  ^m  (
1 ... 7 ) )  |  ( ( a `
 7 )  =  ( ( a ` 
2 )  +  1 )  /\  ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  ( a `  4 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
7 ) ) ) ) }
148 7nn0 9987 . . . . . . . . . . 11  |-  7  e.  NN0
149 ovex 5883 . . . . . . . . . . . 12  |-  ( 1 ... 7 )  e. 
_V
150 7nn 9882 . . . . . . . . . . . . 13  |-  7  e.  NN
151150jm2.27dlem3 27104 . . . . . . . . . . . 12  |-  7  e.  ( 1 ... 7
)
152 mzpproj 26815 . . . . . . . . . . . 12  |-  ( ( ( 1 ... 7
)  e.  _V  /\  7  e.  ( 1 ... 7 ) )  ->  ( a  e.  ( ZZ  ^m  (
1 ... 7 ) ) 
|->  ( a `  7
) )  e.  (mzPoly `  ( 1 ... 7
) ) )
153149, 151, 152mp2an 653 . . . . . . . . . . 11  |-  ( a  e.  ( ZZ  ^m  ( 1 ... 7
) )  |->  ( a `
 7 ) )  e.  (mzPoly `  (
1 ... 7 ) )
154 df-7 9809 . . . . . . . . . . . . . 14  |-  7  =  ( 6  +  1 )
155 6nn 9881 . . . . . . . . . . . . . 14  |-  6  e.  NN
156108, 154, 155jm2.27dlem2 27103 . . . . . . . . . . . . 13  |-  2  e.  ( 1 ... 7
)
157 mzpproj 26815 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... 7
)  e.  _V  /\  2  e.  ( 1 ... 7 ) )  ->  ( a  e.  ( ZZ  ^m  (
1 ... 7 ) ) 
|->  ( a `  2
) )  e.  (mzPoly `  ( 1 ... 7
) ) )
158149, 156, 157mp2an 653 . . . . . . . . . . . 12  |-  ( a  e.  ( ZZ  ^m  ( 1 ... 7
) )  |->  ( a `
 2 ) )  e.  (mzPoly `  (
1 ... 7 ) )
159 1z 10053 . . . . . . . . . . . . 13  |-  1  e.  ZZ
160 mzpconstmpt 26818 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... 7
)  e.  _V  /\  1  e.  ZZ )  ->  ( a  e.  ( ZZ  ^m  ( 1 ... 7 ) ) 
|->  1 )  e.  (mzPoly `  ( 1 ... 7
) ) )
161149, 159, 160mp2an 653 . . . . . . . . . . . 12  |-  ( a  e.  ( ZZ  ^m  ( 1 ... 7
) )  |->  1 )  e.  (mzPoly `  (
1 ... 7 ) )
162 mzpaddmpt 26819 . . . . . . . . . . . 12  |-  ( ( ( a  e.  ( ZZ  ^m  ( 1 ... 7 ) ) 
|->  ( a `  2
) )  e.  (mzPoly `  ( 1 ... 7
) )  /\  (
a  e.  ( ZZ 
^m  ( 1 ... 7 ) )  |->  1 )  e.  (mzPoly `  ( 1 ... 7
) ) )  -> 
( a  e.  ( ZZ  ^m  ( 1 ... 7 ) ) 
|->  ( ( a ` 
2 )  +  1 ) )  e.  (mzPoly `  ( 1 ... 7
) ) )
163158, 161, 162mp2an 653 . . . . . . . . . . 11  |-  ( a  e.  ( ZZ  ^m  ( 1 ... 7
) )  |->  ( ( a `  2 )  +  1 ) )  e.  (mzPoly `  (
1 ... 7 ) )
164 eqrabdioph 26857 . . . . . . . . . . 11  |-  ( ( 7  e.  NN0  /\  ( a  e.  ( ZZ  ^m  ( 1 ... 7 ) ) 
|->  ( a `  7
) )  e.  (mzPoly `  ( 1 ... 7
) )  /\  (
a  e.  ( ZZ 
^m  ( 1 ... 7 ) )  |->  ( ( a `  2
)  +  1 ) )  e.  (mzPoly `  ( 1 ... 7
) ) )  ->  { a  e.  ( NN0  ^m  ( 1 ... 7 ) )  |  ( a ` 
7 )  =  ( ( a `  2
)  +  1 ) }  e.  (Dioph ` 
7 ) )
165148, 153, 163, 164mp3an 1277 . . . . . . . . . 10  |-  { a  e.  ( NN0  ^m  ( 1 ... 7
) )  |  ( a `  7 )  =  ( ( a `
 2 )  +  1 ) }  e.  (Dioph `  7 )
166 rmydioph 27107 . . . . . . . . . . 11  |-  { b  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( ( b `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
b `  3 )  =  ( ( b `
 1 ) Yrm  ( b `
 2 ) ) ) }  e.  (Dioph `  3 )
167 simp1 955 . . . . . . . . . . . . . 14  |-  ( ( ( b `  1
)  =  ( a `
 1 )  /\  ( b `  2
)  =  ( a `
 7 )  /\  ( b `  3
)  =  ( a `
 4 ) )  ->  ( b ` 
1 )  =  ( a `  1 ) )
168167eleq1d 2349 . . . . . . . . . . . . 13  |-  ( ( ( b `  1
)  =  ( a `
 1 )  /\  ( b `  2
)  =  ( a `
 7 )  /\  ( b `  3
)  =  ( a `
 4 ) )  ->  ( ( b `
 1 )  e.  ( ZZ>= `  2 )  <->  ( a `  1 )  e.  ( ZZ>= `  2
) ) )
169 simp3 957 . . . . . . . . . . . . . 14  |-  ( ( ( b `  1
)  =  ( a `
 1 )  /\  ( b `  2
)  =  ( a `
 7 )  /\  ( b `  3
)  =  ( a `
 4 ) )  ->  ( b ` 
3 )  =  ( a `  4 ) )
170 simp2 956 . . . . . . . . . . . . . . 15  |-  ( ( ( b `  1
)  =  ( a `
 1 )  /\  ( b `  2
)  =  ( a `
 7 )  /\  ( b `  3
)  =  ( a `
 4 ) )  ->  ( b ` 
2 )  =  ( a `  7 ) )
171167, 170oveq12d 5876 . . . . . . . . . . . . . 14  |-  ( ( ( b `  1
)  =  ( a `
 1 )  /\  ( b `  2
)  =  ( a `
 7 )  /\  ( b `  3
)  =  ( a `
 4 ) )  ->  ( ( b `
 1 ) Yrm  ( b `
 2 ) )  =  ( ( a `
 1 ) Yrm  ( a `
 7 ) ) )
172169, 171eqeq12d 2297 . . . . . . . . . . . . 13  |-  ( ( ( b `  1
)  =  ( a `
 1 )  /\  ( b `  2
)  =  ( a `
 7 )  /\  ( b `  3
)  =  ( a `
 4 ) )  ->  ( ( b `
 3 )  =  ( ( b ` 
1 ) Yrm  ( b ` 
2 ) )  <->  ( a `  4 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
7 ) ) ) )
173168, 172anbi12d 691 . . . . . . . . . . . 12  |-  ( ( ( b `  1
)  =  ( a `
 1 )  /\  ( b `  2
)  =  ( a `
 7 )  /\  ( b `  3
)  =  ( a `
 4 ) )  ->  ( ( ( b `  1 )  e.  ( ZZ>= `  2
)  /\  ( b `  3 )  =  ( ( b ` 
1 ) Yrm  ( b ` 
2 ) ) )  <-> 
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  4
)  =  ( ( a `  1 ) Yrm  ( a `  7 ) ) ) ) )
174103, 154, 155jm2.27dlem2 27103 . . . . . . . . . . . 12  |-  1  e.  ( 1 ... 7
)
175138, 154, 155jm2.27dlem2 27103 . . . . . . . . . . . 12  |-  4  e.  ( 1 ... 7
)
176173, 174, 151, 175rabren3dioph 26898 . . . . . . . . . . 11  |-  ( ( 7  e.  NN0  /\  { b  e.  ( NN0 
^m  ( 1 ... 3 ) )  |  ( ( b ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( b `  3
)  =  ( ( b `  1 ) Yrm  ( b `  2 ) ) ) }  e.  (Dioph `  3 ) )  ->  { a  e.  ( NN0  ^m  (
1 ... 7 ) )  |  ( ( a `
 1 )  e.  ( ZZ>= `  2 )  /\  ( a `  4
)  =  ( ( a `  1 ) Yrm  ( a `  7 ) ) ) }  e.  (Dioph `  7 ) )
177148, 166, 176mp2an 653 . . . . . . . . . 10  |-  { a  e.  ( NN0  ^m  ( 1 ... 7
) )  |  ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  4 )  =  ( ( a `
 1 ) Yrm  ( a `
 7 ) ) ) }  e.  (Dioph `  7 )
178 anrabdioph 26860 . . . . . . . . . 10  |-  ( ( { a  e.  ( NN0  ^m  ( 1 ... 7 ) )  |  ( a ` 
7 )  =  ( ( a `  2
)  +  1 ) }  e.  (Dioph ` 
7 )  /\  {
a  e.  ( NN0 
^m  ( 1 ... 7 ) )  |  ( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  4
)  =  ( ( a `  1 ) Yrm  ( a `  7 ) ) ) }  e.  (Dioph `  7 ) )  ->  { a  e.  ( NN0  ^m  (
1 ... 7 ) )  |  ( ( a `
 7 )  =  ( ( a ` 
2 )  +  1 )  /\  ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  ( a `  4 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
7 ) ) ) ) }  e.  (Dioph `  7 ) )
179165, 177, 178mp2an 653 . . . . . . . . 9  |-  { a  e.  ( NN0  ^m  ( 1 ... 7
) )  |  ( ( a `  7
)  =  ( ( a `  2 )  +  1 )  /\  ( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  4
)  =  ( ( a `  1 ) Yrm  ( a `  7 ) ) ) ) }  e.  (Dioph `  7
)
180147, 179eqeltri 2353 . . . . . . . 8  |-  { a  e.  ( NN0  ^m  ( 1 ... 7
) )  |  [. ( a  |`  (
1 ... 6 ) )  /  e ]. [. (
a `  7 )  /  b ]. (
b  =  ( ( e `  2 )  +  1 )  /\  ( ( e ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  b ) ) ) }  e.  (Dioph `  7
)
181154rexfrabdioph 26876 . . . . . . . 8  |-  ( ( 6  e.  NN0  /\  { a  e.  ( NN0 
^m  ( 1 ... 7 ) )  | 
[. ( a  |`  ( 1 ... 6
) )  /  e ]. [. ( a ` 
7 )  /  b ]. ( b  =  ( ( e `  2
)  +  1 )  /\  ( ( e `
 1 )  e.  ( ZZ>= `  2 )  /\  ( e `  4
)  =  ( ( e `  1 ) Yrm  b ) ) ) }  e.  (Dioph `  7
) )  ->  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  E. b  e.  NN0  ( b  =  ( ( e `
 2 )  +  1 )  /\  (
( e `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  4 )  =  ( ( e `
 1 ) Yrm  b ) ) ) }  e.  (Dioph `  6 ) )
18291, 180, 181mp2an 653 . . . . . . 7  |-  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  E. b  e.  NN0  ( b  =  ( ( e `
 2 )  +  1 )  /\  (
( e `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  4 )  =  ( ( e `
 1 ) Yrm  b ) ) ) }  e.  (Dioph `  6 )
183125, 182eqeltri 2353 . . . . . 6  |-  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  ( ( e `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  4 )  =  ( ( e `
 1 ) Yrm  ( ( e `  2 )  +  1 ) ) ) }  e.  (Dioph `  6 )
184 rmydioph 27107 . . . . . . . 8  |-  { a  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  3 )  =  ( ( a `
 1 ) Yrm  ( a `
 2 ) ) ) }  e.  (Dioph `  3 )
185 simp1 955 . . . . . . . . . . 11  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 5 ) )  ->  ( a ` 
1 )  =  ( e `  4 ) )
186185eleq1d 2349 . . . . . . . . . 10  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 5 ) )  ->  ( ( a `
 1 )  e.  ( ZZ>= `  2 )  <->  ( e `  4 )  e.  ( ZZ>= `  2
) ) )
187 simp3 957 . . . . . . . . . . 11  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 5 ) )  ->  ( a ` 
3 )  =  ( e `  5 ) )
188 simp2 956 . . . . . . . . . . . 12  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 5 ) )  ->  ( a ` 
2 )  =  ( e `  2 ) )
189185, 188oveq12d 5876 . . . . . . . . . . 11  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 5 ) )  ->  ( ( a `
 1 ) Yrm  ( a `
 2 ) )  =  ( ( e `
 4 ) Yrm  ( e `
 2 ) ) )
190187, 189eqeq12d 2297 . . . . . . . . . 10  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 5 ) )  ->  ( ( a `
 3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) )  <->  ( e `  5 )  =  ( ( e ` 
4 ) Yrm  ( e ` 
2 ) ) ) )
191186, 190anbi12d 691 . . . . . . . . 9  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 5 ) )  ->  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  ( a `  3 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
2 ) ) )  <-> 
( ( e ` 
4 )  e.  (
ZZ>= `  2 )  /\  ( e `  5
)  =  ( ( e `  4 ) Yrm  ( e `  2 ) ) ) ) )
192 5nn 9880 . . . . . . . . . . 11  |-  5  e.  NN
193192jm2.27dlem3 27104 . . . . . . . . . 10  |-  5  e.  ( 1 ... 5
)
194193, 96, 192jm2.27dlem2 27103 . . . . . . . . 9  |-  5  e.  ( 1 ... 6
)
195191, 138, 108, 194rabren3dioph 26898 . . . . . . . 8  |-  ( ( 6  e.  NN0  /\  { a  e.  ( NN0 
^m  ( 1 ... 3 ) )  |  ( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  3
)  =  ( ( a `  1 ) Yrm  ( a `  2 ) ) ) }  e.  (Dioph `  3 ) )  ->  { e  e.  ( NN0  ^m  (
1 ... 6 ) )  |  ( ( e `
 4 )  e.  ( ZZ>= `  2 )  /\  ( e `  5
)  =  ( ( e `  4 ) Yrm  ( e `  2 ) ) ) }  e.  (Dioph `  6 ) )
19691, 184, 195mp2an 653 . . . . . . 7  |-  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  ( ( e `  4
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  5 )  =  ( ( e `
 4 ) Yrm  ( e `
 2 ) ) ) }  e.  (Dioph `  6 )
197 rmxdioph 27109 . . . . . . . . 9  |-  { a  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  3 )  =  ( ( a `
 1 ) Xrm  ( a `
 2 ) ) ) }  e.  (Dioph `  3 )
198 simp1 955 . . . . . . . . . . . 12  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 6 ) )  ->  ( a ` 
1 )  =  ( e `  4 ) )
199198eleq1d 2349 . . . . . . . . . . 11  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 6 ) )  ->  ( ( a `
 1 )  e.  ( ZZ>= `  2 )  <->  ( e `  4 )  e.  ( ZZ>= `  2
) ) )
200 simp3 957 . . . . . . . . . . . 12  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 6 ) )  ->  ( a ` 
3 )  =  ( e `  6 ) )
201 simp2 956 . . . . . . . . . . . . 13  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 6 ) )  ->  ( a ` 
2 )  =  ( e `  2 ) )
202198, 201oveq12d 5876 . . . . . . . . . . . 12  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 6 ) )  ->  ( ( a `
 1 ) Xrm  ( a `
 2 ) )  =  ( ( e `
 4 ) Xrm  ( e `
 2 ) ) )
203200, 202eqeq12d 2297 . . . . . . . . . . 11  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 6 ) )  ->  ( ( a `
 3 )  =  ( ( a ` 
1 ) Xrm  ( a ` 
2 ) )  <->  ( e `  6 )  =  ( ( e ` 
4 ) Xrm  ( e ` 
2 ) ) ) )
204199, 203anbi12d 691 . . . . . . . . . 10  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 6 ) )  ->  ( ( ( a `  1 )  e.  ( ZZ>= `  2
)  /\  ( a `  3 )  =  ( ( a ` 
1 ) Xrm  ( a ` 
2 ) ) )  <-> 
( ( e ` 
4 )  e.  (
ZZ>= `  2 )  /\  ( e `  6
)  =  ( ( e `  4 ) Xrm  ( e `  2 ) ) ) ) )
205155jm2.27dlem3 27104 . . . . . . . . . 10  |-  6  e.  ( 1 ... 6
)
206204, 138, 108, 205rabren3dioph 26898 . . . . . . . . 9  |-  ( ( 6  e.  NN0  /\  { a  e.  ( NN0 
^m  ( 1 ... 3 ) )  |  ( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  3
)  =  ( ( a `  1 ) Xrm  ( a `  2 ) ) ) }  e.  (Dioph `  3 ) )  ->  { e  e.  ( NN0  ^m  (
1 ... 6 ) )  |  ( ( e `
 4 )  e.  ( ZZ>= `  2 )  /\  ( e `  6
)  =  ( ( e `  4 ) Xrm  ( e `  2 ) ) ) }  e.  (Dioph `  6 ) )
20791, 197, 206mp2an 653 . . . . . . . 8  |-  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  ( ( e `  4
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  6 )  =  ( ( e `
 4 ) Xrm  ( e `
 2 ) ) ) }  e.  (Dioph `  6 )
208100, 3sselii 3177 . . . . . . . . . . 11  |-  3  e.  ( 1 ... 6
)
209 mzpproj 26815 . . . . . . . . . . 11  |-  ( ( ( 1 ... 6
)  e.  _V  /\  3  e.  ( 1 ... 6 ) )  ->  ( e  e.  ( ZZ  ^m  (
1 ... 6 ) ) 
|->  ( e `  3
) )  e.  (mzPoly `  ( 1 ... 6
) ) )
21093, 208, 209mp2an 653 . . . . . . . . . 10  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  ( e `
 3 ) )  e.  (mzPoly `  (
1 ... 6 ) )
211 mzpconstmpt 26818 . . . . . . . . . . . . . . 15  |-  ( ( ( 1 ... 6
)  e.  _V  /\  2  e.  ZZ )  ->  ( e  e.  ( ZZ  ^m  ( 1 ... 6 ) ) 
|->  2 )  e.  (mzPoly `  ( 1 ... 6
) ) )
21293, 92, 211mp2an 653 . . . . . . . . . . . . . 14  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  2 )  e.  (mzPoly `  (
1 ... 6 ) )
213 mzpproj 26815 . . . . . . . . . . . . . . 15  |-  ( ( ( 1 ... 6
)  e.  _V  /\  4  e.  ( 1 ... 6 ) )  ->  ( e  e.  ( ZZ  ^m  (
1 ... 6 ) ) 
|->  ( e `  4
) )  e.  (mzPoly `  ( 1 ... 6
) ) )
21493, 138, 213mp2an 653 . . . . . . . . . . . . . 14  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  ( e `
 4 ) )  e.  (mzPoly `  (
1 ... 6 ) )
215 mzpmulmpt 26820 . . . . . . . . . . . . . 14  |-  ( ( ( e  e.  ( ZZ  ^m  ( 1 ... 6 ) ) 
|->  2 )  e.  (mzPoly `  ( 1 ... 6
) )  /\  (
e  e.  ( ZZ 
^m  ( 1 ... 6 ) )  |->  ( e `  4 ) )  e.  (mzPoly `  ( 1 ... 6
) ) )  -> 
( e  e.  ( ZZ  ^m  ( 1 ... 6 ) ) 
|->  ( 2  x.  (
e `  4 )
) )  e.  (mzPoly `  ( 1 ... 6
) ) )
216212, 214, 215mp2an 653 . . . . . . . . . . . . 13  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  ( 2  x.  ( e ` 
4 ) ) )  e.  (mzPoly `  (
1 ... 6 ) )
217 mzpmulmpt 26820 . . . . . . . . . . . . 13  |-  ( ( ( e  e.  ( ZZ  ^m  ( 1 ... 6 ) ) 
|->  ( 2  x.  (
e `  4 )
) )  e.  (mzPoly `  ( 1 ... 6
) )  /\  (
e  e.  ( ZZ 
^m  ( 1 ... 6 ) )  |->  ( e `  1 ) )  e.  (mzPoly `  ( 1 ... 6
) ) )  -> 
( e  e.  ( ZZ  ^m  ( 1 ... 6 ) ) 
|->  ( ( 2  x.  ( e `  4
) )  x.  (
e `  1 )
) )  e.  (mzPoly `  ( 1 ... 6
) ) )
218216, 105, 217mp2an 653 . . . . . . . . . . . 12  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  ( ( 2  x.  ( e `
 4 ) )  x.  ( e ` 
1 ) ) )  e.  (mzPoly `  (
1 ... 6 ) )
219 2nn0 9982 . . . . . . . . . . . . 13  |-  2  e.  NN0
220 mzpexpmpt 26823 . . . . . . . . . . . . 13  |-  ( ( ( e  e.  ( ZZ  ^m  ( 1 ... 6 ) ) 
|->  ( e `  1
) )  e.  (mzPoly `  ( 1 ... 6
) )  /\  2  e.  NN0 )  ->  (
e  e.  ( ZZ 
^m  ( 1 ... 6 ) )  |->  ( ( e `  1
) ^ 2 ) )  e.  (mzPoly `  ( 1 ... 6
) ) )
221105, 219, 220mp2an 653 . . . . . . . . . . . 12  |-  ( e  e.  ( ZZ  ^m  (