pcz

Description: The prime count function can be used as an indicator that a given rational number is an integer. (Contributed by Mario Carneiro, 23-Feb-2014)

		Ref	Expression
	Assertion	pcz	$⊢ A \in ℚ \to (A \in ℤ \leftrightarrow \forall p \in ℙ 0 \leq p pCnt A)$

Proof

Step	Hyp	Ref	Expression
1		pcge0	$⊢ (p \in ℙ \land A \in ℤ) \to 0 \leq p pCnt A$
2	1	ancoms	$⊢ (A \in ℤ \land p \in ℙ) \to 0 \leq p pCnt A$
3	2	ralrimiva	$⊢ A \in ℤ \to \forall p \in ℙ 0 \leq p pCnt A$
4		elq	$⊢ A \in ℚ \leftrightarrow \exists x \in ℤ \exists y \in ℕ A = \frac{x}{y}$
5		nnz	$⊢ y \in ℕ \to y \in ℤ$
6		dvds0	$⊢ y \in ℤ \to y ∥ 0$
7	5 6	syl	$⊢ y \in ℕ \to y ∥ 0$
8	7	ad2antlr	$⊢ ((x \in ℤ \land y \in ℕ) \land x = 0) \to y ∥ 0$
9		simpr	$⊢ ((x \in ℤ \land y \in ℕ) \land x = 0) \to x = 0$
10	8 9	breqtrrd	$⊢ ((x \in ℤ \land y \in ℕ) \land x = 0) \to y ∥ x$
11	10	a1d	$⊢ ((x \in ℤ \land y \in ℕ) \land x = 0) \to (\forall p \in ℙ 0 \leq p pCnt (\frac{x}{y}) \to y ∥ x)$
12		simpr	$⊢ (((x \in ℤ \land y \in ℕ) \land x \neq 0) \land p \in ℙ) \to p \in ℙ$
13		simplll	$⊢ (((x \in ℤ \land y \in ℕ) \land x \neq 0) \land p \in ℙ) \to x \in ℤ$
14		simplr	$⊢ (((x \in ℤ \land y \in ℕ) \land x \neq 0) \land p \in ℙ) \to x \neq 0$
15		simpllr	$⊢ (((x \in ℤ \land y \in ℕ) \land x \neq 0) \land p \in ℙ) \to y \in ℕ$
16		pcdiv	$⊢ (p \in ℙ \land (x \in ℤ \land x \neq 0) \land y \in ℕ) \to p pCnt (\frac{x}{y}) = (p pCnt x) - (p pCnt y)$
17	12 13 14 15 16	syl121anc	$⊢ (((x \in ℤ \land y \in ℕ) \land x \neq 0) \land p \in ℙ) \to p pCnt (\frac{x}{y}) = (p pCnt x) - (p pCnt y)$
18	17	breq2d	$⊢ (((x \in ℤ \land y \in ℕ) \land x \neq 0) \land p \in ℙ) \to (0 \leq p pCnt (\frac{x}{y}) \leftrightarrow 0 \leq (p pCnt x) - (p pCnt y))$
19		pczcl	$⊢ (p \in ℙ \land (x \in ℤ \land x \neq 0)) \to p pCnt x \in ℕ_{0}$
20	12 13 14 19	syl12anc	$⊢ (((x \in ℤ \land y \in ℕ) \land x \neq 0) \land p \in ℙ) \to p pCnt x \in ℕ_{0}$
21	20	nn0red	$⊢ (((x \in ℤ \land y \in ℕ) \land x \neq 0) \land p \in ℙ) \to p pCnt x \in ℝ$
22	12 15	pccld	$⊢ (((x \in ℤ \land y \in ℕ) \land x \neq 0) \land p \in ℙ) \to p pCnt y \in ℕ_{0}$
23	22	nn0red	$⊢ (((x \in ℤ \land y \in ℕ) \land x \neq 0) \land p \in ℙ) \to p pCnt y \in ℝ$
24	21 23	subge0d	$⊢ (((x \in ℤ \land y \in ℕ) \land x \neq 0) \land p \in ℙ) \to (0 \leq (p pCnt x) - (p pCnt y) \leftrightarrow p pCnt y \leq p pCnt x)$
25	18 24	bitrd	$⊢ (((x \in ℤ \land y \in ℕ) \land x \neq 0) \land p \in ℙ) \to (0 \leq p pCnt (\frac{x}{y}) \leftrightarrow p pCnt y \leq p pCnt x)$
26	25	ralbidva	$⊢ ((x \in ℤ \land y \in ℕ) \land x \neq 0) \to (\forall p \in ℙ 0 \leq p pCnt (\frac{x}{y}) \leftrightarrow \forall p \in ℙ p pCnt y \leq p pCnt x)$
27		id	$⊢ x \in ℤ \to x \in ℤ$
28		pc2dvds	$⊢ (y \in ℤ \land x \in ℤ) \to (y ∥ x \leftrightarrow \forall p \in ℙ p pCnt y \leq p pCnt x)$
29	5 27 28	syl2anr	$⊢ (x \in ℤ \land y \in ℕ) \to (y ∥ x \leftrightarrow \forall p \in ℙ p pCnt y \leq p pCnt x)$
30	29	adantr	$⊢ ((x \in ℤ \land y \in ℕ) \land x \neq 0) \to (y ∥ x \leftrightarrow \forall p \in ℙ p pCnt y \leq p pCnt x)$
31	26 30	bitr4d	$⊢ ((x \in ℤ \land y \in ℕ) \land x \neq 0) \to (\forall p \in ℙ 0 \leq p pCnt (\frac{x}{y}) \leftrightarrow y ∥ x)$
32	31	biimpd	$⊢ ((x \in ℤ \land y \in ℕ) \land x \neq 0) \to (\forall p \in ℙ 0 \leq p pCnt (\frac{x}{y}) \to y ∥ x)$
33	11 32	pm2.61dane	$⊢ (x \in ℤ \land y \in ℕ) \to (\forall p \in ℙ 0 \leq p pCnt (\frac{x}{y}) \to y ∥ x)$
34		nnne0	$⊢ y \in ℕ \to y \neq 0$
35		simpl	$⊢ (x \in ℤ \land y \in ℕ) \to x \in ℤ$
36		dvdsval2	$⊢ (y \in ℤ \land y \neq 0 \land x \in ℤ) \to (y ∥ x \leftrightarrow \frac{x}{y} \in ℤ)$
37	5 34 35 36	syl2an23an	$⊢ (x \in ℤ \land y \in ℕ) \to (y ∥ x \leftrightarrow \frac{x}{y} \in ℤ)$
38	33 37	sylibd	$⊢ (x \in ℤ \land y \in ℕ) \to (\forall p \in ℙ 0 \leq p pCnt (\frac{x}{y}) \to \frac{x}{y} \in ℤ)$
39		oveq2	$⊢ A = \frac{x}{y} \to p pCnt A = p pCnt (\frac{x}{y})$
40	39	breq2d	$⊢ A = \frac{x}{y} \to (0 \leq p pCnt A \leftrightarrow 0 \leq p pCnt (\frac{x}{y}))$
41	40	ralbidv	$⊢ A = \frac{x}{y} \to (\forall p \in ℙ 0 \leq p pCnt A \leftrightarrow \forall p \in ℙ 0 \leq p pCnt (\frac{x}{y}))$
42		eleq1	$⊢ A = \frac{x}{y} \to (A \in ℤ \leftrightarrow \frac{x}{y} \in ℤ)$
43	41 42	imbi12d	$⊢ A = \frac{x}{y} \to ((\forall p \in ℙ 0 \leq p pCnt A \to A \in ℤ) \leftrightarrow (\forall p \in ℙ 0 \leq p pCnt (\frac{x}{y}) \to \frac{x}{y} \in ℤ))$
44	38 43	syl5ibrcom	$⊢ (x \in ℤ \land y \in ℕ) \to (A = \frac{x}{y} \to (\forall p \in ℙ 0 \leq p pCnt A \to A \in ℤ))$
45	44	rexlimivv	$⊢ \exists x \in ℤ \exists y \in ℕ A = \frac{x}{y} \to (\forall p \in ℙ 0 \leq p pCnt A \to A \in ℤ)$
46	4 45	sylbi	$⊢ A \in ℚ \to (\forall p \in ℙ 0 \leq p pCnt A \to A \in ℤ)$
47	3 46	impbid2	$⊢ A \in ℚ \to (A \in ℤ \leftrightarrow \forall p \in ℙ 0 \leq p pCnt A)$

Metamath Proof Explorer

Theorem pcz

Proof