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 e. NN /\ A e. NN /\ D e. NN ) -> A e. ( A ( AP ` K ) D ) )

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  { A } C_ ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) )
2 snssg 
 |-  ( A e. NN -> ( A e. ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) <-> { A } C_ ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) ) )
3 2 3ad2ant2 
 |-  ( ( K e. NN /\ A e. NN /\ D e. NN ) -> ( A e. ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) <-> { A } C_ ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) ) )
4 1 3 mpbiri 
 |-  ( ( K e. NN /\ A e. NN /\ D e. NN ) -> A e. ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) )
5 nncn 
 |-  ( K e. NN -> K e. CC )
6 5 3ad2ant1 
 |-  ( ( K e. NN /\ A e. NN /\ D e. NN ) -> K e. CC )
7 ax-1cn 
 |-  1 e. CC
8 npcan 
 |-  ( ( K e. CC /\ 1 e. CC ) -> ( ( K - 1 ) + 1 ) = K )
9 6 7 8 sylancl 
 |-  ( ( K e. NN /\ A e. NN /\ D e. NN ) -> ( ( K - 1 ) + 1 ) = K )
10 9 fveq2d 
 |-  ( ( K e. NN /\ A e. NN /\ D e. NN ) -> ( AP ` ( ( K - 1 ) + 1 ) ) = ( AP ` K ) )
11 10 oveqd 
 |-  ( ( K e. NN /\ A e. NN /\ D e. NN ) -> ( A ( AP ` ( ( K - 1 ) + 1 ) ) D ) = ( A ( AP ` K ) D ) )
12 nnm1nn0 
 |-  ( K e. NN -> ( K - 1 ) e. NN0 )
13 vdwapun 
 |-  ( ( ( K - 1 ) e. NN0 /\ A e. NN /\ D e. NN ) -> ( A ( AP ` ( ( K - 1 ) + 1 ) ) D ) = ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) )
14 12 13 syl3an1 
 |-  ( ( K e. NN /\ A e. NN /\ D e. NN ) -> ( A ( AP ` ( ( K - 1 ) + 1 ) ) D ) = ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) )
15 11 14 eqtr3d 
 |-  ( ( K e. NN /\ A e. NN /\ D e. NN ) -> ( A ( AP ` K ) D ) = ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) )
16 4 15 eleqtrrd 
 |-  ( ( K e. NN /\ A e. NN /\ D e. NN ) -> A e. ( A ( AP ` K ) D ) )