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