Metamath Proof Explorer

Theorem dvdsflip

Description: An involution of the divisors of a number. (Contributed by Stefan O'Rear, 12-Sep-2015) (Proof shortened by Mario Carneiro, 13-May-2016)

Ref Expression
Hypotheses dvdsflip.a 
|- A = { x e. NN | x || N }
dvdsflip.f 
|- F = ( y e. A |-> ( N / y ) )
Assertion dvdsflip 
|- ( N e. NN -> F : A -1-1-onto-> A )

Proof

Step Hyp Ref Expression
1 dvdsflip.a 
 |-  A = { x e. NN | x || N }
2 dvdsflip.f 
 |-  F = ( y e. A |-> ( N / y ) )
3 1 eleq2i 
 |-  ( y e. A <-> y e. { x e. NN | x || N } )
4 dvdsdivcl 
 |-  ( ( N e. NN /\ y e. { x e. NN | x || N } ) -> ( N / y ) e. { x e. NN | x || N } )
5 3 4 sylan2b 
 |-  ( ( N e. NN /\ y e. A ) -> ( N / y ) e. { x e. NN | x || N } )
6 5 1 eleqtrrdi 
 |-  ( ( N e. NN /\ y e. A ) -> ( N / y ) e. A )
7 1 eleq2i 
 |-  ( z e. A <-> z e. { x e. NN | x || N } )
8 dvdsdivcl 
 |-  ( ( N e. NN /\ z e. { x e. NN | x || N } ) -> ( N / z ) e. { x e. NN | x || N } )
9 7 8 sylan2b 
 |-  ( ( N e. NN /\ z e. A ) -> ( N / z ) e. { x e. NN | x || N } )
10 9 1 eleqtrrdi 
 |-  ( ( N e. NN /\ z e. A ) -> ( N / z ) e. A )
11 1 ssrab3 
 |-  A C_ NN
12 11 sseli 
 |-  ( y e. A -> y e. NN )
13 11 sseli 
 |-  ( z e. A -> z e. NN )
14 12 13 anim12i 
 |-  ( ( y e. A /\ z e. A ) -> ( y e. NN /\ z e. NN ) )
15 nncn 
 |-  ( N e. NN -> N e. CC )
16 15 adantr 
 |-  ( ( N e. NN /\ ( y e. NN /\ z e. NN ) ) -> N e. CC )
17 nncn 
 |-  ( y e. NN -> y e. CC )
18 17 ad2antrl 
 |-  ( ( N e. NN /\ ( y e. NN /\ z e. NN ) ) -> y e. CC )
19 nncn 
 |-  ( z e. NN -> z e. CC )
20 19 ad2antll 
 |-  ( ( N e. NN /\ ( y e. NN /\ z e. NN ) ) -> z e. CC )
21 nnne0 
 |-  ( z e. NN -> z =/= 0 )
22 21 ad2antll 
 |-  ( ( N e. NN /\ ( y e. NN /\ z e. NN ) ) -> z =/= 0 )
23 16 18 20 22 divmul3d 
 |-  ( ( N e. NN /\ ( y e. NN /\ z e. NN ) ) -> ( ( N / z ) = y <-> N = ( y x. z ) ) )
24 nnne0 
 |-  ( y e. NN -> y =/= 0 )
25 24 ad2antrl 
 |-  ( ( N e. NN /\ ( y e. NN /\ z e. NN ) ) -> y =/= 0 )
26 16 20 18 25 divmul2d 
 |-  ( ( N e. NN /\ ( y e. NN /\ z e. NN ) ) -> ( ( N / y ) = z <-> N = ( y x. z ) ) )
27 23 26 bitr4d 
 |-  ( ( N e. NN /\ ( y e. NN /\ z e. NN ) ) -> ( ( N / z ) = y <-> ( N / y ) = z ) )
28 14 27 sylan2 
 |-  ( ( N e. NN /\ ( y e. A /\ z e. A ) ) -> ( ( N / z ) = y <-> ( N / y ) = z ) )
29 eqcom 
 |-  ( y = ( N / z ) <-> ( N / z ) = y )
30 eqcom 
 |-  ( z = ( N / y ) <-> ( N / y ) = z )
31 28 29 30 3bitr4g 
 |-  ( ( N e. NN /\ ( y e. A /\ z e. A ) ) -> ( y = ( N / z ) <-> z = ( N / y ) ) )
32 2 6 10 31 f1o2d 
 |-  ( N e. NN -> F : A -1-1-onto-> A )