Metamath Proof Explorer

Theorem rmxdioph

Description: X is a Diophantine function. (Contributed by Stefan O'Rear, 17-Oct-2014)

Ref Expression
Assertion rmxdioph 
|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmX ( a ` 2 ) ) ) } e. ( Dioph ` 3 )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) -> ( a ` 1 ) e. ( ZZ>= ` 2 ) )
2 elmapi 
 |-  ( a e. ( NN0 ^m ( 1 ... 3 ) ) -> a : ( 1 ... 3 ) --> NN0 )
3 df-3 
 |-  3 = ( 2 + 1 )
4 ssid 
 |-  ( 1 ... 3 ) C_ ( 1 ... 3 )
5 3 4 jm2.27dlem5 
 |-  ( 1 ... 2 ) C_ ( 1 ... 3 )
6 2nn 
 |-  2 e. NN
7 6 jm2.27dlem3 
 |-  2 e. ( 1 ... 2 )
8 5 7 sselii 
 |-  2 e. ( 1 ... 3 )
9 ffvelcdm 
 |-  ( ( a : ( 1 ... 3 ) --> NN0 /\ 2 e. ( 1 ... 3 ) ) -> ( a ` 2 ) e. NN0 )
10 2 8 9 sylancl 
 |-  ( a e. ( NN0 ^m ( 1 ... 3 ) ) -> ( a ` 2 ) e. NN0 )
11 10 adantr 
 |-  ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) -> ( a ` 2 ) e. NN0 )
12 3nn 
 |-  3 e. NN
13 12 jm2.27dlem3 
 |-  3 e. ( 1 ... 3 )
14 ffvelcdm 
 |-  ( ( a : ( 1 ... 3 ) --> NN0 /\ 3 e. ( 1 ... 3 ) ) -> ( a ` 3 ) e. NN0 )
15 2 13 14 sylancl 
 |-  ( a e. ( NN0 ^m ( 1 ... 3 ) ) -> ( a ` 3 ) e. NN0 )
16 15 adantr 
 |-  ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) -> ( a ` 3 ) e. NN0 )
17 rmxdiophlem 
 |-  ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 2 ) e. NN0 /\ ( a ` 3 ) e. NN0 ) -> ( ( a ` 3 ) = ( ( a ` 1 ) rmX ( a ` 2 ) ) <-> E. b e. NN0 ( b = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) ) )
18 1 11 16 17 syl3anc 
 |-  ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) -> ( ( a ` 3 ) = ( ( a ` 1 ) rmX ( a ` 2 ) ) <-> E. b e. NN0 ( b = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) ) )
19 18 pm5.32da 
 |-  ( a e. ( NN0 ^m ( 1 ... 3 ) ) -> ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmX ( a ` 2 ) ) ) <-> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ E. b e. NN0 ( b = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) ) ) )
20 anass 
 |-  ( ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) <-> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( b = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) ) )
21 20 rexbii 
 |-  ( E. b e. NN0 ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) <-> E. b e. NN0 ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( b = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) ) )
22 r19.42v 
 |-  ( E. b e. NN0 ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( b = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) ) <-> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ E. b e. NN0 ( b = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) ) )
23 21 22 bitr2i 
 |-  ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ E. b e. NN0 ( b = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) ) <-> E. b e. NN0 ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) )
24 19 23 bitrdi 
 |-  ( a e. ( NN0 ^m ( 1 ... 3 ) ) -> ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmX ( a ` 2 ) ) ) <-> E. b e. NN0 ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) ) )
25 24 rabbiia 
 |-  { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmX ( a ` 2 ) ) ) } = { a e. ( NN0 ^m ( 1 ... 3 ) ) | E. b e. NN0 ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) }
26 3nn0 
 |-  3 e. NN0
27 vex 
 |-  c e. _V
28 27 resex 
 |-  ( c |` ( 1 ... 3 ) ) e. _V
29 fvex 
 |-  ( c ` 4 ) e. _V
30 df-2 
 |-  2 = ( 1 + 1 )
31 30 5 jm2.27dlem5 
 |-  ( 1 ... 1 ) C_ ( 1 ... 3 )
32 1nn 
 |-  1 e. NN
33 32 jm2.27dlem3 
 |-  1 e. ( 1 ... 1 )
34 31 33 sselii 
 |-  1 e. ( 1 ... 3 )
35 34 jm2.27dlem1 
 |-  ( a = ( c |` ( 1 ... 3 ) ) -> ( a ` 1 ) = ( c ` 1 ) )
36 35 eleq1d 
 |-  ( a = ( c |` ( 1 ... 3 ) ) -> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) <-> ( c ` 1 ) e. ( ZZ>= ` 2 ) ) )
37 36 adantr 
 |-  ( ( a = ( c |` ( 1 ... 3 ) ) /\ b = ( c ` 4 ) ) -> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) <-> ( c ` 1 ) e. ( ZZ>= ` 2 ) ) )
38 simpr 
 |-  ( ( a = ( c |` ( 1 ... 3 ) ) /\ b = ( c ` 4 ) ) -> b = ( c ` 4 ) )
39 8 jm2.27dlem1 
 |-  ( a = ( c |` ( 1 ... 3 ) ) -> ( a ` 2 ) = ( c ` 2 ) )
40 35 39 oveq12d 
 |-  ( a = ( c |` ( 1 ... 3 ) ) -> ( ( a ` 1 ) rmY ( a ` 2 ) ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) )
41 40 adantr 
 |-  ( ( a = ( c |` ( 1 ... 3 ) ) /\ b = ( c ` 4 ) ) -> ( ( a ` 1 ) rmY ( a ` 2 ) ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) )
42 38 41 eqeq12d 
 |-  ( ( a = ( c |` ( 1 ... 3 ) ) /\ b = ( c ` 4 ) ) -> ( b = ( ( a ` 1 ) rmY ( a ` 2 ) ) <-> ( c ` 4 ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) ) )
43 37 42 anbi12d 
 |-  ( ( a = ( c |` ( 1 ... 3 ) ) /\ b = ( c ` 4 ) ) -> ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) <-> ( ( c ` 1 ) e. ( ZZ>= ` 2 ) /\ ( c ` 4 ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) ) ) )
44 13 jm2.27dlem1 
 |-  ( a = ( c |` ( 1 ... 3 ) ) -> ( a ` 3 ) = ( c ` 3 ) )
45 44 oveq1d 
 |-  ( a = ( c |` ( 1 ... 3 ) ) -> ( ( a ` 3 ) ^ 2 ) = ( ( c ` 3 ) ^ 2 ) )
46 45 adantr 
 |-  ( ( a = ( c |` ( 1 ... 3 ) ) /\ b = ( c ` 4 ) ) -> ( ( a ` 3 ) ^ 2 ) = ( ( c ` 3 ) ^ 2 ) )
47 35 oveq1d 
 |-  ( a = ( c |` ( 1 ... 3 ) ) -> ( ( a ` 1 ) ^ 2 ) = ( ( c ` 1 ) ^ 2 ) )
48 47 oveq1d 
 |-  ( a = ( c |` ( 1 ... 3 ) ) -> ( ( ( a ` 1 ) ^ 2 ) - 1 ) = ( ( ( c ` 1 ) ^ 2 ) - 1 ) )
49 oveq1 
 |-  ( b = ( c ` 4 ) -> ( b ^ 2 ) = ( ( c ` 4 ) ^ 2 ) )
50 48 49 oveqan12d 
 |-  ( ( a = ( c |` ( 1 ... 3 ) ) /\ b = ( c ` 4 ) ) -> ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) = ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) )
51 46 50 oveq12d 
 |-  ( ( a = ( c |` ( 1 ... 3 ) ) /\ b = ( c ` 4 ) ) -> ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = ( ( ( c ` 3 ) ^ 2 ) - ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) )
52 51 eqeq1d 
 |-  ( ( a = ( c |` ( 1 ... 3 ) ) /\ b = ( c ` 4 ) ) -> ( ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 <-> ( ( ( c ` 3 ) ^ 2 ) - ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) = 1 ) )
53 43 52 anbi12d 
 |-  ( ( a = ( c |` ( 1 ... 3 ) ) /\ b = ( c ` 4 ) ) -> ( ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) <-> ( ( ( c ` 1 ) e. ( ZZ>= ` 2 ) /\ ( c ` 4 ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) ) /\ ( ( ( c ` 3 ) ^ 2 ) - ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) = 1 ) ) )
54 28 29 53 sbc2ie 
 |-  ( [. ( c |` ( 1 ... 3 ) ) / a ]. [. ( c ` 4 ) / b ]. ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) <-> ( ( ( c ` 1 ) e. ( ZZ>= ` 2 ) /\ ( c ` 4 ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) ) /\ ( ( ( c ` 3 ) ^ 2 ) - ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) = 1 ) )
55 54 rabbii 
 |-  { c e. ( NN0 ^m ( 1 ... 4 ) ) | [. ( c |` ( 1 ... 3 ) ) / a ]. [. ( c ` 4 ) / b ]. ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) } = { c e. ( NN0 ^m ( 1 ... 4 ) ) | ( ( ( c ` 1 ) e. ( ZZ>= ` 2 ) /\ ( c ` 4 ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) ) /\ ( ( ( c ` 3 ) ^ 2 ) - ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) = 1 ) }
56 4nn0 
 |-  4 e. NN0
57 rmydioph 
 |-  { b e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( b ` 1 ) e. ( ZZ>= ` 2 ) /\ ( b ` 3 ) = ( ( b ` 1 ) rmY ( b ` 2 ) ) ) } e. ( Dioph ` 3 )
58 simp1 
 |-  ( ( ( b ` 1 ) = ( c ` 1 ) /\ ( b ` 2 ) = ( c ` 2 ) /\ ( b ` 3 ) = ( c ` 4 ) ) -> ( b ` 1 ) = ( c ` 1 ) )
59 58 eleq1d 
 |-  ( ( ( b ` 1 ) = ( c ` 1 ) /\ ( b ` 2 ) = ( c ` 2 ) /\ ( b ` 3 ) = ( c ` 4 ) ) -> ( ( b ` 1 ) e. ( ZZ>= ` 2 ) <-> ( c ` 1 ) e. ( ZZ>= ` 2 ) ) )
60 simp3 
 |-  ( ( ( b ` 1 ) = ( c ` 1 ) /\ ( b ` 2 ) = ( c ` 2 ) /\ ( b ` 3 ) = ( c ` 4 ) ) -> ( b ` 3 ) = ( c ` 4 ) )
61 simp2 
 |-  ( ( ( b ` 1 ) = ( c ` 1 ) /\ ( b ` 2 ) = ( c ` 2 ) /\ ( b ` 3 ) = ( c ` 4 ) ) -> ( b ` 2 ) = ( c ` 2 ) )
62 58 61 oveq12d 
 |-  ( ( ( b ` 1 ) = ( c ` 1 ) /\ ( b ` 2 ) = ( c ` 2 ) /\ ( b ` 3 ) = ( c ` 4 ) ) -> ( ( b ` 1 ) rmY ( b ` 2 ) ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) )
63 60 62 eqeq12d 
 |-  ( ( ( b ` 1 ) = ( c ` 1 ) /\ ( b ` 2 ) = ( c ` 2 ) /\ ( b ` 3 ) = ( c ` 4 ) ) -> ( ( b ` 3 ) = ( ( b ` 1 ) rmY ( b ` 2 ) ) <-> ( c ` 4 ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) ) )
64 59 63 anbi12d 
 |-  ( ( ( b ` 1 ) = ( c ` 1 ) /\ ( b ` 2 ) = ( c ` 2 ) /\ ( b ` 3 ) = ( c ` 4 ) ) -> ( ( ( b ` 1 ) e. ( ZZ>= ` 2 ) /\ ( b ` 3 ) = ( ( b ` 1 ) rmY ( b ` 2 ) ) ) <-> ( ( c ` 1 ) e. ( ZZ>= ` 2 ) /\ ( c ` 4 ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) ) ) )
65 df-4 
 |-  4 = ( 3 + 1 )
66 ssid 
 |-  ( 1 ... 4 ) C_ ( 1 ... 4 )
67 65 66 jm2.27dlem5 
 |-  ( 1 ... 3 ) C_ ( 1 ... 4 )
68 3 67 jm2.27dlem5 
 |-  ( 1 ... 2 ) C_ ( 1 ... 4 )
69 30 68 jm2.27dlem5 
 |-  ( 1 ... 1 ) C_ ( 1 ... 4 )
70 69 33 sselii 
 |-  1 e. ( 1 ... 4 )
71 68 7 sselii 
 |-  2 e. ( 1 ... 4 )
72 4nn 
 |-  4 e. NN
73 72 jm2.27dlem3 
 |-  4 e. ( 1 ... 4 )
74 64 70 71 73 rabren3dioph 
 |-  ( ( 4 e. NN0 /\ { b e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( b ` 1 ) e. ( ZZ>= ` 2 ) /\ ( b ` 3 ) = ( ( b ` 1 ) rmY ( b ` 2 ) ) ) } e. ( Dioph ` 3 ) ) -> { c e. ( NN0 ^m ( 1 ... 4 ) ) | ( ( c ` 1 ) e. ( ZZ>= ` 2 ) /\ ( c ` 4 ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) ) } e. ( Dioph ` 4 ) )
75 56 57 74 mp2an 
 |-  { c e. ( NN0 ^m ( 1 ... 4 ) ) | ( ( c ` 1 ) e. ( ZZ>= ` 2 ) /\ ( c ` 4 ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) ) } e. ( Dioph ` 4 )
76 ovex 
 |-  ( 1 ... 4 ) e. _V
77 67 13 sselii 
 |-  3 e. ( 1 ... 4 )
78 mzpproj 
 |-  ( ( ( 1 ... 4 ) e. _V /\ 3 e. ( 1 ... 4 ) ) -> ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( c ` 3 ) ) e. ( mzPoly ` ( 1 ... 4 ) ) )
79 76 77 78 mp2an 
 |-  ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( c ` 3 ) ) e. ( mzPoly ` ( 1 ... 4 ) )
80 2nn0 
 |-  2 e. NN0
81 mzpexpmpt 
 |-  ( ( ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( c ` 3 ) ) e. ( mzPoly ` ( 1 ... 4 ) ) /\ 2 e. NN0 ) -> ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( c ` 3 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... 4 ) ) )
82 79 80 81 mp2an 
 |-  ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( c ` 3 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... 4 ) )
83 mzpproj 
 |-  ( ( ( 1 ... 4 ) e. _V /\ 1 e. ( 1 ... 4 ) ) -> ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( c ` 1 ) ) e. ( mzPoly ` ( 1 ... 4 ) ) )
84 76 70 83 mp2an 
 |-  ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( c ` 1 ) ) e. ( mzPoly ` ( 1 ... 4 ) )
85 mzpexpmpt 
 |-  ( ( ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( c ` 1 ) ) e. ( mzPoly ` ( 1 ... 4 ) ) /\ 2 e. NN0 ) -> ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( c ` 1 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... 4 ) ) )
86 84 80 85 mp2an 
 |-  ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( c ` 1 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... 4 ) )
87 1z 
 |-  1 e. ZZ
88 mzpconstmpt 
 |-  ( ( ( 1 ... 4 ) e. _V /\ 1 e. ZZ ) -> ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... 4 ) ) )
89 76 87 88 mp2an 
 |-  ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... 4 ) )
90 mzpsubmpt 
 |-  ( ( ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( c ` 1 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... 4 ) ) /\ ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... 4 ) ) ) -> ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( ( c ` 1 ) ^ 2 ) - 1 ) ) e. ( mzPoly ` ( 1 ... 4 ) ) )
91 86 89 90 mp2an 
 |-  ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( ( c ` 1 ) ^ 2 ) - 1 ) ) e. ( mzPoly ` ( 1 ... 4 ) )
92 mzpproj 
 |-  ( ( ( 1 ... 4 ) e. _V /\ 4 e. ( 1 ... 4 ) ) -> ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( c ` 4 ) ) e. ( mzPoly ` ( 1 ... 4 ) ) )
93 76 73 92 mp2an 
 |-  ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( c ` 4 ) ) e. ( mzPoly ` ( 1 ... 4 ) )
94 mzpexpmpt 
 |-  ( ( ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( c ` 4 ) ) e. ( mzPoly ` ( 1 ... 4 ) ) /\ 2 e. NN0 ) -> ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( c ` 4 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... 4 ) ) )
95 93 80 94 mp2an 
 |-  ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( c ` 4 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... 4 ) )
96 mzpmulmpt 
 |-  ( ( ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( ( c ` 1 ) ^ 2 ) - 1 ) ) e. ( mzPoly ` ( 1 ... 4 ) ) /\ ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( c ` 4 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... 4 ) ) ) -> ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... 4 ) ) )
97 91 95 96 mp2an 
 |-  ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... 4 ) )
98 mzpsubmpt 
 |-  ( ( ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( c ` 3 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... 4 ) ) /\ ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... 4 ) ) ) -> ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( ( c ` 3 ) ^ 2 ) - ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... 4 ) ) )
99 82 97 98 mp2an 
 |-  ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( ( c ` 3 ) ^ 2 ) - ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... 4 ) )
100 eqrabdioph 
 |-  ( ( 4 e. NN0 /\ ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> ( ( ( c ` 3 ) ^ 2 ) - ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... 4 ) ) /\ ( c e. ( ZZ ^m ( 1 ... 4 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... 4 ) ) ) -> { c e. ( NN0 ^m ( 1 ... 4 ) ) | ( ( ( c ` 3 ) ^ 2 ) - ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) = 1 } e. ( Dioph ` 4 ) )
101 56 99 89 100 mp3an 
 |-  { c e. ( NN0 ^m ( 1 ... 4 ) ) | ( ( ( c ` 3 ) ^ 2 ) - ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) = 1 } e. ( Dioph ` 4 )
102 anrabdioph 
 |-  ( ( { c e. ( NN0 ^m ( 1 ... 4 ) ) | ( ( c ` 1 ) e. ( ZZ>= ` 2 ) /\ ( c ` 4 ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) ) } e. ( Dioph ` 4 ) /\ { c e. ( NN0 ^m ( 1 ... 4 ) ) | ( ( ( c ` 3 ) ^ 2 ) - ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) = 1 } e. ( Dioph ` 4 ) ) -> { c e. ( NN0 ^m ( 1 ... 4 ) ) | ( ( ( c ` 1 ) e. ( ZZ>= ` 2 ) /\ ( c ` 4 ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) ) /\ ( ( ( c ` 3 ) ^ 2 ) - ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) = 1 ) } e. ( Dioph ` 4 ) )
103 75 101 102 mp2an 
 |-  { c e. ( NN0 ^m ( 1 ... 4 ) ) | ( ( ( c ` 1 ) e. ( ZZ>= ` 2 ) /\ ( c ` 4 ) = ( ( c ` 1 ) rmY ( c ` 2 ) ) ) /\ ( ( ( c ` 3 ) ^ 2 ) - ( ( ( ( c ` 1 ) ^ 2 ) - 1 ) x. ( ( c ` 4 ) ^ 2 ) ) ) = 1 ) } e. ( Dioph ` 4 )
104 55 103 eqeltri 
 |-  { c e. ( NN0 ^m ( 1 ... 4 ) ) | [. ( c |` ( 1 ... 3 ) ) / a ]. [. ( c ` 4 ) / b ]. ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) } e. ( Dioph ` 4 )
105 65 rexfrabdioph 
 |-  ( ( 3 e. NN0 /\ { c e. ( NN0 ^m ( 1 ... 4 ) ) | [. ( c |` ( 1 ... 3 ) ) / a ]. [. ( c ` 4 ) / b ]. ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) } e. ( Dioph ` 4 ) ) -> { a e. ( NN0 ^m ( 1 ... 3 ) ) | E. b e. NN0 ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) } e. ( Dioph ` 3 ) )
106 26 104 105 mp2an 
 |-  { a e. ( NN0 ^m ( 1 ... 3 ) ) | E. b e. NN0 ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ b = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) /\ ( ( ( a ` 3 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( b ^ 2 ) ) ) = 1 ) } e. ( Dioph ` 3 )
107 25 106 eqeltri 
 |-  { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmX ( a ` 2 ) ) ) } e. ( Dioph ` 3 )