Metamath Proof Explorer

Theorem vdwap0

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

Ref Expression
Assertion vdwap0 
|- ( ( A e. NN /\ D e. NN ) -> ( A ( AP ` 0 ) D ) = (/) )

Proof

Step Hyp Ref Expression
1 noel 
 |-  -. m e. (/)
2 1 pm2.21i 
 |-  ( m e. (/) -> -. x = ( A + ( m x. D ) ) )
3 risefall0lem 
 |-  ( 0 ... ( 0 - 1 ) ) = (/)
4 2 3 eleq2s 
 |-  ( m e. ( 0 ... ( 0 - 1 ) ) -> -. x = ( A + ( m x. D ) ) )
5 4 nrex 
 |-  -. E. m e. ( 0 ... ( 0 - 1 ) ) x = ( A + ( m x. D ) )
6 0nn0 
 |-  0 e. NN0
7 vdwapval 
 |-  ( ( 0 e. NN0 /\ A e. NN /\ D e. NN ) -> ( x e. ( A ( AP ` 0 ) D ) <-> E. m e. ( 0 ... ( 0 - 1 ) ) x = ( A + ( m x. D ) ) ) )
8 6 7 mp3an1 
 |-  ( ( A e. NN /\ D e. NN ) -> ( x e. ( A ( AP ` 0 ) D ) <-> E. m e. ( 0 ... ( 0 - 1 ) ) x = ( A + ( m x. D ) ) ) )
9 5 8 mtbiri 
 |-  ( ( A e. NN /\ D e. NN ) -> -. x e. ( A ( AP ` 0 ) D ) )
10 9 eq0rdv 
 |-  ( ( A e. NN /\ D e. NN ) -> ( A ( AP ` 0 ) D ) = (/) )