Metamath Proof Explorer

Theorem pceulem

Description: Lemma for pceu . (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Hypotheses pcval.1 ⊢ 𝑆 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < )
pcval.2 ⊢ 𝑇 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < )
pceu.3 ⊢ 𝑈 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < )
pceu.4 ⊢ 𝑉 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < )
pceu.5 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
pceu.6 ⊢ ( 𝜑 → 𝑁 ≠ 0 )
pceu.7 ⊢ ( 𝜑 → ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) )
pceu.8 ⊢ ( 𝜑 → 𝑁 = ( 𝑥 / 𝑦 ) )
pceu.9 ⊢ ( 𝜑 → ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) )
pceu.10 ⊢ ( 𝜑 → 𝑁 = ( 𝑠 / 𝑡 ) )
Assertion pceulem ( 𝜑 → ( 𝑆 − 𝑇 ) = ( 𝑈 − 𝑉 ) )

Proof

Step Hyp Ref Expression
1 pcval.1 ⊢ 𝑆 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < )
2 pcval.2 ⊢ 𝑇 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < )
3 pceu.3 ⊢ 𝑈 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < )
4 pceu.4 ⊢ 𝑉 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < )
5 pceu.5 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
6 pceu.6 ⊢ ( 𝜑 → 𝑁 ≠ 0 )
7 pceu.7 ⊢ ( 𝜑 → ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) )
8 pceu.8 ⊢ ( 𝜑 → 𝑁 = ( 𝑥 / 𝑦 ) )
9 pceu.9 ⊢ ( 𝜑 → ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) )
10 pceu.10 ⊢ ( 𝜑 → 𝑁 = ( 𝑠 / 𝑡 ) )
11 7 simprd ⊢ ( 𝜑 → 𝑦 ∈ ℕ )
12 11 nncnd ⊢ ( 𝜑 → 𝑦 ∈ ℂ )
13 9 simpld ⊢ ( 𝜑 → 𝑠 ∈ ℤ )
14 13 zcnd ⊢ ( 𝜑 → 𝑠 ∈ ℂ )
15 12 14 mulcomd ⊢ ( 𝜑 → ( 𝑦 · 𝑠 ) = ( 𝑠 · 𝑦 ) )
16 10 8 eqtr3d ⊢ ( 𝜑 → ( 𝑠 / 𝑡 ) = ( 𝑥 / 𝑦 ) )
17 9 simprd ⊢ ( 𝜑 → 𝑡 ∈ ℕ )
18 17 nncnd ⊢ ( 𝜑 → 𝑡 ∈ ℂ )
19 7 simpld ⊢ ( 𝜑 → 𝑥 ∈ ℤ )
20 19 zcnd ⊢ ( 𝜑 → 𝑥 ∈ ℂ )
21 17 nnne0d ⊢ ( 𝜑 → 𝑡 ≠ 0 )
22 11 nnne0d ⊢ ( 𝜑 → 𝑦 ≠ 0 )
23 14 18 20 12 21 22 divmuleqd ⊢ ( 𝜑 → ( ( 𝑠 / 𝑡 ) = ( 𝑥 / 𝑦 ) ↔ ( 𝑠 · 𝑦 ) = ( 𝑥 · 𝑡 ) ) )
24 16 23 mpbid ⊢ ( 𝜑 → ( 𝑠 · 𝑦 ) = ( 𝑥 · 𝑡 ) )
25 15 24 eqtrd ⊢ ( 𝜑 → ( 𝑦 · 𝑠 ) = ( 𝑥 · 𝑡 ) )
26 25 breq2d ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑦 · 𝑠 ) ↔ ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑥 · 𝑡 ) ) )
27 26 rabbidv ⊢ ( 𝜑 → { 𝑧 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑦 · 𝑠 ) } = { 𝑧 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑥 · 𝑡 ) } )
28 oveq2 ⊢ ( 𝑛 = 𝑧 → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ 𝑧 ) )
29 28 breq1d ⊢ ( 𝑛 = 𝑧 → ( ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) ↔ ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑦 · 𝑠 ) ) )
30 29 cbvrabv ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) } = { 𝑧 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑦 · 𝑠 ) }
31 28 breq1d ⊢ ( 𝑛 = 𝑧 → ( ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) ↔ ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑥 · 𝑡 ) ) )
32 31 cbvrabv ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) } = { 𝑧 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑥 · 𝑡 ) }
33 27 30 32 3eqtr4g ⊢ ( 𝜑 → { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) } )
34 33 supeq1d ⊢ ( 𝜑 → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) } , ℝ , < ) )
35 11 nnzd ⊢ ( 𝜑 → 𝑦 ∈ ℤ )
36 18 21 div0d ⊢ ( 𝜑 → ( 0 / 𝑡 ) = 0 )
37 oveq1 ⊢ ( 𝑠 = 0 → ( 𝑠 / 𝑡 ) = ( 0 / 𝑡 ) )
38 37 eqeq1d ⊢ ( 𝑠 = 0 → ( ( 𝑠 / 𝑡 ) = 0 ↔ ( 0 / 𝑡 ) = 0 ) )
39 36 38 syl5ibrcom ⊢ ( 𝜑 → ( 𝑠 = 0 → ( 𝑠 / 𝑡 ) = 0 ) )
40 10 eqeq1d ⊢ ( 𝜑 → ( 𝑁 = 0 ↔ ( 𝑠 / 𝑡 ) = 0 ) )
41 39 40 sylibrd ⊢ ( 𝜑 → ( 𝑠 = 0 → 𝑁 = 0 ) )
42 41 necon3d ⊢ ( 𝜑 → ( 𝑁 ≠ 0 → 𝑠 ≠ 0 ) )
43 6 42 mpd ⊢ ( 𝜑 → 𝑠 ≠ 0 )
44 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) } , ℝ , < )
45 2 3 44 pcpremul ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑠 ≠ 0 ) ) → ( 𝑇 + 𝑈 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) } , ℝ , < ) )
46 5 35 22 13 43 45 syl122anc ⊢ ( 𝜑 → ( 𝑇 + 𝑈 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) } , ℝ , < ) )
47 12 22 div0d ⊢ ( 𝜑 → ( 0 / 𝑦 ) = 0 )
48 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 / 𝑦 ) = ( 0 / 𝑦 ) )
49 48 eqeq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 / 𝑦 ) = 0 ↔ ( 0 / 𝑦 ) = 0 ) )
50 47 49 syl5ibrcom ⊢ ( 𝜑 → ( 𝑥 = 0 → ( 𝑥 / 𝑦 ) = 0 ) )
51 8 eqeq1d ⊢ ( 𝜑 → ( 𝑁 = 0 ↔ ( 𝑥 / 𝑦 ) = 0 ) )
52 50 51 sylibrd ⊢ ( 𝜑 → ( 𝑥 = 0 → 𝑁 = 0 ) )
53 52 necon3d ⊢ ( 𝜑 → ( 𝑁 ≠ 0 → 𝑥 ≠ 0 ) )
54 6 53 mpd ⊢ ( 𝜑 → 𝑥 ≠ 0 )
55 17 nnzd ⊢ ( 𝜑 → 𝑡 ∈ ℤ )
56 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) } , ℝ , < )
57 1 4 56 pcpremul ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑡 ∈ ℤ ∧ 𝑡 ≠ 0 ) ) → ( 𝑆 + 𝑉 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) } , ℝ , < ) )
58 5 19 54 55 21 57 syl122anc ⊢ ( 𝜑 → ( 𝑆 + 𝑉 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) } , ℝ , < ) )
59 34 46 58 3eqtr4d ⊢ ( 𝜑 → ( 𝑇 + 𝑈 ) = ( 𝑆 + 𝑉 ) )
60 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
61 5 60 syl ⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
62 eqid ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 }
63 62 2 pcprecl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) ) → ( 𝑇 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑇 ) ∥ 𝑦 ) )
64 63 simpld ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) ) → 𝑇 ∈ ℕ0 )
65 61 35 22 64 syl12anc ⊢ ( 𝜑 → 𝑇 ∈ ℕ0 )
66 65 nn0cnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
67 eqid ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 }
68 67 3 pcprecl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑠 ≠ 0 ) ) → ( 𝑈 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑈 ) ∥ 𝑠 ) )
69 68 simpld ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑠 ≠ 0 ) ) → 𝑈 ∈ ℕ0 )
70 61 13 43 69 syl12anc ⊢ ( 𝜑 → 𝑈 ∈ ℕ0 )
71 70 nn0cnd ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
72 eqid ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 }
73 72 1 pcprecl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ( 𝑆 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑆 ) ∥ 𝑥 ) )
74 73 simpld ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → 𝑆 ∈ ℕ0 )
75 61 19 54 74 syl12anc ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
76 75 nn0cnd ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
77 eqid ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 }
78 77 4 pcprecl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑡 ∈ ℤ ∧ 𝑡 ≠ 0 ) ) → ( 𝑉 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑉 ) ∥ 𝑡 ) )
79 78 simpld ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑡 ∈ ℤ ∧ 𝑡 ≠ 0 ) ) → 𝑉 ∈ ℕ0 )
80 61 55 21 79 syl12anc ⊢ ( 𝜑 → 𝑉 ∈ ℕ0 )
81 80 nn0cnd ⊢ ( 𝜑 → 𝑉 ∈ ℂ )
82 66 71 76 81 addsubeq4d ⊢ ( 𝜑 → ( ( 𝑇 + 𝑈 ) = ( 𝑆 + 𝑉 ) ↔ ( 𝑆 − 𝑇 ) = ( 𝑈 − 𝑉 ) ) )
83 59 82 mpbid ⊢ ( 𝜑 → ( 𝑆 − 𝑇 ) = ( 𝑈 − 𝑉 ) )