MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pcpremul Structured version   Visualization version   GIF version

Theorem pcpremul 15595
Description: Multiplicative property of the prime count pre-function. Note that the primality of 𝑃 is essential for this property; (4 pCnt 2) = 0 but (4 pCnt (2 · 2)) = 1 ≠ 2 · (4 pCnt 2) = 0. Since this is needed to show uniqueness for the real prime count function (over ), we don't bother to define it off the primes. (Contributed by Mario Carneiro, 23-Feb-2014.)
Hypotheses
Ref Expression
pcpremul.1 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ 𝑀}, ℝ, < )
pcpremul.2 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ 𝑁}, ℝ, < )
pcpremul.3 𝑈 = sup({𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)}, ℝ, < )
Assertion
Ref Expression
pcpremul ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 + 𝑇) = 𝑈)
Distinct variable groups:   𝑛,𝑀   𝑛,𝑁   𝑃,𝑛
Allowed substitution hints:   𝑆(𝑛)   𝑇(𝑛)   𝑈(𝑛)

Proof of Theorem pcpremul
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prmuz2 15455 . . . . . . 7 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
213ad2ant1 1102 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑃 ∈ (ℤ‘2))
3 zmulcl 11464 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 · 𝑁) ∈ ℤ)
43ad2ant2r 798 . . . . . . 7 (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) ∈ ℤ)
543adant1 1099 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) ∈ ℤ)
6 zcn 11420 . . . . . . . . 9 (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
76anim1i 591 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (𝑀 ∈ ℂ ∧ 𝑀 ≠ 0))
8 zcn 11420 . . . . . . . . 9 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
98anim1i 591 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
10 mulne0 10707 . . . . . . . 8 (((𝑀 ∈ ℂ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) ≠ 0)
117, 9, 10syl2an 493 . . . . . . 7 (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) ≠ 0)
12113adant1 1099 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) ≠ 0)
13 eqid 2651 . . . . . . 7 {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)} = {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)}
1413pclem 15590 . . . . . 6 ((𝑃 ∈ (ℤ‘2) ∧ ((𝑀 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ≠ 0)) → ({𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)} ⊆ ℤ ∧ {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)} ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)}𝑦𝑥))
152, 5, 12, 14syl12anc 1364 . . . . 5 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ({𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)} ⊆ ℤ ∧ {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)} ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)}𝑦𝑥))
1615simp1d 1093 . . . 4 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)} ⊆ ℤ)
1715simp3d 1095 . . . 4 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)}𝑦𝑥)
18 simp2l 1107 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑀 ∈ ℤ)
19 simp2r 1108 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑀 ≠ 0)
20 eqid 2651 . . . . . . . . . 10 {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ 𝑀} = {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ 𝑀}
21 pcpremul.1 . . . . . . . . . 10 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ 𝑀}, ℝ, < )
2220, 21pcprecl 15591 . . . . . . . . 9 ((𝑃 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → (𝑆 ∈ ℕ0 ∧ (𝑃𝑆) ∥ 𝑀))
232, 18, 19, 22syl12anc 1364 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 ∈ ℕ0 ∧ (𝑃𝑆) ∥ 𝑀))
2423simpld 474 . . . . . . 7 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑆 ∈ ℕ0)
25 simp3l 1109 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑁 ∈ ℤ)
26 simp3r 1110 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑁 ≠ 0)
27 eqid 2651 . . . . . . . . . 10 {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ 𝑁} = {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ 𝑁}
28 pcpremul.2 . . . . . . . . . 10 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ 𝑁}, ℝ, < )
2927, 28pcprecl 15591 . . . . . . . . 9 ((𝑃 ∈ (ℤ‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑇 ∈ ℕ0 ∧ (𝑃𝑇) ∥ 𝑁))
302, 25, 26, 29syl12anc 1364 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑇 ∈ ℕ0 ∧ (𝑃𝑇) ∥ 𝑁))
3130simpld 474 . . . . . . 7 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑇 ∈ ℕ0)
3224, 31nn0addcld 11393 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 + 𝑇) ∈ ℕ0)
33 prmnn 15435 . . . . . . . . . . 11 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
34333ad2ant1 1102 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑃 ∈ ℕ)
3534nncnd 11074 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑃 ∈ ℂ)
3635, 31, 24expaddd 13050 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑆 + 𝑇)) = ((𝑃𝑆) · (𝑃𝑇)))
3723simprd 478 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃𝑆) ∥ 𝑀)
3834, 24nnexpcld 13070 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃𝑆) ∈ ℕ)
3938nnzd 11519 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃𝑆) ∈ ℤ)
4034, 31nnexpcld 13070 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃𝑇) ∈ ℕ)
4140nnzd 11519 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃𝑇) ∈ ℤ)
42 dvdsmulc 15056 . . . . . . . . . 10 (((𝑃𝑆) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑃𝑇) ∈ ℤ) → ((𝑃𝑆) ∥ 𝑀 → ((𝑃𝑆) · (𝑃𝑇)) ∥ (𝑀 · (𝑃𝑇))))
4339, 18, 41, 42syl3anc 1366 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑃𝑆) ∥ 𝑀 → ((𝑃𝑆) · (𝑃𝑇)) ∥ (𝑀 · (𝑃𝑇))))
4437, 43mpd 15 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑃𝑆) · (𝑃𝑇)) ∥ (𝑀 · (𝑃𝑇)))
4536, 44eqbrtrd 4707 . . . . . . 7 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑆 + 𝑇)) ∥ (𝑀 · (𝑃𝑇)))
4630simprd 478 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃𝑇) ∥ 𝑁)
47 dvdscmul 15055 . . . . . . . . 9 (((𝑃𝑇) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑃𝑇) ∥ 𝑁 → (𝑀 · (𝑃𝑇)) ∥ (𝑀 · 𝑁)))
4841, 25, 18, 47syl3anc 1366 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑃𝑇) ∥ 𝑁 → (𝑀 · (𝑃𝑇)) ∥ (𝑀 · 𝑁)))
4946, 48mpd 15 . . . . . . 7 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑀 · (𝑃𝑇)) ∥ (𝑀 · 𝑁))
5034, 32nnexpcld 13070 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑆 + 𝑇)) ∈ ℕ)
5150nnzd 11519 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑆 + 𝑇)) ∈ ℤ)
5218, 41zmulcld 11526 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑀 · (𝑃𝑇)) ∈ ℤ)
53 dvdstr 15065 . . . . . . . 8 (((𝑃↑(𝑆 + 𝑇)) ∈ ℤ ∧ (𝑀 · (𝑃𝑇)) ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑃↑(𝑆 + 𝑇)) ∥ (𝑀 · (𝑃𝑇)) ∧ (𝑀 · (𝑃𝑇)) ∥ (𝑀 · 𝑁)) → (𝑃↑(𝑆 + 𝑇)) ∥ (𝑀 · 𝑁)))
5451, 52, 5, 53syl3anc 1366 . . . . . . 7 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (((𝑃↑(𝑆 + 𝑇)) ∥ (𝑀 · (𝑃𝑇)) ∧ (𝑀 · (𝑃𝑇)) ∥ (𝑀 · 𝑁)) → (𝑃↑(𝑆 + 𝑇)) ∥ (𝑀 · 𝑁)))
5545, 49, 54mp2and 715 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑆 + 𝑇)) ∥ (𝑀 · 𝑁))
56 oveq2 6698 . . . . . . . 8 (𝑥 = (𝑆 + 𝑇) → (𝑃𝑥) = (𝑃↑(𝑆 + 𝑇)))
5756breq1d 4695 . . . . . . 7 (𝑥 = (𝑆 + 𝑇) → ((𝑃𝑥) ∥ (𝑀 · 𝑁) ↔ (𝑃↑(𝑆 + 𝑇)) ∥ (𝑀 · 𝑁)))
5857elrab 3396 . . . . . 6 ((𝑆 + 𝑇) ∈ {𝑥 ∈ ℕ0 ∣ (𝑃𝑥) ∥ (𝑀 · 𝑁)} ↔ ((𝑆 + 𝑇) ∈ ℕ0 ∧ (𝑃↑(𝑆 + 𝑇)) ∥ (𝑀 · 𝑁)))
5932, 55, 58sylanbrc 699 . . . . 5 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 + 𝑇) ∈ {𝑥 ∈ ℕ0 ∣ (𝑃𝑥) ∥ (𝑀 · 𝑁)})
60 oveq2 6698 . . . . . . 7 (𝑥 = 𝑛 → (𝑃𝑥) = (𝑃𝑛))
6160breq1d 4695 . . . . . 6 (𝑥 = 𝑛 → ((𝑃𝑥) ∥ (𝑀 · 𝑁) ↔ (𝑃𝑛) ∥ (𝑀 · 𝑁)))
6261cbvrabv 3230 . . . . 5 {𝑥 ∈ ℕ0 ∣ (𝑃𝑥) ∥ (𝑀 · 𝑁)} = {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)}
6359, 62syl6eleq 2740 . . . 4 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 + 𝑇) ∈ {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)})
64 suprzub 11817 . . . 4 (({𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)} ⊆ ℤ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)}𝑦𝑥 ∧ (𝑆 + 𝑇) ∈ {𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)}) → (𝑆 + 𝑇) ≤ sup({𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)}, ℝ, < ))
6516, 17, 63, 64syl3anc 1366 . . 3 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 + 𝑇) ≤ sup({𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)}, ℝ, < ))
66 pcpremul.3 . . 3 𝑈 = sup({𝑛 ∈ ℕ0 ∣ (𝑃𝑛) ∥ (𝑀 · 𝑁)}, ℝ, < )
6765, 66syl6breqr 4727 . 2 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 + 𝑇) ≤ 𝑈)
6820, 21pcprendvds2 15593 . . . . . 6 ((𝑃 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ¬ 𝑃 ∥ (𝑀 / (𝑃𝑆)))
692, 18, 19, 68syl12anc 1364 . . . . 5 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ 𝑃 ∥ (𝑀 / (𝑃𝑆)))
7027, 28pcprendvds2 15593 . . . . . 6 ((𝑃 ∈ (ℤ‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ 𝑃 ∥ (𝑁 / (𝑃𝑇)))
712, 25, 26, 70syl12anc 1364 . . . . 5 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ 𝑃 ∥ (𝑁 / (𝑃𝑇)))
72 ioran 510 . . . . 5 (¬ (𝑃 ∥ (𝑀 / (𝑃𝑆)) ∨ 𝑃 ∥ (𝑁 / (𝑃𝑇))) ↔ (¬ 𝑃 ∥ (𝑀 / (𝑃𝑆)) ∧ ¬ 𝑃 ∥ (𝑁 / (𝑃𝑇))))
7369, 71, 72sylanbrc 699 . . . 4 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃 ∥ (𝑀 / (𝑃𝑆)) ∨ 𝑃 ∥ (𝑁 / (𝑃𝑇))))
74 simp1 1081 . . . . 5 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑃 ∈ ℙ)
7538nnne0d 11103 . . . . . . 7 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃𝑆) ≠ 0)
76 dvdsval2 15030 . . . . . . 7 (((𝑃𝑆) ∈ ℤ ∧ (𝑃𝑆) ≠ 0 ∧ 𝑀 ∈ ℤ) → ((𝑃𝑆) ∥ 𝑀 ↔ (𝑀 / (𝑃𝑆)) ∈ ℤ))
7739, 75, 18, 76syl3anc 1366 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑃𝑆) ∥ 𝑀 ↔ (𝑀 / (𝑃𝑆)) ∈ ℤ))
7837, 77mpbid 222 . . . . 5 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑀 / (𝑃𝑆)) ∈ ℤ)
7940nnne0d 11103 . . . . . . 7 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃𝑇) ≠ 0)
80 dvdsval2 15030 . . . . . . 7 (((𝑃𝑇) ∈ ℤ ∧ (𝑃𝑇) ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑃𝑇) ∥ 𝑁 ↔ (𝑁 / (𝑃𝑇)) ∈ ℤ))
8141, 79, 25, 80syl3anc 1366 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑃𝑇) ∥ 𝑁 ↔ (𝑁 / (𝑃𝑇)) ∈ ℤ))
8246, 81mpbid 222 . . . . 5 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑁 / (𝑃𝑇)) ∈ ℤ)
83 euclemma 15472 . . . . 5 ((𝑃 ∈ ℙ ∧ (𝑀 / (𝑃𝑆)) ∈ ℤ ∧ (𝑁 / (𝑃𝑇)) ∈ ℤ) → (𝑃 ∥ ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇))) ↔ (𝑃 ∥ (𝑀 / (𝑃𝑆)) ∨ 𝑃 ∥ (𝑁 / (𝑃𝑇)))))
8474, 78, 82, 83syl3anc 1366 . . . 4 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 ∥ ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇))) ↔ (𝑃 ∥ (𝑀 / (𝑃𝑆)) ∨ 𝑃 ∥ (𝑁 / (𝑃𝑇)))))
8573, 84mtbird 314 . . 3 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ 𝑃 ∥ ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇))))
8613, 66pcprecl 15591 . . . . . . 7 ((𝑃 ∈ (ℤ‘2) ∧ ((𝑀 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ≠ 0)) → (𝑈 ∈ ℕ0 ∧ (𝑃𝑈) ∥ (𝑀 · 𝑁)))
872, 5, 12, 86syl12anc 1364 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑈 ∈ ℕ0 ∧ (𝑃𝑈) ∥ (𝑀 · 𝑁)))
8887simpld 474 . . . . 5 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑈 ∈ ℕ0)
89 nn0ltp1le 11473 . . . . 5 (((𝑆 + 𝑇) ∈ ℕ0𝑈 ∈ ℕ0) → ((𝑆 + 𝑇) < 𝑈 ↔ ((𝑆 + 𝑇) + 1) ≤ 𝑈))
9032, 88, 89syl2anc 694 . . . 4 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑆 + 𝑇) < 𝑈 ↔ ((𝑆 + 𝑇) + 1) ≤ 𝑈))
9134nnzd 11519 . . . . . . 7 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑃 ∈ ℤ)
92 peano2nn0 11371 . . . . . . . 8 ((𝑆 + 𝑇) ∈ ℕ0 → ((𝑆 + 𝑇) + 1) ∈ ℕ0)
9332, 92syl 17 . . . . . . 7 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑆 + 𝑇) + 1) ∈ ℕ0)
94 dvdsexp 15096 . . . . . . . 8 ((𝑃 ∈ ℤ ∧ ((𝑆 + 𝑇) + 1) ∈ ℕ0𝑈 ∈ (ℤ‘((𝑆 + 𝑇) + 1))) → (𝑃↑((𝑆 + 𝑇) + 1)) ∥ (𝑃𝑈))
95943expia 1286 . . . . . . 7 ((𝑃 ∈ ℤ ∧ ((𝑆 + 𝑇) + 1) ∈ ℕ0) → (𝑈 ∈ (ℤ‘((𝑆 + 𝑇) + 1)) → (𝑃↑((𝑆 + 𝑇) + 1)) ∥ (𝑃𝑈)))
9691, 93, 95syl2anc 694 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑈 ∈ (ℤ‘((𝑆 + 𝑇) + 1)) → (𝑃↑((𝑆 + 𝑇) + 1)) ∥ (𝑃𝑈)))
9787simprd 478 . . . . . . 7 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃𝑈) ∥ (𝑀 · 𝑁))
9834, 93nnexpcld 13070 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑((𝑆 + 𝑇) + 1)) ∈ ℕ)
9998nnzd 11519 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑((𝑆 + 𝑇) + 1)) ∈ ℤ)
10034, 88nnexpcld 13070 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃𝑈) ∈ ℕ)
101100nnzd 11519 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃𝑈) ∈ ℤ)
102 dvdstr 15065 . . . . . . . 8 (((𝑃↑((𝑆 + 𝑇) + 1)) ∈ ℤ ∧ (𝑃𝑈) ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑃↑((𝑆 + 𝑇) + 1)) ∥ (𝑃𝑈) ∧ (𝑃𝑈) ∥ (𝑀 · 𝑁)) → (𝑃↑((𝑆 + 𝑇) + 1)) ∥ (𝑀 · 𝑁)))
10399, 101, 5, 102syl3anc 1366 . . . . . . 7 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (((𝑃↑((𝑆 + 𝑇) + 1)) ∥ (𝑃𝑈) ∧ (𝑃𝑈) ∥ (𝑀 · 𝑁)) → (𝑃↑((𝑆 + 𝑇) + 1)) ∥ (𝑀 · 𝑁)))
10497, 103mpan2d 710 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑃↑((𝑆 + 𝑇) + 1)) ∥ (𝑃𝑈) → (𝑃↑((𝑆 + 𝑇) + 1)) ∥ (𝑀 · 𝑁)))
10596, 104syld 47 . . . . 5 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑈 ∈ (ℤ‘((𝑆 + 𝑇) + 1)) → (𝑃↑((𝑆 + 𝑇) + 1)) ∥ (𝑀 · 𝑁)))
10693nn0zd 11518 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑆 + 𝑇) + 1) ∈ ℤ)
10788nn0zd 11518 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑈 ∈ ℤ)
108 eluz 11739 . . . . . 6 ((((𝑆 + 𝑇) + 1) ∈ ℤ ∧ 𝑈 ∈ ℤ) → (𝑈 ∈ (ℤ‘((𝑆 + 𝑇) + 1)) ↔ ((𝑆 + 𝑇) + 1) ≤ 𝑈))
109106, 107, 108syl2anc 694 . . . . 5 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑈 ∈ (ℤ‘((𝑆 + 𝑇) + 1)) ↔ ((𝑆 + 𝑇) + 1) ≤ 𝑈))
11035, 32expp1d 13049 . . . . . . 7 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑((𝑆 + 𝑇) + 1)) = ((𝑃↑(𝑆 + 𝑇)) · 𝑃))
11118zcnd 11521 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑀 ∈ ℂ)
11225zcnd 11521 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑁 ∈ ℂ)
113111, 112mulcld 10098 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) ∈ ℂ)
11450nncnd 11074 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑆 + 𝑇)) ∈ ℂ)
11550nnne0d 11103 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑆 + 𝑇)) ≠ 0)
116113, 114, 115divcan2d 10841 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑃↑(𝑆 + 𝑇)) · ((𝑀 · 𝑁) / (𝑃↑(𝑆 + 𝑇)))) = (𝑀 · 𝑁))
11736oveq2d 6706 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑀 · 𝑁) / (𝑃↑(𝑆 + 𝑇))) = ((𝑀 · 𝑁) / ((𝑃𝑆) · (𝑃𝑇))))
11838nncnd 11074 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃𝑆) ∈ ℂ)
11940nncnd 11074 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃𝑇) ∈ ℂ)
120111, 118, 112, 119, 75, 79divmuldivd 10880 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇))) = ((𝑀 · 𝑁) / ((𝑃𝑆) · (𝑃𝑇))))
121117, 120eqtr4d 2688 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑀 · 𝑁) / (𝑃↑(𝑆 + 𝑇))) = ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇))))
122121oveq2d 6706 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑃↑(𝑆 + 𝑇)) · ((𝑀 · 𝑁) / (𝑃↑(𝑆 + 𝑇)))) = ((𝑃↑(𝑆 + 𝑇)) · ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇)))))
123116, 122eqtr3d 2687 . . . . . . 7 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) = ((𝑃↑(𝑆 + 𝑇)) · ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇)))))
124110, 123breq12d 4698 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑃↑((𝑆 + 𝑇) + 1)) ∥ (𝑀 · 𝑁) ↔ ((𝑃↑(𝑆 + 𝑇)) · 𝑃) ∥ ((𝑃↑(𝑆 + 𝑇)) · ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇))))))
12578, 82zmulcld 11526 . . . . . . 7 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇))) ∈ ℤ)
126 dvdscmulr 15057 . . . . . . 7 ((𝑃 ∈ ℤ ∧ ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇))) ∈ ℤ ∧ ((𝑃↑(𝑆 + 𝑇)) ∈ ℤ ∧ (𝑃↑(𝑆 + 𝑇)) ≠ 0)) → (((𝑃↑(𝑆 + 𝑇)) · 𝑃) ∥ ((𝑃↑(𝑆 + 𝑇)) · ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇)))) ↔ 𝑃 ∥ ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇)))))
12791, 125, 51, 115, 126syl112anc 1370 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (((𝑃↑(𝑆 + 𝑇)) · 𝑃) ∥ ((𝑃↑(𝑆 + 𝑇)) · ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇)))) ↔ 𝑃 ∥ ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇)))))
128124, 127bitrd 268 . . . . 5 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑃↑((𝑆 + 𝑇) + 1)) ∥ (𝑀 · 𝑁) ↔ 𝑃 ∥ ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇)))))
129105, 109, 1283imtr3d 282 . . . 4 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (((𝑆 + 𝑇) + 1) ≤ 𝑈𝑃 ∥ ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇)))))
13090, 129sylbid 230 . . 3 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑆 + 𝑇) < 𝑈𝑃 ∥ ((𝑀 / (𝑃𝑆)) · (𝑁 / (𝑃𝑇)))))
13185, 130mtod 189 . 2 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑆 + 𝑇) < 𝑈)
13232nn0red 11390 . . 3 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 + 𝑇) ∈ ℝ)
13388nn0red 11390 . . 3 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑈 ∈ ℝ)
134132, 133eqleltd 10219 . 2 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑆 + 𝑇) = 𝑈 ↔ ((𝑆 + 𝑇) ≤ 𝑈 ∧ ¬ (𝑆 + 𝑇) < 𝑈)))
13567, 131, 134mpbir2and 977 1 ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 + 𝑇) = 𝑈)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  {crab 2945  wss 3607  c0 3948   class class class wbr 4685  cfv 5926  (class class class)co 6690  supcsup 8387  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112  cle 10113   / cdiv 10722  cn 11058  2c2 11108  0cn0 11330  cz 11415  cuz 11725  cexp 12900  cdvds 15027  cprime 15432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-dvds 15028  df-gcd 15264  df-prm 15433
This theorem is referenced by:  pceulem  15597  pcmul  15603
  Copyright terms: Public domain W3C validator