vdwap1

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

		Ref	Expression
	Assertion	vdwap1	$⊢ (A \in ℕ \land D \in ℕ) \to A AP (1) D = \{A\}$

Step	Hyp	Ref	Expression
1		1e0p1	$⊢ 1 = 0 + 1$
2	1	fveq2i	$⊢ AP (1) = AP (0 + 1)$
3	2	oveqi	$⊢ A AP (1) D = A AP (0 + 1) D$
4		0nn0	$⊢ 0 \in ℕ_{0}$
5		vdwapun	$⊢ (0 \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to A AP (0 + 1) D = \{A\} \cup ((A + D) AP (0) D)$
6	4 5	mp3an1	$⊢ (A \in ℕ \land D \in ℕ) \to A AP (0 + 1) D = \{A\} \cup ((A + D) AP (0) D)$
7	3 6	eqtrid	$⊢ (A \in ℕ \land D \in ℕ) \to A AP (1) D = \{A\} \cup ((A + D) AP (0) D)$
8		nnaddcl	$⊢ (A \in ℕ \land D \in ℕ) \to A + D \in ℕ$
9		vdwap0	$⊢ (A + D \in ℕ \land D \in ℕ) \to (A + D) AP (0) D = \emptyset$
10	8 9	sylancom	$⊢ (A \in ℕ \land D \in ℕ) \to (A + D) AP (0) D = \emptyset$
11	10	uneq2d	$⊢ (A \in ℕ \land D \in ℕ) \to \{A\} \cup ((A + D) AP (0) D) = \{A\} \cup \emptyset$
12		un0	$⊢ \{A\} \cup \emptyset = \{A\}$
13	11 12	eqtrdi	$⊢ (A \in ℕ \land D \in ℕ) \to \{A\} \cup ((A + D) AP (0) D) = \{A\}$
14	7 13	eqtrd	$⊢ (A \in ℕ \land D \in ℕ) \to A AP (1) D = \{A\}$

Metamath Proof Explorer