Metamath Proof Explorer

Theorem expdiophlem2

Description: Lemma for expdioph . Exponentiation on a restricted domain is Diophantine. (Contributed by Stefan O'Rear, 17-Oct-2014)

Ref Expression
Assertion 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

Step Hyp Ref Expression
1 elmapi 
 |-  ( a e. ( NN0 ^m ( 1 ... 3 ) ) -> a : ( 1 ... 3 ) --> NN0 )
2 3nn 
 |-  3 e. NN
3 2 jm2.27dlem3 
 |-  3 e. ( 1 ... 3 )
4 ffvelcdm 
 |-  ( ( a : ( 1 ... 3 ) --> NN0 /\ 3 e. ( 1 ... 3 ) ) -> ( a ` 3 ) e. NN0 )
5 1 3 4 sylancl 
 |-  ( a e. ( NN0 ^m ( 1 ... 3 ) ) -> ( a ` 3 ) e. NN0 )
6 expdiophlem1 
 |-  ( ( 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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 ) ) ) ) ) ) ) ) )
7 5 6 syl 
 |-  ( 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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 ) ) ) ) ) ) ) ) )
8 7 rabbiia 
 |-  { 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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 
 |-  3 e. NN0
10 fvex 
 |-  ( e ` 5 ) e. _V
11 fvex 
 |-  ( e ` 6 ) e. _V
12 eqeq1 
 |-  ( c = ( e ` 5 ) -> ( c = ( b rmY ( a ` 2 ) ) <-> ( e ` 5 ) = ( b rmY ( a ` 2 ) ) ) )
13 12 anbi2d 
 |-  ( c = ( e ` 5 ) -> ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) <-> ( b e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( b rmY ( a ` 2 ) ) ) ) )
14 13 adantr 
 |-  ( ( c = ( e ` 5 ) /\ d = ( e ` 6 ) ) -> ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) <-> ( b e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( b rmY ( a ` 2 ) ) ) ) )
15 eqeq1 
 |-  ( d = ( e ` 6 ) -> ( d = ( b rmX ( a ` 2 ) ) <-> ( e ` 6 ) = ( b rmX ( a ` 2 ) ) ) )
16 15 anbi2d 
 |-  ( d = ( e ` 6 ) -> ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( a ` 2 ) ) ) <-> ( b e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( b rmX ( a ` 2 ) ) ) ) )
17 16 adantl 
 |-  ( ( c = ( e ` 5 ) /\ d = ( e ` 6 ) ) -> ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( a ` 2 ) ) ) <-> ( b e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( b rmX ( a ` 2 ) ) ) ) )
18 simpr 
 |-  ( ( c = ( e ` 5 ) /\ d = ( e ` 6 ) ) -> d = ( e ` 6 ) )
19 oveq2 
 |-  ( c = ( e ` 5 ) -> ( ( b - ( a ` 1 ) ) x. c ) = ( ( b - ( a ` 1 ) ) x. ( e ` 5 ) ) )
20 19 adantr 
 |-  ( ( c = ( e ` 5 ) /\ d = ( e ` 6 ) ) -> ( ( b - ( a ` 1 ) ) x. c ) = ( ( b - ( a ` 1 ) ) x. ( e ` 5 ) ) )
21 18 20 oveq12d 
 |-  ( ( c = ( e ` 5 ) /\ d = ( e ` 6 ) ) -> ( d - ( ( b - ( a ` 1 ) ) x. c ) ) = ( ( e ` 6 ) - ( ( b - ( a ` 1 ) ) x. ( e ` 5 ) ) ) )
22 21 oveq1d 
 |-  ( ( c = ( e ` 5 ) /\ d = ( e ` 6 ) ) -> ( ( d - ( ( b - ( a ` 1 ) ) x. c ) ) - ( a ` 3 ) ) = ( ( ( e ` 6 ) - ( ( b - ( a ` 1 ) ) x. ( e ` 5 ) ) ) - ( a ` 3 ) ) )
23 22 breq2d 
 |-  ( ( 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 ) ) ) )
24 23 anbi2d 
 |-  ( ( 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 ) ) ) ) )
25 17 24 anbi12d 
 |-  ( ( c = ( e ` 5 ) /\ d = ( e ` 6 ) ) -> ( ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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 rmX ( 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 ) ) ) ) ) )
26 14 25 anbi12d 
 |-  ( ( c = ( e ` 5 ) /\ d = ( e ` 6 ) ) -> ( ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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 rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( b rmX ( 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 ) ) ) ) ) ) )
27 26 anbi2d 
 |-  ( ( c = ( e ` 5 ) /\ d = ( e ` 6 ) ) -> ( ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( b rmX ( 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 ) ) ) ) ) ) ) )
28 27 anbi2d 
 |-  ( ( c = ( e ` 5 ) /\ d = ( e ` 6 ) ) -> ( ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 2 ) e. NN ) /\ ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( b rmX ( 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 ) ) ) ) ) ) ) ) )
29 10 11 28 sbc2ie 
 |-  ( [. ( e ` 5 ) / c ]. [. ( e ` 6 ) / d ]. ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 2 ) e. NN ) /\ ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( b rmX ( 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 ) ) ) ) ) ) ) )
30 29 sbcbii 
 |-  ( [. ( 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( b rmX ( 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 ) ) ) ) ) ) ) )
31 30 sbcbii 
 |-  ( [. ( 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( b rmX ( 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 
 |-  e e. _V
33 32 resex 
 |-  ( e |` ( 1 ... 3 ) ) e. _V
34 fvex 
 |-  ( e ` 4 ) e. _V
35 df-2 
 |-  2 = ( 1 + 1 )
36 df-3 
 |-  3 = ( 2 + 1 )
37 ssid 
 |-  ( 1 ... 3 ) C_ ( 1 ... 3 )
38 36 37 jm2.27dlem5 
 |-  ( 1 ... 2 ) C_ ( 1 ... 3 )
39 35 38 jm2.27dlem5 
 |-  ( 1 ... 1 ) C_ ( 1 ... 3 )
40 1nn 
 |-  1 e. NN
41 40 jm2.27dlem3 
 |-  1 e. ( 1 ... 1 )
42 39 41 sselii 
 |-  1 e. ( 1 ... 3 )
43 42 jm2.27dlem1 
 |-  ( a = ( e |` ( 1 ... 3 ) ) -> ( a ` 1 ) = ( e ` 1 ) )
44 43 eleq1d 
 |-  ( a = ( e |` ( 1 ... 3 ) ) -> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) <-> ( e ` 1 ) e. ( ZZ>= ` 2 ) ) )
45 2nn 
 |-  2 e. NN
46 45 jm2.27dlem3 
 |-  2 e. ( 1 ... 2 )
47 46 36 45 jm2.27dlem2 
 |-  2 e. ( 1 ... 3 )
48 47 jm2.27dlem1 
 |-  ( a = ( e |` ( 1 ... 3 ) ) -> ( a ` 2 ) = ( e ` 2 ) )
49 48 eleq1d 
 |-  ( a = ( e |` ( 1 ... 3 ) ) -> ( ( a ` 2 ) e. NN <-> ( e ` 2 ) e. NN ) )
50 44 49 anbi12d 
 |-  ( a = ( e |` ( 1 ... 3 ) ) -> ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 2 ) e. NN ) <-> ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 2 ) e. NN ) ) )
51 50 adantr 
 |-  ( ( 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 ) ) )
52 44 adantr 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) <-> ( e ` 1 ) e. ( ZZ>= ` 2 ) ) )
53 id 
 |-  ( b = ( e ` 4 ) -> b = ( e ` 4 ) )
54 48 oveq1d 
 |-  ( a = ( e |` ( 1 ... 3 ) ) -> ( ( a ` 2 ) + 1 ) = ( ( e ` 2 ) + 1 ) )
55 43 54 oveq12d 
 |-  ( a = ( e |` ( 1 ... 3 ) ) -> ( ( a ` 1 ) rmY ( ( a ` 2 ) + 1 ) ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) )
56 53 55 eqeqan12rd 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( b = ( ( a ` 1 ) rmY ( ( a ` 2 ) + 1 ) ) <-> ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) ) )
57 52 56 anbi12d 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( ( a ` 2 ) + 1 ) ) ) <-> ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) ) ) )
58 eleq1 
 |-  ( b = ( e ` 4 ) -> ( b e. ( ZZ>= ` 2 ) <-> ( e ` 4 ) e. ( ZZ>= ` 2 ) ) )
59 58 adantl 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( b e. ( ZZ>= ` 2 ) <-> ( e ` 4 ) e. ( ZZ>= ` 2 ) ) )
60 53 48 oveqan12rd 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( b rmY ( a ` 2 ) ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) )
61 60 eqeq2d 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( ( e ` 5 ) = ( b rmY ( a ` 2 ) ) <-> ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) )
62 59 61 anbi12d 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( b rmY ( a ` 2 ) ) ) <-> ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) ) )
63 53 48 oveqan12rd 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( b rmX ( a ` 2 ) ) = ( ( e ` 4 ) rmX ( e ` 2 ) ) )
64 63 eqeq2d 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( ( e ` 6 ) = ( b rmX ( a ` 2 ) ) <-> ( e ` 6 ) = ( ( e ` 4 ) rmX ( e ` 2 ) ) ) )
65 59 64 anbi12d 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( b rmX ( a ` 2 ) ) ) <-> ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( e ` 2 ) ) ) ) )
66 3 jm2.27dlem1 
 |-  ( a = ( e |` ( 1 ... 3 ) ) -> ( a ` 3 ) = ( e ` 3 ) )
67 66 adantr 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( a ` 3 ) = ( e ` 3 ) )
68 oveq2 
 |-  ( b = ( e ` 4 ) -> ( 2 x. b ) = ( 2 x. ( e ` 4 ) ) )
69 68 43 oveqan12rd 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( ( 2 x. b ) x. ( a ` 1 ) ) = ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) )
70 43 oveq1d 
 |-  ( a = ( e |` ( 1 ... 3 ) ) -> ( ( a ` 1 ) ^ 2 ) = ( ( e ` 1 ) ^ 2 ) )
71 70 adantr 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( ( a ` 1 ) ^ 2 ) = ( ( e ` 1 ) ^ 2 ) )
72 69 71 oveq12d 
 |-  ( ( 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 ) ) )
73 72 oveq1d 
 |-  ( ( 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 ) )
74 67 73 breq12d 
 |-  ( ( 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 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> b = ( e ` 4 ) )
76 43 adantr 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( a ` 1 ) = ( e ` 1 ) )
77 75 76 oveq12d 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( b - ( a ` 1 ) ) = ( ( e ` 4 ) - ( e ` 1 ) ) )
78 77 oveq1d 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( ( b - ( a ` 1 ) ) x. ( e ` 5 ) ) = ( ( ( e ` 4 ) - ( e ` 1 ) ) x. ( e ` 5 ) ) )
79 78 oveq2d 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( ( e ` 6 ) - ( ( b - ( a ` 1 ) ) x. ( e ` 5 ) ) ) = ( ( e ` 6 ) - ( ( ( e ` 4 ) - ( e ` 1 ) ) x. ( e ` 5 ) ) ) )
80 79 67 oveq12d 
 |-  ( ( 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 ) ) )
81 73 80 breq12d 
 |-  ( ( 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 ) ) ) )
82 74 81 anbi12d 
 |-  ( ( 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 ) ) ) ) )
83 65 82 anbi12d 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( b rmX ( 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 ) rmX ( 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 ) ) ) ) ) )
84 62 83 anbi12d 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( b rmX ( 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 ) rmY ( e ` 2 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) ) ) )
85 57 84 anbi12d 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( b rmX ( 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 ) rmY ( ( e ` 2 ) + 1 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) ) ) ) )
86 51 85 anbi12d 
 |-  ( ( a = ( e |` ( 1 ... 3 ) ) /\ b = ( e ` 4 ) ) -> ( ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 2 ) e. NN ) /\ ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( b rmX ( 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 ) rmY ( ( e ` 2 ) + 1 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) ) ) ) ) )
87 33 34 86 sbc2ie 
 |-  ( [. ( e |` ( 1 ... 3 ) ) / a ]. [. ( e ` 4 ) / b ]. ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 2 ) e. NN ) /\ ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( b rmX ( 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 ) rmY ( ( e ` 2 ) + 1 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) ) ) ) )
88 31 87 bitri 
 |-  ( [. ( 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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 ) rmY ( ( e ` 2 ) + 1 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) ) ) ) )
89 88 rabbii 
 |-  { 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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 ) rmY ( ( e ` 2 ) + 1 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) ) ) ) }
90 6nn0 
 |-  6 e. NN0
91 2z 
 |-  2 e. ZZ
92 ovex 
 |-  ( 1 ... 6 ) e. _V
93 df-4 
 |-  4 = ( 3 + 1 )
94 df-5 
 |-  5 = ( 4 + 1 )
95 df-6 
 |-  6 = ( 5 + 1 )
96 ssid 
 |-  ( 1 ... 6 ) C_ ( 1 ... 6 )
97 95 96 jm2.27dlem5 
 |-  ( 1 ... 5 ) C_ ( 1 ... 6 )
98 94 97 jm2.27dlem5 
 |-  ( 1 ... 4 ) C_ ( 1 ... 6 )
99 93 98 jm2.27dlem5 
 |-  ( 1 ... 3 ) C_ ( 1 ... 6 )
100 36 99 jm2.27dlem5 
 |-  ( 1 ... 2 ) C_ ( 1 ... 6 )
101 35 100 jm2.27dlem5 
 |-  ( 1 ... 1 ) C_ ( 1 ... 6 )
102 101 41 sselii 
 |-  1 e. ( 1 ... 6 )
103 mzpproj 
 |-  ( ( ( 1 ... 6 ) e. _V /\ 1 e. ( 1 ... 6 ) ) -> ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 1 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) )
104 92 102 103 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 1 ) ) e. ( mzPoly ` ( 1 ... 6 ) )
105 eluzrabdioph 
 |-  ( ( 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 ) )
106 90 91 104 105 mp3an 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( e ` 1 ) e. ( ZZ>= ` 2 ) } e. ( Dioph ` 6 )
107 100 46 sselii 
 |-  2 e. ( 1 ... 6 )
108 mzpproj 
 |-  ( ( ( 1 ... 6 ) e. _V /\ 2 e. ( 1 ... 6 ) ) -> ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 2 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) )
109 92 107 108 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 2 ) ) e. ( mzPoly ` ( 1 ... 6 ) )
110 elnnrabdioph 
 |-  ( ( 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 ) )
111 90 109 110 mp2an 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( e ` 2 ) e. NN } e. ( Dioph ` 6 )
112 anrabdioph 
 |-  ( ( { 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 ) )
113 106 111 112 mp2an 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 2 ) e. NN ) } e. ( Dioph ` 6 )
114 elmapi 
 |-  ( e e. ( NN0 ^m ( 1 ... 6 ) ) -> e : ( 1 ... 6 ) --> NN0 )
115 ffvelcdm 
 |-  ( ( e : ( 1 ... 6 ) --> NN0 /\ 2 e. ( 1 ... 6 ) ) -> ( e ` 2 ) e. NN0 )
116 114 107 115 sylancl 
 |-  ( e e. ( NN0 ^m ( 1 ... 6 ) ) -> ( e ` 2 ) e. NN0 )
117 peano2nn0 
 |-  ( ( e ` 2 ) e. NN0 -> ( ( e ` 2 ) + 1 ) e. NN0 )
118 oveq2 
 |-  ( b = ( ( e ` 2 ) + 1 ) -> ( ( e ` 1 ) rmY b ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) )
119 118 eqeq2d 
 |-  ( b = ( ( e ` 2 ) + 1 ) -> ( ( e ` 4 ) = ( ( e ` 1 ) rmY b ) <-> ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) ) )
120 119 anbi2d 
 |-  ( b = ( ( e ` 2 ) + 1 ) -> ( ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY b ) ) <-> ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) ) ) )
121 120 ceqsrexv 
 |-  ( ( ( e ` 2 ) + 1 ) e. NN0 -> ( E. b e. NN0 ( b = ( ( e ` 2 ) + 1 ) /\ ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY b ) ) ) <-> ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) ) ) )
122 116 117 121 3syl 
 |-  ( e e. ( NN0 ^m ( 1 ... 6 ) ) -> ( E. b e. NN0 ( b = ( ( e ` 2 ) + 1 ) /\ ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY b ) ) ) <-> ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) ) ) )
123 122 bicomd 
 |-  ( e e. ( NN0 ^m ( 1 ... 6 ) ) -> ( ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) ) <-> E. b e. NN0 ( b = ( ( e ` 2 ) + 1 ) /\ ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY b ) ) ) ) )
124 123 rabbiia 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( 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 ) rmY b ) ) ) }
125 vex 
 |-  a e. _V
126 125 resex 
 |-  ( a |` ( 1 ... 6 ) ) e. _V
127 fvex 
 |-  ( a ` 7 ) e. _V
128 id 
 |-  ( b = ( a ` 7 ) -> b = ( a ` 7 ) )
129 107 jm2.27dlem1 
 |-  ( e = ( a |` ( 1 ... 6 ) ) -> ( e ` 2 ) = ( a ` 2 ) )
130 129 oveq1d 
 |-  ( e = ( a |` ( 1 ... 6 ) ) -> ( ( e ` 2 ) + 1 ) = ( ( a ` 2 ) + 1 ) )
131 128 130 eqeqan12rd 
 |-  ( ( e = ( a |` ( 1 ... 6 ) ) /\ b = ( a ` 7 ) ) -> ( b = ( ( e ` 2 ) + 1 ) <-> ( a ` 7 ) = ( ( a ` 2 ) + 1 ) ) )
132 102 jm2.27dlem1 
 |-  ( e = ( a |` ( 1 ... 6 ) ) -> ( e ` 1 ) = ( a ` 1 ) )
133 132 adantr 
 |-  ( ( e = ( a |` ( 1 ... 6 ) ) /\ b = ( a ` 7 ) ) -> ( e ` 1 ) = ( a ` 1 ) )
134 133 eleq1d 
 |-  ( ( e = ( a |` ( 1 ... 6 ) ) /\ b = ( a ` 7 ) ) -> ( ( e ` 1 ) e. ( ZZ>= ` 2 ) <-> ( a ` 1 ) e. ( ZZ>= ` 2 ) ) )
135 4nn 
 |-  4 e. NN
136 135 jm2.27dlem3 
 |-  4 e. ( 1 ... 4 )
137 98 136 sselii 
 |-  4 e. ( 1 ... 6 )
138 137 jm2.27dlem1 
 |-  ( e = ( a |` ( 1 ... 6 ) ) -> ( e ` 4 ) = ( a ` 4 ) )
139 138 adantr 
 |-  ( ( e = ( a |` ( 1 ... 6 ) ) /\ b = ( a ` 7 ) ) -> ( e ` 4 ) = ( a ` 4 ) )
140 132 128 oveqan12d 
 |-  ( ( e = ( a |` ( 1 ... 6 ) ) /\ b = ( a ` 7 ) ) -> ( ( e ` 1 ) rmY b ) = ( ( a ` 1 ) rmY ( a ` 7 ) ) )
141 139 140 eqeq12d 
 |-  ( ( e = ( a |` ( 1 ... 6 ) ) /\ b = ( a ` 7 ) ) -> ( ( e ` 4 ) = ( ( e ` 1 ) rmY b ) <-> ( a ` 4 ) = ( ( a ` 1 ) rmY ( a ` 7 ) ) ) )
142 134 141 anbi12d 
 |-  ( ( e = ( a |` ( 1 ... 6 ) ) /\ b = ( a ` 7 ) ) -> ( ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY b ) ) <-> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 4 ) = ( ( a ` 1 ) rmY ( a ` 7 ) ) ) ) )
143 131 142 anbi12d 
 |-  ( ( e = ( a |` ( 1 ... 6 ) ) /\ b = ( a ` 7 ) ) -> ( ( b = ( ( e ` 2 ) + 1 ) /\ ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY b ) ) ) <-> ( ( a ` 7 ) = ( ( a ` 2 ) + 1 ) /\ ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 4 ) = ( ( a ` 1 ) rmY ( a ` 7 ) ) ) ) ) )
144 126 127 143 sbc2ie 
 |-  ( [. ( a |` ( 1 ... 6 ) ) / e ]. [. ( a ` 7 ) / b ]. ( b = ( ( e ` 2 ) + 1 ) /\ ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY b ) ) ) <-> ( ( a ` 7 ) = ( ( a ` 2 ) + 1 ) /\ ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 4 ) = ( ( a ` 1 ) rmY ( a ` 7 ) ) ) ) )
145 144 rabbii 
 |-  { 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 ) rmY b ) ) ) } = { a e. ( NN0 ^m ( 1 ... 7 ) ) | ( ( a ` 7 ) = ( ( a ` 2 ) + 1 ) /\ ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 4 ) = ( ( a ` 1 ) rmY ( a ` 7 ) ) ) ) }
146 7nn0 
 |-  7 e. NN0
147 ovex 
 |-  ( 1 ... 7 ) e. _V
148 7nn 
 |-  7 e. NN
149 148 jm2.27dlem3 
 |-  7 e. ( 1 ... 7 )
150 mzpproj 
 |-  ( ( ( 1 ... 7 ) e. _V /\ 7 e. ( 1 ... 7 ) ) -> ( a e. ( ZZ ^m ( 1 ... 7 ) ) |-> ( a ` 7 ) ) e. ( mzPoly ` ( 1 ... 7 ) ) )
151 147 149 150 mp2an 
 |-  ( a e. ( ZZ ^m ( 1 ... 7 ) ) |-> ( a ` 7 ) ) e. ( mzPoly ` ( 1 ... 7 ) )
152 df-7 
 |-  7 = ( 6 + 1 )
153 6nn 
 |-  6 e. NN
154 107 152 153 jm2.27dlem2 
 |-  2 e. ( 1 ... 7 )
155 mzpproj 
 |-  ( ( ( 1 ... 7 ) e. _V /\ 2 e. ( 1 ... 7 ) ) -> ( a e. ( ZZ ^m ( 1 ... 7 ) ) |-> ( a ` 2 ) ) e. ( mzPoly ` ( 1 ... 7 ) ) )
156 147 154 155 mp2an 
 |-  ( a e. ( ZZ ^m ( 1 ... 7 ) ) |-> ( a ` 2 ) ) e. ( mzPoly ` ( 1 ... 7 ) )
157 1z 
 |-  1 e. ZZ
158 mzpconstmpt 
 |-  ( ( ( 1 ... 7 ) e. _V /\ 1 e. ZZ ) -> ( a e. ( ZZ ^m ( 1 ... 7 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... 7 ) ) )
159 147 157 158 mp2an 
 |-  ( a e. ( ZZ ^m ( 1 ... 7 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... 7 ) )
160 mzpaddmpt 
 |-  ( ( ( 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 ) ) )
161 156 159 160 mp2an 
 |-  ( a e. ( ZZ ^m ( 1 ... 7 ) ) |-> ( ( a ` 2 ) + 1 ) ) e. ( mzPoly ` ( 1 ... 7 ) )
162 eqrabdioph 
 |-  ( ( 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 ) )
163 146 151 161 162 mp3an 
 |-  { a e. ( NN0 ^m ( 1 ... 7 ) ) | ( a ` 7 ) = ( ( a ` 2 ) + 1 ) } e. ( Dioph ` 7 )
164 rmydioph 
 |-  { b e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( b ` 1 ) e. ( ZZ>= ` 2 ) /\ ( b ` 3 ) = ( ( b ` 1 ) rmY ( b ` 2 ) ) ) } e. ( Dioph ` 3 )
165 simp1 
 |-  ( ( ( b ` 1 ) = ( a ` 1 ) /\ ( b ` 2 ) = ( a ` 7 ) /\ ( b ` 3 ) = ( a ` 4 ) ) -> ( b ` 1 ) = ( a ` 1 ) )
166 165 eleq1d 
 |-  ( ( ( b ` 1 ) = ( a ` 1 ) /\ ( b ` 2 ) = ( a ` 7 ) /\ ( b ` 3 ) = ( a ` 4 ) ) -> ( ( b ` 1 ) e. ( ZZ>= ` 2 ) <-> ( a ` 1 ) e. ( ZZ>= ` 2 ) ) )
167 simp3 
 |-  ( ( ( b ` 1 ) = ( a ` 1 ) /\ ( b ` 2 ) = ( a ` 7 ) /\ ( b ` 3 ) = ( a ` 4 ) ) -> ( b ` 3 ) = ( a ` 4 ) )
168 simp2 
 |-  ( ( ( b ` 1 ) = ( a ` 1 ) /\ ( b ` 2 ) = ( a ` 7 ) /\ ( b ` 3 ) = ( a ` 4 ) ) -> ( b ` 2 ) = ( a ` 7 ) )
169 165 168 oveq12d 
 |-  ( ( ( b ` 1 ) = ( a ` 1 ) /\ ( b ` 2 ) = ( a ` 7 ) /\ ( b ` 3 ) = ( a ` 4 ) ) -> ( ( b ` 1 ) rmY ( b ` 2 ) ) = ( ( a ` 1 ) rmY ( a ` 7 ) ) )
170 167 169 eqeq12d 
 |-  ( ( ( b ` 1 ) = ( a ` 1 ) /\ ( b ` 2 ) = ( a ` 7 ) /\ ( b ` 3 ) = ( a ` 4 ) ) -> ( ( b ` 3 ) = ( ( b ` 1 ) rmY ( b ` 2 ) ) <-> ( a ` 4 ) = ( ( a ` 1 ) rmY ( a ` 7 ) ) ) )
171 166 170 anbi12d 
 |-  ( ( ( b ` 1 ) = ( a ` 1 ) /\ ( b ` 2 ) = ( a ` 7 ) /\ ( b ` 3 ) = ( a ` 4 ) ) -> ( ( ( b ` 1 ) e. ( ZZ>= ` 2 ) /\ ( b ` 3 ) = ( ( b ` 1 ) rmY ( b ` 2 ) ) ) <-> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 4 ) = ( ( a ` 1 ) rmY ( a ` 7 ) ) ) ) )
172 102 152 153 jm2.27dlem2 
 |-  1 e. ( 1 ... 7 )
173 137 152 153 jm2.27dlem2 
 |-  4 e. ( 1 ... 7 )
174 171 172 149 173 rabren3dioph 
 |-  ( ( 7 e. NN0 /\ { b e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( b ` 1 ) e. ( ZZ>= ` 2 ) /\ ( b ` 3 ) = ( ( b ` 1 ) rmY ( b ` 2 ) ) ) } e. ( Dioph ` 3 ) ) -> { a e. ( NN0 ^m ( 1 ... 7 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 4 ) = ( ( a ` 1 ) rmY ( a ` 7 ) ) ) } e. ( Dioph ` 7 ) )
175 146 164 174 mp2an 
 |-  { a e. ( NN0 ^m ( 1 ... 7 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 4 ) = ( ( a ` 1 ) rmY ( a ` 7 ) ) ) } e. ( Dioph ` 7 )
176 anrabdioph 
 |-  ( ( { 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 ) rmY ( 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 ) rmY ( a ` 7 ) ) ) ) } e. ( Dioph ` 7 ) )
177 163 175 176 mp2an 
 |-  { a e. ( NN0 ^m ( 1 ... 7 ) ) | ( ( a ` 7 ) = ( ( a ` 2 ) + 1 ) /\ ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 4 ) = ( ( a ` 1 ) rmY ( a ` 7 ) ) ) ) } e. ( Dioph ` 7 )
178 145 177 eqeltri 
 |-  { 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 ) rmY b ) ) ) } e. ( Dioph ` 7 )
179 152 rexfrabdioph 
 |-  ( ( 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 ) rmY 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 ) rmY b ) ) ) } e. ( Dioph ` 6 ) )
180 90 178 179 mp2an 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | E. b e. NN0 ( b = ( ( e ` 2 ) + 1 ) /\ ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY b ) ) ) } e. ( Dioph ` 6 )
181 124 180 eqeltri 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) ) } e. ( Dioph ` 6 )
182 rmydioph 
 |-  { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) } e. ( Dioph ` 3 )
183 simp1 
 |-  ( ( ( a ` 1 ) = ( e ` 4 ) /\ ( a ` 2 ) = ( e ` 2 ) /\ ( a ` 3 ) = ( e ` 5 ) ) -> ( a ` 1 ) = ( e ` 4 ) )
184 183 eleq1d 
 |-  ( ( ( a ` 1 ) = ( e ` 4 ) /\ ( a ` 2 ) = ( e ` 2 ) /\ ( a ` 3 ) = ( e ` 5 ) ) -> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) <-> ( e ` 4 ) e. ( ZZ>= ` 2 ) ) )
185 simp3 
 |-  ( ( ( a ` 1 ) = ( e ` 4 ) /\ ( a ` 2 ) = ( e ` 2 ) /\ ( a ` 3 ) = ( e ` 5 ) ) -> ( a ` 3 ) = ( e ` 5 ) )
186 simp2 
 |-  ( ( ( a ` 1 ) = ( e ` 4 ) /\ ( a ` 2 ) = ( e ` 2 ) /\ ( a ` 3 ) = ( e ` 5 ) ) -> ( a ` 2 ) = ( e ` 2 ) )
187 183 186 oveq12d 
 |-  ( ( ( a ` 1 ) = ( e ` 4 ) /\ ( a ` 2 ) = ( e ` 2 ) /\ ( a ` 3 ) = ( e ` 5 ) ) -> ( ( a ` 1 ) rmY ( a ` 2 ) ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) )
188 185 187 eqeq12d 
 |-  ( ( ( a ` 1 ) = ( e ` 4 ) /\ ( a ` 2 ) = ( e ` 2 ) /\ ( a ` 3 ) = ( e ` 5 ) ) -> ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) <-> ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) )
189 184 188 anbi12d 
 |-  ( ( ( a ` 1 ) = ( e ` 4 ) /\ ( a ` 2 ) = ( e ` 2 ) /\ ( a ` 3 ) = ( e ` 5 ) ) -> ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) <-> ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) ) )
190 5nn 
 |-  5 e. NN
191 190 jm2.27dlem3 
 |-  5 e. ( 1 ... 5 )
192 191 95 190 jm2.27dlem2 
 |-  5 e. ( 1 ... 6 )
193 189 137 107 192 rabren3dioph 
 |-  ( ( 6 e. NN0 /\ { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) } e. ( Dioph ` 3 ) ) -> { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) } e. ( Dioph ` 6 ) )
194 90 182 193 mp2an 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) } e. ( Dioph ` 6 )
195 rmxdioph 
 |-  { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmX ( a ` 2 ) ) ) } e. ( Dioph ` 3 )
196 simp1 
 |-  ( ( ( a ` 1 ) = ( e ` 4 ) /\ ( a ` 2 ) = ( e ` 2 ) /\ ( a ` 3 ) = ( e ` 6 ) ) -> ( a ` 1 ) = ( e ` 4 ) )
197 196 eleq1d 
 |-  ( ( ( a ` 1 ) = ( e ` 4 ) /\ ( a ` 2 ) = ( e ` 2 ) /\ ( a ` 3 ) = ( e ` 6 ) ) -> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) <-> ( e ` 4 ) e. ( ZZ>= ` 2 ) ) )
198 simp3 
 |-  ( ( ( a ` 1 ) = ( e ` 4 ) /\ ( a ` 2 ) = ( e ` 2 ) /\ ( a ` 3 ) = ( e ` 6 ) ) -> ( a ` 3 ) = ( e ` 6 ) )
199 simp2 
 |-  ( ( ( a ` 1 ) = ( e ` 4 ) /\ ( a ` 2 ) = ( e ` 2 ) /\ ( a ` 3 ) = ( e ` 6 ) ) -> ( a ` 2 ) = ( e ` 2 ) )
200 196 199 oveq12d 
 |-  ( ( ( a ` 1 ) = ( e ` 4 ) /\ ( a ` 2 ) = ( e ` 2 ) /\ ( a ` 3 ) = ( e ` 6 ) ) -> ( ( a ` 1 ) rmX ( a ` 2 ) ) = ( ( e ` 4 ) rmX ( e ` 2 ) ) )
201 198 200 eqeq12d 
 |-  ( ( ( a ` 1 ) = ( e ` 4 ) /\ ( a ` 2 ) = ( e ` 2 ) /\ ( a ` 3 ) = ( e ` 6 ) ) -> ( ( a ` 3 ) = ( ( a ` 1 ) rmX ( a ` 2 ) ) <-> ( e ` 6 ) = ( ( e ` 4 ) rmX ( e ` 2 ) ) ) )
202 197 201 anbi12d 
 |-  ( ( ( a ` 1 ) = ( e ` 4 ) /\ ( a ` 2 ) = ( e ` 2 ) /\ ( a ` 3 ) = ( e ` 6 ) ) -> ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmX ( a ` 2 ) ) ) <-> ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( e ` 2 ) ) ) ) )
203 153 jm2.27dlem3 
 |-  6 e. ( 1 ... 6 )
204 202 137 107 203 rabren3dioph 
 |-  ( ( 6 e. NN0 /\ { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmX ( a ` 2 ) ) ) } e. ( Dioph ` 3 ) ) -> { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( e ` 2 ) ) ) } e. ( Dioph ` 6 ) )
205 90 195 204 mp2an 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( e ` 2 ) ) ) } e. ( Dioph ` 6 )
206 99 3 sselii 
 |-  3 e. ( 1 ... 6 )
207 mzpproj 
 |-  ( ( ( 1 ... 6 ) e. _V /\ 3 e. ( 1 ... 6 ) ) -> ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 3 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) )
208 92 206 207 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 3 ) ) e. ( mzPoly ` ( 1 ... 6 ) )
209 mzpconstmpt 
 |-  ( ( ( 1 ... 6 ) e. _V /\ 2 e. ZZ ) -> ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> 2 ) e. ( mzPoly ` ( 1 ... 6 ) ) )
210 92 91 209 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> 2 ) e. ( mzPoly ` ( 1 ... 6 ) )
211 mzpproj 
 |-  ( ( ( 1 ... 6 ) e. _V /\ 4 e. ( 1 ... 6 ) ) -> ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 4 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) )
212 92 137 211 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 4 ) ) e. ( mzPoly ` ( 1 ... 6 ) )
213 mzpmulmpt 
 |-  ( ( ( 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 ) ) )
214 210 212 213 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( 2 x. ( e ` 4 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) )
215 mzpmulmpt 
 |-  ( ( ( 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 ) ) )
216 214 104 215 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) )
217 2nn0 
 |-  2 e. NN0
218 mzpexpmpt 
 |-  ( ( ( 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 ) ) )
219 104 217 218 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( e ` 1 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... 6 ) )
220 mzpsubmpt 
 |-  ( ( ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) ) /\ ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( e ` 1 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) ) -> ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) - ( ( e ` 1 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) ) )
221 216 219 220 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) - ( ( e ` 1 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) )
222 mzpconstmpt 
 |-  ( ( ( 1 ... 6 ) e. _V /\ 1 e. ZZ ) -> ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... 6 ) ) )
223 92 157 222 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... 6 ) )
224 mzpsubmpt 
 |-  ( ( ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) - ( ( e ` 1 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) ) /\ ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... 6 ) ) ) -> ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) - ( ( e ` 1 ) ^ 2 ) ) - 1 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) )
225 221 223 224 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) - ( ( e ` 1 ) ^ 2 ) ) - 1 ) ) e. ( mzPoly ` ( 1 ... 6 ) )
226 ltrabdioph 
 |-  ( ( 6 e. NN0 /\ ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 3 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) /\ ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) - ( ( e ` 1 ) ^ 2 ) ) - 1 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) ) -> { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( e ` 3 ) < ( ( ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) - ( ( e ` 1 ) ^ 2 ) ) - 1 ) } e. ( Dioph ` 6 ) )
227 90 208 225 226 mp3an 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( e ` 3 ) < ( ( ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) - ( ( e ` 1 ) ^ 2 ) ) - 1 ) } e. ( Dioph ` 6 )
228 mzpproj 
 |-  ( ( ( 1 ... 6 ) e. _V /\ 6 e. ( 1 ... 6 ) ) -> ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 6 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) )
229 92 203 228 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 6 ) ) e. ( mzPoly ` ( 1 ... 6 ) )
230 mzpsubmpt 
 |-  ( ( ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 4 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) /\ ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 1 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) ) -> ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( e ` 4 ) - ( e ` 1 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) ) )
231 212 104 230 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( e ` 4 ) - ( e ` 1 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) )
232 mzpproj 
 |-  ( ( ( 1 ... 6 ) e. _V /\ 5 e. ( 1 ... 6 ) ) -> ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 5 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) )
233 92 192 232 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 5 ) ) e. ( mzPoly ` ( 1 ... 6 ) )
234 mzpmulmpt 
 |-  ( ( ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( e ` 4 ) - ( e ` 1 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) ) /\ ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 5 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) ) -> ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( ( e ` 4 ) - ( e ` 1 ) ) x. ( e ` 5 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) ) )
235 231 233 234 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( ( e ` 4 ) - ( e ` 1 ) ) x. ( e ` 5 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) )
236 mzpsubmpt 
 |-  ( ( ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 6 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) /\ ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( ( e ` 4 ) - ( e ` 1 ) ) x. ( e ` 5 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) ) ) -> ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( e ` 6 ) - ( ( ( e ` 4 ) - ( e ` 1 ) ) x. ( e ` 5 ) ) ) ) e. ( mzPoly ` ( 1 ... 6 ) ) )
237 229 235 236 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( e ` 6 ) - ( ( ( e ` 4 ) - ( e ` 1 ) ) x. ( e ` 5 ) ) ) ) e. ( mzPoly ` ( 1 ... 6 ) )
238 mzpsubmpt 
 |-  ( ( ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( e ` 6 ) - ( ( ( e ` 4 ) - ( e ` 1 ) ) x. ( e ` 5 ) ) ) ) e. ( mzPoly ` ( 1 ... 6 ) ) /\ ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( e ` 3 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) ) -> ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( ( e ` 6 ) - ( ( ( e ` 4 ) - ( e ` 1 ) ) x. ( e ` 5 ) ) ) - ( e ` 3 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) ) )
239 237 208 238 mp2an 
 |-  ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( ( e ` 6 ) - ( ( ( e ` 4 ) - ( e ` 1 ) ) x. ( e ` 5 ) ) ) - ( e ` 3 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) )
240 dvdsrabdioph 
 |-  ( ( 6 e. NN0 /\ ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) - ( ( e ` 1 ) ^ 2 ) ) - 1 ) ) e. ( mzPoly ` ( 1 ... 6 ) ) /\ ( e e. ( ZZ ^m ( 1 ... 6 ) ) |-> ( ( ( e ` 6 ) - ( ( ( e ` 4 ) - ( e ` 1 ) ) x. ( e ` 5 ) ) ) - ( e ` 3 ) ) ) e. ( mzPoly ` ( 1 ... 6 ) ) ) -> { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) - ( ( e ` 1 ) ^ 2 ) ) - 1 ) || ( ( ( e ` 6 ) - ( ( ( e ` 4 ) - ( e ` 1 ) ) x. ( e ` 5 ) ) ) - ( e ` 3 ) ) } e. ( Dioph ` 6 ) )
241 90 225 239 240 mp3an 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) - ( ( e ` 1 ) ^ 2 ) ) - 1 ) || ( ( ( e ` 6 ) - ( ( ( e ` 4 ) - ( e ` 1 ) ) x. ( e ` 5 ) ) ) - ( e ` 3 ) ) } e. ( Dioph ` 6 )
242 anrabdioph 
 |-  ( ( { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( e ` 3 ) < ( ( ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) - ( ( e ` 1 ) ^ 2 ) ) - 1 ) } e. ( Dioph ` 6 ) /\ { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( ( ( 2 x. ( e ` 4 ) ) x. ( e ` 1 ) ) - ( ( e ` 1 ) ^ 2 ) ) - 1 ) || ( ( ( e ` 6 ) - ( ( ( e ` 4 ) - ( e ` 1 ) ) x. ( e ` 5 ) ) ) - ( e ` 3 ) ) } e. ( Dioph ` 6 ) ) -> { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( 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 ) ) ) } e. ( Dioph ` 6 ) )
243 227 241 242 mp2an 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( 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 ) ) ) } e. ( Dioph ` 6 )
244 anrabdioph 
 |-  ( ( { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( e ` 2 ) ) ) } e. ( Dioph ` 6 ) /\ { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( 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 ) ) ) } e. ( Dioph ` 6 ) ) -> { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) } e. ( Dioph ` 6 ) )
245 205 243 244 mp2an 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) } e. ( Dioph ` 6 )
246 anrabdioph 
 |-  ( ( { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) } e. ( Dioph ` 6 ) /\ { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) } e. ( Dioph ` 6 ) ) -> { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) ) } e. ( Dioph ` 6 ) )
247 194 245 246 mp2an 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) ) } e. ( Dioph ` 6 )
248 anrabdioph 
 |-  ( ( { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) ) } e. ( Dioph ` 6 ) /\ { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) ) } e. ( Dioph ` 6 ) ) -> { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) ) ) } e. ( Dioph ` 6 ) )
249 181 247 248 mp2an 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) ) ) } e. ( Dioph ` 6 )
250 anrabdioph 
 |-  ( ( { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 2 ) e. NN ) } e. ( Dioph ` 6 ) /\ { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) ) ) } e. ( Dioph ` 6 ) ) -> { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 2 ) e. NN ) /\ ( ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) ) ) ) } e. ( Dioph ` 6 ) )
251 113 249 250 mp2an 
 |-  { e e. ( NN0 ^m ( 1 ... 6 ) ) | ( ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 2 ) e. NN ) /\ ( ( ( e ` 1 ) e. ( ZZ>= ` 2 ) /\ ( e ` 4 ) = ( ( e ` 1 ) rmY ( ( e ` 2 ) + 1 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 5 ) = ( ( e ` 4 ) rmY ( e ` 2 ) ) ) /\ ( ( ( e ` 4 ) e. ( ZZ>= ` 2 ) /\ ( e ` 6 ) = ( ( e ` 4 ) rmX ( 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 ) ) ) ) ) ) ) } e. ( Dioph ` 6 )
252 89 251 eqeltri 
 |-  { 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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. ( Dioph ` 6 )
253 93 94 95 3rexfrabdioph 
 |-  ( ( 3 e. NN0 /\ { 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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. ( Dioph ` 6 ) ) -> { 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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. ( Dioph ` 3 ) )
254 9 252 253 mp2an 
 |-  { 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 ) rmY ( ( a ` 2 ) + 1 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ c = ( b rmY ( a ` 2 ) ) ) /\ ( ( b e. ( ZZ>= ` 2 ) /\ d = ( b rmX ( 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. ( Dioph ` 3 )
255 8 254 eqeltri 
 |-  { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 2 ) e. NN ) /\ ( a ` 3 ) = ( ( a ` 1 ) ^ ( a ` 2 ) ) ) } e. ( Dioph ` 3 )