Metamath Proof Explorer

Theorem vdwapf

Description: The arithmetic progression function is a function. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Assertion vdwapf ⊢ K ∈ ℕ 0 → AP ⁡ K : ℕ × ℕ ⟶ 𝒫 ℕ

Proof

Step Hyp Ref Expression
1 simpll ⊢ a ∈ ℕ ∧ d ∈ ℕ ∧ m ∈ 0 … K − 1 → a ∈ ℕ
2 elfznn0 ⊢ m ∈ 0 … K − 1 → m ∈ ℕ 0
3 2 adantl ⊢ a ∈ ℕ ∧ d ∈ ℕ ∧ m ∈ 0 … K − 1 → m ∈ ℕ 0
4 nnnn0 ⊢ d ∈ ℕ → d ∈ ℕ 0
5 4 ad2antlr ⊢ a ∈ ℕ ∧ d ∈ ℕ ∧ m ∈ 0 … K − 1 → d ∈ ℕ 0
6 3 5 nn0mulcld ⊢ a ∈ ℕ ∧ d ∈ ℕ ∧ m ∈ 0 … K − 1 → m ⁢ d ∈ ℕ 0
7 nnnn0addcl ⊢ a ∈ ℕ ∧ m ⁢ d ∈ ℕ 0 → a + m ⁢ d ∈ ℕ
8 1 6 7 syl2anc ⊢ a ∈ ℕ ∧ d ∈ ℕ ∧ m ∈ 0 … K − 1 → a + m ⁢ d ∈ ℕ
9 8 fmpttd ⊢ a ∈ ℕ ∧ d ∈ ℕ → m ∈ 0 … K − 1 ⟼ a + m ⁢ d : 0 … K − 1 ⟶ ℕ
10 9 frnd ⊢ a ∈ ℕ ∧ d ∈ ℕ → ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d ⊆ ℕ
11 nnex ⊢ ℕ ∈ V
12 11 elpw2 ⊢ ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d ∈ 𝒫 ℕ ↔ ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d ⊆ ℕ
13 10 12 sylibr ⊢ a ∈ ℕ ∧ d ∈ ℕ → ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d ∈ 𝒫 ℕ
14 13 rgen2 ⊢ ∀ a ∈ ℕ ∀ d ∈ ℕ ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d ∈ 𝒫 ℕ
15 eqid ⊢ a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d = a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d
16 15 fmpo ⊢ ∀ a ∈ ℕ ∀ d ∈ ℕ ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d ∈ 𝒫 ℕ ↔ a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d : ℕ × ℕ ⟶ 𝒫 ℕ
17 14 16 mpbi ⊢ a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d : ℕ × ℕ ⟶ 𝒫 ℕ
18 vdwapfval ⊢ K ∈ ℕ 0 → AP ⁡ K = a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d
19 18 feq1d ⊢ K ∈ ℕ 0 → AP ⁡ K : ℕ × ℕ ⟶ 𝒫 ℕ ↔ a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d : ℕ × ℕ ⟶ 𝒫 ℕ
20 17 19 mpbiri ⊢ K ∈ ℕ 0 → AP ⁡ K : ℕ × ℕ ⟶ 𝒫 ℕ