Description: Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | hashgcdeq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq2 | |
|
2 | eqeq2 | |
|
3 | nndivdvds | |
|
4 | 3 | biimpa | |
5 | dfphi2 | |
|
6 | 4 5 | syl | |
7 | eqid | |
|
8 | eqid | |
|
9 | eqid | |
|
10 | 7 8 9 | hashgcdlem | |
11 | 10 | 3expa | |
12 | ovex | |
|
13 | 12 | rabex | |
14 | 13 | f1oen | |
15 | hasheni | |
|
16 | 11 14 15 | 3syl | |
17 | 6 16 | eqtr2d | |
18 | simprr | |
|
19 | elfzoelz | |
|
20 | 19 | ad2antrl | |
21 | nnz | |
|
22 | 21 | ad2antrr | |
23 | gcddvds | |
|
24 | 20 22 23 | syl2anc | |
25 | 24 | simprd | |
26 | 18 25 | eqbrtrrd | |
27 | 26 | expr | |
28 | 27 | con3d | |
29 | 28 | impancom | |
30 | 29 | ralrimiv | |
31 | rabeq0 | |
|
32 | 30 31 | sylibr | |
33 | 32 | fveq2d | |
34 | hash0 | |
|
35 | 33 34 | eqtrdi | |
36 | 1 2 17 35 | ifbothda | |