Metamath Proof Explorer

Theorem vdwap1

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

Ref Expression
Assertion vdwap1 ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ 1 ) 𝐷 ) = { 𝐴 } )

Proof

Step Hyp Ref Expression
1 1e0p1 ⊢ 1 = ( 0 + 1 )
2 1 fveq2i ⊢ ( AP ‘ 1 ) = ( AP ‘ ( 0 + 1 ) )
3 2 oveqi ⊢ ( 𝐴 ( AP ‘ 1 ) 𝐷 ) = ( 𝐴 ( AP ‘ ( 0 + 1 ) ) 𝐷 )
4 0nn0 ⊢ 0 ∈ ℕ0
5 vdwapun ⊢ ( ( 0 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ ( 0 + 1 ) ) 𝐷 ) = ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 0 ) 𝐷 ) ) )
6 4 5 mp3an1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ ( 0 + 1 ) ) 𝐷 ) = ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 0 ) 𝐷 ) ) )
7 3 6 syl5eq ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ 1 ) 𝐷 ) = ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 0 ) 𝐷 ) ) )
8 nnaddcl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 + 𝐷 ) ∈ ℕ )
9 vdwap0 ⊢ ( ( ( 𝐴 + 𝐷 ) ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ( 𝐴 + 𝐷 ) ( AP ‘ 0 ) 𝐷 ) = ∅ )
10 8 9 sylancom ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ( 𝐴 + 𝐷 ) ( AP ‘ 0 ) 𝐷 ) = ∅ )
11 10 uneq2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 0 ) 𝐷 ) ) = ( { 𝐴 } ∪ ∅ ) )
12 un0 ⊢ ( { 𝐴 } ∪ ∅ ) = { 𝐴 }
13 11 12 eqtrdi ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 0 ) 𝐷 ) ) = { 𝐴 } )
14 7 13 eqtrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ 1 ) 𝐷 ) = { 𝐴 } )