Proof of Theorem pcadd2
Step | Hyp | Ref
| Expression |
1 | | pcadd2.1 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ℙ) |
2 | | pcadd2.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℚ) |
3 | | pcadd2.3 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℚ) |
4 | | pcadd2.4 |
. . . 4
⊢ (𝜑 → (𝑃 pCnt 𝐴) < (𝑃 pCnt 𝐵)) |
5 | | pcxcl 15403 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt 𝐴) ∈
ℝ*) |
6 | 1, 2, 5 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝑃 pCnt 𝐴) ∈
ℝ*) |
7 | | pcxcl 15403 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐵 ∈ ℚ) → (𝑃 pCnt 𝐵) ∈
ℝ*) |
8 | 1, 3, 7 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝑃 pCnt 𝐵) ∈
ℝ*) |
9 | | xrltle 11858 |
. . . . 5
⊢ (((𝑃 pCnt 𝐴) ∈ ℝ* ∧ (𝑃 pCnt 𝐵) ∈ ℝ*) → ((𝑃 pCnt 𝐴) < (𝑃 pCnt 𝐵) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵))) |
10 | 6, 8, 9 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ((𝑃 pCnt 𝐴) < (𝑃 pCnt 𝐵) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵))) |
11 | 4, 10 | mpd 15 |
. . 3
⊢ (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) |
12 | 1, 2, 3, 11 | pcadd 15431 |
. 2
⊢ (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))) |
13 | | qaddcl 11680 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ) |
14 | 2, 3, 13 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℚ) |
15 | | qnegcl 11681 |
. . . . 5
⊢ (𝐵 ∈ ℚ → -𝐵 ∈
ℚ) |
16 | 3, 15 | syl 17 |
. . . 4
⊢ (𝜑 → -𝐵 ∈ ℚ) |
17 | | xrltnle 9984 |
. . . . . . . . . 10
⊢ (((𝑃 pCnt 𝐴) ∈ ℝ* ∧ (𝑃 pCnt 𝐵) ∈ ℝ*) → ((𝑃 pCnt 𝐴) < (𝑃 pCnt 𝐵) ↔ ¬ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt 𝐴))) |
18 | 6, 8, 17 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 pCnt 𝐴) < (𝑃 pCnt 𝐵) ↔ ¬ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt 𝐴))) |
19 | 4, 18 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → ¬ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt 𝐴)) |
20 | 1 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵))) → 𝑃 ∈ ℙ) |
21 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵))) → -𝐵 ∈ ℚ) |
22 | 14 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵))) → (𝐴 + 𝐵) ∈ ℚ) |
23 | | pcneg 15416 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐵 ∈ ℚ) → (𝑃 pCnt -𝐵) = (𝑃 pCnt 𝐵)) |
24 | 1, 3, 23 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 pCnt -𝐵) = (𝑃 pCnt 𝐵)) |
25 | 24 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃 pCnt -𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵)) ↔ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵)))) |
26 | 25 | biimpar 501 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵))) → (𝑃 pCnt -𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵))) |
27 | 20, 21, 22, 26 | pcadd 15431 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵))) → (𝑃 pCnt -𝐵) ≤ (𝑃 pCnt (-𝐵 + (𝐴 + 𝐵)))) |
28 | 27 | ex 449 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵)) → (𝑃 pCnt -𝐵) ≤ (𝑃 pCnt (-𝐵 + (𝐴 + 𝐵))))) |
29 | | qcn 11678 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ ℚ → 𝐵 ∈
ℂ) |
30 | 3, 29 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ ℂ) |
31 | 30 | negcld 10258 |
. . . . . . . . . . . . 13
⊢ (𝜑 → -𝐵 ∈ ℂ) |
32 | | qcn 11678 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℂ) |
33 | 2, 32 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℂ) |
34 | 31, 33, 30 | add12d 10141 |
. . . . . . . . . . . 12
⊢ (𝜑 → (-𝐵 + (𝐴 + 𝐵)) = (𝐴 + (-𝐵 + 𝐵))) |
35 | 31, 30 | addcomd 10117 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (-𝐵 + 𝐵) = (𝐵 + -𝐵)) |
36 | 30 | negidd 10261 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 + -𝐵) = 0) |
37 | 35, 36 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (-𝐵 + 𝐵) = 0) |
38 | 37 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 + (-𝐵 + 𝐵)) = (𝐴 + 0)) |
39 | 33 | addid1d 10115 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 + 0) = 𝐴) |
40 | 34, 38, 39 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ (𝜑 → (-𝐵 + (𝐴 + 𝐵)) = 𝐴) |
41 | 40 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 pCnt (-𝐵 + (𝐴 + 𝐵))) = (𝑃 pCnt 𝐴)) |
42 | 24, 41 | breq12d 4596 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 pCnt -𝐵) ≤ (𝑃 pCnt (-𝐵 + (𝐴 + 𝐵))) ↔ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt 𝐴))) |
43 | 28, 42 | sylibd 228 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵)) → (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt 𝐴))) |
44 | 19, 43 | mtod 188 |
. . . . . . 7
⊢ (𝜑 → ¬ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵))) |
45 | | pcxcl 15403 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 + 𝐵) ∈ ℚ) → (𝑃 pCnt (𝐴 + 𝐵)) ∈
ℝ*) |
46 | 1, 14, 45 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt (𝐴 + 𝐵)) ∈
ℝ*) |
47 | | xrltnle 9984 |
. . . . . . . 8
⊢ (((𝑃 pCnt (𝐴 + 𝐵)) ∈ ℝ* ∧ (𝑃 pCnt 𝐵) ∈ ℝ*) → ((𝑃 pCnt (𝐴 + 𝐵)) < (𝑃 pCnt 𝐵) ↔ ¬ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵)))) |
48 | 46, 8, 47 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 pCnt (𝐴 + 𝐵)) < (𝑃 pCnt 𝐵) ↔ ¬ (𝑃 pCnt 𝐵) ≤ (𝑃 pCnt (𝐴 + 𝐵)))) |
49 | 44, 48 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → (𝑃 pCnt (𝐴 + 𝐵)) < (𝑃 pCnt 𝐵)) |
50 | | xrltle 11858 |
. . . . . . 7
⊢ (((𝑃 pCnt (𝐴 + 𝐵)) ∈ ℝ* ∧ (𝑃 pCnt 𝐵) ∈ ℝ*) → ((𝑃 pCnt (𝐴 + 𝐵)) < (𝑃 pCnt 𝐵) → (𝑃 pCnt (𝐴 + 𝐵)) ≤ (𝑃 pCnt 𝐵))) |
51 | 46, 8, 50 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((𝑃 pCnt (𝐴 + 𝐵)) < (𝑃 pCnt 𝐵) → (𝑃 pCnt (𝐴 + 𝐵)) ≤ (𝑃 pCnt 𝐵))) |
52 | 49, 51 | mpd 15 |
. . . . 5
⊢ (𝜑 → (𝑃 pCnt (𝐴 + 𝐵)) ≤ (𝑃 pCnt 𝐵)) |
53 | 52, 24 | breqtrrd 4611 |
. . . 4
⊢ (𝜑 → (𝑃 pCnt (𝐴 + 𝐵)) ≤ (𝑃 pCnt -𝐵)) |
54 | 1, 14, 16, 53 | pcadd 15431 |
. . 3
⊢ (𝜑 → (𝑃 pCnt (𝐴 + 𝐵)) ≤ (𝑃 pCnt ((𝐴 + 𝐵) + -𝐵))) |
55 | 33, 30, 31 | addassd 9941 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝐵) + -𝐵) = (𝐴 + (𝐵 + -𝐵))) |
56 | 36 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (𝐴 + (𝐵 + -𝐵)) = (𝐴 + 0)) |
57 | 55, 56, 39 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 → ((𝐴 + 𝐵) + -𝐵) = 𝐴) |
58 | 57 | oveq2d 6565 |
. . 3
⊢ (𝜑 → (𝑃 pCnt ((𝐴 + 𝐵) + -𝐵)) = (𝑃 pCnt 𝐴)) |
59 | 54, 58 | breqtrd 4609 |
. 2
⊢ (𝜑 → (𝑃 pCnt (𝐴 + 𝐵)) ≤ (𝑃 pCnt 𝐴)) |
60 | | xrletri3 11861 |
. . 3
⊢ (((𝑃 pCnt 𝐴) ∈ ℝ* ∧ (𝑃 pCnt (𝐴 + 𝐵)) ∈ ℝ*) →
((𝑃 pCnt 𝐴) = (𝑃 pCnt (𝐴 + 𝐵)) ↔ ((𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵)) ∧ (𝑃 pCnt (𝐴 + 𝐵)) ≤ (𝑃 pCnt 𝐴)))) |
61 | 6, 46, 60 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝑃 pCnt 𝐴) = (𝑃 pCnt (𝐴 + 𝐵)) ↔ ((𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵)) ∧ (𝑃 pCnt (𝐴 + 𝐵)) ≤ (𝑃 pCnt 𝐴)))) |
62 | 12, 59, 61 | mpbir2and 959 |
1
⊢ (𝜑 → (𝑃 pCnt 𝐴) = (𝑃 pCnt (𝐴 + 𝐵))) |