Metamath Proof Explorer

Theorem pcval

Description: The value of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014) (Revised by Mario Carneiro, 3-Oct-2014)

Ref Expression
Hypotheses pcval.1 ⊢S=supn∈ℕ0|Pn∥xℝ<
pcval.2 ⊢T=supn∈ℕ0|Pn∥yℝ<
Assertion pcval ⊢P∈ℙ∧N∈ℚ∧N≠0→PpCntN=ιz|∃x∈ℤ∃y∈ℕN=xy∧z=S−T

Proof

Step Hyp Ref Expression
1 pcval.1 ⊢S=supn∈ℕ0|Pn∥xℝ<
2 pcval.2 ⊢T=supn∈ℕ0|Pn∥yℝ<
3 simpr ⊢p=P∧r=N→r=N
4 3 eqeq1d ⊢p=P∧r=N→r=0↔N=0
5 eqeq1 ⊢r=N→r=xy↔N=xy
6 oveq1 ⊢p=P→pn=Pn
7 6 breq1d ⊢p=P→pn∥x↔Pn∥x
8 7 rabbidv ⊢p=P→n∈ℕ0|pn∥x=n∈ℕ0|Pn∥x
9 8 supeq1d ⊢p=P→supn∈ℕ0|pn∥xℝ<=supn∈ℕ0|Pn∥xℝ<
10 9 1 eqtr4di ⊢p=P→supn∈ℕ0|pn∥xℝ<=S
11 6 breq1d ⊢p=P→pn∥y↔Pn∥y
12 11 rabbidv ⊢p=P→n∈ℕ0|pn∥y=n∈ℕ0|Pn∥y
13 12 supeq1d ⊢p=P→supn∈ℕ0|pn∥yℝ<=supn∈ℕ0|Pn∥yℝ<
14 13 2 eqtr4di ⊢p=P→supn∈ℕ0|pn∥yℝ<=T
15 10 14 oveq12d ⊢p=P→supn∈ℕ0|pn∥xℝ<−supn∈ℕ0|pn∥yℝ<=S−T
16 15 eqeq2d ⊢p=P→z=supn∈ℕ0|pn∥xℝ<−supn∈ℕ0|pn∥yℝ<↔z=S−T
17 5 16 bi2anan9r ⊢p=P∧r=N→r=xy∧z=supn∈ℕ0|pn∥xℝ<−supn∈ℕ0|pn∥yℝ<↔N=xy∧z=S−T
18 17 2rexbidv ⊢p=P∧r=N→∃x∈ℤ∃y∈ℕr=xy∧z=supn∈ℕ0|pn∥xℝ<−supn∈ℕ0|pn∥yℝ<↔∃x∈ℤ∃y∈ℕN=xy∧z=S−T
19 18 iotabidv ⊢p=P∧r=N→ιz|∃x∈ℤ∃y∈ℕr=xy∧z=supn∈ℕ0|pn∥xℝ<−supn∈ℕ0|pn∥yℝ<=ιz|∃x∈ℤ∃y∈ℕN=xy∧z=S−T
20 4 19 ifbieq2d ⊢p=P∧r=N→ifr=0+∞ιz|∃x∈ℤ∃y∈ℕr=xy∧z=supn∈ℕ0|pn∥xℝ<−supn∈ℕ0|pn∥yℝ<=ifN=0+∞ιz|∃x∈ℤ∃y∈ℕN=xy∧z=S−T
21 df-pc ⊢pCnt=p∈ℙ,r∈ℚ⟼ifr=0+∞ιz|∃x∈ℤ∃y∈ℕr=xy∧z=supn∈ℕ0|pn∥xℝ<−supn∈ℕ0|pn∥yℝ<
22 pnfex ⊢+∞∈V
23 iotaex ⊢ιz|∃x∈ℤ∃y∈ℕN=xy∧z=S−T∈V
24 22 23 ifex ⊢ifN=0+∞ιz|∃x∈ℤ∃y∈ℕN=xy∧z=S−T∈V
25 20 21 24 ovmpoa ⊢P∈ℙ∧N∈ℚ→PpCntN=ifN=0+∞ιz|∃x∈ℤ∃y∈ℕN=xy∧z=S−T
26 ifnefalse ⊢N≠0→ifN=0+∞ιz|∃x∈ℤ∃y∈ℕN=xy∧z=S−T=ιz|∃x∈ℤ∃y∈ℕN=xy∧z=S−T
27 25 26 sylan9eq ⊢P∈ℙ∧N∈ℚ∧N≠0→PpCntN=ιz|∃x∈ℤ∃y∈ℕN=xy∧z=S−T
28 27 anasss ⊢P∈ℙ∧N∈ℚ∧N≠0→PpCntN=ιz|∃x∈ℤ∃y∈ℕN=xy∧z=S−T