Metamath Proof Explorer

Theorem pcadd

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)

Ref Expression
Hypotheses pcadd.1 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
pcadd.2 ⊢ ( 𝜑 → 𝐴 ∈ ℚ )
pcadd.3 ⊢ ( 𝜑 → 𝐵 ∈ ℚ )
pcadd.4 ⊢ ( 𝜑 → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) )
Assertion pcadd ( 𝜑 → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 + 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 pcadd.1 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
2 pcadd.2 ⊢ ( 𝜑 → 𝐴 ∈ ℚ )
3 pcadd.3 ⊢ ( 𝜑 → 𝐵 ∈ ℚ )
4 pcadd.4 ⊢ ( 𝜑 → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) )
5 elq ⊢ ( 𝐴 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
6 2 5 sylib ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
7 elq ⊢ ( 𝐵 ∈ ℚ ↔ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) )
8 3 7 sylib ⊢ ( 𝜑 → ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) )
9 pcxcl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ ) → ( 𝑃 pCnt 𝐴 ) ∈ ℝ* )
10 1 2 9 syl2anc ⊢ ( 𝜑 → ( 𝑃 pCnt 𝐴 ) ∈ ℝ* )
11 10 xrleidd ⊢ ( 𝜑 → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐴 ) )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 0 ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐴 ) )
13 oveq2 ⊢ ( 𝐵 = 0 → ( 𝐴 + 𝐵 ) = ( 𝐴 + 0 ) )
14 qcn ⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ ℂ )
15 2 14 syl ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
16 15 addridd ⊢ ( 𝜑 → ( 𝐴 + 0 ) = 𝐴 )
17 13 16 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝐵 = 0 ) → ( 𝐴 + 𝐵 ) = 𝐴 )
18 17 oveq2d ⊢ ( ( 𝜑 ∧ 𝐵 = 0 ) → ( 𝑃 pCnt ( 𝐴 + 𝐵 ) ) = ( 𝑃 pCnt 𝐴 ) )
19 12 18 breqtrrd ⊢ ( ( 𝜑 ∧ 𝐵 = 0 ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 + 𝐵 ) ) )
20 19 a1d ⊢ ( ( 𝜑 ∧ 𝐵 = 0 ) → ( ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 + 𝐵 ) ) ) )
21 reeanv ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑧 ∈ ℤ ( ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) ↔ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) )
22 reeanv ⊢ ( ∃ 𝑦 ∈ ℕ ∃ 𝑤 ∈ ℕ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ↔ ( ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) )
23 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑃 ∈ ℙ )
24 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
25 23 24 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑃 ∈ ℕ )
26 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑥 ∈ ℤ )
27 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝐴 = ( 𝑥 / 𝑦 ) )
28 pc0 ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 0 ) = +∞ )
29 23 28 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 0 ) = +∞ )
30 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝐵 ∈ ℚ )
31 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝐵 ≠ 0 )
32 pcqcl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐵 ) ∈ ℤ )
33 23 30 31 32 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝐵 ) ∈ ℤ )
34 33 zred ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝐵 ) ∈ ℝ )
35 ltpnf ⊢ ( ( 𝑃 pCnt 𝐵 ) ∈ ℝ → ( 𝑃 pCnt 𝐵 ) < +∞ )
36 rexr ⊢ ( ( 𝑃 pCnt 𝐵 ) ∈ ℝ → ( 𝑃 pCnt 𝐵 ) ∈ ℝ* )
37 pnfxr ⊢ +∞ ∈ ℝ*
38 xrltnle ⊢ ( ( ( 𝑃 pCnt 𝐵 ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝑃 pCnt 𝐵 ) < +∞ ↔ ¬ +∞ ≤ ( 𝑃 pCnt 𝐵 ) ) )
39 36 37 38 sylancl ⊢ ( ( 𝑃 pCnt 𝐵 ) ∈ ℝ → ( ( 𝑃 pCnt 𝐵 ) < +∞ ↔ ¬ +∞ ≤ ( 𝑃 pCnt 𝐵 ) ) )
40 35 39 mpbid ⊢ ( ( 𝑃 pCnt 𝐵 ) ∈ ℝ → ¬ +∞ ≤ ( 𝑃 pCnt 𝐵 ) )
41 34 40 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ¬ +∞ ≤ ( 𝑃 pCnt 𝐵 ) )
42 29 41 eqnbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ¬ ( 𝑃 pCnt 0 ) ≤ ( 𝑃 pCnt 𝐵 ) )
43 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) )
44 oveq2 ⊢ ( 𝐴 = 0 → ( 𝑃 pCnt 𝐴 ) = ( 𝑃 pCnt 0 ) )
45 44 breq1d ⊢ ( 𝐴 = 0 → ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ↔ ( 𝑃 pCnt 0 ) ≤ ( 𝑃 pCnt 𝐵 ) ) )
46 43 45 syl5ibcom ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝐴 = 0 → ( 𝑃 pCnt 0 ) ≤ ( 𝑃 pCnt 𝐵 ) ) )
47 46 necon3bd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ¬ ( 𝑃 pCnt 0 ) ≤ ( 𝑃 pCnt 𝐵 ) → 𝐴 ≠ 0 ) )
48 42 47 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝐴 ≠ 0 )
49 27 48 eqnetrrd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑥 / 𝑦 ) ≠ 0 )
50 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑦 ∈ ℕ )
51 50 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑦 ∈ ℂ )
52 50 nnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑦 ≠ 0 )
53 51 52 div0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 0 / 𝑦 ) = 0 )
54 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 / 𝑦 ) = ( 0 / 𝑦 ) )
55 54 eqeq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 / 𝑦 ) = 0 ↔ ( 0 / 𝑦 ) = 0 ) )
56 53 55 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑥 = 0 → ( 𝑥 / 𝑦 ) = 0 ) )
57 56 necon3d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑥 / 𝑦 ) ≠ 0 → 𝑥 ≠ 0 ) )
58 49 57 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑥 ≠ 0 )
59 pczcl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ( 𝑃 pCnt 𝑥 ) ∈ ℕ0 )
60 23 26 58 59 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝑥 ) ∈ ℕ0 )
61 25 60 nnexpcld ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ∈ ℕ )
62 61 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ∈ ℂ )
63 62 51 mulcomd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) · 𝑦 ) = ( 𝑦 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) )
64 63 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑥 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) / ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) · 𝑦 ) ) = ( ( 𝑥 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) / ( 𝑦 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) ) )
65 26 zcnd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑥 ∈ ℂ )
66 23 50 pccld ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℕ0 )
67 25 66 nnexpcld ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ∈ ℕ )
68 67 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ∈ ℂ )
69 61 nnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ≠ 0 )
70 67 nnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ≠ 0 )
71 65 62 51 68 69 70 52 divdivdivd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑥 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) / ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) = ( ( 𝑥 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) / ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) · 𝑦 ) ) )
72 27 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝐴 ) = ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) )
73 pcdiv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) = ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) )
74 23 26 58 50 73 syl121anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) = ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) )
75 72 74 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝐴 ) = ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) )
76 75 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) = ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) ) )
77 25 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑃 ∈ ℂ )
78 25 nnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑃 ≠ 0 )
79 66 nn0zd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℤ )
80 60 nn0zd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝑥 ) ∈ ℤ )
81 77 78 79 80 expsubd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) ) = ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) )
82 76 81 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) = ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) )
83 82 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) = ( 𝐴 / ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) )
84 27 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝐴 / ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) = ( ( 𝑥 / 𝑦 ) / ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) )
85 65 51 62 68 52 70 69 divdivdivd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑥 / 𝑦 ) / ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) = ( ( 𝑥 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) / ( 𝑦 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) ) )
86 83 84 85 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) = ( ( 𝑥 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) / ( 𝑦 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) ) )
87 64 71 86 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑥 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) / ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) = ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
88 87 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) · ( ( 𝑥 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) / ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) ) = ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) · ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
89 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝐴 ∈ ℚ )
90 89 14 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝐴 ∈ ℂ )
91 pcqcl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 pCnt 𝐴 ) ∈ ℤ )
92 23 89 48 91 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝐴 ) ∈ ℤ )
93 77 78 92 expclzd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℂ )
94 77 78 92 expne0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ≠ 0 )
95 90 93 94 divcan2d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) · ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 𝐴 )
96 88 95 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝐴 = ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) · ( ( 𝑥 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) / ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) ) )
97 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑧 ∈ ℤ )
98 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝐵 = ( 𝑧 / 𝑤 ) )
99 98 31 eqnetrrd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑧 / 𝑤 ) ≠ 0 )
100 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑤 ∈ ℕ )
101 100 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑤 ∈ ℂ )
102 100 nnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑤 ≠ 0 )
103 101 102 div0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 0 / 𝑤 ) = 0 )
104 oveq1 ⊢ ( 𝑧 = 0 → ( 𝑧 / 𝑤 ) = ( 0 / 𝑤 ) )
105 104 eqeq1d ⊢ ( 𝑧 = 0 → ( ( 𝑧 / 𝑤 ) = 0 ↔ ( 0 / 𝑤 ) = 0 ) )
106 103 105 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑧 = 0 → ( 𝑧 / 𝑤 ) = 0 ) )
107 106 necon3d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑧 / 𝑤 ) ≠ 0 → 𝑧 ≠ 0 ) )
108 99 107 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑧 ≠ 0 )
109 pczcl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑧 ≠ 0 ) ) → ( 𝑃 pCnt 𝑧 ) ∈ ℕ0 )
110 23 97 108 109 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝑧 ) ∈ ℕ0 )
111 25 110 nnexpcld ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ∈ ℕ )
112 111 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ∈ ℂ )
113 112 101 mulcomd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) · 𝑤 ) = ( 𝑤 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) )
114 113 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑧 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) / ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) · 𝑤 ) ) = ( ( 𝑧 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) / ( 𝑤 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) )
115 97 zcnd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑧 ∈ ℂ )
116 23 100 pccld ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝑤 ) ∈ ℕ0 )
117 25 116 nnexpcld ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ∈ ℕ )
118 117 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ∈ ℂ )
119 111 nnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ≠ 0 )
120 117 nnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ≠ 0 )
121 115 112 101 118 119 120 102 divdivdivd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑧 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) / ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ) = ( ( 𝑧 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) / ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) · 𝑤 ) ) )
122 98 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝐵 ) = ( 𝑃 pCnt ( 𝑧 / 𝑤 ) ) )
123 pcdiv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑧 ≠ 0 ) ∧ 𝑤 ∈ ℕ ) → ( 𝑃 pCnt ( 𝑧 / 𝑤 ) ) = ( ( 𝑃 pCnt 𝑧 ) − ( 𝑃 pCnt 𝑤 ) ) )
124 23 97 108 100 123 syl121anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt ( 𝑧 / 𝑤 ) ) = ( ( 𝑃 pCnt 𝑧 ) − ( 𝑃 pCnt 𝑤 ) ) )
125 122 124 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝐵 ) = ( ( 𝑃 pCnt 𝑧 ) − ( 𝑃 pCnt 𝑤 ) ) )
126 125 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐵 ) ) = ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑧 ) − ( 𝑃 pCnt 𝑤 ) ) ) )
127 116 nn0zd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝑤 ) ∈ ℤ )
128 110 nn0zd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝑧 ) ∈ ℤ )
129 77 78 127 128 expsubd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑧 ) − ( 𝑃 pCnt 𝑤 ) ) ) = ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) )
130 126 129 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐵 ) ) = ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) )
131 130 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝐵 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐵 ) ) ) = ( 𝐵 / ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ) )
132 98 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝐵 / ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ) = ( ( 𝑧 / 𝑤 ) / ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ) )
133 115 101 112 118 102 120 119 divdivdivd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑧 / 𝑤 ) / ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ) = ( ( 𝑧 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) / ( 𝑤 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) )
134 131 132 133 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝐵 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐵 ) ) ) = ( ( 𝑧 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) / ( 𝑤 · ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) )
135 114 121 134 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑧 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) / ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ) = ( 𝐵 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐵 ) ) ) )
136 135 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐵 ) ) · ( ( 𝑧 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) / ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ) ) = ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐵 ) ) · ( 𝐵 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐵 ) ) ) ) )
137 qcn ⊢ ( 𝐵 ∈ ℚ → 𝐵 ∈ ℂ )
138 30 137 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝐵 ∈ ℂ )
139 77 78 33 expclzd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐵 ) ) ∈ ℂ )
140 77 78 33 expne0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐵 ) ) ≠ 0 )
141 138 139 140 divcan2d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐵 ) ) · ( 𝐵 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐵 ) ) ) ) = 𝐵 )
142 136 141 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝐵 = ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐵 ) ) · ( ( 𝑧 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) / ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ) ) )
143 eluz ⊢ ( ( ( 𝑃 pCnt 𝐴 ) ∈ ℤ ∧ ( 𝑃 pCnt 𝐵 ) ∈ ℤ ) → ( ( 𝑃 pCnt 𝐵 ) ∈ ( ℤ≥ ‘ ( 𝑃 pCnt 𝐴 ) ) ↔ ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ) )
144 92 33 143 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑃 pCnt 𝐵 ) ∈ ( ℤ≥ ‘ ( 𝑃 pCnt 𝐴 ) ) ↔ ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ) )
145 43 144 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝐵 ) ∈ ( ℤ≥ ‘ ( 𝑃 pCnt 𝐴 ) ) )
146 pczdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ∥ 𝑥 )
147 23 26 58 146 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ∥ 𝑥 )
148 61 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ∈ ℤ )
149 dvdsval2 ⊢ ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ∈ ℤ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ≠ 0 ∧ 𝑥 ∈ ℤ ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ∥ 𝑥 ↔ ( 𝑥 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) ∈ ℤ ) )
150 148 69 26 149 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ∥ 𝑥 ↔ ( 𝑥 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) ∈ ℤ ) )
151 147 150 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑥 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) ∈ ℤ )
152 pczndvds2 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ¬ 𝑃 ∥ ( 𝑥 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) )
153 23 26 58 152 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ¬ 𝑃 ∥ ( 𝑥 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) )
154 151 153 jca ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑥 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) ∈ ℤ ∧ ¬ 𝑃 ∥ ( 𝑥 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑥 ) ) ) ) )
155 pcdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ∥ 𝑦 )
156 23 50 155 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ∥ 𝑦 )
157 67 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ∈ ℤ )
158 50 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑦 ∈ ℤ )
159 dvdsval2 ⊢ ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ∈ ℤ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ∥ 𝑦 ↔ ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ∈ ℤ ) )
160 157 70 158 159 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ∥ 𝑦 ↔ ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ∈ ℤ ) )
161 156 160 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ∈ ℤ )
162 50 nnred ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑦 ∈ ℝ )
163 67 nnred ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ∈ ℝ )
164 50 nngt0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 0 < 𝑦 )
165 67 nngt0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 0 < ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) )
166 162 163 164 165 divgt0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 0 < ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) )
167 elnnz ⊢ ( ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ∈ ℕ ↔ ( ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ∈ ℤ ∧ 0 < ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) )
168 161 166 167 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ∈ ℕ )
169 pcndvds2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ ) → ¬ 𝑃 ∥ ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) )
170 23 50 169 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ¬ 𝑃 ∥ ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) )
171 168 170 jca ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ∈ ℕ ∧ ¬ 𝑃 ∥ ( 𝑦 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) )
172 pczdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑧 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ∥ 𝑧 )
173 23 97 108 172 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ∥ 𝑧 )
174 111 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ∈ ℤ )
175 dvdsval2 ⊢ ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ∈ ℤ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ≠ 0 ∧ 𝑧 ∈ ℤ ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ∥ 𝑧 ↔ ( 𝑧 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ∈ ℤ ) )
176 174 119 97 175 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ∥ 𝑧 ↔ ( 𝑧 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ∈ ℤ ) )
177 173 176 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑧 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ∈ ℤ )
178 pczndvds2 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑧 ≠ 0 ) ) → ¬ 𝑃 ∥ ( 𝑧 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) )
179 23 97 108 178 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ¬ 𝑃 ∥ ( 𝑧 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) )
180 177 179 jca ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑧 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ∈ ℤ ∧ ¬ 𝑃 ∥ ( 𝑧 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) )
181 pcdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑤 ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ∥ 𝑤 )
182 23 100 181 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ∥ 𝑤 )
183 117 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ∈ ℤ )
184 100 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑤 ∈ ℤ )
185 dvdsval2 ⊢ ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ∈ ℤ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ≠ 0 ∧ 𝑤 ∈ ℤ ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ∥ 𝑤 ↔ ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ∈ ℤ ) )
186 183 120 184 185 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ∥ 𝑤 ↔ ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ∈ ℤ ) )
187 182 186 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ∈ ℤ )
188 100 nnred ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 𝑤 ∈ ℝ )
189 117 nnred ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ∈ ℝ )
190 100 nngt0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 0 < 𝑤 )
191 117 nngt0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 0 < ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) )
192 188 189 190 191 divgt0d ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → 0 < ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) )
193 elnnz ⊢ ( ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ∈ ℕ ↔ ( ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ∈ ℤ ∧ 0 < ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ) )
194 187 192 193 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ∈ ℕ )
195 pcndvds2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑤 ∈ ℕ ) → ¬ 𝑃 ∥ ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) )
196 23 100 195 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ¬ 𝑃 ∥ ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) )
197 194 196 jca ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ∈ ℕ ∧ ¬ 𝑃 ∥ ( 𝑤 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑤 ) ) ) ) )
198 23 96 142 145 154 171 180 197 pcaddlem ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 + 𝐵 ) ) )
199 198 expr ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 + 𝐵 ) ) ) )
200 199 rexlimdvva ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ∃ 𝑦 ∈ ℕ ∃ 𝑤 ∈ ℕ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 + 𝐵 ) ) ) )
201 22 200 biimtrrid ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 + 𝐵 ) ) ) )
202 201 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑧 ∈ ℤ ( ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 + 𝐵 ) ) ) )
203 21 202 biimtrrid ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0 ) → ( ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 + 𝐵 ) ) ) )
204 20 203 pm2.61dane ⊢ ( 𝜑 → ( ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 + 𝐵 ) ) ) )
205 6 8 204 mp2and ⊢ ( 𝜑 → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 + 𝐵 ) ) )