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 𝑁 ) = ( ℩ 𝑧𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆𝑇 ) ) ) )