Description: The null set is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | 0dioph | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1ne0 | |
|
2 | 1 | neii | |
3 | 2 | rgenw | |
4 | rabeq0 | |
|
5 | 3 4 | mpbir | |
6 | ovex | |
|
7 | 1z | |
|
8 | mzpconstmpt | |
|
9 | 6 7 8 | mp2an | |
10 | eq0rabdioph | |
|
11 | 9 10 | mpan2 | |
12 | 5 11 | eqeltrrid | |