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 | |
|
dvdsflip.f | |
||
Assertion | dvdsflip | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvdsflip.a | |
|
2 | dvdsflip.f | |
|
3 | 1 | eleq2i | |
4 | dvdsdivcl | |
|
5 | 3 4 | sylan2b | |
6 | 5 1 | eleqtrrdi | |
7 | 1 | eleq2i | |
8 | dvdsdivcl | |
|
9 | 7 8 | sylan2b | |
10 | 9 1 | eleqtrrdi | |
11 | 1 | ssrab3 | |
12 | 11 | sseli | |
13 | 11 | sseli | |
14 | 12 13 | anim12i | |
15 | nncn | |
|
16 | 15 | adantr | |
17 | nncn | |
|
18 | 17 | ad2antrl | |
19 | nncn | |
|
20 | 19 | ad2antll | |
21 | nnne0 | |
|
22 | 21 | ad2antll | |
23 | 16 18 20 22 | divmul3d | |
24 | nnne0 | |
|
25 | 24 | ad2antrl | |
26 | 16 20 18 25 | divmul2d | |
27 | 23 26 | bitr4d | |
28 | 14 27 | sylan2 | |
29 | eqcom | |
|
30 | eqcom | |
|
31 | 28 29 30 | 3bitr4g | |
32 | 2 6 10 31 | f1o2d | |