vdwapval

Description: Value of the arithmetic progression function. (Contributed by Mario Carneiro, 18-Aug-2014)

		Ref	Expression
	Assertion	vdwapval	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (X \in (A AP (K) D) \leftrightarrow \exists m \in (0 \dots K - 1) X = A + m D)$

Proof

Step	Hyp	Ref	Expression
1		vdwapfval	$⊢ K \in ℕ_{0} \to AP (K) = (a \in ℕ, d \in ℕ ⟼ ran (m \in (0 \dots K - 1) ⟼ a + m d))$
2	1	3ad2ant1	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to AP (K) = (a \in ℕ, d \in ℕ ⟼ ran (m \in (0 \dots K - 1) ⟼ a + m d))$
3	2	oveqd	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to A AP (K) D = A (a \in ℕ, d \in ℕ ⟼ ran (m \in (0 \dots K - 1) ⟼ a + m d)) D$
4		oveq2	$⊢ d = D \to m d = m D$
5		oveq12	$⊢ (a = A \land m d = m D) \to a + m d = A + m D$
6	4 5	sylan2	$⊢ (a = A \land d = D) \to a + m d = A + m D$
7	6	mpteq2dv	$⊢ (a = A \land d = D) \to (m \in (0 \dots K - 1) ⟼ a + m d) = (m \in (0 \dots K - 1) ⟼ A + m D)$
8	7	rneqd	$⊢ (a = A \land d = D) \to ran (m \in (0 \dots K - 1) ⟼ a + m d) = ran (m \in (0 \dots K - 1) ⟼ A + m D)$
9		eqid	$⊢ (a \in ℕ, d \in ℕ ⟼ ran (m \in (0 \dots K - 1) ⟼ a + m d)) = (a \in ℕ, d \in ℕ ⟼ ran (m \in (0 \dots K - 1) ⟼ a + m d))$
10		ovex	$⊢ (0 \dots K - 1) \in V$
11	10	mptex	$⊢ (m \in (0 \dots K - 1) ⟼ A + m D) \in V$
12	11	rnex	$⊢ ran (m \in (0 \dots K - 1) ⟼ A + m D) \in V$
13	8 9 12	ovmpoa	$⊢ (A \in ℕ \land D \in ℕ) \to A (a \in ℕ, d \in ℕ ⟼ ran (m \in (0 \dots K - 1) ⟼ a + m d)) D = ran (m \in (0 \dots K - 1) ⟼ A + m D)$
14	13	3adant1	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to A (a \in ℕ, d \in ℕ ⟼ ran (m \in (0 \dots K - 1) ⟼ a + m d)) D = ran (m \in (0 \dots K - 1) ⟼ A + m D)$
15	3 14	eqtrd	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to A AP (K) D = ran (m \in (0 \dots K - 1) ⟼ A + m D)$
16		eqid	$⊢ (m \in (0 \dots K - 1) ⟼ A + m D) = (m \in (0 \dots K - 1) ⟼ A + m D)$
17	16	rnmpt	$⊢ ran (m \in (0 \dots K - 1) ⟼ A + m D) = \{x \| \exists m \in (0 \dots K - 1) x = A + m D\}$
18	15 17	eqtrdi	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to A AP (K) D = \{x \| \exists m \in (0 \dots K - 1) x = A + m D\}$
19	18	eleq2d	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (X \in (A AP (K) D) \leftrightarrow X \in \{x \| \exists m \in (0 \dots K - 1) x = A + m D\})$
20		id	$⊢ X = A + m D \to X = A + m D$
21		ovex	$⊢ A + m D \in V$
22	20 21	eqeltrdi	$⊢ X = A + m D \to X \in V$
23	22	rexlimivw	$⊢ \exists m \in (0 \dots K - 1) X = A + m D \to X \in V$
24		eqeq1	$⊢ x = X \to (x = A + m D \leftrightarrow X = A + m D)$
25	24	rexbidv	$⊢ x = X \to (\exists m \in (0 \dots K - 1) x = A + m D \leftrightarrow \exists m \in (0 \dots K - 1) X = A + m D)$
26	23 25	elab3	$⊢ X \in \{x \| \exists m \in (0 \dots K - 1) x = A + m D\} \leftrightarrow \exists m \in (0 \dots K - 1) X = A + m D$
27	19 26	bitrdi	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (X \in (A AP (K) D) \leftrightarrow \exists m \in (0 \dots K - 1) X = A + m D)$

Metamath Proof Explorer

Theorem vdwapval

Proof