Metamath Proof Explorer

Theorem pcqcl

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

Ref Expression
Assertion pcqcl ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → 𝑁 ∈ ℚ )
2 elq ⊢ ( 𝑁 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝑁 = ( 𝑥 / 𝑦 ) )
3 1 2 sylib ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝑁 = ( 𝑥 / 𝑦 ) )
4 nncn ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
5 nnne0 ⊢ ( 𝑦 ∈ ℕ → 𝑦 ≠ 0 )
6 4 5 div0d ⊢ ( 𝑦 ∈ ℕ → ( 0 / 𝑦 ) = 0 )
7 6 ad2antll ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( 0 / 𝑦 ) = 0 )
8 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 / 𝑦 ) = ( 0 / 𝑦 ) )
9 8 eqeq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 / 𝑦 ) = 0 ↔ ( 0 / 𝑦 ) = 0 ) )
10 7 9 syl5ibrcom ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑥 = 0 → ( 𝑥 / 𝑦 ) = 0 ) )
11 10 necon3d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( ( 𝑥 / 𝑦 ) ≠ 0 → 𝑥 ≠ 0 ) )
12 an32 ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) ↔ ( ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ℕ ) )
13 pcdiv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) = ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) )
14 pczcl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ( 𝑃 pCnt 𝑥 ) ∈ ℕ0 )
15 14 nn0zd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ( 𝑃 pCnt 𝑥 ) ∈ ℤ )
16 15 3adant3 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 pCnt 𝑥 ) ∈ ℤ )
17 nnz ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
18 17 5 jca ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) )
19 pczcl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℕ0 )
20 19 nn0zd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℤ )
21 18 20 sylan2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ ) → ( 𝑃 pCnt 𝑦 ) ∈ ℤ )
22 21 3adant2 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 pCnt 𝑦 ) ∈ ℤ )
23 16 22 zsubcld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) ∈ ℤ )
24 13 23 eqeltrd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) ∈ ℤ )
25 24 3expb ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ℕ ) ) → ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) ∈ ℤ )
26 12 25 sylan2b ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) ∈ ℤ )
27 26 expr ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑥 ≠ 0 → ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) ∈ ℤ ) )
28 11 27 syld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( ( 𝑥 / 𝑦 ) ≠ 0 → ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) ∈ ℤ ) )
29 neeq1 ⊢ ( 𝑁 = ( 𝑥 / 𝑦 ) → ( 𝑁 ≠ 0 ↔ ( 𝑥 / 𝑦 ) ≠ 0 ) )
30 oveq2 ⊢ ( 𝑁 = ( 𝑥 / 𝑦 ) → ( 𝑃 pCnt 𝑁 ) = ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) )
31 30 eleq1d ⊢ ( 𝑁 = ( 𝑥 / 𝑦 ) → ( ( 𝑃 pCnt 𝑁 ) ∈ ℤ ↔ ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) ∈ ℤ ) )
32 29 31 imbi12d ⊢ ( 𝑁 = ( 𝑥 / 𝑦 ) → ( ( 𝑁 ≠ 0 → ( 𝑃 pCnt 𝑁 ) ∈ ℤ ) ↔ ( ( 𝑥 / 𝑦 ) ≠ 0 → ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) ∈ ℤ ) ) )
33 28 32 syl5ibrcom ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑁 = ( 𝑥 / 𝑦 ) → ( 𝑁 ≠ 0 → ( 𝑃 pCnt 𝑁 ) ∈ ℤ ) ) )
34 33 com23 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑁 ≠ 0 → ( 𝑁 = ( 𝑥 / 𝑦 ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ ) ) )
35 34 impancom ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ≠ 0 ) → ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝑁 = ( 𝑥 / 𝑦 ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ ) ) )
36 35 adantrl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝑁 = ( 𝑥 / 𝑦 ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ ) ) )
37 36 rexlimdvv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝑁 = ( 𝑥 / 𝑦 ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ ) )
38 3 37 mpd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ )