Metamath Proof Explorer

Theorem vdwap1

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

Ref Expression
Assertion vdwap1 ⊢ A ∈ ℕ ∧ D ∈ ℕ → A AP ⁡ 1 D = A

Proof

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 ∈ ℕ 0
5 vdwapun ⊢ 0 ∈ ℕ 0 ∧ A ∈ ℕ ∧ D ∈ ℕ → A AP ⁡ 0 + 1 D = A ∪ A + D AP ⁡ 0 D
6 4 5 mp3an1 ⊢ A ∈ ℕ ∧ D ∈ ℕ → A AP ⁡ 0 + 1 D = A ∪ A + D AP ⁡ 0 D
7 3 6 eqtrid ⊢ A ∈ ℕ ∧ D ∈ ℕ → A AP ⁡ 1 D = A ∪ A + D AP ⁡ 0 D
8 nnaddcl ⊢ A ∈ ℕ ∧ D ∈ ℕ → A + D ∈ ℕ
9 vdwap0 ⊢ A + D ∈ ℕ ∧ D ∈ ℕ → A + D AP ⁡ 0 D = ∅
10 8 9 sylancom ⊢ A ∈ ℕ ∧ D ∈ ℕ → A + D AP ⁡ 0 D = ∅
11 10 uneq2d ⊢ A ∈ ℕ ∧ D ∈ ℕ → A ∪ A + D AP ⁡ 0 D = A ∪ ∅
12 un0 ⊢ A ∪ ∅ = A
13 11 12 eqtrdi ⊢ A ∈ ℕ ∧ D ∈ ℕ → A ∪ A + D AP ⁡ 0 D = A
14 7 13 eqtrd ⊢ A ∈ ℕ ∧ D ∈ ℕ → A AP ⁡ 1 D = A