Metamath Proof Explorer

Theorem pcdvdstr

Description: The prime count increases under the divisibility relation. (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Assertion pcdvdstr ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) )

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 zq ⊢ ( 0 ∈ ℤ → 0 ∈ ℚ )
3 1 2 ax-mp ⊢ 0 ∈ ℚ
4 pcxcl ⊢ ( ( 𝑃 ∈ ℙ ∧ 0 ∈ ℚ ) → ( 𝑃 pCnt 0 ) ∈ ℝ* )
5 3 4 mpan2 ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 0 ) ∈ ℝ* )
6 5 xrleidd ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 0 ) ≤ ( 𝑃 pCnt 0 ) )
7 6 ad2antrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 = 0 ) → ( 𝑃 pCnt 0 ) ≤ ( 𝑃 pCnt 0 ) )
8 simpr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 = 0 ) → 𝐴 = 0 )
9 8 oveq2d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 = 0 ) → ( 𝑃 pCnt 𝐴 ) = ( 𝑃 pCnt 0 ) )
10 simplr3 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 = 0 ) → 𝐴 ∥ 𝐵 )
11 8 10 eqbrtrrd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 = 0 ) → 0 ∥ 𝐵 )
12 simplr2 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 = 0 ) → 𝐵 ∈ ℤ )
13 0dvds ⊢ ( 𝐵 ∈ ℤ → ( 0 ∥ 𝐵 ↔ 𝐵 = 0 ) )
14 12 13 syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 = 0 ) → ( 0 ∥ 𝐵 ↔ 𝐵 = 0 ) )
15 11 14 mpbid ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 = 0 ) → 𝐵 = 0 )
16 15 oveq2d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 = 0 ) → ( 𝑃 pCnt 𝐵 ) = ( 𝑃 pCnt 0 ) )
17 7 9 16 3brtr4d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 = 0 ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) )
18 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
19 18 ad2antrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → 𝑃 ∈ ℕ )
20 simpll ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → 𝑃 ∈ ℙ )
21 simplr1 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℤ )
22 simpr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
23 pczcl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 )
24 20 21 22 23 syl12anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 )
25 19 24 nnexpcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℕ )
26 25 nnzd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℤ )
27 simplr2 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → 𝐵 ∈ ℤ )
28 pczdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 )
29 20 21 22 28 syl12anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 )
30 simplr3 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∥ 𝐵 )
31 26 21 27 29 30 dvdstrd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐵 )
32 pcdvdsb ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐵 ∈ ℤ ∧ ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 ) → ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ↔ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐵 ) )
33 20 27 24 32 syl3anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ↔ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐵 ) )
34 31 33 mpbird ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) )
35 17 34 pm2.61dane ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) )