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∈AAP⁡KD

Proof

Step Hyp Ref Expression
1 ssun1 ⊢A⊆A∪A+DAP⁡K−1D
2 snssg ⊢A∈ℕ→A∈A∪A+DAP⁡K−1D↔A⊆A∪A+DAP⁡K−1D
3 2 3ad2ant2 ⊢K∈ℕ∧A∈ℕ∧D∈ℕ→A∈A∪A+DAP⁡K−1D↔A⊆A∪A+DAP⁡K−1D
4 1 3 mpbiri ⊢K∈ℕ∧A∈ℕ∧D∈ℕ→A∈A∪A+DAP⁡K−1D
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∈ℕ→AAP⁡K-1+1D=AAP⁡KD
12 nnm1nn0 ⊢K∈ℕ→K−1∈ℕ0
13 vdwapun ⊢K−1∈ℕ0∧A∈ℕ∧D∈ℕ→AAP⁡K-1+1D=A∪A+DAP⁡K−1D
14 12 13 syl3an1 ⊢K∈ℕ∧A∈ℕ∧D∈ℕ→AAP⁡K-1+1D=A∪A+DAP⁡K−1D
15 11 14 eqtr3d ⊢K∈ℕ∧A∈ℕ∧D∈ℕ→AAP⁡KD=A∪A+DAP⁡K−1D
16 4 15 eleqtrrd ⊢K∈ℕ∧A∈ℕ∧D∈ℕ→A∈AAP⁡KD