Proof of Theorem pcadd2
Step | Hyp | Ref
| Expression |
1 | | pcadd2.1 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ℙ) |
2 | | pcadd2.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℚ) |
3 | | pcxcl 12449 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt 𝐴) ∈
ℝ*) |
4 | 1, 2, 3 | syl2anc 411 |
. 2
⊢ (𝜑 → (𝑃 pCnt 𝐴) ∈
ℝ*) |
5 | | pcadd2.3 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℚ) |
6 | | qaddcl 9700 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ) |
7 | 2, 5, 6 | syl2anc 411 |
. . 3
⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℚ) |
8 | | pcxcl 12449 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 + 𝐵) ∈ ℚ) → (𝑃 pCnt (𝐴 + 𝐵)) ∈
ℝ*) |
9 | 1, 7, 8 | syl2anc 411 |
. 2
⊢ (𝜑 → (𝑃 pCnt (𝐴 + 𝐵)) ∈
ℝ*) |
10 | | pcxcl 12449 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐵 ∈ ℚ) → (𝑃 pCnt 𝐵) ∈
ℝ*) |
11 | 1, 5, 10 | syl2anc 411 |
. . . 4
⊢ (𝜑 → (𝑃 pCnt 𝐵) ∈
ℝ*) |
12 | | pcadd2.4 |
. . . 4
⊢ (𝜑 → (𝑃 pCnt 𝐴) < (𝑃 pCnt 𝐵)) |
13 | 4, 11, 12 | xrltled 9865 |
. . 3
⊢ (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) |
14 | 1, 2, 5, 13 | pcadd 12478 |
. 2
⊢ (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))) |
15 | | qnegcl 9701 |
. . . . 5
⊢ (𝐵 ∈ ℚ → -𝐵 ∈
ℚ) |
16 | 5, 15 | syl 14 |
. . . 4
⊢ (𝜑 → -𝐵 ∈ ℚ) |
17 | | pcxqcl 12450 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → ((𝑃 pCnt 𝐴) ∈ ℤ ∨ (𝑃 pCnt 𝐴) = +∞)) |
18 | | zq 9691 |
. . . . . . . . . . . . 13
⊢ ((𝑃 pCnt 𝐴) ∈ ℤ → (𝑃 pCnt 𝐴) ∈ ℚ) |
19 | 18 | orim1i 761 |
. . . . . . . . . . . 12
⊢ (((𝑃 pCnt 𝐴) ∈ ℤ ∨ (𝑃 pCnt 𝐴) = +∞) → ((𝑃 pCnt 𝐴) ∈ ℚ ∨ (𝑃 pCnt 𝐴) = +∞)) |
20 | 17, 19 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → ((𝑃 pCnt 𝐴) ∈ ℚ ∨ (𝑃 pCnt 𝐴) = +∞)) |
21 | 1, 2, 20 | syl2anc 411 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑃 pCnt 𝐴) ∈ ℚ ∨ (𝑃 pCnt 𝐴) = +∞)) |
22 | | pcxqcl 12450 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐵 ∈ ℚ) → ((𝑃 pCnt 𝐵) ∈ ℤ ∨ (𝑃 pCnt 𝐵) = +∞)) |
23 | | zq 9691 |
. . . . . . . . . . . . 13
⊢ ((𝑃 pCnt 𝐵) ∈ ℤ → (𝑃 pCnt 𝐵) ∈ ℚ) |
24 | 23 | orim1i 761 |
. . . . . . . . . . . 12
⊢ (((𝑃 pCnt 𝐵) ∈ ℤ ∨ (𝑃 pCnt 𝐵) = +∞) → ((𝑃 pCnt 𝐵) ∈ ℚ ∨ (𝑃 pCnt 𝐵) = +∞)) |
25 | 22, 24 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐵 ∈ ℚ) → ((𝑃 pCnt 𝐵) ∈ ℚ ∨ (𝑃 pCnt 𝐵) = +∞)) |
26 | 1, 5, 25 | syl2anc 411 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑃 pCnt 𝐵) ∈ ℚ ∨ (𝑃 pCnt 𝐵) = +∞)) |
27 | | xqltnle 10336 |
. . . . . . . . . 10
⊢ ((((𝑃 pCnt 𝐴) ∈ ℚ ∨ (𝑃 pCnt 𝐴) = +∞) ∧ ((𝑃 pCnt 𝐵) ∈ ℚ ∨ (𝑃 pCnt 𝐵) = +∞)) → ((𝑃 pCnt 𝐴) < (𝑃 pCnt 𝐵) ↔ ¬ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt 𝐴))) |
28 | 21, 26, 27 | syl2anc 411 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 pCnt 𝐴) < (𝑃 pCnt 𝐵) ↔ ¬ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt 𝐴))) |
29 | 12, 28 | mpbid 147 |
. . . . . . . 8
⊢ (𝜑 → ¬ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt 𝐴)) |
30 | 1 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵))) → 𝑃 ∈ ℙ) |
31 | 16 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵))) → -𝐵 ∈ ℚ) |
32 | 7 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵))) → (𝐴 + 𝐵) ∈ ℚ) |
33 | | pcneg 12463 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐵 ∈ ℚ) → (𝑃 pCnt -𝐵) = (𝑃 pCnt 𝐵)) |
34 | 1, 5, 33 | syl2anc 411 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 pCnt -𝐵) = (𝑃 pCnt 𝐵)) |
35 | 34 | breq1d 4039 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃 pCnt -𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵)) ↔ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵)))) |
36 | 35 | biimpar 297 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵))) → (𝑃 pCnt -𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵))) |
37 | 30, 31, 32, 36 | pcadd 12478 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵))) → (𝑃 pCnt -𝐵) ≤ (𝑃 pCnt (-𝐵 + (𝐴 + 𝐵)))) |
38 | 37 | ex 115 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵)) → (𝑃 pCnt -𝐵) ≤ (𝑃 pCnt (-𝐵 + (𝐴 + 𝐵))))) |
39 | | qcn 9699 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ ℚ → 𝐵 ∈
ℂ) |
40 | 5, 39 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ ℂ) |
41 | 40 | negcld 8317 |
. . . . . . . . . . . . 13
⊢ (𝜑 → -𝐵 ∈ ℂ) |
42 | | qcn 9699 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℂ) |
43 | 2, 42 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℂ) |
44 | 41, 43, 40 | add12d 8186 |
. . . . . . . . . . . 12
⊢ (𝜑 → (-𝐵 + (𝐴 + 𝐵)) = (𝐴 + (-𝐵 + 𝐵))) |
45 | 41, 40 | addcomd 8170 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (-𝐵 + 𝐵) = (𝐵 + -𝐵)) |
46 | 40 | negidd 8320 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 + -𝐵) = 0) |
47 | 45, 46 | eqtrd 2226 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (-𝐵 + 𝐵) = 0) |
48 | 47 | oveq2d 5934 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 + (-𝐵 + 𝐵)) = (𝐴 + 0)) |
49 | 43 | addridd 8168 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 + 0) = 𝐴) |
50 | 44, 48, 49 | 3eqtrd 2230 |
. . . . . . . . . . 11
⊢ (𝜑 → (-𝐵 + (𝐴 + 𝐵)) = 𝐴) |
51 | 50 | oveq2d 5934 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 pCnt (-𝐵 + (𝐴 + 𝐵))) = (𝑃 pCnt 𝐴)) |
52 | 34, 51 | breq12d 4042 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 pCnt -𝐵) ≤ (𝑃 pCnt (-𝐵 + (𝐴 + 𝐵))) ↔ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt 𝐴))) |
53 | 38, 52 | sylibd 149 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵)) → (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt 𝐴))) |
54 | 29, 53 | mtod 664 |
. . . . . . 7
⊢ (𝜑 → ¬ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵))) |
55 | | pcxqcl 12450 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 + 𝐵) ∈ ℚ) → ((𝑃 pCnt (𝐴 + 𝐵)) ∈ ℤ ∨ (𝑃 pCnt (𝐴 + 𝐵)) = +∞)) |
56 | | zq 9691 |
. . . . . . . . . . 11
⊢ ((𝑃 pCnt (𝐴 + 𝐵)) ∈ ℤ → (𝑃 pCnt (𝐴 + 𝐵)) ∈ ℚ) |
57 | 56 | orim1i 761 |
. . . . . . . . . 10
⊢ (((𝑃 pCnt (𝐴 + 𝐵)) ∈ ℤ ∨ (𝑃 pCnt (𝐴 + 𝐵)) = +∞) → ((𝑃 pCnt (𝐴 + 𝐵)) ∈ ℚ ∨ (𝑃 pCnt (𝐴 + 𝐵)) = +∞)) |
58 | 55, 57 | syl 14 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 + 𝐵) ∈ ℚ) → ((𝑃 pCnt (𝐴 + 𝐵)) ∈ ℚ ∨ (𝑃 pCnt (𝐴 + 𝐵)) = +∞)) |
59 | 1, 7, 58 | syl2anc 411 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃 pCnt (𝐴 + 𝐵)) ∈ ℚ ∨ (𝑃 pCnt (𝐴 + 𝐵)) = +∞)) |
60 | | xqltnle 10336 |
. . . . . . . 8
⊢ ((((𝑃 pCnt (𝐴 + 𝐵)) ∈ ℚ ∨ (𝑃 pCnt (𝐴 + 𝐵)) = +∞) ∧ ((𝑃 pCnt 𝐵) ∈ ℚ ∨ (𝑃 pCnt 𝐵) = +∞)) → ((𝑃 pCnt (𝐴 + 𝐵)) < (𝑃 pCnt 𝐵) ↔ ¬ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵)))) |
61 | 59, 26, 60 | syl2anc 411 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 pCnt (𝐴 + 𝐵)) < (𝑃 pCnt 𝐵) ↔ ¬ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵)))) |
62 | 54, 61 | mpbird 167 |
. . . . . 6
⊢ (𝜑 → (𝑃 pCnt (𝐴 + 𝐵)) < (𝑃 pCnt 𝐵)) |
63 | 9, 11, 62 | xrltled 9865 |
. . . . 5
⊢ (𝜑 → (𝑃 pCnt (𝐴 + 𝐵)) ≤ (𝑃 pCnt 𝐵)) |
64 | 63, 34 | breqtrrd 4057 |
. . . 4
⊢ (𝜑 → (𝑃 pCnt (𝐴 + 𝐵)) ≤ (𝑃 pCnt -𝐵)) |
65 | 1, 7, 16, 64 | pcadd 12478 |
. . 3
⊢ (𝜑 → (𝑃 pCnt (𝐴 + 𝐵)) ≤ (𝑃 pCnt ((𝐴 + 𝐵) + -𝐵))) |
66 | 43, 40, 41 | addassd 8042 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝐵) + -𝐵) = (𝐴 + (𝐵 + -𝐵))) |
67 | 46 | oveq2d 5934 |
. . . . 5
⊢ (𝜑 → (𝐴 + (𝐵 + -𝐵)) = (𝐴 + 0)) |
68 | 66, 67, 49 | 3eqtrd 2230 |
. . . 4
⊢ (𝜑 → ((𝐴 + 𝐵) + -𝐵) = 𝐴) |
69 | 68 | oveq2d 5934 |
. . 3
⊢ (𝜑 → (𝑃 pCnt ((𝐴 + 𝐵) + -𝐵)) = (𝑃 pCnt 𝐴)) |
70 | 65, 69 | breqtrd 4055 |
. 2
⊢ (𝜑 → (𝑃 pCnt (𝐴 + 𝐵)) ≤ (𝑃 pCnt 𝐴)) |
71 | 4, 9, 14, 70 | xrletrid 9871 |
1
⊢ (𝜑 → (𝑃 pCnt 𝐴) = (𝑃 pCnt (𝐴 + 𝐵))) |