vdwap0

Description: Value of a length-1 arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014)

		Ref	Expression
	Assertion	vdwap0	$⊢ (A \in ℕ \land D \in ℕ) \to A AP (0) D = \emptyset$

Step	Hyp	Ref	Expression
1		noel	$⊢ \neg m \in \emptyset$
2	1	pm2.21i	$⊢ m \in \emptyset \to \neg x = A + m D$
3		risefall0lem	$⊢ (0 \dots 0 - 1) = \emptyset$
4	2 3	eleq2s	$⊢ m \in (0 \dots 0 - 1) \to \neg x = A + m D$
5	4	nrex	$⊢ \neg \exists m \in (0 \dots 0 - 1) x = A + m D$
6		0nn0	$⊢ 0 \in ℕ_{0}$
7		vdwapval	$⊢ (0 \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (x \in (A AP (0) D) \leftrightarrow \exists m \in (0 \dots 0 - 1) x = A + m D)$
8	6 7	mp3an1	$⊢ (A \in ℕ \land D \in ℕ) \to (x \in (A AP (0) D) \leftrightarrow \exists m \in (0 \dots 0 - 1) x = A + m D)$
9	5 8	mtbiri	$⊢ (A \in ℕ \land D \in ℕ) \to \neg x \in (A AP (0) D)$
10	9	eq0rdv	$⊢ (A \in ℕ \land D \in ℕ) \to A AP (0) D = \emptyset$

Metamath Proof Explorer