dirith

		Ref	Expression
	Assertion	dirith	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to \{p \in ℙ \| N ∥ (p - A)\} \approx ℕ$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to N \in ℕ$
2	1	nnnn0d	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to N \in ℕ_{0}$
3	2	adantr	$⊢ ((N \in ℕ \land A \in ℤ \land A \gcd N = 1) \land p \in ℙ) \to N \in ℕ_{0}$
4		eqid	$⊢ ℤ / N ℤ = ℤ / N ℤ$
5		eqid	$⊢ {Base}_{ℤ / N ℤ} = {Base}_{ℤ / N ℤ}$
6		eqid	$⊢ ℤRHom (ℤ / N ℤ) = ℤRHom (ℤ / N ℤ)$
7	4 5 6	znzrhfo	$⊢ N \in ℕ_{0} \to ℤRHom (ℤ / N ℤ) : ℤ \underset{onto}{⟶} {Base}_{ℤ / N ℤ}$
8		fofn	$⊢ ℤRHom (ℤ / N ℤ) : ℤ \underset{onto}{⟶} {Base}_{ℤ / N ℤ} \to ℤRHom (ℤ / N ℤ) Fn ℤ$
9	3 7 8	3syl	$⊢ ((N \in ℕ \land A \in ℤ \land A \gcd N = 1) \land p \in ℙ) \to ℤRHom (ℤ / N ℤ) Fn ℤ$
10		prmz	$⊢ p \in ℙ \to p \in ℤ$
11	10	adantl	$⊢ ((N \in ℕ \land A \in ℤ \land A \gcd N = 1) \land p \in ℙ) \to p \in ℤ$
12		fniniseg	$⊢ ℤRHom (ℤ / N ℤ) Fn ℤ \to (p \in {ℤRHom (ℤ / N ℤ)}^{-1} [\{ℤRHom (ℤ / N ℤ) (A)\}] \leftrightarrow (p \in ℤ \land ℤRHom (ℤ / N ℤ) (p) = ℤRHom (ℤ / N ℤ) (A)))$
13	12	baibd	$⊢ (ℤRHom (ℤ / N ℤ) Fn ℤ \land p \in ℤ) \to (p \in {ℤRHom (ℤ / N ℤ)}^{-1} [\{ℤRHom (ℤ / N ℤ) (A)\}] \leftrightarrow ℤRHom (ℤ / N ℤ) (p) = ℤRHom (ℤ / N ℤ) (A))$
14	9 11 13	syl2anc	$⊢ ((N \in ℕ \land A \in ℤ \land A \gcd N = 1) \land p \in ℙ) \to (p \in {ℤRHom (ℤ / N ℤ)}^{-1} [\{ℤRHom (ℤ / N ℤ) (A)\}] \leftrightarrow ℤRHom (ℤ / N ℤ) (p) = ℤRHom (ℤ / N ℤ) (A))$
15		simp2	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to A \in ℤ$
16	15	adantr	$⊢ ((N \in ℕ \land A \in ℤ \land A \gcd N = 1) \land p \in ℙ) \to A \in ℤ$
17	4 6	zndvds	$⊢ (N \in ℕ_{0} \land p \in ℤ \land A \in ℤ) \to (ℤRHom (ℤ / N ℤ) (p) = ℤRHom (ℤ / N ℤ) (A) \leftrightarrow N ∥ (p - A))$
18	3 11 16 17	syl3anc	$⊢ ((N \in ℕ \land A \in ℤ \land A \gcd N = 1) \land p \in ℙ) \to (ℤRHom (ℤ / N ℤ) (p) = ℤRHom (ℤ / N ℤ) (A) \leftrightarrow N ∥ (p - A))$
19	14 18	bitrd	$⊢ ((N \in ℕ \land A \in ℤ \land A \gcd N = 1) \land p \in ℙ) \to (p \in {ℤRHom (ℤ / N ℤ)}^{-1} [\{ℤRHom (ℤ / N ℤ) (A)\}] \leftrightarrow N ∥ (p - A))$
20	19	rabbi2dva	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to ℙ \cap {ℤRHom (ℤ / N ℤ)}^{-1} [\{ℤRHom (ℤ / N ℤ) (A)\}] = \{p \in ℙ \| N ∥ (p - A)\}$
21		eqid	$⊢ Unit (ℤ / N ℤ) = Unit (ℤ / N ℤ)$
22		simp3	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to A \gcd N = 1$
23	4 21 6	znunit	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (ℤRHom (ℤ / N ℤ) (A) \in Unit (ℤ / N ℤ) \leftrightarrow A \gcd N = 1)$
24	2 15 23	syl2anc	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to (ℤRHom (ℤ / N ℤ) (A) \in Unit (ℤ / N ℤ) \leftrightarrow A \gcd N = 1)$
25	22 24	mpbird	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to ℤRHom (ℤ / N ℤ) (A) \in Unit (ℤ / N ℤ)$
26		eqid	$⊢ {ℤRHom (ℤ / N ℤ)}^{-1} [\{ℤRHom (ℤ / N ℤ) (A)\}] = {ℤRHom (ℤ / N ℤ)}^{-1} [\{ℤRHom (ℤ / N ℤ) (A)\}]$
27	4 6 1 21 25 26	dirith2	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to (ℙ \cap {ℤRHom (ℤ / N ℤ)}^{-1} [\{ℤRHom (ℤ / N ℤ) (A)\}]) \approx ℕ$
28	20 27	eqbrtrrd	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to \{p \in ℙ \| N ∥ (p - A)\} \approx ℕ$

Metamath Proof Explorer

Theorem dirith

Proof