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|xN
dvdsflip.f F=yANy
Assertion dvdsflip NF:A1-1 ontoA

Proof

Step Hyp Ref Expression
1 dvdsflip.a A=x|xN
2 dvdsflip.f F=yANy
3 1 eleq2i yAyx|xN
4 dvdsdivcl Nyx|xNNyx|xN
5 3 4 sylan2b NyANyx|xN
6 5 1 eleqtrrdi NyANyA
7 1 eleq2i zAzx|xN
8 dvdsdivcl Nzx|xNNzx|xN
9 7 8 sylan2b NzANzx|xN
10 9 1 eleqtrrdi NzANzA
11 1 ssrab3 A
12 11 sseli yAy
13 11 sseli zAz
14 12 13 anim12i yAzAyz
15 nncn NN
16 15 adantr NyzN
17 nncn yy
18 17 ad2antrl Nyzy
19 nncn zz
20 19 ad2antll Nyzz
21 nnne0 zz0
22 21 ad2antll Nyzz0
23 16 18 20 22 divmul3d NyzNz=yN=yz
24 nnne0 yy0
25 24 ad2antrl Nyzy0
26 16 20 18 25 divmul2d NyzNy=zN=yz
27 23 26 bitr4d NyzNz=yNy=z
28 14 27 sylan2 NyAzANz=yNy=z
29 eqcom y=NzNz=y
30 eqcom z=NyNy=z
31 28 29 30 3bitr4g NyAzAy=Nzz=Ny
32 2 6 10 31 f1o2d NF:A1-1 ontoA