Proof of Theorem angpieqvdlem
Step | Hyp | Ref
| Expression |
1 | | angpieqvdlem.C |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) |
2 | | angpieqvdlem.B |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℂ) |
3 | 1, 2 | subcld 11189 |
. . . . 5
⊢ (𝜑 → (𝐶 − 𝐵) ∈ ℂ) |
4 | | angpieqvdlem.A |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
5 | 4, 2 | subcld 11189 |
. . . . 5
⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ) |
6 | | angpieqvdlem.AneB |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
7 | 4, 2, 6 | subne0d 11198 |
. . . . 5
⊢ (𝜑 → (𝐴 − 𝐵) ≠ 0) |
8 | 3, 5, 7 | divcld 11608 |
. . . 4
⊢ (𝜑 → ((𝐶 − 𝐵) / (𝐴 − 𝐵)) ∈ ℂ) |
9 | 8 | negcld 11176 |
. . 3
⊢ (𝜑 → -((𝐶 − 𝐵) / (𝐴 − 𝐵)) ∈ ℂ) |
10 | | 1cnd 10828 |
. . . 4
⊢ (𝜑 → 1 ∈
ℂ) |
11 | | angpieqvdlem.AneC |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≠ 𝐶) |
12 | 11 | necomd 2996 |
. . . . . 6
⊢ (𝜑 → 𝐶 ≠ 𝐴) |
13 | 1, 4, 2, 12 | subneintr2d 11235 |
. . . . 5
⊢ (𝜑 → (𝐶 − 𝐵) ≠ (𝐴 − 𝐵)) |
14 | 3, 5, 7, 13 | divne1d 11619 |
. . . 4
⊢ (𝜑 → ((𝐶 − 𝐵) / (𝐴 − 𝐵)) ≠ 1) |
15 | 8, 10, 14 | negned 11186 |
. . 3
⊢ (𝜑 → -((𝐶 − 𝐵) / (𝐴 − 𝐵)) ≠ -1) |
16 | 9, 15 | xov1plusxeqvd 13086 |
. 2
⊢ (𝜑 → (-((𝐶 − 𝐵) / (𝐴 − 𝐵)) ∈ ℝ+ ↔
(-((𝐶 − 𝐵) / (𝐴 − 𝐵)) / (1 + -((𝐶 − 𝐵) / (𝐴 − 𝐵)))) ∈ (0(,)1))) |
17 | 3, 5, 7 | divnegd 11621 |
. . . . . 6
⊢ (𝜑 → -((𝐶 − 𝐵) / (𝐴 − 𝐵)) = (-(𝐶 − 𝐵) / (𝐴 − 𝐵))) |
18 | 1, 2 | negsubdi2d 11205 |
. . . . . . 7
⊢ (𝜑 → -(𝐶 − 𝐵) = (𝐵 − 𝐶)) |
19 | 18 | oveq1d 7228 |
. . . . . 6
⊢ (𝜑 → (-(𝐶 − 𝐵) / (𝐴 − 𝐵)) = ((𝐵 − 𝐶) / (𝐴 − 𝐵))) |
20 | 17, 19 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → -((𝐶 − 𝐵) / (𝐴 − 𝐵)) = ((𝐵 − 𝐶) / (𝐴 − 𝐵))) |
21 | 5, 7 | dividd 11606 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 − 𝐵) / (𝐴 − 𝐵)) = 1) |
22 | 21 | oveq1d 7228 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 − 𝐵) / (𝐴 − 𝐵)) − ((𝐶 − 𝐵) / (𝐴 − 𝐵))) = (1 − ((𝐶 − 𝐵) / (𝐴 − 𝐵)))) |
23 | 5, 3, 5, 7 | divsubdird 11647 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 − 𝐵) − (𝐶 − 𝐵)) / (𝐴 − 𝐵)) = (((𝐴 − 𝐵) / (𝐴 − 𝐵)) − ((𝐶 − 𝐵) / (𝐴 − 𝐵)))) |
24 | 10, 8 | negsubd 11195 |
. . . . . . 7
⊢ (𝜑 → (1 + -((𝐶 − 𝐵) / (𝐴 − 𝐵))) = (1 − ((𝐶 − 𝐵) / (𝐴 − 𝐵)))) |
25 | 22, 23, 24 | 3eqtr4rd 2788 |
. . . . . 6
⊢ (𝜑 → (1 + -((𝐶 − 𝐵) / (𝐴 − 𝐵))) = (((𝐴 − 𝐵) − (𝐶 − 𝐵)) / (𝐴 − 𝐵))) |
26 | 4, 1, 2 | nnncan2d 11224 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 − 𝐵) − (𝐶 − 𝐵)) = (𝐴 − 𝐶)) |
27 | 26 | oveq1d 7228 |
. . . . . 6
⊢ (𝜑 → (((𝐴 − 𝐵) − (𝐶 − 𝐵)) / (𝐴 − 𝐵)) = ((𝐴 − 𝐶) / (𝐴 − 𝐵))) |
28 | 25, 27 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (1 + -((𝐶 − 𝐵) / (𝐴 − 𝐵))) = ((𝐴 − 𝐶) / (𝐴 − 𝐵))) |
29 | 20, 28 | oveq12d 7231 |
. . . 4
⊢ (𝜑 → (-((𝐶 − 𝐵) / (𝐴 − 𝐵)) / (1 + -((𝐶 − 𝐵) / (𝐴 − 𝐵)))) = (((𝐵 − 𝐶) / (𝐴 − 𝐵)) / ((𝐴 − 𝐶) / (𝐴 − 𝐵)))) |
30 | 2, 1 | subcld 11189 |
. . . . 5
⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ) |
31 | 4, 1 | subcld 11189 |
. . . . 5
⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ) |
32 | 4, 1, 11 | subne0d 11198 |
. . . . 5
⊢ (𝜑 → (𝐴 − 𝐶) ≠ 0) |
33 | 30, 31, 5, 32, 7 | divcan7d 11636 |
. . . 4
⊢ (𝜑 → (((𝐵 − 𝐶) / (𝐴 − 𝐵)) / ((𝐴 − 𝐶) / (𝐴 − 𝐵))) = ((𝐵 − 𝐶) / (𝐴 − 𝐶))) |
34 | 2, 1, 4, 1, 11 | div2subd 11658 |
. . . 4
⊢ (𝜑 → ((𝐵 − 𝐶) / (𝐴 − 𝐶)) = ((𝐶 − 𝐵) / (𝐶 − 𝐴))) |
35 | 29, 33, 34 | 3eqtrrd 2782 |
. . 3
⊢ (𝜑 → ((𝐶 − 𝐵) / (𝐶 − 𝐴)) = (-((𝐶 − 𝐵) / (𝐴 − 𝐵)) / (1 + -((𝐶 − 𝐵) / (𝐴 − 𝐵))))) |
36 | 35 | eleq1d 2822 |
. 2
⊢ (𝜑 → (((𝐶 − 𝐵) / (𝐶 − 𝐴)) ∈ (0(,)1) ↔ (-((𝐶 − 𝐵) / (𝐴 − 𝐵)) / (1 + -((𝐶 − 𝐵) / (𝐴 − 𝐵)))) ∈ (0(,)1))) |
37 | 16, 36 | bitr4d 285 |
1
⊢ (𝜑 → (-((𝐶 − 𝐵) / (𝐴 − 𝐵)) ∈ ℝ+ ↔ ((𝐶 − 𝐵) / (𝐶 − 𝐴)) ∈ (0(,)1))) |