Theorem 0dioph

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

	Ref	Expression
Assertion	0dioph	|- ( A e. NN0 -> (/) e. ( Dioph ` A ) )

Proof

Step	Hyp	Ref	Expression
1		ax-1ne0	|- 1 =/= 0
2	1	neii	|- -. 1 = 0
3	2	rgenw	|- A. a e. ( NN0 ^m ( 1 ... A ) ) -. 1 = 0
4		rabeq0	|- ( { a e. ( NN0 ^m ( 1 ... A ) ) | 1 = 0 } = (/) <-> A. a e. ( NN0 ^m ( 1 ... A ) ) -. 1 = 0 )
5	3 4	mpbir	|- { a e. ( NN0 ^m ( 1 ... A ) ) | 1 = 0 } = (/)
6		ovex	|- ( 1 ... A ) e. _V
7		1z	|- 1 e. ZZ
8		mzpconstmpt	|- ( ( ( 1 ... A ) e. _V /\ 1 e. ZZ ) -> ( a e. ( ZZ ^m ( 1 ... A ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... A ) ) )
9	6 7 8	mp2an	|- ( a e. ( ZZ ^m ( 1 ... A ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... A ) )
10		eq0rabdioph	|- ( ( A e. NN0 /\ ( a e. ( ZZ ^m ( 1 ... A ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... A ) ) ) -> { a e. ( NN0 ^m ( 1 ... A ) ) | 1 = 0 } e. ( Dioph ` A ) )
11	9 10	mpan2	|- ( A e. NN0 -> { a e. ( NN0 ^m ( 1 ... A ) ) | 1 = 0 } e. ( Dioph ` A ) )
12	5 11	eqeltrrid	|- ( A e. NN0 -> (/) e. ( Dioph ` A ) )