Metamath Proof Explorer

Theorem dvdsflf1o

Description: A bijection from the numbers less than N / A to the multiples of A less than N . Useful for some sum manipulations. (Contributed by Mario Carneiro, 3-May-2016)

Ref Expression
Hypotheses dvdsflf1o.1 
|- ( ph -> A e. RR )
dvdsflf1o.2 
|- ( ph -> N e. NN )
dvdsflf1o.f 
|- F = ( n e. ( 1 ... ( |_ ` ( A / N ) ) ) |-> ( N x. n ) )
Assertion dvdsflf1o 
|- ( ph -> F : ( 1 ... ( |_ ` ( A / N ) ) ) -1-1-onto-> { x e. ( 1 ... ( |_ ` A ) ) | N || x } )

Proof

Step Hyp Ref Expression
1 dvdsflf1o.1 
 |-  ( ph -> A e. RR )
2 dvdsflf1o.2 
 |-  ( ph -> N e. NN )
3 dvdsflf1o.f 
 |-  F = ( n e. ( 1 ... ( |_ ` ( A / N ) ) ) |-> ( N x. n ) )
4 breq2 
 |-  ( x = ( N x. n ) -> ( N || x <-> N || ( N x. n ) ) )
5 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` ( A / N ) ) ) -> n e. NN )
6 nnmulcl 
 |-  ( ( N e. NN /\ n e. NN ) -> ( N x. n ) e. NN )
7 2 5 6 syl2an 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> ( N x. n ) e. NN )
8 1 2 nndivred 
 |-  ( ph -> ( A / N ) e. RR )
9 fznnfl 
 |-  ( ( A / N ) e. RR -> ( n e. ( 1 ... ( |_ ` ( A / N ) ) ) <-> ( n e. NN /\ n <_ ( A / N ) ) ) )
10 8 9 syl 
 |-  ( ph -> ( n e. ( 1 ... ( |_ ` ( A / N ) ) ) <-> ( n e. NN /\ n <_ ( A / N ) ) ) )
11 10 simplbda 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> n <_ ( A / N ) )
12 5 adantl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> n e. NN )
13 12 nnred 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> n e. RR )
14 1 adantr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> A e. RR )
15 2 nnred 
 |-  ( ph -> N e. RR )
16 15 adantr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> N e. RR )
17 2 nngt0d 
 |-  ( ph -> 0 < N )
18 17 adantr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> 0 < N )
19 lemuldiv2 
 |-  ( ( n e. RR /\ A e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( N x. n ) <_ A <-> n <_ ( A / N ) ) )
20 13 14 16 18 19 syl112anc 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> ( ( N x. n ) <_ A <-> n <_ ( A / N ) ) )
21 11 20 mpbird 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> ( N x. n ) <_ A )
22 2 nnzd 
 |-  ( ph -> N e. ZZ )
23 elfzelz 
 |-  ( n e. ( 1 ... ( |_ ` ( A / N ) ) ) -> n e. ZZ )
24 zmulcl 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> ( N x. n ) e. ZZ )
25 22 23 24 syl2an 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> ( N x. n ) e. ZZ )
26 flge 
 |-  ( ( A e. RR /\ ( N x. n ) e. ZZ ) -> ( ( N x. n ) <_ A <-> ( N x. n ) <_ ( |_ ` A ) ) )
27 14 25 26 syl2anc 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> ( ( N x. n ) <_ A <-> ( N x. n ) <_ ( |_ ` A ) ) )
28 21 27 mpbid 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> ( N x. n ) <_ ( |_ ` A ) )
29 1 flcld 
 |-  ( ph -> ( |_ ` A ) e. ZZ )
30 29 adantr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> ( |_ ` A ) e. ZZ )
31 fznn 
 |-  ( ( |_ ` A ) e. ZZ -> ( ( N x. n ) e. ( 1 ... ( |_ ` A ) ) <-> ( ( N x. n ) e. NN /\ ( N x. n ) <_ ( |_ ` A ) ) ) )
32 30 31 syl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> ( ( N x. n ) e. ( 1 ... ( |_ ` A ) ) <-> ( ( N x. n ) e. NN /\ ( N x. n ) <_ ( |_ ` A ) ) ) )
33 7 28 32 mpbir2and 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> ( N x. n ) e. ( 1 ... ( |_ ` A ) ) )
34 dvdsmul1 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> N || ( N x. n ) )
35 22 23 34 syl2an 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> N || ( N x. n ) )
36 4 33 35 elrabd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> ( N x. n ) e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } )
37 breq2 
 |-  ( x = m -> ( N || x <-> N || m ) )
38 37 elrab 
 |-  ( m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } <-> ( m e. ( 1 ... ( |_ ` A ) ) /\ N || m ) )
39 38 simprbi 
 |-  ( m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } -> N || m )
40 39 adantl 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> N || m )
41 elrabi 
 |-  ( m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } -> m e. ( 1 ... ( |_ ` A ) ) )
42 41 adantl 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> m e. ( 1 ... ( |_ ` A ) ) )
43 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` A ) ) -> m e. NN )
44 42 43 syl 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> m e. NN )
45 2 adantr 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> N e. NN )
46 nndivdvds 
 |-  ( ( m e. NN /\ N e. NN ) -> ( N || m <-> ( m / N ) e. NN ) )
47 44 45 46 syl2anc 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> ( N || m <-> ( m / N ) e. NN ) )
48 40 47 mpbid 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> ( m / N ) e. NN )
49 fznnfl 
 |-  ( A e. RR -> ( m e. ( 1 ... ( |_ ` A ) ) <-> ( m e. NN /\ m <_ A ) ) )
50 1 49 syl 
 |-  ( ph -> ( m e. ( 1 ... ( |_ ` A ) ) <-> ( m e. NN /\ m <_ A ) ) )
51 50 simplbda 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> m <_ A )
52 41 51 sylan2 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> m <_ A )
53 44 nnred 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> m e. RR )
54 1 adantr 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> A e. RR )
55 15 adantr 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> N e. RR )
56 17 adantr 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> 0 < N )
57 lediv1 
 |-  ( ( m e. RR /\ A e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( m <_ A <-> ( m / N ) <_ ( A / N ) ) )
58 53 54 55 56 57 syl112anc 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> ( m <_ A <-> ( m / N ) <_ ( A / N ) ) )
59 52 58 mpbid 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> ( m / N ) <_ ( A / N ) )
60 8 adantr 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> ( A / N ) e. RR )
61 fznnfl 
 |-  ( ( A / N ) e. RR -> ( ( m / N ) e. ( 1 ... ( |_ ` ( A / N ) ) ) <-> ( ( m / N ) e. NN /\ ( m / N ) <_ ( A / N ) ) ) )
62 60 61 syl 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> ( ( m / N ) e. ( 1 ... ( |_ ` ( A / N ) ) ) <-> ( ( m / N ) e. NN /\ ( m / N ) <_ ( A / N ) ) ) )
63 48 59 62 mpbir2and 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> ( m / N ) e. ( 1 ... ( |_ ` ( A / N ) ) ) )
64 44 nncnd 
 |-  ( ( ph /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) -> m e. CC )
65 64 adantrl 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` ( A / N ) ) ) /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) ) -> m e. CC )
66 2 nncnd 
 |-  ( ph -> N e. CC )
67 66 adantr 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` ( A / N ) ) ) /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) ) -> N e. CC )
68 12 nncnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / N ) ) ) ) -> n e. CC )
69 68 adantrr 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` ( A / N ) ) ) /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) ) -> n e. CC )
70 2 nnne0d 
 |-  ( ph -> N =/= 0 )
71 70 adantr 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` ( A / N ) ) ) /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) ) -> N =/= 0 )
72 65 67 69 71 divmuld 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` ( A / N ) ) ) /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) ) -> ( ( m / N ) = n <-> ( N x. n ) = m ) )
73 eqcom 
 |-  ( n = ( m / N ) <-> ( m / N ) = n )
74 eqcom 
 |-  ( m = ( N x. n ) <-> ( N x. n ) = m )
75 72 73 74 3bitr4g 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` ( A / N ) ) ) /\ m e. { x e. ( 1 ... ( |_ ` A ) ) | N || x } ) ) -> ( n = ( m / N ) <-> m = ( N x. n ) ) )
76 3 36 63 75 f1o2d 
 |-  ( ph -> F : ( 1 ... ( |_ ` ( A / N ) ) ) -1-1-onto-> { x e. ( 1 ... ( |_ ` A ) ) | N || x } )