Metamath Proof Explorer

Theorem 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 ( 𝐴 ∈ ℚ → ( 𝐴 ∈ ℤ ↔ ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 pcge0 ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → 0 ≤ ( 𝑝 pCnt 𝐴 ) )
2 1 ancoms ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ℙ ) → 0 ≤ ( 𝑝 pCnt 𝐴 ) )
3 2 ralrimiva ⊢ ( 𝐴 ∈ ℤ → ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt 𝐴 ) )
4 elq ⊢ ( 𝐴 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
5 nnz ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
6 dvds0 ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∥ 0 )
7 5 6 syl ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∥ 0 )
8 7 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 = 0 ) → 𝑦 ∥ 0 )
9 simpr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 = 0 ) → 𝑥 = 0 )
10 8 9 breqtrrd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 = 0 ) → 𝑦 ∥ 𝑥 )
11 10 a1d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 = 0 ) → ( ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt ( 𝑥 / 𝑦 ) ) → 𝑦 ∥ 𝑥 ) )
12 simpr ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
13 simplll ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 𝑥 ∈ ℤ )
14 simplr ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 𝑥 ≠ 0 )
15 simpllr ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 𝑦 ∈ ℕ )
16 pcdiv ⊢ ( ( 𝑝 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ℕ ) → ( 𝑝 pCnt ( 𝑥 / 𝑦 ) ) = ( ( 𝑝 pCnt 𝑥 ) − ( 𝑝 pCnt 𝑦 ) ) )
17 12 13 14 15 16 syl121anc ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( 𝑥 / 𝑦 ) ) = ( ( 𝑝 pCnt 𝑥 ) − ( 𝑝 pCnt 𝑦 ) ) )
18 17 breq2d ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 0 ≤ ( 𝑝 pCnt ( 𝑥 / 𝑦 ) ) ↔ 0 ≤ ( ( 𝑝 pCnt 𝑥 ) − ( 𝑝 pCnt 𝑦 ) ) ) )
19 pczcl ⊢ ( ( 𝑝 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ( 𝑝 pCnt 𝑥 ) ∈ ℕ0 )
20 12 13 14 19 syl12anc ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝑥 ) ∈ ℕ0 )
21 20 nn0red ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝑥 ) ∈ ℝ )
22 12 15 pccld ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝑦 ) ∈ ℕ0 )
23 22 nn0red ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝑦 ) ∈ ℝ )
24 21 23 subge0d ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 0 ≤ ( ( 𝑝 pCnt 𝑥 ) − ( 𝑝 pCnt 𝑦 ) ) ↔ ( 𝑝 pCnt 𝑦 ) ≤ ( 𝑝 pCnt 𝑥 ) ) )
25 18 24 bitrd ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 0 ≤ ( 𝑝 pCnt ( 𝑥 / 𝑦 ) ) ↔ ( 𝑝 pCnt 𝑦 ) ≤ ( 𝑝 pCnt 𝑥 ) ) )
26 25 ralbidva ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) → ( ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt ( 𝑥 / 𝑦 ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑦 ) ≤ ( 𝑝 pCnt 𝑥 ) ) )
27 id ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℤ )
28 pc2dvds ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑦 ∥ 𝑥 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑦 ) ≤ ( 𝑝 pCnt 𝑥 ) ) )
29 5 27 28 syl2anr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝑦 ∥ 𝑥 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑦 ) ≤ ( 𝑝 pCnt 𝑥 ) ) )
30 29 adantr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) → ( 𝑦 ∥ 𝑥 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑦 ) ≤ ( 𝑝 pCnt 𝑥 ) ) )
31 26 30 bitr4d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) → ( ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt ( 𝑥 / 𝑦 ) ) ↔ 𝑦 ∥ 𝑥 ) )
32 31 biimpd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) → ( ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt ( 𝑥 / 𝑦 ) ) → 𝑦 ∥ 𝑥 ) )
33 11 32 pm2.61dane ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt ( 𝑥 / 𝑦 ) ) → 𝑦 ∥ 𝑥 ) )
34 nnne0 ⊢ ( 𝑦 ∈ ℕ → 𝑦 ≠ 0 )
35 simpl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → 𝑥 ∈ ℤ )
36 dvdsval2 ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ 𝑥 ∈ ℤ ) → ( 𝑦 ∥ 𝑥 ↔ ( 𝑥 / 𝑦 ) ∈ ℤ ) )
37 5 34 35 36 syl2an23an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝑦 ∥ 𝑥 ↔ ( 𝑥 / 𝑦 ) ∈ ℤ ) )
38 33 37 sylibd ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt ( 𝑥 / 𝑦 ) ) → ( 𝑥 / 𝑦 ) ∈ ℤ ) )
39 oveq2 ⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt ( 𝑥 / 𝑦 ) ) )
40 39 breq2d ⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 0 ≤ ( 𝑝 pCnt 𝐴 ) ↔ 0 ≤ ( 𝑝 pCnt ( 𝑥 / 𝑦 ) ) ) )
41 40 ralbidv ⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt 𝐴 ) ↔ ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt ( 𝑥 / 𝑦 ) ) ) )
42 eleq1 ⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝐴 ∈ ℤ ↔ ( 𝑥 / 𝑦 ) ∈ ℤ ) )
43 41 42 imbi12d ⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( ( ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt 𝐴 ) → 𝐴 ∈ ℤ ) ↔ ( ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt ( 𝑥 / 𝑦 ) ) → ( 𝑥 / 𝑦 ) ∈ ℤ ) ) )
44 38 43 syl5ibrcom ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝐴 = ( 𝑥 / 𝑦 ) → ( ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt 𝐴 ) → 𝐴 ∈ ℤ ) ) )
45 44 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) → ( ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt 𝐴 ) → 𝐴 ∈ ℤ ) )
46 4 45 sylbi ⊢ ( 𝐴 ∈ ℚ → ( ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt 𝐴 ) → 𝐴 ∈ ℤ ) )
47 3 46 impbid2 ⊢ ( 𝐴 ∈ ℚ → ( 𝐴 ∈ ℤ ↔ ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt 𝐴 ) ) )