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 = sup n ∈ ℕ 0 | P n ∥ x ℝ <
pcval.2 ⊢ T = sup n ∈ ℕ 0 | P n ∥ y ℝ <
Assertion pcval ⊢ P ∈ ℙ ∧ N ∈ ℚ ∧ N ≠ 0 → P pCnt N = ι z | ∃ x ∈ ℤ ∃ y ∈ ℕ N = x y ∧ z = S − T

Proof

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