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 e. NN /\ D e. NN ) -> ( 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 e. NN0
5 vdwapun 
 |-  ( ( 0 e. NN0 /\ A e. NN /\ D e. NN ) -> ( A ( AP ` ( 0 + 1 ) ) D ) = ( { A } u. ( ( A + D ) ( AP ` 0 ) D ) ) )
6 4 5 mp3an1 
 |-  ( ( A e. NN /\ D e. NN ) -> ( A ( AP ` ( 0 + 1 ) ) D ) = ( { A } u. ( ( A + D ) ( AP ` 0 ) D ) ) )
7 3 6 syl5eq 
 |-  ( ( A e. NN /\ D e. NN ) -> ( A ( AP ` 1 ) D ) = ( { A } u. ( ( A + D ) ( AP ` 0 ) D ) ) )
8 nnaddcl 
 |-  ( ( A e. NN /\ D e. NN ) -> ( A + D ) e. NN )
9 vdwap0 
 |-  ( ( ( A + D ) e. NN /\ D e. NN ) -> ( ( A + D ) ( AP ` 0 ) D ) = (/) )
10 8 9 sylancom 
 |-  ( ( A e. NN /\ D e. NN ) -> ( ( A + D ) ( AP ` 0 ) D ) = (/) )
11 10 uneq2d 
 |-  ( ( A e. NN /\ D e. NN ) -> ( { A } u. ( ( A + D ) ( AP ` 0 ) D ) ) = ( { A } u. (/) ) )
12 un0 
 |-  ( { A } u. (/) ) = { A }
13 11 12 eqtrdi 
 |-  ( ( A e. NN /\ D e. NN ) -> ( { A } u. ( ( A + D ) ( AP ` 0 ) D ) ) = { A } )
14 7 13 eqtrd 
 |-  ( ( A e. NN /\ D e. NN ) -> ( A ( AP ` 1 ) D ) = { A } )