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

Theorem pcadd 16325
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 12432 . . 3 (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
31, 2sylib 221 . 2 (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
4 pcadd.3 . . 3 (𝜑𝐵 ∈ ℚ)
5 elq 12432 . . 3 (𝐵 ∈ ℚ ↔ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤))
64, 5sylib 221 . 2 (𝜑 → ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤))
7 pcadd.1 . . . . . . . 8 (𝜑𝑃 ∈ ℙ)
8 pcxcl 16297 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt 𝐴) ∈ ℝ*)
97, 1, 8syl2anc 587 . . . . . . 7 (𝜑 → (𝑃 pCnt 𝐴) ∈ ℝ*)
109xrleidd 12628 . . . . . 6 (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐴))
1110adantr 484 . . . . 5 ((𝜑𝐵 = 0) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐴))
12 oveq2 7178 . . . . . . 7 (𝐵 = 0 → (𝐴 + 𝐵) = (𝐴 + 0))
13 qcn 12445 . . . . . . . . 9 (𝐴 ∈ ℚ → 𝐴 ∈ ℂ)
141, 13syl 17 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
1514addid1d 10918 . . . . . . 7 (𝜑 → (𝐴 + 0) = 𝐴)
1612, 15sylan9eqr 2795 . . . . . 6 ((𝜑𝐵 = 0) → (𝐴 + 𝐵) = 𝐴)
1716oveq2d 7186 . . . . 5 ((𝜑𝐵 = 0) → (𝑃 pCnt (𝐴 + 𝐵)) = (𝑃 pCnt 𝐴))
1811, 17breqtrrd 5058 . . . 4 ((𝜑𝐵 = 0) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵)))
1918a1d 25 . . 3 ((𝜑𝐵 = 0) → ((∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))))
20 reeanv 3270 . . . 4 (∃𝑥 ∈ ℤ ∃𝑧 ∈ ℤ (∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) ↔ (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)))
21 reeanv 3270 . . . . . 6 (∃𝑦 ∈ ℕ ∃𝑤 ∈ ℕ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) ↔ (∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)))
227ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑃 ∈ ℙ)
23 prmnn 16115 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2422, 23syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑃 ∈ ℕ)
25 simplrl 777 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑥 ∈ ℤ)
26 simprrl 781 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐴 = (𝑥 / 𝑦))
27 pc0 16291 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℙ → (𝑃 pCnt 0) = +∞)
2822, 27syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 0) = +∞)
294ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐵 ∈ ℚ)
30 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐵 ≠ 0)
31 pcqcl 16293 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃 ∈ ℙ ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt 𝐵) ∈ ℤ)
3222, 29, 30, 31syl12anc 836 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐵) ∈ ℤ)
3332zred 12168 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐵) ∈ ℝ)
34 ltpnf 12598 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 pCnt 𝐵) ∈ ℝ → (𝑃 pCnt 𝐵) < +∞)
35 rexr 10765 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃 pCnt 𝐵) ∈ ℝ → (𝑃 pCnt 𝐵) ∈ ℝ*)
36 pnfxr 10773 . . . . . . . . . . . . . . . . . . . . . . . 24 +∞ ∈ ℝ*
37 xrltnle 10786 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑃 pCnt 𝐵) ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝑃 pCnt 𝐵) < +∞ ↔ ¬ +∞ ≤ (𝑃 pCnt 𝐵)))
3835, 36, 37sylancl 589 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 pCnt 𝐵) ∈ ℝ → ((𝑃 pCnt 𝐵) < +∞ ↔ ¬ +∞ ≤ (𝑃 pCnt 𝐵)))
3934, 38mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 pCnt 𝐵) ∈ ℝ → ¬ +∞ ≤ (𝑃 pCnt 𝐵))
4033, 39syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ¬ +∞ ≤ (𝑃 pCnt 𝐵))
4128, 40eqnbrtrd 5048 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ¬ (𝑃 pCnt 0) ≤ (𝑃 pCnt 𝐵))
42 pcadd.4 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵))
4342ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵))
44 oveq2 7178 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 = 0 → (𝑃 pCnt 𝐴) = (𝑃 pCnt 0))
4544breq1d 5040 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 = 0 → ((𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵) ↔ (𝑃 pCnt 0) ≤ (𝑃 pCnt 𝐵)))
4643, 45syl5ibcom 248 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝐴 = 0 → (𝑃 pCnt 0) ≤ (𝑃 pCnt 𝐵)))
4746necon3bd 2948 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (¬ (𝑃 pCnt 0) ≤ (𝑃 pCnt 𝐵) → 𝐴 ≠ 0))
4841, 47mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐴 ≠ 0)
4926, 48eqnetrrd 3002 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑥 / 𝑦) ≠ 0)
50 simprll 779 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑦 ∈ ℕ)
5150nncnd 11732 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑦 ∈ ℂ)
5250nnne0d 11766 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑦 ≠ 0)
5351, 52div0d 11493 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (0 / 𝑦) = 0)
54 oveq1 7177 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 0 → (𝑥 / 𝑦) = (0 / 𝑦))
5554eqeq1d 2740 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 0 → ((𝑥 / 𝑦) = 0 ↔ (0 / 𝑦) = 0))
5653, 55syl5ibrcom 250 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑥 = 0 → (𝑥 / 𝑦) = 0))
5756necon3d 2955 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑥 / 𝑦) ≠ 0 → 𝑥 ≠ 0))
5849, 57mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑥 ≠ 0)
59 pczcl 16285 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈ ℕ0)
6022, 25, 58, 59syl12anc 836 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑥) ∈ ℕ0)
6124, 60nnexpcld 13698 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑥)) ∈ ℕ)
6261nncnd 11732 . . . . . . . . . . . . . 14 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑥)) ∈ ℂ)
6362, 51mulcomd 10740 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝑥)) · 𝑦) = (𝑦 · (𝑃↑(𝑃 pCnt 𝑥))))
6463oveq2d 7186 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑥 · (𝑃↑(𝑃 pCnt 𝑦))) / ((𝑃↑(𝑃 pCnt 𝑥)) · 𝑦)) = ((𝑥 · (𝑃↑(𝑃 pCnt 𝑦))) / (𝑦 · (𝑃↑(𝑃 pCnt 𝑥)))))
6525zcnd 12169 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑥 ∈ ℂ)
6622, 50pccld 16287 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑦) ∈ ℕ0)
6724, 66nnexpcld 13698 . . . . . . . . . . . . . 14 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑦)) ∈ ℕ)
6867nncnd 11732 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑦)) ∈ ℂ)
6961nnne0d 11766 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑥)) ≠ 0)
7067nnne0d 11766 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑦)) ≠ 0)
7165, 62, 51, 68, 69, 70, 52divdivdivd 11541 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) / (𝑦 / (𝑃↑(𝑃 pCnt 𝑦)))) = ((𝑥 · (𝑃↑(𝑃 pCnt 𝑦))) / ((𝑃↑(𝑃 pCnt 𝑥)) · 𝑦)))
7226oveq2d 7186 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐴) = (𝑃 pCnt (𝑥 / 𝑦)))
73 pcdiv 16289 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦)))
7422, 25, 58, 50, 73syl121anc 1376 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦)))
7572, 74eqtrd 2773 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐴) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦)))
7675oveq2d 7186 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐴)) = (𝑃↑((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦))))
7724nncnd 11732 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑃 ∈ ℂ)
7824nnne0d 11766 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑃 ≠ 0)
7966nn0zd 12166 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑦) ∈ ℤ)
8060nn0zd 12166 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑥) ∈ ℤ)
8177, 78, 79, 80expsubd 13613 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦))) = ((𝑃↑(𝑃 pCnt 𝑥)) / (𝑃↑(𝑃 pCnt 𝑦))))
8276, 81eqtrd 2773 . . . . . . . . . . . . . 14 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐴)) = ((𝑃↑(𝑃 pCnt 𝑥)) / (𝑃↑(𝑃 pCnt 𝑦))))
8382oveq2d 7186 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) = (𝐴 / ((𝑃↑(𝑃 pCnt 𝑥)) / (𝑃↑(𝑃 pCnt 𝑦)))))
8426oveq1d 7185 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝐴 / ((𝑃↑(𝑃 pCnt 𝑥)) / (𝑃↑(𝑃 pCnt 𝑦)))) = ((𝑥 / 𝑦) / ((𝑃↑(𝑃 pCnt 𝑥)) / (𝑃↑(𝑃 pCnt 𝑦)))))
8565, 51, 62, 68, 52, 70, 69divdivdivd 11541 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑥 / 𝑦) / ((𝑃↑(𝑃 pCnt 𝑥)) / (𝑃↑(𝑃 pCnt 𝑦)))) = ((𝑥 · (𝑃↑(𝑃 pCnt 𝑦))) / (𝑦 · (𝑃↑(𝑃 pCnt 𝑥)))))
8683, 84, 853eqtrd 2777 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) = ((𝑥 · (𝑃↑(𝑃 pCnt 𝑦))) / (𝑦 · (𝑃↑(𝑃 pCnt 𝑥)))))
8764, 71, 863eqtr4d 2783 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) / (𝑦 / (𝑃↑(𝑃 pCnt 𝑦)))) = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))
8887oveq2d 7186 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝐴)) · ((𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) / (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))))) = ((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))
891ad3antrrr 730 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐴 ∈ ℚ)
9089, 13syl 17 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐴 ∈ ℂ)
91 pcqcl 16293 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt 𝐴) ∈ ℤ)
9222, 89, 48, 91syl12anc 836 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐴) ∈ ℤ)
9377, 78, 92expclzd 13607 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℂ)
9477, 78, 92expne0d 13608 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐴)) ≠ 0)
9590, 93, 94divcan2d 11496 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 𝐴)
9688, 95eqtr2d 2774 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐴 = ((𝑃↑(𝑃 pCnt 𝐴)) · ((𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) / (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))))))
97 simplrr 778 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑧 ∈ ℤ)
98 simprrr 782 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐵 = (𝑧 / 𝑤))
9998, 30eqnetrrd 3002 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑧 / 𝑤) ≠ 0)
100 simprlr 780 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑤 ∈ ℕ)
101100nncnd 11732 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑤 ∈ ℂ)
102100nnne0d 11766 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑤 ≠ 0)
103101, 102div0d 11493 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (0 / 𝑤) = 0)
104 oveq1 7177 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 0 → (𝑧 / 𝑤) = (0 / 𝑤))
105104eqeq1d 2740 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 0 → ((𝑧 / 𝑤) = 0 ↔ (0 / 𝑤) = 0))
106103, 105syl5ibrcom 250 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑧 = 0 → (𝑧 / 𝑤) = 0))
107106necon3d 2955 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑧 / 𝑤) ≠ 0 → 𝑧 ≠ 0))
10899, 107mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑧 ≠ 0)
109 pczcl 16285 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑧) ∈ ℕ0)
11022, 97, 108, 109syl12anc 836 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑧) ∈ ℕ0)
11124, 110nnexpcld 13698 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑧)) ∈ ℕ)
112111nncnd 11732 . . . . . . . . . . . . . 14 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑧)) ∈ ℂ)
113112, 101mulcomd 10740 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝑧)) · 𝑤) = (𝑤 · (𝑃↑(𝑃 pCnt 𝑧))))
114113oveq2d 7186 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑧 · (𝑃↑(𝑃 pCnt 𝑤))) / ((𝑃↑(𝑃 pCnt 𝑧)) · 𝑤)) = ((𝑧 · (𝑃↑(𝑃 pCnt 𝑤))) / (𝑤 · (𝑃↑(𝑃 pCnt 𝑧)))))
11597zcnd 12169 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑧 ∈ ℂ)
11622, 100pccld 16287 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑤) ∈ ℕ0)
11724, 116nnexpcld 13698 . . . . . . . . . . . . . 14 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑤)) ∈ ℕ)
118117nncnd 11732 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑤)) ∈ ℂ)
119111nnne0d 11766 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑧)) ≠ 0)
120117nnne0d 11766 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑤)) ≠ 0)
121115, 112, 101, 118, 119, 120, 102divdivdivd 11541 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) / (𝑤 / (𝑃↑(𝑃 pCnt 𝑤)))) = ((𝑧 · (𝑃↑(𝑃 pCnt 𝑤))) / ((𝑃↑(𝑃 pCnt 𝑧)) · 𝑤)))
12298oveq2d 7186 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐵) = (𝑃 pCnt (𝑧 / 𝑤)))
123 pcdiv 16289 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑧 ≠ 0) ∧ 𝑤 ∈ ℕ) → (𝑃 pCnt (𝑧 / 𝑤)) = ((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤)))
12422, 97, 108, 100, 123syl121anc 1376 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt (𝑧 / 𝑤)) = ((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤)))
125122, 124eqtrd 2773 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐵) = ((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤)))
126125oveq2d 7186 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐵)) = (𝑃↑((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤))))
127116nn0zd 12166 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑤) ∈ ℤ)
128110nn0zd 12166 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝑧) ∈ ℤ)
12977, 78, 127, 128expsubd 13613 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤))) = ((𝑃↑(𝑃 pCnt 𝑧)) / (𝑃↑(𝑃 pCnt 𝑤))))
130126, 129eqtrd 2773 . . . . . . . . . . . . . 14 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐵)) = ((𝑃↑(𝑃 pCnt 𝑧)) / (𝑃↑(𝑃 pCnt 𝑤))))
131130oveq2d 7186 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝐵 / (𝑃↑(𝑃 pCnt 𝐵))) = (𝐵 / ((𝑃↑(𝑃 pCnt 𝑧)) / (𝑃↑(𝑃 pCnt 𝑤)))))
13298oveq1d 7185 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝐵 / ((𝑃↑(𝑃 pCnt 𝑧)) / (𝑃↑(𝑃 pCnt 𝑤)))) = ((𝑧 / 𝑤) / ((𝑃↑(𝑃 pCnt 𝑧)) / (𝑃↑(𝑃 pCnt 𝑤)))))
133115, 101, 112, 118, 102, 120, 119divdivdivd 11541 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑧 / 𝑤) / ((𝑃↑(𝑃 pCnt 𝑧)) / (𝑃↑(𝑃 pCnt 𝑤)))) = ((𝑧 · (𝑃↑(𝑃 pCnt 𝑤))) / (𝑤 · (𝑃↑(𝑃 pCnt 𝑧)))))
134131, 132, 1333eqtrd 2777 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝐵 / (𝑃↑(𝑃 pCnt 𝐵))) = ((𝑧 · (𝑃↑(𝑃 pCnt 𝑤))) / (𝑤 · (𝑃↑(𝑃 pCnt 𝑧)))))
135114, 121, 1343eqtr4d 2783 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) / (𝑤 / (𝑃↑(𝑃 pCnt 𝑤)))) = (𝐵 / (𝑃↑(𝑃 pCnt 𝐵))))
136135oveq2d 7186 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝐵)) · ((𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) / (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))))) = ((𝑃↑(𝑃 pCnt 𝐵)) · (𝐵 / (𝑃↑(𝑃 pCnt 𝐵)))))
137 qcn 12445 . . . . . . . . . . . 12 (𝐵 ∈ ℚ → 𝐵 ∈ ℂ)
13829, 137syl 17 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐵 ∈ ℂ)
13977, 78, 32expclzd 13607 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐵)) ∈ ℂ)
14077, 78, 32expne0d 13608 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝐵)) ≠ 0)
141138, 139, 140divcan2d 11496 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝐵)) · (𝐵 / (𝑃↑(𝑃 pCnt 𝐵)))) = 𝐵)
142136, 141eqtr2d 2774 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝐵 = ((𝑃↑(𝑃 pCnt 𝐵)) · ((𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) / (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))))))
143 eluz 12338 . . . . . . . . . . 11 (((𝑃 pCnt 𝐴) ∈ ℤ ∧ (𝑃 pCnt 𝐵) ∈ ℤ) → ((𝑃 pCnt 𝐵) ∈ (ℤ‘(𝑃 pCnt 𝐴)) ↔ (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)))
14492, 32, 143syl2anc 587 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃 pCnt 𝐵) ∈ (ℤ‘(𝑃 pCnt 𝐴)) ↔ (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)))
14543, 144mpbird 260 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐵) ∈ (ℤ‘(𝑃 pCnt 𝐴)))
146 pczdvds 16299 . . . . . . . . . . . 12 ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑥)) ∥ 𝑥)
14722, 25, 58, 146syl12anc 836 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑥)) ∥ 𝑥)
14861nnzd 12167 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑥)) ∈ ℤ)
149 dvdsval2 15702 . . . . . . . . . . . 12 (((𝑃↑(𝑃 pCnt 𝑥)) ∈ ℤ ∧ (𝑃↑(𝑃 pCnt 𝑥)) ≠ 0 ∧ 𝑥 ∈ ℤ) → ((𝑃↑(𝑃 pCnt 𝑥)) ∥ 𝑥 ↔ (𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) ∈ ℤ))
150148, 69, 25, 149syl3anc 1372 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝑥)) ∥ 𝑥 ↔ (𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) ∈ ℤ))
151147, 150mpbid 235 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) ∈ ℤ)
152 pczndvds2 16303 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → ¬ 𝑃 ∥ (𝑥 / (𝑃↑(𝑃 pCnt 𝑥))))
15322, 25, 58, 152syl12anc 836 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ¬ 𝑃 ∥ (𝑥 / (𝑃↑(𝑃 pCnt 𝑥))))
154151, 153jca 515 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑥 / (𝑃↑(𝑃 pCnt 𝑥))) ∈ ℤ ∧ ¬ 𝑃 ∥ (𝑥 / (𝑃↑(𝑃 pCnt 𝑥)))))
155 pcdvds 16300 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝑦)) ∥ 𝑦)
15622, 50, 155syl2anc 587 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑦)) ∥ 𝑦)
15767nnzd 12167 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑦)) ∈ ℤ)
15850nnzd 12167 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑦 ∈ ℤ)
159 dvdsval2 15702 . . . . . . . . . . . . 13 (((𝑃↑(𝑃 pCnt 𝑦)) ∈ ℤ ∧ (𝑃↑(𝑃 pCnt 𝑦)) ≠ 0 ∧ 𝑦 ∈ ℤ) → ((𝑃↑(𝑃 pCnt 𝑦)) ∥ 𝑦 ↔ (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))) ∈ ℤ))
160157, 70, 158, 159syl3anc 1372 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝑦)) ∥ 𝑦 ↔ (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))) ∈ ℤ))
161156, 160mpbid 235 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))) ∈ ℤ)
16250nnred 11731 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑦 ∈ ℝ)
16367nnred 11731 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑦)) ∈ ℝ)
16450nngt0d 11765 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 0 < 𝑦)
16567nngt0d 11765 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 0 < (𝑃↑(𝑃 pCnt 𝑦)))
166162, 163, 164, 165divgt0d 11653 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 0 < (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))))
167 elnnz 12072 . . . . . . . . . . 11 ((𝑦 / (𝑃↑(𝑃 pCnt 𝑦))) ∈ ℕ ↔ ((𝑦 / (𝑃↑(𝑃 pCnt 𝑦))) ∈ ℤ ∧ 0 < (𝑦 / (𝑃↑(𝑃 pCnt 𝑦)))))
168161, 166, 167sylanbrc 586 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))) ∈ ℕ)
169 pcndvds2 16304 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ∥ (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))))
17022, 50, 169syl2anc 587 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ¬ 𝑃 ∥ (𝑦 / (𝑃↑(𝑃 pCnt 𝑦))))
171168, 170jca 515 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑦 / (𝑃↑(𝑃 pCnt 𝑦))) ∈ ℕ ∧ ¬ 𝑃 ∥ (𝑦 / (𝑃↑(𝑃 pCnt 𝑦)))))
172 pczdvds 16299 . . . . . . . . . . . 12 ((𝑃 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑧 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑧)) ∥ 𝑧)
17322, 97, 108, 172syl12anc 836 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑧)) ∥ 𝑧)
174111nnzd 12167 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑧)) ∈ ℤ)
175 dvdsval2 15702 . . . . . . . . . . . 12 (((𝑃↑(𝑃 pCnt 𝑧)) ∈ ℤ ∧ (𝑃↑(𝑃 pCnt 𝑧)) ≠ 0 ∧ 𝑧 ∈ ℤ) → ((𝑃↑(𝑃 pCnt 𝑧)) ∥ 𝑧 ↔ (𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) ∈ ℤ))
176174, 119, 97, 175syl3anc 1372 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝑧)) ∥ 𝑧 ↔ (𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) ∈ ℤ))
177173, 176mpbid 235 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) ∈ ℤ)
178 pczndvds2 16303 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑧 ≠ 0)) → ¬ 𝑃 ∥ (𝑧 / (𝑃↑(𝑃 pCnt 𝑧))))
17922, 97, 108, 178syl12anc 836 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ¬ 𝑃 ∥ (𝑧 / (𝑃↑(𝑃 pCnt 𝑧))))
180177, 179jca 515 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑧 / (𝑃↑(𝑃 pCnt 𝑧))) ∈ ℤ ∧ ¬ 𝑃 ∥ (𝑧 / (𝑃↑(𝑃 pCnt 𝑧)))))
181 pcdvds 16300 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ 𝑤 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝑤)) ∥ 𝑤)
18222, 100, 181syl2anc 587 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑤)) ∥ 𝑤)
183117nnzd 12167 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑤)) ∈ ℤ)
184100nnzd 12167 . . . . . . . . . . . . 13 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑤 ∈ ℤ)
185 dvdsval2 15702 . . . . . . . . . . . . 13 (((𝑃↑(𝑃 pCnt 𝑤)) ∈ ℤ ∧ (𝑃↑(𝑃 pCnt 𝑤)) ≠ 0 ∧ 𝑤 ∈ ℤ) → ((𝑃↑(𝑃 pCnt 𝑤)) ∥ 𝑤 ↔ (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))) ∈ ℤ))
186183, 120, 184, 185syl3anc 1372 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑃↑(𝑃 pCnt 𝑤)) ∥ 𝑤 ↔ (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))) ∈ ℤ))
187182, 186mpbid 235 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))) ∈ ℤ)
188100nnred 11731 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 𝑤 ∈ ℝ)
189117nnred 11731 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃↑(𝑃 pCnt 𝑤)) ∈ ℝ)
190100nngt0d 11765 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 0 < 𝑤)
191117nngt0d 11765 . . . . . . . . . . . 12 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 0 < (𝑃↑(𝑃 pCnt 𝑤)))
192188, 189, 190, 191divgt0d 11653 . . . . . . . . . . 11 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → 0 < (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))))
193 elnnz 12072 . . . . . . . . . . 11 ((𝑤 / (𝑃↑(𝑃 pCnt 𝑤))) ∈ ℕ ↔ ((𝑤 / (𝑃↑(𝑃 pCnt 𝑤))) ∈ ℤ ∧ 0 < (𝑤 / (𝑃↑(𝑃 pCnt 𝑤)))))
194187, 192, 193sylanbrc 586 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))) ∈ ℕ)
195 pcndvds2 16304 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ 𝑤 ∈ ℕ) → ¬ 𝑃 ∥ (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))))
19622, 100, 195syl2anc 587 . . . . . . . . . 10 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ¬ 𝑃 ∥ (𝑤 / (𝑃↑(𝑃 pCnt 𝑤))))
197194, 196jca 515 . . . . . . . . 9 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → ((𝑤 / (𝑃↑(𝑃 pCnt 𝑤))) ∈ ℕ ∧ ¬ 𝑃 ∥ (𝑤 / (𝑃↑(𝑃 pCnt 𝑤)))))
19822, 96, 142, 145, 154, 171, 180, 197pcaddlem 16324 . . . . . . . 8 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)))) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵)))
199198expr 460 . . . . . . 7 ((((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ((𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))))
200199rexlimdvva 3204 . . . . . 6 (((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → (∃𝑦 ∈ ℕ ∃𝑤 ∈ ℕ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))))
20121, 200syl5bir 246 . . . . 5 (((𝜑𝐵 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → ((∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))))
202201rexlimdvva 3204 . . . 4 ((𝜑𝐵 ≠ 0) → (∃𝑥 ∈ ℤ ∃𝑧 ∈ ℤ (∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))))
20320, 202syl5bir 246 . . 3 ((𝜑𝐵 ≠ 0) → ((∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))))
20419, 203pm2.61dane 3021 . 2 (𝜑 → ((∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))))
2053, 6, 204mp2and 699 1 (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1542  wcel 2114  wne 2934  wrex 3054   class class class wbr 5030  cfv 6339  (class class class)co 7170  cc 10613  cr 10614  0cc0 10615   + caddc 10618   · cmul 10620  +∞cpnf 10750  *cxr 10752   < clt 10753  cle 10754  cmin 10948   / cdiv 11375  cn 11716  0cn0 11976  cz 12062  cuz 12324  cq 12430  cexp 13521  cdvds 15699  cprime 16112   pCnt cpc 16273
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-cnex 10671  ax-resscn 10672  ax-1cn 10673  ax-icn 10674  ax-addcl 10675  ax-addrcl 10676  ax-mulcl 10677  ax-mulrcl 10678  ax-mulcom 10679  ax-addass 10680  ax-mulass 10681  ax-distr 10682  ax-i2m1 10683  ax-1ne0 10684  ax-1rid 10685  ax-rnegex 10686  ax-rrecex 10687  ax-cnre 10688  ax-pre-lttri 10689  ax-pre-lttrn 10690  ax-pre-ltadd 10691  ax-pre-mulgt0 10692  ax-pre-sup 10693
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-om 7600  df-1st 7714  df-2nd 7715  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-1o 8131  df-2o 8132  df-er 8320  df-en 8556  df-dom 8557  df-sdom 8558  df-fin 8559  df-sup 8979  df-inf 8980  df-pnf 10755  df-mnf 10756  df-xr 10757  df-ltxr 10758  df-le 10759  df-sub 10950  df-neg 10951  df-div 11376  df-nn 11717  df-2 11779  df-3 11780  df-n0 11977  df-z 12063  df-uz 12325  df-q 12431  df-rp 12473  df-fl 13253  df-mod 13329  df-seq 13461  df-exp 13522  df-cj 14548  df-re 14549  df-im 14550  df-sqrt 14684  df-abs 14685  df-dvds 15700  df-gcd 15938  df-prm 16113  df-pc 16274
This theorem is referenced by:  pcadd2  16326  padicabv  26366
  Copyright terms: Public domain W3C validator