Metamath Proof Explorer


Theorem rmxdioph

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

Ref Expression
Assertion rmxdioph a 0 1 3 | a 1 2 a 3 = a 1 X rm a 2 Dioph 3

Proof

Step Hyp Ref Expression
1 simpr a 0 1 3 a 1 2 a 1 2
2 elmapi a 0 1 3 a : 1 3 0
3 df-3 3 = 2 + 1
4 ssid 1 3 1 3
5 3 4 jm2.27dlem5 1 2 1 3
6 2nn 2
7 6 jm2.27dlem3 2 1 2
8 5 7 sselii 2 1 3
9 ffvelrn a : 1 3 0 2 1 3 a 2 0
10 2 8 9 sylancl a 0 1 3 a 2 0
11 10 adantr a 0 1 3 a 1 2 a 2 0
12 3nn 3
13 12 jm2.27dlem3 3 1 3
14 ffvelrn a : 1 3 0 3 1 3 a 3 0
15 2 13 14 sylancl a 0 1 3 a 3 0
16 15 adantr a 0 1 3 a 1 2 a 3 0
17 rmxdiophlem a 1 2 a 2 0 a 3 0 a 3 = a 1 X rm a 2 b 0 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1
18 1 11 16 17 syl3anc a 0 1 3 a 1 2 a 3 = a 1 X rm a 2 b 0 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1
19 18 pm5.32da a 0 1 3 a 1 2 a 3 = a 1 X rm a 2 a 1 2 b 0 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1
20 anass a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1 a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1
21 20 rexbii b 0 a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1 b 0 a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1
22 r19.42v b 0 a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1 a 1 2 b 0 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1
23 21 22 bitr2i a 1 2 b 0 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1 b 0 a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1
24 19 23 bitrdi a 0 1 3 a 1 2 a 3 = a 1 X rm a 2 b 0 a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1
25 24 rabbiia a 0 1 3 | a 1 2 a 3 = a 1 X rm a 2 = a 0 1 3 | b 0 a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1
26 3nn0 3 0
27 vex c V
28 27 resex c 1 3 V
29 fvex c 4 V
30 df-2 2 = 1 + 1
31 30 5 jm2.27dlem5 1 1 1 3
32 1nn 1
33 32 jm2.27dlem3 1 1 1
34 31 33 sselii 1 1 3
35 34 jm2.27dlem1 a = c 1 3 a 1 = c 1
36 35 eleq1d a = c 1 3 a 1 2 c 1 2
37 36 adantr a = c 1 3 b = c 4 a 1 2 c 1 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 Y rm a 2 = c 1 Y rm c 2
41 40 adantr a = c 1 3 b = c 4 a 1 Y rm a 2 = c 1 Y rm c 2
42 38 41 eqeq12d a = c 1 3 b = c 4 b = a 1 Y rm a 2 c 4 = c 1 Y rm c 2
43 37 42 anbi12d a = c 1 3 b = c 4 a 1 2 b = a 1 Y rm a 2 c 1 2 c 4 = c 1 Y rm 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 b 2 = c 1 2 1 c 4 2
51 46 50 oveq12d a = c 1 3 b = c 4 a 3 2 a 1 2 1 b 2 = c 3 2 c 1 2 1 c 4 2
52 51 eqeq1d a = c 1 3 b = c 4 a 3 2 a 1 2 1 b 2 = 1 c 3 2 c 1 2 1 c 4 2 = 1
53 43 52 anbi12d a = c 1 3 b = c 4 a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1 c 1 2 c 4 = c 1 Y rm c 2 c 3 2 c 1 2 1 c 4 2 = 1
54 28 29 53 sbc2ie [˙ c 1 3 / a]˙ [˙ c 4 / b]˙ a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1 c 1 2 c 4 = c 1 Y rm c 2 c 3 2 c 1 2 1 c 4 2 = 1
55 54 rabbii c 0 1 4 | [˙ c 1 3 / a]˙ [˙ c 4 / b]˙ a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1 = c 0 1 4 | c 1 2 c 4 = c 1 Y rm c 2 c 3 2 c 1 2 1 c 4 2 = 1
56 4nn0 4 0
57 rmydioph b 0 1 3 | b 1 2 b 3 = b 1 Y rm b 2 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 2 c 1 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 Y rm b 2 = c 1 Y rm c 2
63 60 62 eqeq12d b 1 = c 1 b 2 = c 2 b 3 = c 4 b 3 = b 1 Y rm b 2 c 4 = c 1 Y rm c 2
64 59 63 anbi12d b 1 = c 1 b 2 = c 2 b 3 = c 4 b 1 2 b 3 = b 1 Y rm b 2 c 1 2 c 4 = c 1 Y rm c 2
65 df-4 4 = 3 + 1
66 ssid 1 4 1 4
67 65 66 jm2.27dlem5 1 3 1 4
68 3 67 jm2.27dlem5 1 2 1 4
69 30 68 jm2.27dlem5 1 1 1 4
70 69 33 sselii 1 1 4
71 68 7 sselii 2 1 4
72 4nn 4
73 72 jm2.27dlem3 4 1 4
74 64 70 71 73 rabren3dioph 4 0 b 0 1 3 | b 1 2 b 3 = b 1 Y rm b 2 Dioph 3 c 0 1 4 | c 1 2 c 4 = c 1 Y rm c 2 Dioph 4
75 56 57 74 mp2an c 0 1 4 | c 1 2 c 4 = c 1 Y rm c 2 Dioph 4
76 ovex 1 4 V
77 67 13 sselii 3 1 4
78 mzpproj 1 4 V 3 1 4 c 1 4 c 3 mzPoly 1 4
79 76 77 78 mp2an c 1 4 c 3 mzPoly 1 4
80 2nn0 2 0
81 mzpexpmpt c 1 4 c 3 mzPoly 1 4 2 0 c 1 4 c 3 2 mzPoly 1 4
82 79 80 81 mp2an c 1 4 c 3 2 mzPoly 1 4
83 mzpproj 1 4 V 1 1 4 c 1 4 c 1 mzPoly 1 4
84 76 70 83 mp2an c 1 4 c 1 mzPoly 1 4
85 mzpexpmpt c 1 4 c 1 mzPoly 1 4 2 0 c 1 4 c 1 2 mzPoly 1 4
86 84 80 85 mp2an c 1 4 c 1 2 mzPoly 1 4
87 1z 1
88 mzpconstmpt 1 4 V 1 c 1 4 1 mzPoly 1 4
89 76 87 88 mp2an c 1 4 1 mzPoly 1 4
90 mzpsubmpt c 1 4 c 1 2 mzPoly 1 4 c 1 4 1 mzPoly 1 4 c 1 4 c 1 2 1 mzPoly 1 4
91 86 89 90 mp2an c 1 4 c 1 2 1 mzPoly 1 4
92 mzpproj 1 4 V 4 1 4 c 1 4 c 4 mzPoly 1 4
93 76 73 92 mp2an c 1 4 c 4 mzPoly 1 4
94 mzpexpmpt c 1 4 c 4 mzPoly 1 4 2 0 c 1 4 c 4 2 mzPoly 1 4
95 93 80 94 mp2an c 1 4 c 4 2 mzPoly 1 4
96 mzpmulmpt c 1 4 c 1 2 1 mzPoly 1 4 c 1 4 c 4 2 mzPoly 1 4 c 1 4 c 1 2 1 c 4 2 mzPoly 1 4
97 91 95 96 mp2an c 1 4 c 1 2 1 c 4 2 mzPoly 1 4
98 mzpsubmpt c 1 4 c 3 2 mzPoly 1 4 c 1 4 c 1 2 1 c 4 2 mzPoly 1 4 c 1 4 c 3 2 c 1 2 1 c 4 2 mzPoly 1 4
99 82 97 98 mp2an c 1 4 c 3 2 c 1 2 1 c 4 2 mzPoly 1 4
100 eqrabdioph 4 0 c 1 4 c 3 2 c 1 2 1 c 4 2 mzPoly 1 4 c 1 4 1 mzPoly 1 4 c 0 1 4 | c 3 2 c 1 2 1 c 4 2 = 1 Dioph 4
101 56 99 89 100 mp3an c 0 1 4 | c 3 2 c 1 2 1 c 4 2 = 1 Dioph 4
102 anrabdioph c 0 1 4 | c 1 2 c 4 = c 1 Y rm c 2 Dioph 4 c 0 1 4 | c 3 2 c 1 2 1 c 4 2 = 1 Dioph 4 c 0 1 4 | c 1 2 c 4 = c 1 Y rm c 2 c 3 2 c 1 2 1 c 4 2 = 1 Dioph 4
103 75 101 102 mp2an c 0 1 4 | c 1 2 c 4 = c 1 Y rm c 2 c 3 2 c 1 2 1 c 4 2 = 1 Dioph 4
104 55 103 eqeltri c 0 1 4 | [˙ c 1 3 / a]˙ [˙ c 4 / b]˙ a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1 Dioph 4
105 65 rexfrabdioph 3 0 c 0 1 4 | [˙ c 1 3 / a]˙ [˙ c 4 / b]˙ a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1 Dioph 4 a 0 1 3 | b 0 a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1 Dioph 3
106 26 104 105 mp2an a 0 1 3 | b 0 a 1 2 b = a 1 Y rm a 2 a 3 2 a 1 2 1 b 2 = 1 Dioph 3
107 25 106 eqeltri a 0 1 3 | a 1 2 a 3 = a 1 X rm a 2 Dioph 3