Proof of Theorem pcaddlem
Step | Hyp | Ref
| Expression |
1 | | oveq2 7178 |
. . 3
⊢ ((𝐴 + 𝐵) = 0 → (𝑃 pCnt (𝐴 + 𝐵)) = (𝑃 pCnt 0)) |
2 | 1 | breq2d 5042 |
. 2
⊢ ((𝐴 + 𝐵) = 0 → (𝑀 ≤ (𝑃 pCnt (𝐴 + 𝐵)) ↔ 𝑀 ≤ (𝑃 pCnt 0))) |
3 | | pcaddlem.4 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
4 | | eluzel2 12329 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
6 | 5 | zred 12168 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℝ) |
7 | 6 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → 𝑀 ∈ ℝ) |
8 | | pcaddlem.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℙ) |
9 | | prmnn 16115 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℕ) |
11 | 10 | nncnd 11732 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℂ) |
12 | 10 | nnne0d 11766 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ≠ 0) |
13 | | eluzelz 12334 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
14 | 3, 13 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℤ) |
15 | 14, 5 | zsubcld 12173 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℤ) |
16 | 11, 12, 15 | expclzd 13607 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃↑(𝑁 − 𝑀)) ∈ ℂ) |
17 | | pcaddlem.7 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑇 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑇)) |
18 | 17 | simpld 498 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ ℤ) |
19 | 18 | zcnd 12169 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ ℂ) |
20 | | pcaddlem.8 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑈 ∈ ℕ ∧ ¬ 𝑃 ∥ 𝑈)) |
21 | 20 | simpld 498 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ ℕ) |
22 | 21 | nncnd 11732 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ ℂ) |
23 | 21 | nnne0d 11766 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ≠ 0) |
24 | 16, 19, 22, 23 | divassd 11529 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑃↑(𝑁 − 𝑀)) · 𝑇) / 𝑈) = ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))) |
25 | 24 | oveq2d 7186 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑅 / 𝑆) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) / 𝑈)) = ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) |
26 | | pcaddlem.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑅 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑅)) |
27 | 26 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ ℤ) |
28 | 27 | zcnd 12169 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ ℂ) |
29 | | pcaddlem.6 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 ∈ ℕ ∧ ¬ 𝑃 ∥ 𝑆)) |
30 | 29 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ ℕ) |
31 | 30 | nncnd 11732 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℂ) |
32 | 16, 19 | mulcld 10739 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑃↑(𝑁 − 𝑀)) · 𝑇) ∈ ℂ) |
33 | 30 | nnne0d 11766 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ≠ 0) |
34 | 28, 31, 32, 22, 33, 23 | divadddivd 11538 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑅 / 𝑆) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) / 𝑈)) = (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) / (𝑆 · 𝑈))) |
35 | 25, 34 | eqtr3d 2775 |
. . . . . . . 8
⊢ (𝜑 → ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))) = (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) / (𝑆 · 𝑈))) |
36 | 35 | oveq2d 7186 |
. . . . . . 7
⊢ (𝜑 → (𝑃 pCnt ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) = (𝑃 pCnt (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) / (𝑆 · 𝑈)))) |
37 | 36 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → (𝑃 pCnt ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) = (𝑃 pCnt (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) / (𝑆 · 𝑈)))) |
38 | 8 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → 𝑃 ∈ ℙ) |
39 | 21 | nnzd 12167 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ ℤ) |
40 | 27, 39 | zmulcld 12174 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 · 𝑈) ∈ ℤ) |
41 | | uznn0sub 12359 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 − 𝑀) ∈
ℕ0) |
42 | 3, 41 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 𝑀) ∈
ℕ0) |
43 | 10, 42 | nnexpcld 13698 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃↑(𝑁 − 𝑀)) ∈ ℕ) |
44 | 43 | nnzd 12167 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃↑(𝑁 − 𝑀)) ∈ ℤ) |
45 | 44, 18 | zmulcld 12174 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑃↑(𝑁 − 𝑀)) · 𝑇) ∈ ℤ) |
46 | 30 | nnzd 12167 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℤ) |
47 | 45, 46 | zmulcld 12174 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆) ∈ ℤ) |
48 | 40, 47 | zaddcld 12172 |
. . . . . . . 8
⊢ (𝜑 → ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) ∈ ℤ) |
49 | 48 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) ∈ ℤ) |
50 | 11, 12, 5 | expclzd 13607 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃↑𝑀) ∈ ℂ) |
51 | 50 | mul01d 10917 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃↑𝑀) · 0) = 0) |
52 | | oveq2 7178 |
. . . . . . . . . . . . 13
⊢ (((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))) = 0 → ((𝑃↑𝑀) · ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) = ((𝑃↑𝑀) · 0)) |
53 | 52 | eqeq1d 2740 |
. . . . . . . . . . . 12
⊢ (((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))) = 0 → (((𝑃↑𝑀) · ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) = 0 ↔ ((𝑃↑𝑀) · 0) = 0)) |
54 | 51, 53 | syl5ibrcom 250 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))) = 0 → ((𝑃↑𝑀) · ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) = 0)) |
55 | 54 | necon3d 2955 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑃↑𝑀) · ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) ≠ 0 → ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))) ≠ 0)) |
56 | 28, 31, 33 | divcld 11494 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅 / 𝑆) ∈ ℂ) |
57 | 19, 22, 23 | divcld 11494 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑇 / 𝑈) ∈ ℂ) |
58 | 16, 57 | mulcld 10739 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)) ∈ ℂ) |
59 | 50, 56, 58 | adddid 10743 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃↑𝑀) · ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) = (((𝑃↑𝑀) · (𝑅 / 𝑆)) + ((𝑃↑𝑀) · ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))))) |
60 | | pcaddlem.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 = ((𝑃↑𝑀) · (𝑅 / 𝑆))) |
61 | | pcaddlem.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 = ((𝑃↑𝑁) · (𝑇 / 𝑈))) |
62 | 5 | zcnd 12169 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈ ℂ) |
63 | 14 | zcnd 12169 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℂ) |
64 | 62, 63 | pncan3d 11078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 + (𝑁 − 𝑀)) = 𝑁) |
65 | 64 | oveq2d 7186 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃↑(𝑀 + (𝑁 − 𝑀))) = (𝑃↑𝑁)) |
66 | | expaddz 13565 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ ℂ ∧ 𝑃 ≠ 0) ∧ (𝑀 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ)) → (𝑃↑(𝑀 + (𝑁 − 𝑀))) = ((𝑃↑𝑀) · (𝑃↑(𝑁 − 𝑀)))) |
67 | 11, 12, 5, 15, 66 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃↑(𝑀 + (𝑁 − 𝑀))) = ((𝑃↑𝑀) · (𝑃↑(𝑁 − 𝑀)))) |
68 | 65, 67 | eqtr3d 2775 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃↑𝑁) = ((𝑃↑𝑀) · (𝑃↑(𝑁 − 𝑀)))) |
69 | 68 | oveq1d 7185 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑃↑𝑁) · (𝑇 / 𝑈)) = (((𝑃↑𝑀) · (𝑃↑(𝑁 − 𝑀))) · (𝑇 / 𝑈))) |
70 | 50, 16, 57 | mulassd 10742 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑃↑𝑀) · (𝑃↑(𝑁 − 𝑀))) · (𝑇 / 𝑈)) = ((𝑃↑𝑀) · ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) |
71 | 61, 69, 70 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 = ((𝑃↑𝑀) · ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) |
72 | 60, 71 | oveq12d 7188 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 + 𝐵) = (((𝑃↑𝑀) · (𝑅 / 𝑆)) + ((𝑃↑𝑀) · ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))))) |
73 | 59, 72 | eqtr4d 2776 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑃↑𝑀) · ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) = (𝐴 + 𝐵)) |
74 | 73 | neeq1d 2993 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑃↑𝑀) · ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) ≠ 0 ↔ (𝐴 + 𝐵) ≠ 0)) |
75 | 35 | neeq1d 2993 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))) ≠ 0 ↔ (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) / (𝑆 · 𝑈)) ≠ 0)) |
76 | 55, 74, 75 | 3imtr3d 296 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 + 𝐵) ≠ 0 → (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) / (𝑆 · 𝑈)) ≠ 0)) |
77 | 30, 21 | nnmulcld 11769 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 · 𝑈) ∈ ℕ) |
78 | 77 | nncnd 11732 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 · 𝑈) ∈ ℂ) |
79 | 77 | nnne0d 11766 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 · 𝑈) ≠ 0) |
80 | 78, 79 | div0d 11493 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 / (𝑆 · 𝑈)) = 0) |
81 | | oveq1 7177 |
. . . . . . . . . . . 12
⊢ (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) = 0 → (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) / (𝑆 · 𝑈)) = (0 / (𝑆 · 𝑈))) |
82 | 81 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) = 0 → ((((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) / (𝑆 · 𝑈)) = 0 ↔ (0 / (𝑆 · 𝑈)) = 0)) |
83 | 80, 82 | syl5ibrcom 250 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) = 0 → (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) / (𝑆 · 𝑈)) = 0)) |
84 | 83 | necon3d 2955 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) / (𝑆 · 𝑈)) ≠ 0 → ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) ≠ 0)) |
85 | 76, 84 | syld 47 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 + 𝐵) ≠ 0 → ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) ≠ 0)) |
86 | 85 | imp 410 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) ≠ 0) |
87 | 77 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → (𝑆 · 𝑈) ∈ ℕ) |
88 | | pcdiv 16289 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) ∈ ℤ ∧ ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) ≠ 0) ∧ (𝑆 · 𝑈) ∈ ℕ) → (𝑃 pCnt (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) / (𝑆 · 𝑈))) = ((𝑃 pCnt ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆))) − (𝑃 pCnt (𝑆 · 𝑈)))) |
89 | 38, 49, 86, 87, 88 | syl121anc 1376 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → (𝑃 pCnt (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) / (𝑆 · 𝑈))) = ((𝑃 pCnt ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆))) − (𝑃 pCnt (𝑆 · 𝑈)))) |
90 | | pcmul 16288 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ (𝑆 ∈ ℤ ∧ 𝑆 ≠ 0) ∧ (𝑈 ∈ ℤ ∧ 𝑈 ≠ 0)) → (𝑃 pCnt (𝑆 · 𝑈)) = ((𝑃 pCnt 𝑆) + (𝑃 pCnt 𝑈))) |
91 | 8, 46, 33, 39, 23, 90 | syl122anc 1380 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 pCnt (𝑆 · 𝑈)) = ((𝑃 pCnt 𝑆) + (𝑃 pCnt 𝑈))) |
92 | 29 | simprd 499 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑃 ∥ 𝑆) |
93 | | pceq0 16307 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝑆 ∈ ℕ) → ((𝑃 pCnt 𝑆) = 0 ↔ ¬ 𝑃 ∥ 𝑆)) |
94 | 8, 30, 93 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 pCnt 𝑆) = 0 ↔ ¬ 𝑃 ∥ 𝑆)) |
95 | 92, 94 | mpbird 260 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 pCnt 𝑆) = 0) |
96 | 20 | simprd 499 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑃 ∥ 𝑈) |
97 | | pceq0 16307 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝑈 ∈ ℕ) → ((𝑃 pCnt 𝑈) = 0 ↔ ¬ 𝑃 ∥ 𝑈)) |
98 | 8, 21, 97 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 pCnt 𝑈) = 0 ↔ ¬ 𝑃 ∥ 𝑈)) |
99 | 96, 98 | mpbird 260 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 pCnt 𝑈) = 0) |
100 | 95, 99 | oveq12d 7188 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 pCnt 𝑆) + (𝑃 pCnt 𝑈)) = (0 + 0)) |
101 | | 00id 10893 |
. . . . . . . . . . 11
⊢ (0 + 0) =
0 |
102 | 100, 101 | eqtrdi 2789 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑃 pCnt 𝑆) + (𝑃 pCnt 𝑈)) = 0) |
103 | 91, 102 | eqtrd 2773 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 pCnt (𝑆 · 𝑈)) = 0) |
104 | 103 | oveq2d 7186 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃 pCnt ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆))) − (𝑃 pCnt (𝑆 · 𝑈))) = ((𝑃 pCnt ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆))) − 0)) |
105 | 104 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → ((𝑃 pCnt ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆))) − (𝑃 pCnt (𝑆 · 𝑈))) = ((𝑃 pCnt ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆))) − 0)) |
106 | | pczcl 16285 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ (((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) ∈ ℤ ∧ ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)) ≠ 0)) → (𝑃 pCnt ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆))) ∈
ℕ0) |
107 | 38, 49, 86, 106 | syl12anc 836 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → (𝑃 pCnt ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆))) ∈
ℕ0) |
108 | 107 | nn0cnd 12038 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → (𝑃 pCnt ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆))) ∈ ℂ) |
109 | 108 | subid1d 11064 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → ((𝑃 pCnt ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆))) − 0) = (𝑃 pCnt ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)))) |
110 | 105, 109 | eqtrd 2773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → ((𝑃 pCnt ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆))) − (𝑃 pCnt (𝑆 · 𝑈))) = (𝑃 pCnt ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)))) |
111 | 37, 89, 110 | 3eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → (𝑃 pCnt ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) = (𝑃 pCnt ((𝑅 · 𝑈) + (((𝑃↑(𝑁 − 𝑀)) · 𝑇) · 𝑆)))) |
112 | 111, 107 | eqeltrd 2833 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → (𝑃 pCnt ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) ∈
ℕ0) |
113 | | nn0addge1 12022 |
. . . 4
⊢ ((𝑀 ∈ ℝ ∧ (𝑃 pCnt ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))) ∈ ℕ0) →
𝑀 ≤ (𝑀 + (𝑃 pCnt ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))))) |
114 | 7, 112, 113 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → 𝑀 ≤ (𝑀 + (𝑃 pCnt ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))))) |
115 | | nnq 12444 |
. . . . . . . 8
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℚ) |
116 | 10, 115 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℚ) |
117 | | qexpclz 13542 |
. . . . . . 7
⊢ ((𝑃 ∈ ℚ ∧ 𝑃 ≠ 0 ∧ 𝑀 ∈ ℤ) → (𝑃↑𝑀) ∈ ℚ) |
118 | 116, 12, 5, 117 | syl3anc 1372 |
. . . . . 6
⊢ (𝜑 → (𝑃↑𝑀) ∈ ℚ) |
119 | 118 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → (𝑃↑𝑀) ∈ ℚ) |
120 | 11, 12, 5 | expne0d 13608 |
. . . . . 6
⊢ (𝜑 → (𝑃↑𝑀) ≠ 0) |
121 | 120 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → (𝑃↑𝑀) ≠ 0) |
122 | | znq 12434 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℤ ∧ 𝑆 ∈ ℕ) → (𝑅 / 𝑆) ∈ ℚ) |
123 | 27, 30, 122 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝑅 / 𝑆) ∈ ℚ) |
124 | | qexpclz 13542 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℚ ∧ 𝑃 ≠ 0 ∧ (𝑁 − 𝑀) ∈ ℤ) → (𝑃↑(𝑁 − 𝑀)) ∈ ℚ) |
125 | 116, 12, 15, 124 | syl3anc 1372 |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑(𝑁 − 𝑀)) ∈ ℚ) |
126 | | znq 12434 |
. . . . . . . . 9
⊢ ((𝑇 ∈ ℤ ∧ 𝑈 ∈ ℕ) → (𝑇 / 𝑈) ∈ ℚ) |
127 | 18, 21, 126 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 / 𝑈) ∈ ℚ) |
128 | | qmulcl 12449 |
. . . . . . . 8
⊢ (((𝑃↑(𝑁 − 𝑀)) ∈ ℚ ∧ (𝑇 / 𝑈) ∈ ℚ) → ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)) ∈ ℚ) |
129 | 125, 127,
128 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)) ∈ ℚ) |
130 | | qaddcl 12447 |
. . . . . . 7
⊢ (((𝑅 / 𝑆) ∈ ℚ ∧ ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)) ∈ ℚ) → ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))) ∈ ℚ) |
131 | 123, 129,
130 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))) ∈ ℚ) |
132 | 131 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))) ∈ ℚ) |
133 | 74, 55 | sylbird 263 |
. . . . . 6
⊢ (𝜑 → ((𝐴 + 𝐵) ≠ 0 → ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))) ≠ 0)) |
134 | 133 | imp 410 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))) ≠ 0) |
135 | | pcqmul 16290 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ ((𝑃↑𝑀) ∈ ℚ ∧ (𝑃↑𝑀) ≠ 0) ∧ (((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))) ∈ ℚ ∧ ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))) ≠ 0)) → (𝑃 pCnt ((𝑃↑𝑀) · ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))))) = ((𝑃 pCnt (𝑃↑𝑀)) + (𝑃 pCnt ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))))) |
136 | 38, 119, 121, 132, 134, 135 | syl122anc 1380 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → (𝑃 pCnt ((𝑃↑𝑀) · ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))))) = ((𝑃 pCnt (𝑃↑𝑀)) + (𝑃 pCnt ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))))) |
137 | 73 | oveq2d 7186 |
. . . . 5
⊢ (𝜑 → (𝑃 pCnt ((𝑃↑𝑀) · ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))))) = (𝑃 pCnt (𝐴 + 𝐵))) |
138 | 137 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → (𝑃 pCnt ((𝑃↑𝑀) · ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))))) = (𝑃 pCnt (𝐴 + 𝐵))) |
139 | | pcid 16309 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ) → (𝑃 pCnt (𝑃↑𝑀)) = 𝑀) |
140 | 8, 5, 139 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝑃 pCnt (𝑃↑𝑀)) = 𝑀) |
141 | 140 | oveq1d 7185 |
. . . . 5
⊢ (𝜑 → ((𝑃 pCnt (𝑃↑𝑀)) + (𝑃 pCnt ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))))) = (𝑀 + (𝑃 pCnt ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))))) |
142 | 141 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → ((𝑃 pCnt (𝑃↑𝑀)) + (𝑃 pCnt ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈))))) = (𝑀 + (𝑃 pCnt ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))))) |
143 | 136, 138,
142 | 3eqtr3d 2781 |
. . 3
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → (𝑃 pCnt (𝐴 + 𝐵)) = (𝑀 + (𝑃 pCnt ((𝑅 / 𝑆) + ((𝑃↑(𝑁 − 𝑀)) · (𝑇 / 𝑈)))))) |
144 | 114, 143 | breqtrrd 5058 |
. 2
⊢ ((𝜑 ∧ (𝐴 + 𝐵) ≠ 0) → 𝑀 ≤ (𝑃 pCnt (𝐴 + 𝐵))) |
145 | 6 | rexrd 10769 |
. . . 4
⊢ (𝜑 → 𝑀 ∈
ℝ*) |
146 | | pnfge 12608 |
. . . 4
⊢ (𝑀 ∈ ℝ*
→ 𝑀 ≤
+∞) |
147 | 145, 146 | syl 17 |
. . 3
⊢ (𝜑 → 𝑀 ≤ +∞) |
148 | | pc0 16291 |
. . . 4
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) =
+∞) |
149 | 8, 148 | syl 17 |
. . 3
⊢ (𝜑 → (𝑃 pCnt 0) = +∞) |
150 | 147, 149 | breqtrrd 5058 |
. 2
⊢ (𝜑 → 𝑀 ≤ (𝑃 pCnt 0)) |
151 | 2, 144, 150 | pm2.61ne 3019 |
1
⊢ (𝜑 → 𝑀 ≤ (𝑃 pCnt (𝐴 + 𝐵))) |