Metamath Proof Explorer

Theorem vdwapf

Description: The arithmetic progression function is a function. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Assertion vdwapf 
|- ( K e. NN0 -> ( AP ` K ) : ( NN X. NN ) --> ~P NN )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( a e. NN /\ d e. NN ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> a e. NN )
2 elfznn0 
 |-  ( m e. ( 0 ... ( K - 1 ) ) -> m e. NN0 )
3 2 adantl 
 |-  ( ( ( a e. NN /\ d e. NN ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> m e. NN0 )
4 nnnn0 
 |-  ( d e. NN -> d e. NN0 )
5 4 ad2antlr 
 |-  ( ( ( a e. NN /\ d e. NN ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> d e. NN0 )
6 3 5 nn0mulcld 
 |-  ( ( ( a e. NN /\ d e. NN ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. d ) e. NN0 )
7 nnnn0addcl 
 |-  ( ( a e. NN /\ ( m x. d ) e. NN0 ) -> ( a + ( m x. d ) ) e. NN )
8 1 6 7 syl2anc 
 |-  ( ( ( a e. NN /\ d e. NN ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( a + ( m x. d ) ) e. NN )
9 8 fmpttd 
 |-  ( ( a e. NN /\ d e. NN ) -> ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) : ( 0 ... ( K - 1 ) ) --> NN )
10 9 frnd 
 |-  ( ( a e. NN /\ d e. NN ) -> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) C_ NN )
11 nnex 
 |-  NN e. _V
12 11 elpw2 
 |-  ( ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) e. ~P NN <-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) C_ NN )
13 10 12 sylibr 
 |-  ( ( a e. NN /\ d e. NN ) -> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) e. ~P NN )
14 13 rgen2 
 |-  A. a e. NN A. d e. NN ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) e. ~P NN
15 eqid 
 |-  ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) = ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) )
16 15 fmpo 
 |-  ( A. a e. NN A. d e. NN ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) e. ~P NN <-> ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) : ( NN X. NN ) --> ~P NN )
17 14 16 mpbi 
 |-  ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) : ( NN X. NN ) --> ~P NN
18 vdwapfval 
 |-  ( K e. NN0 -> ( AP ` K ) = ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )
19 18 feq1d 
 |-  ( K e. NN0 -> ( ( AP ` K ) : ( NN X. NN ) --> ~P NN <-> ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) : ( NN X. NN ) --> ~P NN ) )
20 17 19 mpbiri 
 |-  ( K e. NN0 -> ( AP ` K ) : ( NN X. NN ) --> ~P NN )