hashgcdeq

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

		Ref	Expression
	Assertion	hashgcdeq	$⊢ (M \in ℕ \land N \in ℕ) \to \|\{x \in (0 ..^M) \| x \gcd M = N\}\| = if (N ∥ M, ϕ (\frac{M}{N}), 0)$

Proof

Step	Hyp	Ref	Expression
1		eqeq2	$⊢ ϕ (\frac{M}{N}) = if (N ∥ M, ϕ (\frac{M}{N}), 0) \to (\|\{x \in (0 ..^M) \| x \gcd M = N\}\| = ϕ (\frac{M}{N}) \leftrightarrow \|\{x \in (0 ..^M) \| x \gcd M = N\}\| = if (N ∥ M, ϕ (\frac{M}{N}), 0))$
2		eqeq2	$⊢ 0 = if (N ∥ M, ϕ (\frac{M}{N}), 0) \to (\|\{x \in (0 ..^M) \| x \gcd M = N\}\| = 0 \leftrightarrow \|\{x \in (0 ..^M) \| x \gcd M = N\}\| = if (N ∥ M, ϕ (\frac{M}{N}), 0))$
3		nndivdvds	$⊢ (M \in ℕ \land N \in ℕ) \to (N ∥ M \leftrightarrow \frac{M}{N} \in ℕ)$
4	3	biimpa	$⊢ ((M \in ℕ \land N \in ℕ) \land N ∥ M) \to \frac{M}{N} \in ℕ$
5		dfphi2	$⊢ \frac{M}{N} \in ℕ \to ϕ (\frac{M}{N}) = \|\{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\}\|$
6	4 5	syl	$⊢ ((M \in ℕ \land N \in ℕ) \land N ∥ M) \to ϕ (\frac{M}{N}) = \|\{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\}\|$
7		eqid	$⊢ \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\} = \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\}$
8		eqid	$⊢ \{x \in (0 ..^M) \| x \gcd M = N\} = \{x \in (0 ..^M) \| x \gcd M = N\}$
9		eqid	$⊢ (z \in \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\} ⟼ z \cdot N) = (z \in \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\} ⟼ z \cdot N)$
10	7 8 9	hashgcdlem	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to (z \in \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\} ⟼ z \cdot N) : \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\} \underset{1-1 onto}{⟶} \{x \in (0 ..^M) \| x \gcd M = N\}$
11	10	3expa	$⊢ ((M \in ℕ \land N \in ℕ) \land N ∥ M) \to (z \in \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\} ⟼ z \cdot N) : \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\} \underset{1-1 onto}{⟶} \{x \in (0 ..^M) \| x \gcd M = N\}$
12		ovex	$⊢ (0 ..^\frac{M}{N}) \in V$
13	12	rabex	$⊢ \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\} \in V$
14	13	f1oen	$⊢ (z \in \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\} ⟼ z \cdot N) : \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\} \underset{1-1 onto}{⟶} \{x \in (0 ..^M) \| x \gcd M = N\} \to \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\} \approx \{x \in (0 ..^M) \| x \gcd M = N\}$
15		hasheni	$⊢ \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\} \approx \{x \in (0 ..^M) \| x \gcd M = N\} \to \|\{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\}\| = \|\{x \in (0 ..^M) \| x \gcd M = N\}\|$
16	11 14 15	3syl	$⊢ ((M \in ℕ \land N \in ℕ) \land N ∥ M) \to \|\{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\}\| = \|\{x \in (0 ..^M) \| x \gcd M = N\}\|$
17	6 16	eqtr2d	$⊢ ((M \in ℕ \land N \in ℕ) \land N ∥ M) \to \|\{x \in (0 ..^M) \| x \gcd M = N\}\| = ϕ (\frac{M}{N})$
18		simprr	$⊢ ((M \in ℕ \land N \in ℕ) \land (x \in (0 ..^M) \land x \gcd M = N)) \to x \gcd M = N$
19		elfzoelz	$⊢ x \in (0 ..^M) \to x \in ℤ$
20	19	ad2antrl	$⊢ ((M \in ℕ \land N \in ℕ) \land (x \in (0 ..^M) \land x \gcd M = N)) \to x \in ℤ$
21		nnz	$⊢ M \in ℕ \to M \in ℤ$
22	21	ad2antrr	$⊢ ((M \in ℕ \land N \in ℕ) \land (x \in (0 ..^M) \land x \gcd M = N)) \to M \in ℤ$
23		gcddvds	$⊢ (x \in ℤ \land M \in ℤ) \to ((x \gcd M) ∥ x \land (x \gcd M) ∥ M)$
24	20 22 23	syl2anc	$⊢ ((M \in ℕ \land N \in ℕ) \land (x \in (0 ..^M) \land x \gcd M = N)) \to ((x \gcd M) ∥ x \land (x \gcd M) ∥ M)$
25	24	simprd	$⊢ ((M \in ℕ \land N \in ℕ) \land (x \in (0 ..^M) \land x \gcd M = N)) \to (x \gcd M) ∥ M$
26	18 25	eqbrtrrd	$⊢ ((M \in ℕ \land N \in ℕ) \land (x \in (0 ..^M) \land x \gcd M = N)) \to N ∥ M$
27	26	expr	$⊢ ((M \in ℕ \land N \in ℕ) \land x \in (0 ..^M)) \to (x \gcd M = N \to N ∥ M)$
28	27	con3d	$⊢ ((M \in ℕ \land N \in ℕ) \land x \in (0 ..^M)) \to (\neg N ∥ M \to \neg x \gcd M = N)$
29	28	impancom	$⊢ ((M \in ℕ \land N \in ℕ) \land \neg N ∥ M) \to (x \in (0 ..^M) \to \neg x \gcd M = N)$
30	29	ralrimiv	$⊢ ((M \in ℕ \land N \in ℕ) \land \neg N ∥ M) \to \forall x \in (0 ..^M) \neg x \gcd M = N$
31		rabeq0	$⊢ \{x \in (0 ..^M) \| x \gcd M = N\} = \emptyset \leftrightarrow \forall x \in (0 ..^M) \neg x \gcd M = N$
32	30 31	sylibr	$⊢ ((M \in ℕ \land N \in ℕ) \land \neg N ∥ M) \to \{x \in (0 ..^M) \| x \gcd M = N\} = \emptyset$
33	32	fveq2d	$⊢ ((M \in ℕ \land N \in ℕ) \land \neg N ∥ M) \to \|\{x \in (0 ..^M) \| x \gcd M = N\}\| = \|\emptyset\|$
34		hash0	$⊢ \|\emptyset\| = 0$
35	33 34	syl6eq	$⊢ ((M \in ℕ \land N \in ℕ) \land \neg N ∥ M) \to \|\{x \in (0 ..^M) \| x \gcd M = N\}\| = 0$
36	1 2 17 35	ifbothda	$⊢ (M \in ℕ \land N \in ℕ) \to \|\{x \in (0 ..^M) \| x \gcd M = N\}\| = if (N ∥ M, ϕ (\frac{M}{N}), 0)$

Metamath Proof Explorer

Theorem hashgcdeq

Proof