Metamath Proof Explorer

Theorem pcneg

Description: The prime count of a negative number. (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Assertion pcneg ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ ) → ( 𝑃 pCnt - 𝐴 ) = ( 𝑃 pCnt 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elq ⊢ ( 𝐴 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
2 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
3 2 ad2antrl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → 𝑥 ∈ ℂ )
4 nncn ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
5 4 ad2antll ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → 𝑦 ∈ ℂ )
6 nnne0 ⊢ ( 𝑦 ∈ ℕ → 𝑦 ≠ 0 )
7 6 ad2antll ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → 𝑦 ≠ 0 )
8 3 5 7 divnegd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → - ( 𝑥 / 𝑦 ) = ( - 𝑥 / 𝑦 ) )
9 8 oveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑃 pCnt - ( 𝑥 / 𝑦 ) ) = ( 𝑃 pCnt ( - 𝑥 / 𝑦 ) ) )
10 neg0 ⊢ - 0 = 0
11 simpr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 = 0 ) → 𝑥 = 0 )
12 11 negeqd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 = 0 ) → - 𝑥 = - 0 )
13 10 12 11 3eqtr4a ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 = 0 ) → - 𝑥 = 𝑥 )
14 13 oveq1d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 = 0 ) → ( - 𝑥 / 𝑦 ) = ( 𝑥 / 𝑦 ) )
15 14 oveq2d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 = 0 ) → ( 𝑃 pCnt ( - 𝑥 / 𝑦 ) ) = ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) )
16 simpll ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → 𝑃 ∈ ℙ )
17 simplrl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → 𝑥 ∈ ℤ )
18 17 znegcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → - 𝑥 ∈ ℤ )
19 simpr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → 𝑥 ≠ 0 )
20 2 negne0bd ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 ≠ 0 ↔ - 𝑥 ≠ 0 ) )
21 17 20 syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → ( 𝑥 ≠ 0 ↔ - 𝑥 ≠ 0 ) )
22 19 21 mpbid ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → - 𝑥 ≠ 0 )
23 simplrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → 𝑦 ∈ ℕ )
24 pcdiv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( - 𝑥 ∈ ℤ ∧ - 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 pCnt ( - 𝑥 / 𝑦 ) ) = ( ( 𝑃 pCnt - 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) )
25 16 18 22 23 24 syl121anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → ( 𝑃 pCnt ( - 𝑥 / 𝑦 ) ) = ( ( 𝑃 pCnt - 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) )
26 pcdiv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) = ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) )
27 16 17 19 23 26 syl121anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) = ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) )
28 eqid ⊢ sup ( { 𝑦 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑦 ) ∥ - 𝑥 } , ℝ , < ) = sup ( { 𝑦 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑦 ) ∥ - 𝑥 } , ℝ , < )
29 28 pczpre ⊢ ( ( 𝑃 ∈ ℙ ∧ ( - 𝑥 ∈ ℤ ∧ - 𝑥 ≠ 0 ) ) → ( 𝑃 pCnt - 𝑥 ) = sup ( { 𝑦 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑦 ) ∥ - 𝑥 } , ℝ , < ) )
30 16 18 22 29 syl12anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → ( 𝑃 pCnt - 𝑥 ) = sup ( { 𝑦 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑦 ) ∥ - 𝑥 } , ℝ , < ) )
31 eqid ⊢ sup ( { 𝑦 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑦 ) ∥ 𝑥 } , ℝ , < ) = sup ( { 𝑦 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑦 ) ∥ 𝑥 } , ℝ , < )
32 31 pczpre ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ( 𝑃 pCnt 𝑥 ) = sup ( { 𝑦 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑦 ) ∥ 𝑥 } , ℝ , < ) )
33 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
34 zexpcl ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑦 ) ∈ ℤ )
35 33 34 sylan ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑦 ) ∈ ℤ )
36 simpl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) → 𝑥 ∈ ℤ )
37 dvdsnegb ⊢ ( ( ( 𝑃 ↑ 𝑦 ) ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( ( 𝑃 ↑ 𝑦 ) ∥ 𝑥 ↔ ( 𝑃 ↑ 𝑦 ) ∥ - 𝑥 ) )
38 35 36 37 syl2an ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ( ( 𝑃 ↑ 𝑦 ) ∥ 𝑥 ↔ ( 𝑃 ↑ 𝑦 ) ∥ - 𝑥 ) )
39 38 an32s ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑃 ↑ 𝑦 ) ∥ 𝑥 ↔ ( 𝑃 ↑ 𝑦 ) ∥ - 𝑥 ) )
40 39 rabbidva ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → { 𝑦 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑦 ) ∥ 𝑥 } = { 𝑦 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑦 ) ∥ - 𝑥 } )
41 40 supeq1d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → sup ( { 𝑦 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑦 ) ∥ 𝑥 } , ℝ , < ) = sup ( { 𝑦 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑦 ) ∥ - 𝑥 } , ℝ , < ) )
42 32 41 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ( 𝑃 pCnt 𝑥 ) = sup ( { 𝑦 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑦 ) ∥ - 𝑥 } , ℝ , < ) )
43 16 17 19 42 syl12anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → ( 𝑃 pCnt 𝑥 ) = sup ( { 𝑦 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑦 ) ∥ - 𝑥 } , ℝ , < ) )
44 30 43 eqtr4d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → ( 𝑃 pCnt - 𝑥 ) = ( 𝑃 pCnt 𝑥 ) )
45 44 oveq1d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → ( ( 𝑃 pCnt - 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) = ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) )
46 27 45 eqtr4d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) = ( ( 𝑃 pCnt - 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) )
47 25 46 eqtr4d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 ≠ 0 ) → ( 𝑃 pCnt ( - 𝑥 / 𝑦 ) ) = ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) )
48 15 47 pm2.61dane ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑃 pCnt ( - 𝑥 / 𝑦 ) ) = ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) )
49 9 48 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑃 pCnt - ( 𝑥 / 𝑦 ) ) = ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) )
50 negeq ⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → - 𝐴 = - ( 𝑥 / 𝑦 ) )
51 50 oveq2d ⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝑃 pCnt - 𝐴 ) = ( 𝑃 pCnt - ( 𝑥 / 𝑦 ) ) )
52 oveq2 ⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝑃 pCnt 𝐴 ) = ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) )
53 51 52 eqeq12d ⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( ( 𝑃 pCnt - 𝐴 ) = ( 𝑃 pCnt 𝐴 ) ↔ ( 𝑃 pCnt - ( 𝑥 / 𝑦 ) ) = ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) ) )
54 49 53 syl5ibrcom ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝑃 pCnt - 𝐴 ) = ( 𝑃 pCnt 𝐴 ) ) )
55 54 rexlimdvva ⊢ ( 𝑃 ∈ ℙ → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝑃 pCnt - 𝐴 ) = ( 𝑃 pCnt 𝐴 ) ) )
56 1 55 syl5bi ⊢ ( 𝑃 ∈ ℙ → ( 𝐴 ∈ ℚ → ( 𝑃 pCnt - 𝐴 ) = ( 𝑃 pCnt 𝐴 ) ) )
57 56 imp ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ ) → ( 𝑃 pCnt - 𝐴 ) = ( 𝑃 pCnt 𝐴 ) )