Theorem 0dioph

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

	Ref	Expression
Assertion	0dioph	⊢ ( 𝐴 ∈ ℕ0 → ∅ ∈ ( Dioph ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-1ne0	⊢ 1 ≠ 0
2	1	neii	⊢ ¬ 1 = 0
3	2	rgenw	⊢ ∀ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ¬ 1 = 0
4		rabeq0	⊢ ( { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 1 = 0 } = ∅ ↔ ∀ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ¬ 1 = 0 )
5	3 4	mpbir	⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 1 = 0 } = ∅
6		ovex	⊢ ( 1 ... 𝐴 ) ∈ V
7		1z	⊢ 1 ∈ ℤ
8		mzpconstmpt	⊢ ( ( ( 1 ... 𝐴 ) ∈ V ∧ 1 ∈ ℤ ) → ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 𝐴 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 𝐴 ) ) )
9	6 7 8	mp2an	⊢ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 𝐴 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 𝐴 ) )
10		eq0rabdioph	⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 𝐴 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 𝐴 ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 1 = 0 } ∈ ( Dioph ‘ 𝐴 ) )
11	9 10	mpan2	⊢ ( 𝐴 ∈ ℕ0 → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 1 = 0 } ∈ ( Dioph ‘ 𝐴 ) )
12	5 11	eqeltrrid	⊢ ( 𝐴 ∈ ℕ0 → ∅ ∈ ( Dioph ‘ 𝐴 ) )