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 simpll ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → 𝑃 ∈ ℙ )
19 simplr1 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℤ )
20 simpr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
21 pczdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 )
22 18 19 20 21 syl12anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 )
23 simplr3 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∥ 𝐵 )
24 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
25 24 ad2antrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → 𝑃 ∈ ℕ )
26 pczcl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 )
27 18 19 20 26 syl12anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 )
28 25 27 nnexpcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℕ )
29 28 nnzd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℤ )
30 simplr2 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → 𝐵 ∈ ℤ )
31 dvdstr ⊢ ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 ∧ 𝐴 ∥ 𝐵 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐵 ) )
32 29 19 30 31 syl3anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 ∧ 𝐴 ∥ 𝐵 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐵 ) )
33 22 23 32 mp2and ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐵 )
34 pcdvdsb ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐵 ∈ ℤ ∧ ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 ) → ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ↔ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐵 ) )
35 18 30 27 34 syl3anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ↔ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐵 ) )
36 33 35 mpbird ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) ∧ 𝐴 ≠ 0 ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) )
37 17 36 pm2.61dane ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵 ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) )