Metamath Proof Explorer

Theorem vdwapid1

Description: The first element of an arithmetic progression. (Contributed by Mario Carneiro, 12-Sep-2014)

Ref Expression
Assertion vdwapid1 ⊢ K ∈ ℕ ∧ A ∈ ℕ ∧ D ∈ ℕ → A ∈ A AP ⁡ K D

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ A ⊆ A ∪ A + D AP ⁡ K − 1 D
2 snssg ⊢ A ∈ ℕ → A ∈ A ∪ A + D AP ⁡ K − 1 D ↔ A ⊆ A ∪ A + D AP ⁡ K − 1 D
3 2 3ad2ant2 ⊢ K ∈ ℕ ∧ A ∈ ℕ ∧ D ∈ ℕ → A ∈ A ∪ A + D AP ⁡ K − 1 D ↔ A ⊆ A ∪ A + D AP ⁡ K − 1 D
4 1 3 mpbiri ⊢ K ∈ ℕ ∧ A ∈ ℕ ∧ D ∈ ℕ → A ∈ A ∪ A + D AP ⁡ K − 1 D
5 nncn ⊢ K ∈ ℕ → K ∈ ℂ
6 5 3ad2ant1 ⊢ K ∈ ℕ ∧ A ∈ ℕ ∧ D ∈ ℕ → K ∈ ℂ
7 ax-1cn ⊢ 1 ∈ ℂ
8 npcan ⊢ K ∈ ℂ ∧ 1 ∈ ℂ → K - 1 + 1 = K
9 6 7 8 sylancl ⊢ K ∈ ℕ ∧ A ∈ ℕ ∧ D ∈ ℕ → K - 1 + 1 = K
10 9 fveq2d ⊢ K ∈ ℕ ∧ A ∈ ℕ ∧ D ∈ ℕ → AP ⁡ K - 1 + 1 = AP ⁡ K
11 10 oveqd ⊢ K ∈ ℕ ∧ A ∈ ℕ ∧ D ∈ ℕ → A AP ⁡ K - 1 + 1 D = A AP ⁡ K D
12 nnm1nn0 ⊢ K ∈ ℕ → K − 1 ∈ ℕ 0
13 vdwapun ⊢ K − 1 ∈ ℕ 0 ∧ A ∈ ℕ ∧ D ∈ ℕ → A AP ⁡ K - 1 + 1 D = A ∪ A + D AP ⁡ K − 1 D
14 12 13 syl3an1 ⊢ K ∈ ℕ ∧ A ∈ ℕ ∧ D ∈ ℕ → A AP ⁡ K - 1 + 1 D = A ∪ A + D AP ⁡ K − 1 D
15 11 14 eqtr3d ⊢ K ∈ ℕ ∧ A ∈ ℕ ∧ D ∈ ℕ → A AP ⁡ K D = A ∪ A + D AP ⁡ K − 1 D
16 4 15 eleqtrrd ⊢ K ∈ ℕ ∧ A ∈ ℕ ∧ D ∈ ℕ → A ∈ A AP ⁡ K D