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

Theorem expdiophlem2 26777
Description: Lemma for expdioph 26778. 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 6967 . . . . 5  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  a : ( 1 ... 3 ) --> NN0 )
2 3nn 10059 . . . . . 6  |-  3  e.  NN
32jm2.27dlem3 26766 . . . . 5  |-  3  e.  ( 1 ... 3
)
4 ffvelrn 5800 . . . . 5  |-  ( ( a : ( 1 ... 3 ) --> NN0 
/\  3  e.  ( 1 ... 3 ) )  ->  ( a `  3 )  e. 
NN0 )
51, 3, 4sylancl 644 . . . 4  |-  ( a  e.  ( NN0  ^m  ( 1 ... 3
) )  ->  (
a `  3 )  e.  NN0 )
6 expdiophlem1 26776 . . . 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 16 . . 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 2882 . 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 10164 . . 3  |-  3  e.  NN0
10 fvex 5675 . . . . . . . . . 10  |-  ( e `
 5 )  e. 
_V
11 fvex 5675 . . . . . . . . . 10  |-  ( e `
 6 )  e. 
_V
12 eqeq1 2386 . . . . . . . . . . . . . . 15  |-  ( c  =  ( e ` 
5 )  ->  (
c  =  ( b Yrm  ( a `  2 ) )  <->  ( e ` 
5 )  =  ( b Yrm  ( a `  2
) ) ) )
1312anbi2d 685 . . . . . . . . . . . . . 14  |-  ( c  =  ( e ` 
5 )  ->  (
( b  e.  (
ZZ>= `  2 )  /\  c  =  ( b Yrm  ( a `  2 ) ) )  <->  ( b  e.  ( ZZ>= `  2 )  /\  ( e `  5
)  =  ( b Yrm  ( a `  2 ) ) ) ) )
1413adantr 452 . . . . . . . . . . . . 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 ) ) ) ) )
15 eqeq1 2386 . . . . . . . . . . . . . . . 16  |-  ( d  =  ( e ` 
6 )  ->  (
d  =  ( b Xrm  ( a `  2 ) )  <->  ( e ` 
6 )  =  ( b Xrm  ( a `  2
) ) ) )
1615anbi2d 685 . . . . . . . . . . . . . . 15  |-  ( d  =  ( e ` 
6 )  ->  (
( b  e.  (
ZZ>= `  2 )  /\  d  =  ( b Xrm  ( a `  2 ) ) )  <->  ( b  e.  ( ZZ>= `  2 )  /\  ( e `  6
)  =  ( b Xrm  ( a `  2 ) ) ) ) )
1716adantl 453 . . . . . . . . . . . . . 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 ) ) ) ) )
18 simpr 448 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  d  =  ( e `  6 ) )
19 oveq2 6021 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  ( e ` 
5 )  ->  (
( b  -  (
a `  1 )
)  x.  c )  =  ( ( b  -  ( a ` 
1 ) )  x.  ( e `  5
) ) )
2019adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  ( ( b  -  ( a ` 
1 ) )  x.  c )  =  ( ( b  -  (
a `  1 )
)  x.  ( e `
 5 ) ) )
2118, 20oveq12d 6031 . . . . . . . . . . . . . . . . 17  |-  ( ( c  =  ( e `
 5 )  /\  d  =  ( e `  6 ) )  ->  ( d  -  ( ( b  -  ( a `  1
) )  x.  c
) )  =  ( ( e `  6
)  -  ( ( b  -  ( a `
 1 ) )  x.  ( e ` 
5 ) ) ) )
2221oveq1d 6028 . . . . . . . . . . . . . . . 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 ) ) )
2322breq2d 4158 . . . . . . . . . . . . . . 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 ) ) ) )
2423anbi2d 685 . . . . . . . . . . . . . 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 )
) ) ) )
2517, 24anbi12d 692 . . . . . . . . . . . . 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 ) ) ) ) ) )
2614, 25anbi12d 692 . . . . . . . . . . . 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 )
) ) ) ) ) )
2726anbi2d 685 . . . . . . . . . . 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
) ) ) ) ) ) ) )
2827anbi2d 685 . . . . . . . . . 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 )
) ) ) ) ) ) ) )
2910, 11, 28sbc2ie 3164 . . . . . . . . 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 ) ) ) ) ) ) ) )
3029sbcbii 3152 . . . . . . . 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 ) ) ) ) ) ) ) )
3130sbcbii 3152 . . . . . . 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 )
) ) ) ) ) ) )
32 vex 2895 . . . . . . . . 9  |-  e  e. 
_V
3332resex 5119 . . . . . . . 8  |-  ( e  |`  ( 1 ... 3
) )  e.  _V
34 fvex 5675 . . . . . . . 8  |-  ( e `
 4 )  e. 
_V
35 df-2 9983 . . . . . . . . . . . . . . 15  |-  2  =  ( 1  +  1 )
36 df-3 9984 . . . . . . . . . . . . . . . 16  |-  3  =  ( 2  +  1 )
37 ssid 3303 . . . . . . . . . . . . . . . 16  |-  ( 1 ... 3 )  C_  ( 1 ... 3
)
3836, 37jm2.27dlem5 26768 . . . . . . . . . . . . . . 15  |-  ( 1 ... 2 )  C_  ( 1 ... 3
)
3935, 38jm2.27dlem5 26768 . . . . . . . . . . . . . 14  |-  ( 1 ... 1 )  C_  ( 1 ... 3
)
40 1nn 9936 . . . . . . . . . . . . . . 15  |-  1  e.  NN
4140jm2.27dlem3 26766 . . . . . . . . . . . . . 14  |-  1  e.  ( 1 ... 1
)
4239, 41sselii 3281 . . . . . . . . . . . . 13  |-  1  e.  ( 1 ... 3
)
4342jm2.27dlem1 26764 . . . . . . . . . . . 12  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
a `  1 )  =  ( e ` 
1 ) )
4443eleq1d 2446 . . . . . . . . . . 11  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
( a `  1
)  e.  ( ZZ>= ` 
2 )  <->  ( e `  1 )  e.  ( ZZ>= `  2 )
) )
45 2nn 10058 . . . . . . . . . . . . . . 15  |-  2  e.  NN
4645jm2.27dlem3 26766 . . . . . . . . . . . . . 14  |-  2  e.  ( 1 ... 2
)
4746, 36, 45jm2.27dlem2 26765 . . . . . . . . . . . . 13  |-  2  e.  ( 1 ... 3
)
4847jm2.27dlem1 26764 . . . . . . . . . . . 12  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
a `  2 )  =  ( e ` 
2 ) )
4948eleq1d 2446 . . . . . . . . . . 11  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
( a `  2
)  e.  NN  <->  ( e `  2 )  e.  NN ) )
5044, 49anbi12d 692 . . . . . . . . . 10  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( a `  2
)  e.  NN )  <-> 
( ( e ` 
1 )  e.  (
ZZ>= `  2 )  /\  ( e `  2
)  e.  NN ) ) )
5150adantr 452 . . . . . . . . 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 452 . . . . . . . . . . 11  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( a ` 
1 )  e.  (
ZZ>= `  2 )  <->  ( e `  1 )  e.  ( ZZ>= `  2 )
) )
53 id 20 . . . . . . . . . . . 12  |-  ( b  =  ( e ` 
4 )  ->  b  =  ( e ` 
4 ) )
5448oveq1d 6028 . . . . . . . . . . . . 13  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
( a `  2
)  +  1 )  =  ( ( e `
 2 )  +  1 ) )
5543, 54oveq12d 6031 . . . . . . . . . . . 12  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
( a `  1
) Yrm  ( ( a ` 
2 )  +  1 ) )  =  ( ( e `  1
) Yrm  ( ( e ` 
2 )  +  1 ) ) )
5653, 55eqeqan12rd 2396 . . . . . . . . . . 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 692 . . . . . . . . . 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 2440 . . . . . . . . . . . . 13  |-  ( b  =  ( e ` 
4 )  ->  (
b  e.  ( ZZ>= ` 
2 )  <->  ( e `  4 )  e.  ( ZZ>= `  2 )
) )
5958adantl 453 . . . . . . . . . . . 12  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( b  e.  (
ZZ>= `  2 )  <->  ( e `  4 )  e.  ( ZZ>= `  2 )
) )
6053, 48oveqan12rd 6033 . . . . . . . . . . . . 13  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( b Yrm  ( a ` 
2 ) )  =  ( ( e ` 
4 ) Yrm  ( e ` 
2 ) ) )
6160eqeq2d 2391 . . . . . . . . . . . 12  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( e ` 
5 )  =  ( b Yrm  ( a `  2
) )  <->  ( e `  5 )  =  ( ( e ` 
4 ) Yrm  ( e ` 
2 ) ) ) )
6259, 61anbi12d 692 . . . . . . . . . . 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 6033 . . . . . . . . . . . . . 14  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( b Xrm  ( a ` 
2 ) )  =  ( ( e ` 
4 ) Xrm  ( e ` 
2 ) ) )
6463eqeq2d 2391 . . . . . . . . . . . . 13  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( e ` 
6 )  =  ( b Xrm  ( a `  2
) )  <->  ( e `  6 )  =  ( ( e ` 
4 ) Xrm  ( e ` 
2 ) ) ) )
6559, 64anbi12d 692 . . . . . . . . . . . 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 26764 . . . . . . . . . . . . . . 15  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
a `  3 )  =  ( e ` 
3 ) )
6766adantr 452 . . . . . . . . . . . . . 14  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( a `  3
)  =  ( e `
 3 ) )
68 oveq2 6021 . . . . . . . . . . . . . . . . 17  |-  ( b  =  ( e ` 
4 )  ->  (
2  x.  b )  =  ( 2  x.  ( e `  4
) ) )
6968, 43oveqan12rd 6033 . . . . . . . . . . . . . . . 16  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( 2  x.  b )  x.  (
a `  1 )
)  =  ( ( 2  x.  ( e `
 4 ) )  x.  ( e ` 
1 ) ) )
7043oveq1d 6028 . . . . . . . . . . . . . . . . 17  |-  ( a  =  ( e  |`  ( 1 ... 3
) )  ->  (
( a `  1
) ^ 2 )  =  ( ( e `
 1 ) ^
2 ) )
7170adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( a ` 
1 ) ^ 2 )  =  ( ( e `  1 ) ^ 2 ) )
7269, 71oveq12d 6031 . . . . . . . . . . . . . . 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 6028 . . . . . . . . . . . . . 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 4159 . . . . . . . . . . . . 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 448 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
b  =  ( e `
 4 ) )
7643adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( a `  1
)  =  ( e `
 1 ) )
7775, 76oveq12d 6031 . . . . . . . . . . . . . . . . 17  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( b  -  (
a `  1 )
)  =  ( ( e `  4 )  -  ( e ` 
1 ) ) )
7877oveq1d 6028 . . . . . . . . . . . . . . . 16  |-  ( ( a  =  ( e  |`  ( 1 ... 3
) )  /\  b  =  ( e ` 
4 ) )  -> 
( ( b  -  ( a `  1
) )  x.  (
e `  5 )
)  =  ( ( ( e `  4
)  -  ( e `
 1 ) )  x.  ( e ` 
5 ) ) )
7978oveq2d 6029 . . . . . . . . . . . . . . 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 6031 . . . . . . . . . . . . . 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 4159 . . . . . . . . . . . . 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 692 . . . . . . . . . . . 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 692 . . . . . . . . . . 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 692 . . . . . . . . . 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 692 . . . . . . . . 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 692 . . . . . . . 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 )
) ) ) ) ) ) ) )
8733, 34, 86sbc2ie 3164 . . . . . . 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 ) ) ) ) ) ) ) )
8831, 87bitri 241 . . . . . 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 11 . . . . 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 2882 . . . 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 10167 . . . . . . 7  |-  6  e.  NN0
92 2z 10237 . . . . . . 7  |-  2  e.  ZZ
93 ovex 6038 . . . . . . . 8  |-  ( 1 ... 6 )  e. 
_V
94 df-4 9985 . . . . . . . . . . . 12  |-  4  =  ( 3  +  1 )
95 df-5 9986 . . . . . . . . . . . . 13  |-  5  =  ( 4  +  1 )
96 df-6 9987 . . . . . . . . . . . . . 14  |-  6  =  ( 5  +  1 )
97 ssid 3303 . . . . . . . . . . . . . 14  |-  ( 1 ... 6 )  C_  ( 1 ... 6
)
9896, 97jm2.27dlem5 26768 . . . . . . . . . . . . 13  |-  ( 1 ... 5 )  C_  ( 1 ... 6
)
9995, 98jm2.27dlem5 26768 . . . . . . . . . . . 12  |-  ( 1 ... 4 )  C_  ( 1 ... 6
)
10094, 99jm2.27dlem5 26768 . . . . . . . . . . 11  |-  ( 1 ... 3 )  C_  ( 1 ... 6
)
10136, 100jm2.27dlem5 26768 . . . . . . . . . 10  |-  ( 1 ... 2 )  C_  ( 1 ... 6
)
10235, 101jm2.27dlem5 26768 . . . . . . . . 9  |-  ( 1 ... 1 )  C_  ( 1 ... 6
)
103102, 41sselii 3281 . . . . . . . 8  |-  1  e.  ( 1 ... 6
)
104 mzpproj 26478 . . . . . . . 8  |-  ( ( ( 1 ... 6
)  e.  _V  /\  1  e.  ( 1 ... 6 ) )  ->  ( e  e.  ( ZZ  ^m  (
1 ... 6 ) ) 
|->  ( e `  1
) )  e.  (mzPoly `  ( 1 ... 6
) ) )
10593, 103, 104mp2an 654 . . . . . . 7  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  ( e `
 1 ) )  e.  (mzPoly `  (
1 ... 6 ) )
106 eluzrabdioph 26550 . . . . . . 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 1279 . . . . . 6  |-  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  ( e `  1 )  e.  ( ZZ>= `  2
) }  e.  (Dioph `  6 )
108101, 46sselii 3281 . . . . . . . 8  |-  2  e.  ( 1 ... 6
)
109 mzpproj 26478 . . . . . . . 8  |-  ( ( ( 1 ... 6
)  e.  _V  /\  2  e.  ( 1 ... 6 ) )  ->  ( e  e.  ( ZZ  ^m  (
1 ... 6 ) ) 
|->  ( e `  2
) )  e.  (mzPoly `  ( 1 ... 6
) ) )
11093, 108, 109mp2an 654 . . . . . . 7  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  ( e `
 2 ) )  e.  (mzPoly `  (
1 ... 6 ) )
111 elnnrabdioph 26551 . . . . . . 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 654 . . . . . 6  |-  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  ( e `  2 )  e.  NN }  e.  (Dioph `  6 )
113 anrabdioph 26523 . . . . . 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 654 . . . . 5  |-  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  ( ( e `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  2 )  e.  NN ) }  e.  (Dioph `  6 )
115 elmapi 6967 . . . . . . . . . . 11  |-  ( e  e.  ( NN0  ^m  ( 1 ... 6
) )  ->  e : ( 1 ... 6 ) --> NN0 )
116 ffvelrn 5800 . . . . . . . . . . 11  |-  ( ( e : ( 1 ... 6 ) --> NN0 
/\  2  e.  ( 1 ... 6 ) )  ->  ( e `  2 )  e. 
NN0 )
117115, 108, 116sylancl 644 . . . . . . . . . 10  |-  ( e  e.  ( NN0  ^m  ( 1 ... 6
) )  ->  (
e `  2 )  e.  NN0 )
118 peano2nn0 10185 . . . . . . . . . 10  |-  ( ( e `  2 )  e.  NN0  ->  ( ( e `  2 )  +  1 )  e. 
NN0 )
119 oveq2 6021 . . . . . . . . . . . . 13  |-  ( b  =  ( ( e `
 2 )  +  1 )  ->  (
( e `  1
) Yrm  b )  =  ( ( e `  1
) Yrm  ( ( e ` 
2 )  +  1 ) ) )
120119eqeq2d 2391 . . . . . . . . . . . 12  |-  ( b  =  ( ( e `
 2 )  +  1 )  ->  (
( e `  4
)  =  ( ( e `  1 ) Yrm  b )  <->  ( e ` 
4 )  =  ( ( e `  1
) Yrm  ( ( e ` 
2 )  +  1 ) ) ) )
121120anbi2d 685 . . . . . . . . . . 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 3005 . . . . . . . . . 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 19 . . . . . . . . 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 193 . . . . . . . 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 2882 . . . . . . 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 2895 . . . . . . . . . . . . 13  |-  a  e. 
_V
127126resex 5119 . . . . . . . . . . . 12  |-  ( a  |`  ( 1 ... 6
) )  e.  _V
128 fvex 5675 . . . . . . . . . . . 12  |-  ( a `
 7 )  e. 
_V
129 id 20 . . . . . . . . . . . . . 14  |-  ( b  =  ( a ` 
7 )  ->  b  =  ( a ` 
7 ) )
130108jm2.27dlem1 26764 . . . . . . . . . . . . . . 15  |-  ( e  =  ( a  |`  ( 1 ... 6
) )  ->  (
e `  2 )  =  ( a ` 
2 ) )
131130oveq1d 6028 . . . . . . . . . . . . . 14  |-  ( e  =  ( a  |`  ( 1 ... 6
) )  ->  (
( e `  2
)  +  1 )  =  ( ( a `
 2 )  +  1 ) )
132129, 131eqeqan12rd 2396 . . . . . . . . . . . . 13  |-  ( ( e  =  ( a  |`  ( 1 ... 6
) )  /\  b  =  ( a ` 
7 ) )  -> 
( b  =  ( ( e `  2
)  +  1 )  <-> 
( a `  7
)  =  ( ( a `  2 )  +  1 ) ) )
133103jm2.27dlem1 26764 . . . . . . . . . . . . . . . 16  |-  ( e  =  ( a  |`  ( 1 ... 6
) )  ->  (
e `  1 )  =  ( a ` 
1 ) )
134133adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( e  =  ( a  |`  ( 1 ... 6
) )  /\  b  =  ( a ` 
7 ) )  -> 
( e `  1
)  =  ( a `
 1 ) )
135134eleq1d 2446 . . . . . . . . . . . . . 14  |-  ( ( e  =  ( a  |`  ( 1 ... 6
) )  /\  b  =  ( a ` 
7 ) )  -> 
( ( e ` 
1 )  e.  (
ZZ>= `  2 )  <->  ( a `  1 )  e.  ( ZZ>= `  2 )
) )
136 4nn 10060 . . . . . . . . . . . . . . . . . . 19  |-  4  e.  NN
137136jm2.27dlem3 26766 . . . . . . . . . . . . . . . . . 18  |-  4  e.  ( 1 ... 4
)
13899, 137sselii 3281 . . . . . . . . . . . . . . . . 17  |-  4  e.  ( 1 ... 6
)
139138jm2.27dlem1 26764 . . . . . . . . . . . . . . . 16  |-  ( e  =  ( a  |`  ( 1 ... 6
) )  ->  (
e `  4 )  =  ( a ` 
4 ) )
140139adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( e  =  ( a  |`  ( 1 ... 6
) )  /\  b  =  ( a ` 
7 ) )  -> 
( e `  4
)  =  ( a `
 4 ) )
141133, 129oveqan12d 6032 . . . . . . . . . . . . . . 15  |-  ( ( e  =  ( a  |`  ( 1 ... 6
) )  /\  b  =  ( a ` 
7 ) )  -> 
( ( e ` 
1 ) Yrm  b )  =  ( ( a ` 
1 ) Yrm  ( a ` 
7 ) ) )
142140, 141eqeq12d 2394 . . . . . . . . . . . . . 14  |-  ( ( e  =  ( a  |`  ( 1 ... 6
) )  /\  b  =  ( a ` 
7 ) )  -> 
( ( e ` 
4 )  =  ( ( e `  1
) Yrm  b )  <->  ( a `  4 )  =  ( ( a ` 
1 ) Yrm  ( a ` 
7 ) ) ) )
143135, 142anbi12d 692 . . . . . . . . . . . . 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 692 . . . . . . . . . . . 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 3164 . . . . . . . . . . 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 11 . . . . . . . . . 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 2882 . . . . . . . . 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 10168 . . . . . . . . . . 11  |-  7  e.  NN0
149 ovex 6038 . . . . . . . . . . . 12  |-  ( 1 ... 7 )  e. 
_V
150 7nn 10063 . . . . . . . . . . . . 13  |-  7  e.  NN
151150jm2.27dlem3 26766 . . . . . . . . . . . 12  |-  7  e.  ( 1 ... 7
)
152 mzpproj 26478 . . . . . . . . . . . 12  |-  ( ( ( 1 ... 7
)  e.  _V  /\  7  e.  ( 1 ... 7 ) )  ->  ( a  e.  ( ZZ  ^m  (
1 ... 7 ) ) 
|->  ( a `  7
) )  e.  (mzPoly `  ( 1 ... 7
) ) )
153149, 151, 152mp2an 654 . . . . . . . . . . 11  |-  ( a  e.  ( ZZ  ^m  ( 1 ... 7
) )  |->  ( a `
 7 ) )  e.  (mzPoly `  (
1 ... 7 ) )
154 df-7 9988 . . . . . . . . . . . . . 14  |-  7  =  ( 6  +  1 )
155 6nn 10062 . . . . . . . . . . . . . 14  |-  6  e.  NN
156108, 154, 155jm2.27dlem2 26765 . . . . . . . . . . . . 13  |-  2  e.  ( 1 ... 7
)
157 mzpproj 26478 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... 7
)  e.  _V  /\  2  e.  ( 1 ... 7 ) )  ->  ( a  e.  ( ZZ  ^m  (
1 ... 7 ) ) 
|->  ( a `  2
) )  e.  (mzPoly `  ( 1 ... 7
) ) )
158149, 156, 157mp2an 654 . . . . . . . . . . . 12  |-  ( a  e.  ( ZZ  ^m  ( 1 ... 7
) )  |->  ( a `
 2 ) )  e.  (mzPoly `  (
1 ... 7 ) )
159 1z 10236 . . . . . . . . . . . . 13  |-  1  e.  ZZ
160 mzpconstmpt 26481 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... 7
)  e.  _V  /\  1  e.  ZZ )  ->  ( a  e.  ( ZZ  ^m  ( 1 ... 7 ) ) 
|->  1 )  e.  (mzPoly `  ( 1 ... 7
) ) )
161149, 159, 160mp2an 654 . . . . . . . . . . . 12  |-  ( a  e.  ( ZZ  ^m  ( 1 ... 7
) )  |->  1 )  e.  (mzPoly `  (
1 ... 7 ) )
162 mzpaddmpt 26482 . . . . . . . . . . . 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 654 . . . . . . . . . . 11  |-  ( a  e.  ( ZZ  ^m  ( 1 ... 7
) )  |->  ( ( a `  2 )  +  1 ) )  e.  (mzPoly `  (
1 ... 7 ) )
164 eqrabdioph 26520 . . . . . . . . . . 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 1279 . . . . . . . . . 10  |-  { a  e.  ( NN0  ^m  ( 1 ... 7
) )  |  ( a `  7 )  =  ( ( a `
 2 )  +  1 ) }  e.  (Dioph `  7 )
166 rmydioph 26769 . . . . . . . . . . 11  |-  { b  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( ( b `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
b `  3 )  =  ( ( b `
 1 ) Yrm  ( b `
 2 ) ) ) }  e.  (Dioph `  3 )
167 simp1 957 . . . . . . . . . . . . . 14  |-  ( ( ( b `  1
)  =  ( a `
 1 )  /\  ( b `  2
)  =  ( a `
 7 )  /\  ( b `  3
)  =  ( a `
 4 ) )  ->  ( b ` 
1 )  =  ( a `  1 ) )
168167eleq1d 2446 . . . . . . . . . . . . 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 959 . . . . . . . . . . . . . 14  |-  ( ( ( b `  1
)  =  ( a `
 1 )  /\  ( b `  2
)  =  ( a `
 7 )  /\  ( b `  3
)  =  ( a `
 4 ) )  ->  ( b ` 
3 )  =  ( a `  4 ) )
170 simp2 958 . . . . . . . . . . . . . . 15  |-  ( ( ( b `  1
)  =  ( a `
 1 )  /\  ( b `  2
)  =  ( a `
 7 )  /\  ( b `  3
)  =  ( a `
 4 ) )  ->  ( b ` 
2 )  =  ( a `  7 ) )
171167, 170oveq12d 6031 . . . . . . . . . . . . . 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 2394 . . . . . . . . . . . . 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 692 . . . . . . . . . . . 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 26765 . . . . . . . . . . . 12  |-  1  e.  ( 1 ... 7
)
175138, 154, 155jm2.27dlem2 26765 . . . . . . . . . . . 12  |-  4  e.  ( 1 ... 7
)
176173, 174, 151, 175rabren3dioph 26560 . . . . . . . . . . 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 654 . . . . . . . . . 10  |-  { a  e.  ( NN0  ^m  ( 1 ... 7
) )  |  ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  4 )  =  ( ( a `
 1 ) Yrm  ( a `
 7 ) ) ) }  e.  (Dioph `  7 )
178 anrabdioph 26523 . . . . . . . . . 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 654 . . . . . . . . 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 2450 . . . . . . . 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 26539 . . . . . . . 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 654 . . . . . . 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 2450 . . . . . 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 26769 . . . . . . . 8  |-  { a  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  3 )  =  ( ( a `
 1 ) Yrm  ( a `
 2 ) ) ) }  e.  (Dioph `  3 )
185 simp1 957 . . . . . . . . . . 11  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 5 ) )  ->  ( a ` 
1 )  =  ( e `  4 ) )
186185eleq1d 2446 . . . . . . . . . 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 959 . . . . . . . . . . 11  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 5 ) )  ->  ( a ` 
3 )  =  ( e `  5 ) )
188 simp2 958 . . . . . . . . . . . 12  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 5 ) )  ->  ( a ` 
2 )  =  ( e `  2 ) )
189185, 188oveq12d 6031 . . . . . . . . . . 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 2394 . . . . . . . . . 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 692 . . . . . . . . 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 10061 . . . . . . . . . . 11  |-  5  e.  NN
193192jm2.27dlem3 26766 . . . . . . . . . 10  |-  5  e.  ( 1 ... 5
)
194193, 96, 192jm2.27dlem2 26765 . . . . . . . . 9  |-  5  e.  ( 1 ... 6
)
195191, 138, 108, 194rabren3dioph 26560 . . . . . . . 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 654 . . . . . . 7  |-  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  ( ( e `  4
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  5 )  =  ( ( e `
 4 ) Yrm  ( e `
 2 ) ) ) }  e.  (Dioph `  6 )
197 rmxdioph 26771 . . . . . . . . 9  |-  { a  e.  ( NN0  ^m  ( 1 ... 3
) )  |  ( ( a `  1
)  e.  ( ZZ>= ` 
2 )  /\  (
a `  3 )  =  ( ( a `
 1 ) Xrm  ( a `
 2 ) ) ) }  e.  (Dioph `  3 )
198 simp1 957 . . . . . . . . . . . 12  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 6 ) )  ->  ( a ` 
1 )  =  ( e `  4 ) )
199198eleq1d 2446 . . . . . . . . . . 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 959 . . . . . . . . . . . 12  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 6 ) )  ->  ( a ` 
3 )  =  ( e `  6 ) )
201 simp2 958 . . . . . . . . . . . . 13  |-  ( ( ( a `  1
)  =  ( e `
 4 )  /\  ( a `  2
)  =  ( e `
 2 )  /\  ( a `  3
)  =  ( e `
 6 ) )  ->  ( a ` 
2 )  =  ( e `  2 ) )
202198, 201oveq12d 6031 . . . . . . . . . . . 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 2394 . . . . . . . . . . 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 692 . . . . . . . . . 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 26766 . . . . . . . . . 10  |-  6  e.  ( 1 ... 6
)
206204, 138, 108, 205rabren3dioph 26560 . . . . . . . . 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 654 . . . . . . . 8  |-  { e  e.  ( NN0  ^m  ( 1 ... 6
) )  |  ( ( e `  4
)  e.  ( ZZ>= ` 
2 )  /\  (
e `  6 )  =  ( ( e `
 4 ) Xrm  ( e `
 2 ) ) ) }  e.  (Dioph `  6 )
208100, 3sselii 3281 . . . . . . . . . . 11  |-  3  e.  ( 1 ... 6
)
209 mzpproj 26478 . . . . . . . . . . 11  |-  ( ( ( 1 ... 6
)  e.  _V  /\  3  e.  ( 1 ... 6 ) )  ->  ( e  e.  ( ZZ  ^m  (
1 ... 6 ) ) 
|->  ( e `  3
) )  e.  (mzPoly `  ( 1 ... 6
) ) )
21093, 208, 209mp2an 654 . . . . . . . . . 10  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  ( e `
 3 ) )  e.  (mzPoly `  (
1 ... 6 ) )
211 mzpconstmpt 26481 . . . . . . . . . . . . . . 15  |-  ( ( ( 1 ... 6
)  e.  _V  /\  2  e.  ZZ )  ->  ( e  e.  ( ZZ  ^m  ( 1 ... 6 ) ) 
|->  2 )  e.  (mzPoly `  ( 1 ... 6
) ) )
21293, 92, 211mp2an 654 . . . . . . . . . . . . . 14  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  2 )  e.  (mzPoly `  (
1 ... 6 ) )
213 mzpproj 26478 . . . . . . . . . . . . . . 15  |-  ( ( ( 1 ... 6
)  e.  _V  /\  4  e.  ( 1 ... 6 ) )  ->  ( e  e.  ( ZZ  ^m  (
1 ... 6 ) ) 
|->  ( e `  4
) )  e.  (mzPoly `  ( 1 ... 6
) ) )
21493, 138, 213mp2an 654 . . . . . . . . . . . . . 14  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  ( e `
 4 ) )  e.  (mzPoly `  (
1 ... 6 ) )
215 mzpmulmpt 26483 . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . 13  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  ( 2  x.  ( e ` 
4 ) ) )  e.  (mzPoly `  (
1 ... 6 ) )
217 mzpmulmpt 26483 . . . . . . . . . . . . 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 654 . . . . . . . . . . . 12  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  ( ( 2  x.  ( e `
 4 ) )  x.  ( e ` 
1 ) ) )  e.  (mzPoly `  (
1 ... 6 ) )
219 2nn0 10163 . . . . . . . . . . . . 13  |-  2  e.  NN0
220 mzpexpmpt 26486 . . . . . . . . . . . . 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 654 . . . . . . . . . . . 12  |-  ( e  e.  ( ZZ  ^m  ( 1 ... 6
) )  |->  ( ( e `  1 ) ^ 2 ) )  e.  (mzPoly `  (
1 ... 6 ) )
222 mzpsubmpt 26484 . . . . . . . . . . . 12  |-  ( ( (