Proof of Theorem ssscongptld
Step | Hyp | Ref
| Expression |
1 | | negpitopissre 25694 |
. . . . 5
⊢
(-π(,]π) ⊆ ℝ |
2 | | ax-resscn 10926 |
. . . . 5
⊢ ℝ
⊆ ℂ |
3 | 1, 2 | sstri 3931 |
. . . 4
⊢
(-π(,]π) ⊆ ℂ |
4 | | ssscongptld.angdef |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0})
↦ (ℑ‘(log‘(𝑦 / 𝑥)))) |
5 | | ssscongptld.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
6 | | ssscongptld.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℂ) |
7 | 5, 6 | subcld 11330 |
. . . . 5
⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ) |
8 | | ssscongptld.7 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
9 | 5, 6, 8 | subne0d 11339 |
. . . . 5
⊢ (𝜑 → (𝐴 − 𝐵) ≠ 0) |
10 | | ssscongptld.3 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) |
11 | 10, 6 | subcld 11330 |
. . . . 5
⊢ (𝜑 → (𝐶 − 𝐵) ∈ ℂ) |
12 | | ssscongptld.8 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ≠ 𝐶) |
13 | 12 | necomd 2999 |
. . . . . 6
⊢ (𝜑 → 𝐶 ≠ 𝐵) |
14 | 10, 6, 13 | subne0d 11339 |
. . . . 5
⊢ (𝜑 → (𝐶 − 𝐵) ≠ 0) |
15 | 4, 7, 9, 11, 14 | angcld 25953 |
. . . 4
⊢ (𝜑 → ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) ∈ (-π(,]π)) |
16 | 3, 15 | sselid 3920 |
. . 3
⊢ (𝜑 → ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) ∈ ℂ) |
17 | 16 | coscld 15838 |
. 2
⊢ (𝜑 → (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))) ∈ ℂ) |
18 | | ssscongptld.4 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ ℂ) |
19 | | ssscongptld.5 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ ℂ) |
20 | 18, 19 | subcld 11330 |
. . . . 5
⊢ (𝜑 → (𝐷 − 𝐸) ∈ ℂ) |
21 | | ssscongptld.9 |
. . . . . 6
⊢ (𝜑 → 𝐷 ≠ 𝐸) |
22 | 18, 19, 21 | subne0d 11339 |
. . . . 5
⊢ (𝜑 → (𝐷 − 𝐸) ≠ 0) |
23 | | ssscongptld.6 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ ℂ) |
24 | 23, 19 | subcld 11330 |
. . . . 5
⊢ (𝜑 → (𝐺 − 𝐸) ∈ ℂ) |
25 | | ssscongptld.10 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ≠ 𝐺) |
26 | 25 | necomd 2999 |
. . . . . 6
⊢ (𝜑 → 𝐺 ≠ 𝐸) |
27 | 23, 19, 26 | subne0d 11339 |
. . . . 5
⊢ (𝜑 → (𝐺 − 𝐸) ≠ 0) |
28 | 4, 20, 22, 24, 27 | angcld 25953 |
. . . 4
⊢ (𝜑 → ((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)) ∈ (-π(,]π)) |
29 | 3, 28 | sselid 3920 |
. . 3
⊢ (𝜑 → ((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)) ∈ ℂ) |
30 | 29 | coscld 15838 |
. 2
⊢ (𝜑 → (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))) ∈ ℂ) |
31 | 20 | abscld 15146 |
. . . 4
⊢ (𝜑 → (abs‘(𝐷 − 𝐸)) ∈ ℝ) |
32 | 31 | recnd 11001 |
. . 3
⊢ (𝜑 → (abs‘(𝐷 − 𝐸)) ∈ ℂ) |
33 | 24 | abscld 15146 |
. . . 4
⊢ (𝜑 → (abs‘(𝐺 − 𝐸)) ∈ ℝ) |
34 | 33 | recnd 11001 |
. . 3
⊢ (𝜑 → (abs‘(𝐺 − 𝐸)) ∈ ℂ) |
35 | 32, 34 | mulcld 10993 |
. 2
⊢ (𝜑 → ((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) ∈ ℂ) |
36 | 20, 22 | absne0d 15157 |
. . 3
⊢ (𝜑 → (abs‘(𝐷 − 𝐸)) ≠ 0) |
37 | 24, 27 | absne0d 15157 |
. . 3
⊢ (𝜑 → (abs‘(𝐺 − 𝐸)) ≠ 0) |
38 | 32, 34, 36, 37 | mulne0d 11625 |
. 2
⊢ (𝜑 → ((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) ≠ 0) |
39 | | ssscongptld.11 |
. . . . 5
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) = (abs‘(𝐷 − 𝐸))) |
40 | | ssscongptld.12 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) = (abs‘(𝐸 − 𝐺))) |
41 | 10, 6 | abssubd 15163 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐶 − 𝐵)) = (abs‘(𝐵 − 𝐶))) |
42 | 23, 19 | abssubd 15163 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐺 − 𝐸)) = (abs‘(𝐸 − 𝐺))) |
43 | 40, 41, 42 | 3eqtr4d 2788 |
. . . . 5
⊢ (𝜑 → (abs‘(𝐶 − 𝐵)) = (abs‘(𝐺 − 𝐸))) |
44 | 39, 43 | oveq12d 7295 |
. . . 4
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) = ((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸)))) |
45 | 44 | oveq1d 7292 |
. . 3
⊢ (𝜑 → (((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))) = (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))))) |
46 | 39, 32 | eqeltrd 2839 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ∈ ℂ) |
47 | 43, 34 | eqeltrd 2839 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐶 − 𝐵)) ∈ ℂ) |
48 | 46, 47 | mulcld 10993 |
. . . . 5
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) ∈ ℂ) |
49 | 48, 17 | mulcld 10993 |
. . . 4
⊢ (𝜑 → (((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))) ∈ ℂ) |
50 | 35, 30 | mulcld 10993 |
. . . 4
⊢ (𝜑 → (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)))) ∈ ℂ) |
51 | | 2cnd 12049 |
. . . 4
⊢ (𝜑 → 2 ∈
ℂ) |
52 | | 2ne0 12075 |
. . . . 5
⊢ 2 ≠
0 |
53 | 52 | a1i 11 |
. . . 4
⊢ (𝜑 → 2 ≠ 0) |
54 | 32 | sqcld 13860 |
. . . . . 6
⊢ (𝜑 → ((abs‘(𝐷 − 𝐸))↑2) ∈ ℂ) |
55 | 34 | sqcld 13860 |
. . . . . 6
⊢ (𝜑 → ((abs‘(𝐺 − 𝐸))↑2) ∈ ℂ) |
56 | 54, 55 | addcld 10992 |
. . . . 5
⊢ (𝜑 → (((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)) ∈ ℂ) |
57 | 51, 49 | mulcld 10993 |
. . . . 5
⊢ (𝜑 → (2 ·
(((abs‘(𝐴 −
𝐵)) ·
(abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))))) ∈ ℂ) |
58 | 51, 50 | mulcld 10993 |
. . . . 5
⊢ (𝜑 → (2 ·
(((abs‘(𝐷 −
𝐸)) ·
(abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))))) ∈ ℂ) |
59 | 39 | oveq1d 7292 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵))↑2) = ((abs‘(𝐷 − 𝐸))↑2)) |
60 | 43 | oveq1d 7292 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘(𝐶 − 𝐵))↑2) = ((abs‘(𝐺 − 𝐸))↑2)) |
61 | 59, 60 | oveq12d 7295 |
. . . . . . 7
⊢ (𝜑 → (((abs‘(𝐴 − 𝐵))↑2) + ((abs‘(𝐶 − 𝐵))↑2)) = (((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2))) |
62 | 61 | oveq1d 7292 |
. . . . . 6
⊢ (𝜑 → ((((abs‘(𝐴 − 𝐵))↑2) + ((abs‘(𝐶 − 𝐵))↑2)) − (2 ·
(((abs‘(𝐴 −
𝐵)) ·
(abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))))) = ((((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)) − (2 ·
(((abs‘(𝐴 −
𝐵)) ·
(abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))))))) |
63 | | ssscongptld.13 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(𝐶 − 𝐴)) = (abs‘(𝐺 − 𝐷))) |
64 | 63 | oveq1d 7292 |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐶 − 𝐴))↑2) = ((abs‘(𝐺 − 𝐷))↑2)) |
65 | | eqid 2738 |
. . . . . . . . 9
⊢
(abs‘(𝐴
− 𝐵)) =
(abs‘(𝐴 − 𝐵)) |
66 | | eqid 2738 |
. . . . . . . . 9
⊢
(abs‘(𝐶
− 𝐵)) =
(abs‘(𝐶 − 𝐵)) |
67 | | eqid 2738 |
. . . . . . . . 9
⊢
(abs‘(𝐶
− 𝐴)) =
(abs‘(𝐶 − 𝐴)) |
68 | | eqid 2738 |
. . . . . . . . 9
⊢ ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) = ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) |
69 | 4, 65, 66, 67, 68 | lawcos 25964 |
. . . . . . . 8
⊢ (((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) → ((abs‘(𝐶 − 𝐴))↑2) = ((((abs‘(𝐴 − 𝐵))↑2) + ((abs‘(𝐶 − 𝐵))↑2)) − (2 ·
(((abs‘(𝐴 −
𝐵)) ·
(abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))))))) |
70 | 10, 5, 6, 13, 8, 69 | syl32anc 1377 |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐶 − 𝐴))↑2) = ((((abs‘(𝐴 − 𝐵))↑2) + ((abs‘(𝐶 − 𝐵))↑2)) − (2 ·
(((abs‘(𝐴 −
𝐵)) ·
(abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))))))) |
71 | | eqid 2738 |
. . . . . . . . 9
⊢
(abs‘(𝐷
− 𝐸)) =
(abs‘(𝐷 − 𝐸)) |
72 | | eqid 2738 |
. . . . . . . . 9
⊢
(abs‘(𝐺
− 𝐸)) =
(abs‘(𝐺 − 𝐸)) |
73 | | eqid 2738 |
. . . . . . . . 9
⊢
(abs‘(𝐺
− 𝐷)) =
(abs‘(𝐺 − 𝐷)) |
74 | | eqid 2738 |
. . . . . . . . 9
⊢ ((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)) = ((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)) |
75 | 4, 71, 72, 73, 74 | lawcos 25964 |
. . . . . . . 8
⊢ (((𝐺 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ) ∧ (𝐺 ≠ 𝐸 ∧ 𝐷 ≠ 𝐸)) → ((abs‘(𝐺 − 𝐷))↑2) = ((((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)) − (2 ·
(((abs‘(𝐷 −
𝐸)) ·
(abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))))))) |
76 | 23, 18, 19, 26, 21, 75 | syl32anc 1377 |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐺 − 𝐷))↑2) = ((((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)) − (2 ·
(((abs‘(𝐷 −
𝐸)) ·
(abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))))))) |
77 | 64, 70, 76 | 3eqtr3d 2786 |
. . . . . 6
⊢ (𝜑 → ((((abs‘(𝐴 − 𝐵))↑2) + ((abs‘(𝐶 − 𝐵))↑2)) − (2 ·
(((abs‘(𝐴 −
𝐵)) ·
(abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))))) = ((((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)) − (2 ·
(((abs‘(𝐷 −
𝐸)) ·
(abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))))))) |
78 | 62, 77 | eqtr3d 2780 |
. . . . 5
⊢ (𝜑 → ((((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)) − (2 ·
(((abs‘(𝐴 −
𝐵)) ·
(abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))))) = ((((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)) − (2 ·
(((abs‘(𝐷 −
𝐸)) ·
(abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))))))) |
79 | 56, 57, 58, 78 | subcand 11371 |
. . . 4
⊢ (𝜑 → (2 ·
(((abs‘(𝐴 −
𝐵)) ·
(abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))))) = (2 · (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)))))) |
80 | 49, 50, 51, 53, 79 | mulcanad 11608 |
. . 3
⊢ (𝜑 → (((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))) = (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))))) |
81 | 45, 80 | eqtr3d 2780 |
. 2
⊢ (𝜑 → (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))) = (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))))) |
82 | 17, 30, 35, 38, 81 | mulcanad 11608 |
1
⊢ (𝜑 → (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))) = (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)))) |