Metamath Proof Explorer


Theorem hashgcdeq

Description: Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Assertion hashgcdeq MNx0..^M|xgcdM=N=ifNMϕMN0

Proof

Step Hyp Ref Expression
1 eqeq2 ϕMN=ifNMϕMN0x0..^M|xgcdM=N=ϕMNx0..^M|xgcdM=N=ifNMϕMN0
2 eqeq2 0=ifNMϕMN0x0..^M|xgcdM=N=0x0..^M|xgcdM=N=ifNMϕMN0
3 nndivdvds MNNMMN
4 3 biimpa MNNMMN
5 dfphi2 MNϕMN=y0..^MN|ygcdMN=1
6 4 5 syl MNNMϕMN=y0..^MN|ygcdMN=1
7 eqid y0..^MN|ygcdMN=1=y0..^MN|ygcdMN=1
8 eqid x0..^M|xgcdM=N=x0..^M|xgcdM=N
9 eqid zy0..^MN|ygcdMN=1z N=zy0..^MN|ygcdMN=1z N
10 7 8 9 hashgcdlem MNNMzy0..^MN|ygcdMN=1z N:y0..^MN|ygcdMN=11-1 ontox0..^M|xgcdM=N
11 10 3expa MNNMzy0..^MN|ygcdMN=1z N:y0..^MN|ygcdMN=11-1 ontox0..^M|xgcdM=N
12 ovex 0..^MNV
13 12 rabex y0..^MN|ygcdMN=1V
14 13 f1oen zy0..^MN|ygcdMN=1z N:y0..^MN|ygcdMN=11-1 ontox0..^M|xgcdM=Ny0..^MN|ygcdMN=1x0..^M|xgcdM=N
15 hasheni y0..^MN|ygcdMN=1x0..^M|xgcdM=Ny0..^MN|ygcdMN=1=x0..^M|xgcdM=N
16 11 14 15 3syl MNNMy0..^MN|ygcdMN=1=x0..^M|xgcdM=N
17 6 16 eqtr2d MNNMx0..^M|xgcdM=N=ϕMN
18 simprr MNx0..^MxgcdM=NxgcdM=N
19 elfzoelz x0..^Mx
20 19 ad2antrl MNx0..^MxgcdM=Nx
21 nnz MM
22 21 ad2antrr MNx0..^MxgcdM=NM
23 gcddvds xMxgcdMxxgcdMM
24 20 22 23 syl2anc MNx0..^MxgcdM=NxgcdMxxgcdMM
25 24 simprd MNx0..^MxgcdM=NxgcdMM
26 18 25 eqbrtrrd MNx0..^MxgcdM=NNM
27 26 expr MNx0..^MxgcdM=NNM
28 27 con3d MNx0..^M¬NM¬xgcdM=N
29 28 impancom MN¬NMx0..^M¬xgcdM=N
30 29 ralrimiv MN¬NMx0..^M¬xgcdM=N
31 rabeq0 x0..^M|xgcdM=N=x0..^M¬xgcdM=N
32 30 31 sylibr MN¬NMx0..^M|xgcdM=N=
33 32 fveq2d MN¬NMx0..^M|xgcdM=N=
34 hash0 =0
35 33 34 eqtrdi MN¬NMx0..^M|xgcdM=N=0
36 1 2 17 35 ifbothda MNx0..^M|xgcdM=N=ifNMϕMN0