Metamath Proof Explorer

Theorem pceu

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

Ref Expression
Hypotheses pcval.1 ⊢ 𝑆 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < )
pcval.2 ⊢ 𝑇 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < )
Assertion pceu ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ∃! 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 pcval.1 ⊢ 𝑆 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < )
2 pcval.2 ⊢ 𝑇 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < )
3 simprl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → 𝑁 ∈ ℚ )
4 elq ⊢ ( 𝑁 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝑁 = ( 𝑥 / 𝑦 ) )
5 3 4 sylib ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝑁 = ( 𝑥 / 𝑦 ) )
6 ovex ⊢ ( 𝑆 − 𝑇 ) ∈ V
7 biidd ⊢ ( 𝑧 = ( 𝑆 − 𝑇 ) → ( 𝑁 = ( 𝑥 / 𝑦 ) ↔ 𝑁 = ( 𝑥 / 𝑦 ) ) )
8 6 7 ceqsexv ⊢ ( ∃ 𝑧 ( 𝑧 = ( 𝑆 − 𝑇 ) ∧ 𝑁 = ( 𝑥 / 𝑦 ) ) ↔ 𝑁 = ( 𝑥 / 𝑦 ) )
9 exancom ⊢ ( ∃ 𝑧 ( 𝑧 = ( 𝑆 − 𝑇 ) ∧ 𝑁 = ( 𝑥 / 𝑦 ) ) ↔ ∃ 𝑧 ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) )
10 8 9 bitr3i ⊢ ( 𝑁 = ( 𝑥 / 𝑦 ) ↔ ∃ 𝑧 ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) )
11 10 rexbii ⊢ ( ∃ 𝑦 ∈ ℕ 𝑁 = ( 𝑥 / 𝑦 ) ↔ ∃ 𝑦 ∈ ℕ ∃ 𝑧 ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) )
12 rexcom4 ⊢ ( ∃ 𝑦 ∈ ℕ ∃ 𝑧 ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ↔ ∃ 𝑧 ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) )
13 11 12 bitri ⊢ ( ∃ 𝑦 ∈ ℕ 𝑁 = ( 𝑥 / 𝑦 ) ↔ ∃ 𝑧 ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) )
14 13 rexbii ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝑁 = ( 𝑥 / 𝑦 ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑧 ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) )
15 rexcom4 ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑧 ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ↔ ∃ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) )
16 14 15 bitri ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝑁 = ( 𝑥 / 𝑦 ) ↔ ∃ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) )
17 5 16 sylib ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ∃ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) )
18 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < )
19 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < )
20 simp11l ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) → 𝑃 ∈ ℙ )
21 simp11r ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) → 𝑁 ≠ 0 )
22 simp12 ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) → ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) )
23 simp13l ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) → 𝑁 = ( 𝑥 / 𝑦 ) )
24 simp2 ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) → ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) )
25 simp3l ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) → 𝑁 = ( 𝑠 / 𝑡 ) )
26 1 2 18 19 20 21 22 23 24 25 pceulem ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) → ( 𝑆 − 𝑇 ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) )
27 simp13r ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) → 𝑧 = ( 𝑆 − 𝑇 ) )
28 simp3r ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) → 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) )
29 26 27 28 3eqtr4d ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) → 𝑧 = 𝑤 )
30 29 3exp ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) → ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) → ( ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) → 𝑧 = 𝑤 ) ) )
31 30 rexlimdvv ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ) → ( ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℕ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) → 𝑧 = 𝑤 ) )
32 31 3exp ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ≠ 0 ) → ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) → ( ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℕ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) → 𝑧 = 𝑤 ) ) ) )
33 32 adantrl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) → ( ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℕ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) → 𝑧 = 𝑤 ) ) ) )
34 33 rexlimdvv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) → ( ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℕ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) → 𝑧 = 𝑤 ) ) )
35 34 impd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ( ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ∧ ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℕ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) → 𝑧 = 𝑤 ) )
36 35 alrimivv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ∀ 𝑧 ∀ 𝑤 ( ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ∧ ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℕ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) → 𝑧 = 𝑤 ) )
37 eqeq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 = ( 𝑆 − 𝑇 ) ↔ 𝑤 = ( 𝑆 − 𝑇 ) ) )
38 37 anbi2d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ↔ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑤 = ( 𝑆 − 𝑇 ) ) ) )
39 38 2rexbidv ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑤 = ( 𝑆 − 𝑇 ) ) ) )
40 oveq1 ⊢ ( 𝑥 = 𝑠 → ( 𝑥 / 𝑦 ) = ( 𝑠 / 𝑦 ) )
41 40 eqeq2d ⊢ ( 𝑥 = 𝑠 → ( 𝑁 = ( 𝑥 / 𝑦 ) ↔ 𝑁 = ( 𝑠 / 𝑦 ) ) )
42 breq2 ⊢ ( 𝑥 = 𝑠 → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 ↔ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 ) )
43 42 rabbidv ⊢ ( 𝑥 = 𝑠 → { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } )
44 43 supeq1d ⊢ ( 𝑥 = 𝑠 → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) )
45 1 44 syl5eq ⊢ ( 𝑥 = 𝑠 → 𝑆 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) )
46 45 oveq1d ⊢ ( 𝑥 = 𝑠 → ( 𝑆 − 𝑇 ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − 𝑇 ) )
47 46 eqeq2d ⊢ ( 𝑥 = 𝑠 → ( 𝑤 = ( 𝑆 − 𝑇 ) ↔ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − 𝑇 ) ) )
48 41 47 anbi12d ⊢ ( 𝑥 = 𝑠 → ( ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑤 = ( 𝑆 − 𝑇 ) ) ↔ ( 𝑁 = ( 𝑠 / 𝑦 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − 𝑇 ) ) ) )
49 48 rexbidv ⊢ ( 𝑥 = 𝑠 → ( ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑤 = ( 𝑆 − 𝑇 ) ) ↔ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑠 / 𝑦 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − 𝑇 ) ) ) )
50 oveq2 ⊢ ( 𝑦 = 𝑡 → ( 𝑠 / 𝑦 ) = ( 𝑠 / 𝑡 ) )
51 50 eqeq2d ⊢ ( 𝑦 = 𝑡 → ( 𝑁 = ( 𝑠 / 𝑦 ) ↔ 𝑁 = ( 𝑠 / 𝑡 ) ) )
52 breq2 ⊢ ( 𝑦 = 𝑡 → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 ↔ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 ) )
53 52 rabbidv ⊢ ( 𝑦 = 𝑡 → { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } )
54 53 supeq1d ⊢ ( 𝑦 = 𝑡 → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) )
55 2 54 syl5eq ⊢ ( 𝑦 = 𝑡 → 𝑇 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) )
56 55 oveq2d ⊢ ( 𝑦 = 𝑡 → ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − 𝑇 ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) )
57 56 eqeq2d ⊢ ( 𝑦 = 𝑡 → ( 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − 𝑇 ) ↔ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) )
58 51 57 anbi12d ⊢ ( 𝑦 = 𝑡 → ( ( 𝑁 = ( 𝑠 / 𝑦 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − 𝑇 ) ) ↔ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) )
59 58 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑠 / 𝑦 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − 𝑇 ) ) ↔ ∃ 𝑡 ∈ ℕ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) )
60 49 59 syl6bb ⊢ ( 𝑥 = 𝑠 → ( ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑤 = ( 𝑆 − 𝑇 ) ) ↔ ∃ 𝑡 ∈ ℕ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) )
61 60 cbvrexvw ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑤 = ( 𝑆 − 𝑇 ) ) ↔ ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℕ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) )
62 39 61 syl6bb ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ↔ ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℕ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) )
63 62 eu4 ⊢ ( ∃! 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ↔ ( ∃ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ∧ ∀ 𝑧 ∀ 𝑤 ( ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) ∧ ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℕ ( 𝑁 = ( 𝑠 / 𝑡 ) ∧ 𝑤 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < ) ) ) ) → 𝑧 = 𝑤 ) ) )
64 17 36 63 sylanbrc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ∃! 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( 𝑆 − 𝑇 ) ) )