Metamath Proof Explorer


Theorem 0dioph

Description: The null set is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion 0dioph A0DiophA

Proof

Step Hyp Ref Expression
1 ax-1ne0 10
2 1 neii ¬1=0
3 2 rgenw a01A¬1=0
4 rabeq0 a01A|1=0=a01A¬1=0
5 3 4 mpbir a01A|1=0=
6 ovex 1AV
7 1z 1
8 mzpconstmpt 1AV1a1A1mzPoly1A
9 6 7 8 mp2an a1A1mzPoly1A
10 eq0rabdioph A0a1A1mzPoly1Aa01A|1=0DiophA
11 9 10 mpan2 A0a01A|1=0DiophA
12 5 11 eqeltrrid A0DiophA