pcqcl

Description: Closure of the general prime count function. (Contributed by Mario Carneiro, 23-Feb-2014)

		Ref	Expression
	Assertion	pcqcl	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to P pCnt N \in ℤ$

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to N \in ℚ$
2		elq	$⊢ N \in ℚ \leftrightarrow \exists x \in ℤ \exists y \in ℕ N = \frac{x}{y}$
3	1 2	sylib	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to \exists x \in ℤ \exists y \in ℕ N = \frac{x}{y}$
4		nncn	$⊢ y \in ℕ \to y \in ℂ$
5		nnne0	$⊢ y \in ℕ \to y \neq 0$
6	4 5	div0d	$⊢ y \in ℕ \to \frac{0}{y} = 0$
7	6	ad2antll	$⊢ (P \in ℙ \land (x \in ℤ \land y \in ℕ)) \to \frac{0}{y} = 0$
8		oveq1	$⊢ x = 0 \to \frac{x}{y} = \frac{0}{y}$
9	8	eqeq1d	$⊢ x = 0 \to (\frac{x}{y} = 0 \leftrightarrow \frac{0}{y} = 0)$
10	7 9	syl5ibrcom	$⊢ (P \in ℙ \land (x \in ℤ \land y \in ℕ)) \to (x = 0 \to \frac{x}{y} = 0)$
11	10	necon3d	$⊢ (P \in ℙ \land (x \in ℤ \land y \in ℕ)) \to (\frac{x}{y} \neq 0 \to x \neq 0)$
12		an32	$⊢ ((x \in ℤ \land y \in ℕ) \land x \neq 0) \leftrightarrow ((x \in ℤ \land x \neq 0) \land y \in ℕ)$
13		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)$
14		pczcl	$⊢ (P \in ℙ \land (x \in ℤ \land x \neq 0)) \to P pCnt x \in ℕ_{0}$
15	14	nn0zd	$⊢ (P \in ℙ \land (x \in ℤ \land x \neq 0)) \to P pCnt x \in ℤ$
16	15	3adant3	$⊢ (P \in ℙ \land (x \in ℤ \land x \neq 0) \land y \in ℕ) \to P pCnt x \in ℤ$
17		nnz	$⊢ y \in ℕ \to y \in ℤ$
18	17 5	jca	$⊢ y \in ℕ \to (y \in ℤ \land y \neq 0)$
19		pczcl	$⊢ (P \in ℙ \land (y \in ℤ \land y \neq 0)) \to P pCnt y \in ℕ_{0}$
20	19	nn0zd	$⊢ (P \in ℙ \land (y \in ℤ \land y \neq 0)) \to P pCnt y \in ℤ$
21	18 20	sylan2	$⊢ (P \in ℙ \land y \in ℕ) \to P pCnt y \in ℤ$
22	21	3adant2	$⊢ (P \in ℙ \land (x \in ℤ \land x \neq 0) \land y \in ℕ) \to P pCnt y \in ℤ$
23	16 22	zsubcld	$⊢ (P \in ℙ \land (x \in ℤ \land x \neq 0) \land y \in ℕ) \to (P pCnt x) - (P pCnt y) \in ℤ$
24	13 23	eqeltrd	$⊢ (P \in ℙ \land (x \in ℤ \land x \neq 0) \land y \in ℕ) \to P pCnt (\frac{x}{y}) \in ℤ$
25	24	3expb	$⊢ (P \in ℙ \land ((x \in ℤ \land x \neq 0) \land y \in ℕ)) \to P pCnt (\frac{x}{y}) \in ℤ$
26	12 25	sylan2b	$⊢ (P \in ℙ \land ((x \in ℤ \land y \in ℕ) \land x \neq 0)) \to P pCnt (\frac{x}{y}) \in ℤ$
27	26	expr	$⊢ (P \in ℙ \land (x \in ℤ \land y \in ℕ)) \to (x \neq 0 \to P pCnt (\frac{x}{y}) \in ℤ)$
28	11 27	syld	$⊢ (P \in ℙ \land (x \in ℤ \land y \in ℕ)) \to (\frac{x}{y} \neq 0 \to P pCnt (\frac{x}{y}) \in ℤ)$
29		neeq1	$⊢ N = \frac{x}{y} \to (N \neq 0 \leftrightarrow \frac{x}{y} \neq 0)$
30		oveq2	$⊢ N = \frac{x}{y} \to P pCnt N = P pCnt (\frac{x}{y})$
31	30	eleq1d	$⊢ N = \frac{x}{y} \to (P pCnt N \in ℤ \leftrightarrow P pCnt (\frac{x}{y}) \in ℤ)$
32	29 31	imbi12d	$⊢ N = \frac{x}{y} \to ((N \neq 0 \to P pCnt N \in ℤ) \leftrightarrow (\frac{x}{y} \neq 0 \to P pCnt (\frac{x}{y}) \in ℤ))$
33	28 32	syl5ibrcom	$⊢ (P \in ℙ \land (x \in ℤ \land y \in ℕ)) \to (N = \frac{x}{y} \to (N \neq 0 \to P pCnt N \in ℤ))$
34	33	com23	$⊢ (P \in ℙ \land (x \in ℤ \land y \in ℕ)) \to (N \neq 0 \to (N = \frac{x}{y} \to P pCnt N \in ℤ))$
35	34	impancom	$⊢ (P \in ℙ \land N \neq 0) \to ((x \in ℤ \land y \in ℕ) \to (N = \frac{x}{y} \to P pCnt N \in ℤ))$
36	35	adantrl	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to ((x \in ℤ \land y \in ℕ) \to (N = \frac{x}{y} \to P pCnt N \in ℤ))$
37	36	rexlimdvv	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to (\exists x \in ℤ \exists y \in ℕ N = \frac{x}{y} \to P pCnt N \in ℤ)$
38	3 37	mpd	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to P pCnt N \in ℤ$

Metamath Proof Explorer

Theorem pcqcl

Proof