Theorem pceu 16183

Description: Uniqueness for the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.)

Hypotheses

Ref	Expression
pcval.1	⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < )
pcval.2	⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )

Assertion

Ref	Expression
pceu	⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ∃!𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))

Distinct variable groups:   𝑥,𝑛,𝑦,𝑧,𝑁   𝑃,𝑛,𝑥,𝑦,𝑧   𝑧,𝑆   𝑧,𝑇

Allowed substitution hints:   𝑆(𝑥,𝑦,𝑛)   𝑇(𝑥,𝑦,𝑛)

Proof of Theorem pceu

Dummy variables 𝑠 𝑡 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprl 769	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → 𝑁 ∈ ℚ)
2		elq 12351	. . . 4 ⊢ (𝑁 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝑁 = (𝑥 / 𝑦))
3	1, 2	sylib 220	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝑁 = (𝑥 / 𝑦))
4		ovex 7189	. . . . . . . . 9 ⊢ (𝑆 − 𝑇) ∈ V
5		biidd 264	. . . . . . . . 9 ⊢ (𝑧 = (𝑆 − 𝑇) → (𝑁 = (𝑥 / 𝑦) ↔ 𝑁 = (𝑥 / 𝑦)))
6	4, 5	ceqsexv 3541	. . . . . . . 8 ⊢ (∃𝑧(𝑧 = (𝑆 − 𝑇) ∧ 𝑁 = (𝑥 / 𝑦)) ↔ 𝑁 = (𝑥 / 𝑦))
7		exancom 1861	. . . . . . . 8 ⊢ (∃𝑧(𝑧 = (𝑆 − 𝑇) ∧ 𝑁 = (𝑥 / 𝑦)) ↔ ∃𝑧(𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))
8	6, 7	bitr3i 279	. . . . . . 7 ⊢ (𝑁 = (𝑥 / 𝑦) ↔ ∃𝑧(𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))
9	8	rexbii 3247	. . . . . 6 ⊢ (∃𝑦 ∈ ℕ 𝑁 = (𝑥 / 𝑦) ↔ ∃𝑦 ∈ ℕ ∃𝑧(𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))
10		rexcom4 3249	. . . . . 6 ⊢ (∃𝑦 ∈ ℕ ∃𝑧(𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)) ↔ ∃𝑧∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))
11	9, 10	bitri 277	. . . . 5 ⊢ (∃𝑦 ∈ ℕ 𝑁 = (𝑥 / 𝑦) ↔ ∃𝑧∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))
12	11	rexbii 3247	. . . 4 ⊢ (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝑁 = (𝑥 / 𝑦) ↔ ∃𝑥 ∈ ℤ ∃𝑧∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))
13		rexcom4 3249	. . . 4 ⊢ (∃𝑥 ∈ ℤ ∃𝑧∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)) ↔ ∃𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))
14	12, 13	bitri 277	. . 3 ⊢ (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝑁 = (𝑥 / 𝑦) ↔ ∃𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))
15	3, 14	sylib 220	. 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ∃𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))
16		pcval.1	. . . . . . . . . . 11 ⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < )
17		pcval.2	. . . . . . . . . . 11 ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )
18		eqid 2821	. . . . . . . . . . 11 ⊢ sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < )
19		eqid 2821	. . . . . . . . . . 11 ⊢ sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )
20		simp11l 1280	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ) ∧ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))) → 𝑃 ∈ ℙ)
21		simp11r 1281	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ) ∧ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))) → 𝑁 ≠ 0)
22		simp12 1200	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ) ∧ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))) → (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ))
23		simp13l 1284	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ) ∧ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))) → 𝑁 = (𝑥 / 𝑦))
24		simp2 1133	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ) ∧ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))) → (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ))
25		simp3l 1197	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ) ∧ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))) → 𝑁 = (𝑠 / 𝑡))
26	16, 17, 18, 19, 20, 21, 22, 23, 24, 25	pceulem 16182	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ) ∧ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))) → (𝑆 − 𝑇) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))
27		simp13r 1285	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ) ∧ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))) → 𝑧 = (𝑆 − 𝑇))
28		simp3r 1198	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ) ∧ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))) → 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))
29	26, 27, 28	3eqtr4d 2866	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ) ∧ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))) → 𝑧 = 𝑤)
30	29	3exp 1115	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))) → ((𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ) → ((𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < ))) → 𝑧 = 𝑤)))
31	30	rexlimdvv 3293	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))) → (∃𝑠 ∈ ℤ ∃𝑡 ∈ ℕ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < ))) → 𝑧 = 𝑤))
32	31	3exp 1115	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) → ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → ((𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)) → (∃𝑠 ∈ ℤ ∃𝑡 ∈ ℕ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < ))) → 𝑧 = 𝑤))))
33	32	adantrl 714	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → ((𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)) → (∃𝑠 ∈ ℤ ∃𝑡 ∈ ℕ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < ))) → 𝑧 = 𝑤))))
34	33	rexlimdvv 3293	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)) → (∃𝑠 ∈ ℤ ∃𝑡 ∈ ℕ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < ))) → 𝑧 = 𝑤)))
35	34	impd 413	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ((∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)) ∧ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℕ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))) → 𝑧 = 𝑤))
36	35	alrimivv 1929	. 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ∀𝑧∀𝑤((∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)) ∧ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℕ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))) → 𝑧 = 𝑤))
37		eqeq1 2825	. . . . . 6 ⊢ (𝑧 = 𝑤 → (𝑧 = (𝑆 − 𝑇) ↔ 𝑤 = (𝑆 − 𝑇)))
38	37	anbi2d 630	. . . . 5 ⊢ (𝑧 = 𝑤 → ((𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)) ↔ (𝑁 = (𝑥 / 𝑦) ∧ 𝑤 = (𝑆 − 𝑇))))
39	38	2rexbidv 3300	. . . 4 ⊢ (𝑧 = 𝑤 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑤 = (𝑆 − 𝑇))))
40		oveq1 7163	. . . . . . . . 9 ⊢ (𝑥 = 𝑠 → (𝑥 / 𝑦) = (𝑠 / 𝑦))
41	40	eqeq2d 2832	. . . . . . . 8 ⊢ (𝑥 = 𝑠 → (𝑁 = (𝑥 / 𝑦) ↔ 𝑁 = (𝑠 / 𝑦)))
42		breq2 5070	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑠 → ((𝑃↑𝑛) ∥ 𝑥 ↔ (𝑃↑𝑛) ∥ 𝑠))
43	42	rabbidv 3480	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑠 → {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥} = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠})
44	43	supeq1d 8910	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑠 → sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ))
45	16, 44	syl5eq 2868	. . . . . . . . . 10 ⊢ (𝑥 = 𝑠 → 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ))
46	45	oveq1d 7171	. . . . . . . . 9 ⊢ (𝑥 = 𝑠 → (𝑆 − 𝑇) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − 𝑇))
47	46	eqeq2d 2832	. . . . . . . 8 ⊢ (𝑥 = 𝑠 → (𝑤 = (𝑆 − 𝑇) ↔ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − 𝑇)))
48	41, 47	anbi12d 632	. . . . . . 7 ⊢ (𝑥 = 𝑠 → ((𝑁 = (𝑥 / 𝑦) ∧ 𝑤 = (𝑆 − 𝑇)) ↔ (𝑁 = (𝑠 / 𝑦) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − 𝑇))))
49	48	rexbidv 3297	. . . . . 6 ⊢ (𝑥 = 𝑠 → (∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑤 = (𝑆 − 𝑇)) ↔ ∃𝑦 ∈ ℕ (𝑁 = (𝑠 / 𝑦) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − 𝑇))))
50		oveq2 7164	. . . . . . . . 9 ⊢ (𝑦 = 𝑡 → (𝑠 / 𝑦) = (𝑠 / 𝑡))
51	50	eqeq2d 2832	. . . . . . . 8 ⊢ (𝑦 = 𝑡 → (𝑁 = (𝑠 / 𝑦) ↔ 𝑁 = (𝑠 / 𝑡)))
52		breq2 5070	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑡 → ((𝑃↑𝑛) ∥ 𝑦 ↔ (𝑃↑𝑛) ∥ 𝑡))
53	52	rabbidv 3480	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑡 → {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦} = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡})
54	53	supeq1d 8910	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑡 → sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < ))
55	17, 54	syl5eq 2868	. . . . . . . . . 10 ⊢ (𝑦 = 𝑡 → 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < ))
56	55	oveq2d 7172	. . . . . . . . 9 ⊢ (𝑦 = 𝑡 → (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − 𝑇) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))
57	56	eqeq2d 2832	. . . . . . . 8 ⊢ (𝑦 = 𝑡 → (𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − 𝑇) ↔ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < ))))
58	51, 57	anbi12d 632	. . . . . . 7 ⊢ (𝑦 = 𝑡 → ((𝑁 = (𝑠 / 𝑦) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − 𝑇)) ↔ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))))
59	58	cbvrexvw 3450	. . . . . 6 ⊢ (∃𝑦 ∈ ℕ (𝑁 = (𝑠 / 𝑦) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − 𝑇)) ↔ ∃𝑡 ∈ ℕ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < ))))
60	49, 59	syl6bb 289	. . . . 5 ⊢ (𝑥 = 𝑠 → (∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑤 = (𝑆 − 𝑇)) ↔ ∃𝑡 ∈ ℕ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))))
61	60	cbvrexvw 3450	. . . 4 ⊢ (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑤 = (𝑆 − 𝑇)) ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℕ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < ))))
62	39, 61	syl6bb 289	. . 3 ⊢ (𝑧 = 𝑤 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)) ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℕ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))))
63	62	eu4 2699	. 2 ⊢ (∃!𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)) ↔ (∃𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)) ∧ ∀𝑧∀𝑤((∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)) ∧ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℕ (𝑁 = (𝑠 / 𝑡) ∧ 𝑤 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )))) → 𝑧 = 𝑤)))
64	15, 36, 63	sylanbrc 585	1 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ∃!𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083  ∀wal 1535   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ∃!weu 2653   ≠ wne 3016  ∃wrex 3139  {crab 3142   class class class wbr 5066  (class class class)co 7156  supcsup 8904  ℝcr 10536  0cc0 10537   < clt 10675   − cmin 10870   / cdiv 11297  ℕcn 11638  ℕ₀cn0 11898  ℤcz 11982  ℚcq 12349  ↑cexp 13430   ∥ cdvds 15607  ℙcprime 16015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614  ax-pre-sup 10615

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-1st 7689  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-1o 8102  df-2o 8103  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-fin 8513  df-sup 8906  df-inf 8907  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-div 11298  df-nn 11639  df-2 11701  df-3 11702  df-n0 11899  df-z 11983  df-uz 12245  df-q 12350  df-rp 12391  df-fl 13163  df-mod 13239  df-seq 13371  df-exp 13431  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-dvds 15608  df-gcd 15844  df-prm 16016

This theorem is referenced by:  pczpre  16184  pcdiv  16189