This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑆 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < )
pcval.2 ⊢ 𝑇 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < )
Assertion pcval ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) = ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) )

Proof

Step Hyp Ref Expression
1 pcval.1 ⊢ 𝑆 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < )
2 pcval.2 ⊢ 𝑇 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < )
3 simpr ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑟 = 𝑁 ) → 𝑟 = 𝑁 )
4 3 eqeq1d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑟 = 𝑁 ) → ( 𝑟 = 0 ↔ 𝑁 = 0 ) )
5 eqeq1 ⊢ ( 𝑟 = 𝑁 → ( 𝑟 = ( 𝑥 / 𝑦 ) ↔ 𝑁 = ( 𝑥 / 𝑦 ) ) )
6 oveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ↑ 𝑛 ) = ( 𝑃 ↑ 𝑛 ) )
7 6 breq1d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 ↔ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 ) )
8 7 rabbidv ⊢ ( 𝑝 = 𝑃 → { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } )
9 8 supeq1d ⊢ ( 𝑝 = 𝑃 → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) )
10 9 1 eqtr4di ⊢ ( 𝑝 = 𝑃 → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) = 𝑆 )
11 6 breq1d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 ↔ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 ) )
12 11 rabbidv ⊢ ( 𝑝 = 𝑃 → { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } )
13 12 supeq1d ⊢ ( 𝑝 = 𝑃 → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) )
14 13 2 eqtr4di ⊢ ( 𝑝 = 𝑃 → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) = 𝑇 )
15 10 14 oveq12d ⊢ ( 𝑝 = 𝑃 → ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) = ( 𝑆 − 𝑇 ) )
16 15 eqeq2d ⊢ ( 𝑝 = 𝑃 → ( 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ↔ 𝑧 = ( 𝑆 − 𝑇 ) ) )
17 5 16 bi2anan9r ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑟 = 𝑁 ) → ( ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ↔ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) )
18 17 2rexbidv ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑟 = 𝑁 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) )
19 18 iotabidv ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑟 = 𝑁 ) → ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) = ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) )
20 4 19 ifbieq2d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑟 = 𝑁 ) → if ( 𝑟 = 0 , +∞ , ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) ) = if ( 𝑁 = 0 , +∞ , ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ) )
21 df-pc ⊢ pCnt = ( 𝑝 ∈ ℙ , 𝑟 ∈ ℚ ↦ if ( 𝑟 = 0 , +∞ , ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) ) )
22 pnfex ⊢ +∞ ∈ V
23 iotaex ⊢ ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ∈ V
24 22 23 ifex ⊢ if ( 𝑁 = 0 , +∞ , ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ) ∈ V
25 20 21 24 ovmpoa ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℚ ) → ( 𝑃 pCnt 𝑁 ) = if ( 𝑁 = 0 , +∞ , ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ) )
26 ifnefalse ⊢ ( 𝑁 ≠ 0 → if ( 𝑁 = 0 , +∞ , ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ) = ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) )
27 25 26 sylan9eq ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℚ ) ∧ 𝑁 ≠ 0 ) → ( 𝑃 pCnt 𝑁 ) = ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) )
28 27 anasss ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) = ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) )