Theorem vdwapid1

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

	Ref	Expression
Assertion	vdwapid1	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → 𝐴 ∈ ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) )

Proof

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