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

Theorem pcadd 15795
Description: An inequality for the prime count of a sum. This is the source of the ultrametric inequality for the p-adic metric. (Contributed by Mario Carneiro, 9-Sep-2014.)
Hypotheses
Ref Expression
pcadd.1 (𝜑𝑃 ∈ ℙ)
pcadd.2 (𝜑𝐴 ∈ ℚ)
pcadd.3 (𝜑𝐵 ∈ ℚ)
pcadd.4 (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵))
Assertion
Ref Expression
pcadd (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵)))

Proof of Theorem pcadd
Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pcadd.2 . . 3 (𝜑𝐴 ∈ ℚ)
2 elq 11983 . . 3 (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
31, 2sylib 208 . 2 (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
4 pcadd.3 . . 3 (𝜑𝐵 ∈ ℚ)
5 elq 11983 . . 3 (𝐵 ∈ ℚ ↔ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤))
64, 5sylib 208 . 2 (𝜑 → ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤))
7 pcadd.1 . . . . . . . 8 (𝜑𝑃 ∈ ℙ)
8 pcxcl 15767 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt 𝐴) ∈ ℝ*)
97, 1, 8syl2anc 696 . . . . . . 7 (𝜑 → (𝑃 pCnt 𝐴) ∈ ℝ*)
10 xrleid 12176 . . . . . . 7 ((𝑃 pCnt 𝐴) ∈ ℝ* → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐴))
119, 10syl 17 . . . . . 6 (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐴))
1211adantr 472 . . . . 5 ((𝜑𝐵 = 0) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐴))
13 oveq2 6821 . . . . . . 7 (𝐵 = 0 → (𝐴 + 𝐵) = (𝐴 + 0))
14 qcn 11995 . . . . . . . . 9 (𝐴 ∈ ℚ → 𝐴 ∈ ℂ)
151, 14syl 17 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
1615addid1d 10428 . . . . . . 7 (𝜑 → (𝐴 + 0) = 𝐴)
1713, 16sylan9eqr 2816 . . . . . 6 ((𝜑𝐵 = 0) → (𝐴 + 𝐵) = 𝐴)
1817oveq2d 6829 . . . . 5 ((𝜑𝐵 = 0) → (𝑃 pCnt (𝐴 + 𝐵)) = (𝑃 pCnt 𝐴))
1912, 18breqtrrd 4832 . . . 4 ((𝜑𝐵 = 0) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵)))
2019a1d 25 . . 3 ((𝜑𝐵 = 0) → ((∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))))
21 reeanv 3245 . . . 4 (∃𝑥 ∈ ℤ ∃𝑧 ∈ ℤ (∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) ↔ (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)))
22 reeanv 3245 . . . . . 6 (∃𝑦 ∈ ℕ ∃𝑤 ∈ ℕ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) ↔ (∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)))
237ad3antrrr 768 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑃 ∈ ℙ)
24 prmnn 15590 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2523, 24syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑃 ∈ ℕ)
26 simplrl 819 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑥 ∈ ℤ)
27 simprrl 823 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐴 = (𝑥 / 𝑦))
284ad3antrrr 768 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐵 ∈ ℚ)
29 simpllr 817 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐵 ≠ 0)
30 pcqcl 15763 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃 ∈ ℙ ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt 𝐵) ∈ ℤ)
3123, 28, 29, 30syl12anc 1475 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐵) ∈ ℤ)
3231zred 11674 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐵) ∈ ℝ)
33 ltpnf 12147 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 pCnt 𝐵) ∈ ℝ → (𝑃 pCnt 𝐵) < +∞)
34 rexr 10277 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃 pCnt 𝐵) ∈ ℝ → (𝑃 pCnt 𝐵) ∈ ℝ*)
35 pnfxr 10284 . . . . . . . . . . . . . . . . . . . . . . . 24 +∞ ∈ ℝ*
36 xrltnle 10297 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑃 pCnt 𝐵) ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝑃 pCnt 𝐵) < +∞ ↔ ¬ +∞ ≤ (𝑃 pCnt 𝐵)))
3734, 35, 36sylancl 697 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 pCnt 𝐵) ∈ ℝ → ((𝑃 pCnt 𝐵) < +∞ ↔ ¬ +∞ ≤ (𝑃 pCnt 𝐵)))
3833, 37mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 pCnt 𝐵) ∈ ℝ → ¬ +∞ ≤ (𝑃 pCnt 𝐵))
3932, 38syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ¬ +∞ ≤ (𝑃 pCnt 𝐵))
40 pc0 15761 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ ℙ → (𝑃 pCnt 0) = +∞)
4123, 40syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 0) = +∞)
4241breq1d 4814 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃 pCnt 0) ≤ (𝑃 pCnt 𝐵) ↔ +∞ ≤ (𝑃 pCnt 𝐵)))
4339, 42mtbird 314 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ¬ (𝑃 pCnt 0) ≤ (𝑃 pCnt 𝐵))
44 pcadd.4 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵))
4544ad3antrrr 768 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵))
46 oveq2 6821 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 = 0 → (𝑃 pCnt 𝐴) = (𝑃 pCnt 0))
4746breq1d 4814 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 = 0 → ((𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵) ↔ (𝑃 pCnt 0) ≤ (𝑃 pCnt 𝐵)))
4845, 47syl5ibcom 235 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝐴 = 0 → (𝑃 pCnt 0) ≤ (𝑃 pCnt 𝐵)))
4948necon3bd 2946 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (¬ (𝑃 pCnt 0) ≤ (𝑃 pCnt 𝐵) → 𝐴 ≠ 0))
5043, 49mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐴 ≠ 0)
5127, 50eqnetrrd 3000 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑥 / 𝑦) ≠ 0)
52 simprll 821 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑦 ∈ ℕ)
5352nncnd 11228 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑦 ∈ ℂ)
5452nnne0d 11257 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑦 ≠ 0)
5553, 54div0d 10992 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (0 / 𝑦) = 0)
56 oveq1 6820 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 0 → (𝑥 / 𝑦) = (0 / 𝑦))
5756eqeq1d 2762 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 0 → ((𝑥 / 𝑦) = 0 ↔ (0 / 𝑦) = 0))
5855, 57syl5ibrcom 237 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑥 = 0 → (𝑥 / 𝑦) = 0))
5958necon3d 2953 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑥 / 𝑦) ≠ 0 → 𝑥 ≠ 0))
6051, 59mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑥 ≠ 0)
61 pczcl 15755 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈ ℕ0)
6223, 26, 60, 61syl12anc 1475 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑥) ∈ ℕ0)
6325, 62nnexpcld 13224 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑥)) ∈ ℕ)
6463nncnd 11228 . . . . . . . . . . . . . 14 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑥)) ∈ ℂ)
6564, 53mulcomd 10253 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝑥)) · 𝑦) = (𝑦 · (𝑃↑(𝑃 pCnt 𝑥))))
6665oveq2d 6829 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑥 · (𝑃↑(𝑃 pCnt 𝑦))) / ((𝑃↑(𝑃 pCnt 𝑥)) · 𝑦)) = ((𝑥 · (𝑃↑(𝑃 pCnt 𝑦))) / (𝑦 · (𝑃↑(𝑃 pCnt 𝑥)))))
6726zcnd 11675 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑥 ∈ ℂ)
6823, 52pccld 15757 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑦) ∈ ℕ0)
6925, 68nnexpcld 13224 . . . . . . . . . . . . . 14 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑦)) ∈ ℕ)
7069nncnd 11228 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑦)) ∈ ℂ)
7163nnne0d 11257 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑥)) ≠ 0)
7269nnne0d 11257 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑦)) ≠ 0)
7367, 64, 53, 70, 71, 72, 54divdivdivd 11040 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) / (𝑦 / (𝑃↑(𝑃 pCnt 𝑦)))) = ((𝑥 · (𝑃↑(𝑃 pCnt 𝑦))) / ((𝑃↑(𝑃 pCnt 𝑥)) · 𝑦)))
7427oveq2d 6829 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐴) = (𝑃 pCnt (𝑥 / 𝑦)))
75 pcdiv 15759 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦)))
7623, 26, 60, 52, 75syl121anc 1482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦)))
7774, 76eqtrd 2794 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐴) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦)))
7877oveq2d 6829 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐴)) = (𝑃↑((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦))))
7925nncnd 11228 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑃 ∈ ℂ)
8025nnne0d 11257 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑃 ≠ 0)
8168nn0zd 11672 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑦) ∈ ℤ)
8262nn0zd 11672 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑥) ∈ ℤ)
8379, 80, 81, 82expsubd 13213 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦))) = ((𝑃↑(𝑃 pCnt 𝑥)) / (𝑃↑(𝑃 pCnt 𝑦))))
8478, 83eqtrd 2794 . . . . . . . . . . . . . 14 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐴)) = ((𝑃↑(𝑃 pCnt 𝑥)) / (𝑃↑(𝑃 pCnt 𝑦))))
8584oveq2d 6829 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) = (𝐴 / ((𝑃↑(𝑃 pCnt 𝑥)) / (𝑃↑(𝑃 pCnt 𝑦)))))
8627oveq1d 6828 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝐴 / ((𝑃↑(𝑃 pCnt 𝑥)) / (𝑃↑(𝑃 pCnt 𝑦)))) = ((𝑥 / 𝑦) / ((𝑃↑(𝑃 pCnt 𝑥)) / (𝑃↑(𝑃 pCnt 𝑦)))))
8767, 53, 64, 70, 54, 72, 71divdivdivd 11040 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑥 / 𝑦) / ((𝑃↑(𝑃 pCnt 𝑥)) / (𝑃↑(𝑃 pCnt 𝑦)))) = ((𝑥 · (𝑃↑(𝑃 pCnt 𝑦))) / (𝑦 · (𝑃↑(𝑃 pCnt 𝑥)))))
8885, 86, 873eqtrd 2798 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) = ((𝑥 · (𝑃↑(𝑃 pCnt 𝑦))) / (𝑦 · (𝑃↑(𝑃 pCnt 𝑥)))))
8966, 73, 883eqtr4d 2804 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) / (𝑦 / (𝑃↑(𝑃 pCnt 𝑦)))) = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))
9089oveq2d 6829 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝐴)) · ((𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) / (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))))) = ((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))
911ad3antrrr 768 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐴 ∈ ℚ)
9291, 14syl 17 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐴 ∈ ℂ)
93 pcqcl 15763 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt 𝐴) ∈ ℤ)
9423, 91, 50, 93syl12anc 1475 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐴) ∈ ℤ)
9579, 80, 94expclzd 13207 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℂ)
9679, 80, 94expne0d 13208 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐴)) ≠ 0)
9792, 95, 96divcan2d 10995 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 𝐴)
9890, 97eqtr2d 2795 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐴 = ((𝑃↑(𝑃 pCnt 𝐴)) · ((𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) / (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))))))
99 simplrr 820 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑧 ∈ ℤ)
100 simprrr 824 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐵 = (𝑧 / 𝑤))
101100, 29eqnetrrd 3000 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑧 / 𝑤) ≠ 0)
102 simprlr 822 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑤 ∈ ℕ)
103102nncnd 11228 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑤 ∈ ℂ)
104102nnne0d 11257 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑤 ≠ 0)
105103, 104div0d 10992 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (0 / 𝑤) = 0)
106 oveq1 6820 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 0 → (𝑧 / 𝑤) = (0 / 𝑤))
107106eqeq1d 2762 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 0 → ((𝑧 / 𝑤) = 0 ↔ (0 / 𝑤) = 0))
108105, 107syl5ibrcom 237 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑧 = 0 → (𝑧 / 𝑤) = 0))
109108necon3d 2953 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑧 / 𝑤) ≠ 0 → 𝑧 ≠ 0))
110101, 109mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑧 ≠ 0)
111 pczcl 15755 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑧) ∈ ℕ0)
11223, 99, 110, 111syl12anc 1475 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑧) ∈ ℕ0)
11325, 112nnexpcld 13224 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑧)) ∈ ℕ)
114113nncnd 11228 . . . . . . . . . . . . . 14 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑧)) ∈ ℂ)
115114, 103mulcomd 10253 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝑧)) · 𝑤) = (𝑤 · (𝑃↑(𝑃 pCnt 𝑧))))
116115oveq2d 6829 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑧 · (𝑃↑(𝑃 pCnt 𝑤))) / ((𝑃↑(𝑃 pCnt 𝑧)) · 𝑤)) = ((𝑧 · (𝑃↑(𝑃 pCnt 𝑤))) / (𝑤 · (𝑃↑(𝑃 pCnt 𝑧)))))
11799zcnd 11675 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑧 ∈ ℂ)
11823, 102pccld 15757 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑤) ∈ ℕ0)
11925, 118nnexpcld 13224 . . . . . . . . . . . . . 14 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑤)) ∈ ℕ)
120119nncnd 11228 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑤)) ∈ ℂ)
121113nnne0d 11257 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑧)) ≠ 0)
122119nnne0d 11257 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑤)) ≠ 0)
123117, 114, 103, 120, 121, 122, 104divdivdivd 11040 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) / (𝑤 / (𝑃↑(𝑃 pCnt 𝑤)))) = ((𝑧 · (𝑃↑(𝑃 pCnt 𝑤))) / ((𝑃↑(𝑃 pCnt 𝑧)) · 𝑤)))
124100oveq2d 6829 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐵) = (𝑃 pCnt (𝑧 / 𝑤)))
125 pcdiv 15759 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑧 ≠ 0) ∧ 𝑤 ∈ ℕ) → (𝑃 pCnt (𝑧 / 𝑤)) = ((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤)))
12623, 99, 110, 102, 125syl121anc 1482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt (𝑧 / 𝑤)) = ((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤)))
127124, 126eqtrd 2794 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐵) = ((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤)))
128127oveq2d 6829 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐵)) = (𝑃↑((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤))))
129118nn0zd 11672 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑤) ∈ ℤ)
130112nn0zd 11672 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑧) ∈ ℤ)
13179, 80, 129, 130expsubd 13213 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤))) = ((𝑃↑(𝑃 pCnt 𝑧)) / (𝑃↑(𝑃 pCnt 𝑤))))
132128, 131eqtrd 2794 . . . . . . . . . . . . . 14 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐵)) = ((𝑃↑(𝑃 pCnt 𝑧)) / (𝑃↑(𝑃 pCnt 𝑤))))
133132oveq2d 6829 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝐵 / (𝑃↑(𝑃 pCnt 𝐵))) = (𝐵 / ((𝑃↑(𝑃 pCnt 𝑧)) / (𝑃↑(𝑃 pCnt 𝑤)))))
134100oveq1d 6828 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝐵 / ((𝑃↑(𝑃 pCnt 𝑧)) / (𝑃↑(𝑃 pCnt 𝑤)))) = ((𝑧 / 𝑤) / ((𝑃↑(𝑃 pCnt 𝑧)) / (𝑃↑(𝑃 pCnt 𝑤)))))
135117, 103, 114, 120, 104, 122, 121divdivdivd 11040 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑧 / 𝑤) / ((𝑃↑(𝑃 pCnt 𝑧)) / (𝑃↑(𝑃 pCnt 𝑤)))) = ((𝑧 · (𝑃↑(𝑃 pCnt 𝑤))) / (𝑤 · (𝑃↑(𝑃 pCnt 𝑧)))))
136133, 134, 1353eqtrd 2798 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝐵 / (𝑃↑(𝑃 pCnt 𝐵))) = ((𝑧 · (𝑃↑(𝑃 pCnt 𝑤))) / (𝑤 · (𝑃↑(𝑃 pCnt 𝑧)))))
137116, 123, 1363eqtr4d 2804 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) / (𝑤 / (𝑃↑(𝑃 pCnt 𝑤)))) = (𝐵 / (𝑃↑(𝑃 pCnt 𝐵))))
138137oveq2d 6829 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝐵)) · ((𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) / (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))))) = ((𝑃↑(𝑃 pCnt 𝐵)) · (𝐵 / (𝑃↑(𝑃 pCnt 𝐵)))))
139 qcn 11995 . . . . . . . . . . . 12 (𝐵 ∈ ℚ → 𝐵 ∈ ℂ)
14028, 139syl 17 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐵 ∈ ℂ)
14179, 80, 31expclzd 13207 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐵)) ∈ ℂ)
14279, 80, 31expne0d 13208 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐵)) ≠ 0)
143140, 141, 142divcan2d 10995 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝐵)) · (𝐵 / (𝑃↑(𝑃 pCnt 𝐵)))) = 𝐵)
144138, 143eqtr2d 2795 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐵 = ((𝑃↑(𝑃 pCnt 𝐵)) · ((𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) / (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))))))
145 eluz 11893 . . . . . . . . . . 11 (((𝑃 pCnt 𝐴) ∈ ℤ ∧ (𝑃 pCnt 𝐵) ∈ ℤ) → ((𝑃 pCnt 𝐵) ∈ (ℤ‘(𝑃 pCnt 𝐴)) ↔ (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)))
14694, 31, 145syl2anc 696 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃 pCnt 𝐵) ∈ (ℤ‘(𝑃 pCnt 𝐴)) ↔ (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)))
14745, 146mpbird 247 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐵) ∈ (ℤ‘(𝑃 pCnt 𝐴)))
148 pczdvds 15769 . . . . . . . . . . . 12 ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑥)) ∥ 𝑥)
14923, 26, 60, 148syl12anc 1475 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑥)) ∥ 𝑥)
15063nnzd 11673 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑥)) ∈ ℤ)
151 dvdsval2 15185 . . . . . . . . . . . 12 (((𝑃↑(𝑃 pCnt 𝑥)) ∈ ℤ ∧ (𝑃↑(𝑃 pCnt 𝑥)) ≠ 0 ∧ 𝑥 ∈ ℤ) → ((𝑃↑(𝑃 pCnt 𝑥)) ∥ 𝑥 ↔ (𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) ∈ ℤ))
152150, 71, 26, 151syl3anc 1477 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝑥)) ∥ 𝑥 ↔ (𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) ∈ ℤ))
153149, 152mpbid 222 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) ∈ ℤ)
154 pczndvds2 15773 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → ¬ 𝑃 ∥ (𝑥 / (𝑃↑(𝑃 pCnt 𝑥))))
15523, 26, 60, 154syl12anc 1475 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ¬ 𝑃 ∥ (𝑥 / (𝑃↑(𝑃 pCnt 𝑥))))
156153, 155jca 555 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) ∈ ℤ ∧ ¬ 𝑃 ∥ (𝑥 / (𝑃↑(𝑃 pCnt 𝑥)))))
157 pcdvds 15770 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝑦)) ∥ 𝑦)
15823, 52, 157syl2anc 696 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑦)) ∥ 𝑦)
15969nnzd 11673 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑦)) ∈ ℤ)
16052nnzd 11673 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑦 ∈ ℤ)
161 dvdsval2 15185 . . . . . . . . . . . . 13 (((𝑃↑(𝑃 pCnt 𝑦)) ∈ ℤ ∧ (𝑃↑(𝑃 pCnt 𝑦)) ≠ 0 ∧ 𝑦 ∈ ℤ) → ((𝑃↑(𝑃 pCnt 𝑦)) ∥ 𝑦 ↔ (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))) ∈ ℤ))
162159, 72, 160, 161syl3anc 1477 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝑦)) ∥ 𝑦 ↔ (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))) ∈ ℤ))
163158, 162mpbid 222 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))) ∈ ℤ)
16452nnred 11227 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑦 ∈ ℝ)
16569nnred 11227 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑦)) ∈ ℝ)
16652nngt0d 11256 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 0 < 𝑦)
16769nngt0d 11256 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 0 < (𝑃↑(𝑃 pCnt 𝑦)))
168164, 165, 166, 167divgt0d 11151 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 0 < (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))))
169 elnnz 11579 . . . . . . . . . . 11 ((𝑦 / (𝑃↑(𝑃 pCnt 𝑦))) ∈ ℕ ↔ ((𝑦 / (𝑃↑(𝑃 pCnt 𝑦))) ∈ ℤ ∧ 0 < (𝑦 / (𝑃↑(𝑃 pCnt 𝑦)))))
170163, 168, 169sylanbrc 701 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))) ∈ ℕ)
171 pcndvds2 15774 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ∥ (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))))
17223, 52, 171syl2anc 696 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ¬ 𝑃 ∥ (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))))
173170, 172jca 555 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑦 / (𝑃↑(𝑃 pCnt 𝑦))) ∈ ℕ ∧ ¬ 𝑃 ∥ (𝑦 / (𝑃↑(𝑃 pCnt 𝑦)))))
174 pczdvds 15769 . . . . . . . . . . . 12 ((𝑃 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑧 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑧)) ∥ 𝑧)
17523, 99, 110, 174syl12anc 1475 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑧)) ∥ 𝑧)
176113nnzd 11673 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑧)) ∈ ℤ)
177 dvdsval2 15185 . . . . . . . . . . . 12 (((𝑃↑(𝑃 pCnt 𝑧)) ∈ ℤ ∧ (𝑃↑(𝑃 pCnt 𝑧)) ≠ 0 ∧ 𝑧 ∈ ℤ) → ((𝑃↑(𝑃 pCnt 𝑧)) ∥ 𝑧 ↔ (𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) ∈ ℤ))
178176, 121, 99, 177syl3anc 1477 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝑧)) ∥ 𝑧 ↔ (𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) ∈ ℤ))
179175, 178mpbid 222 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) ∈ ℤ)
180 pczndvds2 15773 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑧 ≠ 0)) → ¬ 𝑃 ∥ (𝑧 / (𝑃↑(𝑃 pCnt 𝑧))))
18123, 99, 110, 180syl12anc 1475 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ¬ 𝑃 ∥ (𝑧 / (𝑃↑(𝑃 pCnt 𝑧))))
182179, 181jca 555 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) ∈ ℤ ∧ ¬ 𝑃 ∥ (𝑧 / (𝑃↑(𝑃 pCnt 𝑧)))))
183 pcdvds 15770 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ 𝑤 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝑤)) ∥ 𝑤)
18423, 102, 183syl2anc 696 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑤)) ∥ 𝑤)
185119nnzd 11673 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑤)) ∈ ℤ)
186102nnzd 11673 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑤 ∈ ℤ)
187 dvdsval2 15185 . . . . . . . . . . . . 13 (((𝑃↑(𝑃 pCnt 𝑤)) ∈ ℤ ∧ (𝑃↑(𝑃 pCnt 𝑤)) ≠ 0 ∧ 𝑤 ∈ ℤ) → ((𝑃↑(𝑃 pCnt 𝑤)) ∥ 𝑤 ↔ (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))) ∈ ℤ))
188185, 122, 186, 187syl3anc 1477 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝑤)) ∥ 𝑤 ↔ (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))) ∈ ℤ))
189184, 188mpbid 222 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))) ∈ ℤ)
190102nnred 11227 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑤 ∈ ℝ)
191119nnred 11227 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑤)) ∈ ℝ)
192102nngt0d 11256 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 0 < 𝑤)
193119nngt0d 11256 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 0 < (𝑃↑(𝑃 pCnt 𝑤)))
194190, 191, 192, 193divgt0d 11151 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 0 < (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))))
195 elnnz 11579 . . . . . . . . . . 11 ((𝑤 / (𝑃↑(𝑃 pCnt 𝑤))) ∈ ℕ ↔ ((𝑤 / (𝑃↑(𝑃 pCnt 𝑤))) ∈ ℤ ∧ 0 < (𝑤 / (𝑃↑(𝑃 pCnt 𝑤)))))
196189, 194, 195sylanbrc 701 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))) ∈ ℕ)
197 pcndvds2 15774 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ 𝑤 ∈ ℕ) → ¬ 𝑃 ∥ (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))))
19823, 102, 197syl2anc 696 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ¬ 𝑃 ∥ (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))))
199196, 198jca 555 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑤 / (𝑃↑(𝑃 pCnt 𝑤))) ∈ ℕ ∧ ¬ 𝑃 ∥ (𝑤 / (𝑃↑(𝑃 pCnt 𝑤)))))
20023, 98, 144, 147, 156, 173, 182, 199pcaddlem 15794 . . . . . . . 8 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵)))
201200expr 644 . . . . . . 7 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ((𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))))
202201rexlimdvva 3176 . . . . . 6 (((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → (∃𝑦 ∈ ℕ ∃𝑤 ∈ ℕ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))))
20322, 202syl5bir 233 . . . . 5 (((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → ((∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))))
204203rexlimdvva 3176 . . . 4 ((𝜑𝐵 ≠ 0) → (∃𝑥 ∈ ℤ ∃𝑧 ∈ ℤ (∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))))
20521, 204syl5bir 233 . . 3 ((𝜑𝐵 ≠ 0) → ((∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))))
20620, 205pm2.61dane 3019 . 2 (𝜑 → ((∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))))
2073, 6, 206mp2and 717 1 (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1632  wcel 2139  wne 2932  wrex 3051   class class class wbr 4804  cfv 6049  (class class class)co 6813  cc 10126  cr 10127  0cc0 10128   + caddc 10131   · cmul 10133  +∞cpnf 10263  *cxr 10265   < clt 10266  cle 10267  cmin 10458   / cdiv 10876  cn 11212  0cn0 11484  cz 11569  cuz 11879  cq 11981  cexp 13054  cdvds 15182  cprime 15587   pCnt cpc 15743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-sup 8513  df-inf 8514  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-n0 11485  df-z 11570  df-uz 11880  df-q 11982  df-rp 12026  df-fl 12787  df-mod 12863  df-seq 12996  df-exp 13055  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-dvds 15183  df-gcd 15419  df-prm 15588  df-pc 15744
This theorem is referenced by:  pcadd2  15796  padicabv  25518
  Copyright terms: Public domain W3C validator