Proof of Theorem heron
Step | Hyp | Ref
| Expression |
1 | | 1red 10379 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
2 | 1 | rehalfcld 11634 |
. . . . 5
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
3 | | heron.x |
. . . . . . 7
⊢ 𝑋 = (abs‘(𝐵 − 𝐶)) |
4 | | heron.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℂ) |
5 | | heron.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) |
6 | 4, 5 | subcld 10736 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ) |
7 | 6 | abscld 14590 |
. . . . . . 7
⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) ∈ ℝ) |
8 | 3, 7 | syl5eqel 2863 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ ℝ) |
9 | | heron.y |
. . . . . . 7
⊢ 𝑌 = (abs‘(𝐴 − 𝐶)) |
10 | | heron.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
11 | 10, 5 | subcld 10736 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ) |
12 | 11 | abscld 14590 |
. . . . . . 7
⊢ (𝜑 → (abs‘(𝐴 − 𝐶)) ∈ ℝ) |
13 | 9, 12 | syl5eqel 2863 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ ℝ) |
14 | 8, 13 | remulcld 10409 |
. . . . 5
⊢ (𝜑 → (𝑋 · 𝑌) ∈ ℝ) |
15 | 2, 14 | remulcld 10409 |
. . . 4
⊢ (𝜑 → ((1 / 2) · (𝑋 · 𝑌)) ∈ ℝ) |
16 | | heron.o |
. . . . . . 7
⊢ 𝑂 = ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) |
17 | | negpitopissre 24735 |
. . . . . . . . 9
⊢
(-π(,]π) ⊆ ℝ |
18 | | heron.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0})
↦ (ℑ‘(log‘(𝑦 / 𝑥)))) |
19 | | heron.bc |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ≠ 𝐶) |
20 | 4, 5, 19 | subne0d 10745 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐶) ≠ 0) |
21 | | heron.ac |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≠ 𝐶) |
22 | 10, 5, 21 | subne0d 10745 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 − 𝐶) ≠ 0) |
23 | 18, 6, 20, 11, 22 | angcld 24994 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ (-π(,]π)) |
24 | 17, 23 | sseldi 3819 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ ℝ) |
25 | 24 | recnd 10407 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ ℂ) |
26 | 16, 25 | syl5eqel 2863 |
. . . . . 6
⊢ (𝜑 → 𝑂 ∈ ℂ) |
27 | 26 | sincld 15271 |
. . . . 5
⊢ (𝜑 → (sin‘𝑂) ∈
ℂ) |
28 | 27 | abscld 14590 |
. . . 4
⊢ (𝜑 →
(abs‘(sin‘𝑂))
∈ ℝ) |
29 | 15, 28 | remulcld 10409 |
. . 3
⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))) ∈
ℝ) |
30 | | 0re 10380 |
. . . . . . 7
⊢ 0 ∈
ℝ |
31 | | halfre 11601 |
. . . . . . 7
⊢ (1 / 2)
∈ ℝ |
32 | | halfgt0 11603 |
. . . . . . 7
⊢ 0 < (1
/ 2) |
33 | 30, 31, 32 | ltleii 10501 |
. . . . . 6
⊢ 0 ≤ (1
/ 2) |
34 | 33 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ≤ (1 /
2)) |
35 | 6 | absge0d 14598 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (abs‘(𝐵 − 𝐶))) |
36 | 35, 3 | syl6breqr 4930 |
. . . . . 6
⊢ (𝜑 → 0 ≤ 𝑋) |
37 | 11 | absge0d 14598 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (abs‘(𝐴 − 𝐶))) |
38 | 37, 9 | syl6breqr 4930 |
. . . . . 6
⊢ (𝜑 → 0 ≤ 𝑌) |
39 | 8, 13, 36, 38 | mulge0d 10955 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝑋 · 𝑌)) |
40 | 2, 14, 34, 39 | mulge0d 10955 |
. . . 4
⊢ (𝜑 → 0 ≤ ((1 / 2) ·
(𝑋 · 𝑌))) |
41 | 27 | absge0d 14598 |
. . . 4
⊢ (𝜑 → 0 ≤
(abs‘(sin‘𝑂))) |
42 | 15, 28, 40, 41 | mulge0d 10955 |
. . 3
⊢ (𝜑 → 0 ≤ (((1 / 2) ·
(𝑋 · 𝑌)) ·
(abs‘(sin‘𝑂)))) |
43 | 29, 42 | sqrtsqd 14573 |
. 2
⊢ (𝜑 → (√‘((((1 / 2)
· (𝑋 · 𝑌)) ·
(abs‘(sin‘𝑂)))↑2)) = (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))) |
44 | | halfcn 11602 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
45 | 44 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (1 / 2) ∈
ℂ) |
46 | 8 | recnd 10407 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℂ) |
47 | 13 | recnd 10407 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℂ) |
48 | 46, 47 | mulcld 10399 |
. . . . . 6
⊢ (𝜑 → (𝑋 · 𝑌) ∈ ℂ) |
49 | 45, 48 | mulcld 10399 |
. . . . 5
⊢ (𝜑 → ((1 / 2) · (𝑋 · 𝑌)) ∈ ℂ) |
50 | 28 | recnd 10407 |
. . . . 5
⊢ (𝜑 →
(abs‘(sin‘𝑂))
∈ ℂ) |
51 | 49, 50 | sqmuld 13344 |
. . . 4
⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2) = ((((1 / 2)
· (𝑋 · 𝑌))↑2) ·
((abs‘(sin‘𝑂))↑2))) |
52 | | 2cnd 11458 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℂ) |
53 | | 2ne0 11491 |
. . . . . . . 8
⊢ 2 ≠
0 |
54 | 53 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2 ≠ 0) |
55 | 48, 52, 54 | sqdivd 13345 |
. . . . . 6
⊢ (𝜑 → (((𝑋 · 𝑌) / 2)↑2) = (((𝑋 · 𝑌)↑2) / (2↑2))) |
56 | 48, 52, 54 | divrec2d 11158 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 · 𝑌) / 2) = ((1 / 2) · (𝑋 · 𝑌))) |
57 | 56 | oveq1d 6939 |
. . . . . 6
⊢ (𝜑 → (((𝑋 · 𝑌) / 2)↑2) = (((1 / 2) · (𝑋 · 𝑌))↑2)) |
58 | | sq2 13284 |
. . . . . . . 8
⊢
(2↑2) = 4 |
59 | 58 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (2↑2) =
4) |
60 | 59 | oveq2d 6940 |
. . . . . 6
⊢ (𝜑 → (((𝑋 · 𝑌)↑2) / (2↑2)) = (((𝑋 · 𝑌)↑2) / 4)) |
61 | 55, 57, 60 | 3eqtr3d 2822 |
. . . . 5
⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌))↑2) = (((𝑋 · 𝑌)↑2) / 4)) |
62 | 16, 24 | syl5eqel 2863 |
. . . . . . 7
⊢ (𝜑 → 𝑂 ∈ ℝ) |
63 | 62 | resincld 15284 |
. . . . . 6
⊢ (𝜑 → (sin‘𝑂) ∈
ℝ) |
64 | | absresq 14456 |
. . . . . 6
⊢
((sin‘𝑂)
∈ ℝ → ((abs‘(sin‘𝑂))↑2) = ((sin‘𝑂)↑2)) |
65 | 63, 64 | syl 17 |
. . . . 5
⊢ (𝜑 →
((abs‘(sin‘𝑂))↑2) = ((sin‘𝑂)↑2)) |
66 | 61, 65 | oveq12d 6942 |
. . . 4
⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌))↑2) ·
((abs‘(sin‘𝑂))↑2)) = ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2))) |
67 | 48 | sqcld 13330 |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 · 𝑌)↑2) ∈ ℂ) |
68 | 27 | sqcld 13330 |
. . . . . . . 8
⊢ (𝜑 → ((sin‘𝑂)↑2) ∈
ℂ) |
69 | 67, 68 | mulcld 10399 |
. . . . . . 7
⊢ (𝜑 → (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) ∈
ℂ) |
70 | | 4cn 11466 |
. . . . . . . . 9
⊢ 4 ∈
ℂ |
71 | 70 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 4 ∈
ℂ) |
72 | | heron.s |
. . . . . . . . . . . 12
⊢ 𝑆 = (((𝑋 + 𝑌) + 𝑍) / 2) |
73 | 8, 13 | readdcld 10408 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 + 𝑌) ∈ ℝ) |
74 | | heron.z |
. . . . . . . . . . . . . . 15
⊢ 𝑍 = (abs‘(𝐴 − 𝐵)) |
75 | 10, 4 | subcld 10736 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ) |
76 | 75 | abscld 14590 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ∈ ℝ) |
77 | 74, 76 | syl5eqel 2863 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑍 ∈ ℝ) |
78 | 73, 77 | readdcld 10408 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) ∈ ℝ) |
79 | 78 | rehalfcld 11634 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) / 2) ∈ ℝ) |
80 | 72, 79 | syl5eqel 2863 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ ℝ) |
81 | 80 | recnd 10407 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℂ) |
82 | 81, 46 | subcld 10736 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 − 𝑋) ∈ ℂ) |
83 | 81, 82 | mulcld 10399 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 · (𝑆 − 𝑋)) ∈ ℂ) |
84 | 81, 47 | subcld 10736 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 − 𝑌) ∈ ℂ) |
85 | 77 | recnd 10407 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑍 ∈ ℂ) |
86 | 81, 85 | subcld 10736 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 − 𝑍) ∈ ℂ) |
87 | 84, 86 | mulcld 10399 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑆 − 𝑌) · (𝑆 − 𝑍)) ∈ ℂ) |
88 | 83, 87 | mulcld 10399 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ) |
89 | 71, 88 | mulcld 10399 |
. . . . . . 7
⊢ (𝜑 → (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) ∈ ℂ) |
90 | | 4ne0 11495 |
. . . . . . . 8
⊢ 4 ≠
0 |
91 | 90 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 4 ≠ 0) |
92 | 52, 48 | sqmuld 13344 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = ((2↑2) · ((𝑋 · 𝑌)↑2))) |
93 | 59 | oveq1d 6939 |
. . . . . . . . . 10
⊢ (𝜑 → ((2↑2) ·
((𝑋 · 𝑌)↑2)) = (4 · ((𝑋 · 𝑌)↑2))) |
94 | 92, 93 | eqtr2d 2815 |
. . . . . . . . 9
⊢ (𝜑 → (4 · ((𝑋 · 𝑌)↑2)) = ((2 · (𝑋 · 𝑌))↑2)) |
95 | 94 | oveq1d 6939 |
. . . . . . . 8
⊢ (𝜑 → ((4 · ((𝑋 · 𝑌)↑2)) · ((sin‘𝑂)↑2)) = (((2 ·
(𝑋 · 𝑌))↑2) ·
((sin‘𝑂)↑2))) |
96 | 71, 67, 68 | mulassd 10402 |
. . . . . . . 8
⊢ (𝜑 → ((4 · ((𝑋 · 𝑌)↑2)) · ((sin‘𝑂)↑2)) = (4 ·
(((𝑋 · 𝑌)↑2) ·
((sin‘𝑂)↑2)))) |
97 | 52, 48 | mulcld 10399 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · (𝑋 · 𝑌)) ∈ ℂ) |
98 | 97 | sqcld 13330 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) ∈ ℂ) |
99 | 98, 68 | mulcld 10399 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) ∈
ℂ) |
100 | 47, 85 | mulcld 10399 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 · 𝑍) ∈ ℂ) |
101 | 52, 100 | mulcld 10399 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · (𝑌 · 𝑍)) ∈ ℂ) |
102 | 101 | sqcld 13330 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) ∈ ℂ) |
103 | 47 | sqcld 13330 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌↑2) ∈ ℂ) |
104 | 85 | sqcld 13330 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑍↑2) ∈ ℂ) |
105 | 46 | sqcld 13330 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋↑2) ∈ ℂ) |
106 | 104, 105 | subcld 10736 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑍↑2) − (𝑋↑2)) ∈ ℂ) |
107 | 103, 106 | addcld 10398 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) ∈ ℂ) |
108 | 107 | sqcld 13330 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) ∈
ℂ) |
109 | 102, 108 | subcld 10736 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) ∈
ℂ) |
110 | 26 | coscld 15272 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (cos‘𝑂) ∈
ℂ) |
111 | 110 | sqcld 13330 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((cos‘𝑂)↑2) ∈
ℂ) |
112 | 98, 111 | mulcld 10399 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)) ∈
ℂ) |
113 | | sincossq 15317 |
. . . . . . . . . . . . . 14
⊢ (𝑂 ∈ ℂ →
(((sin‘𝑂)↑2) +
((cos‘𝑂)↑2)) =
1) |
114 | 26, 113 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2)) = 1) |
115 | 114 | oveq2d 6940 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2))) = (((2 ·
(𝑋 · 𝑌))↑2) ·
1)) |
116 | 98, 68, 111 | adddid 10403 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2))) = ((((2 ·
(𝑋 · 𝑌))↑2) ·
((sin‘𝑂)↑2)) +
(((2 · (𝑋 ·
𝑌))↑2) ·
((cos‘𝑂)↑2)))) |
117 | 103 | 2timesd 11630 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2 · (𝑌↑2)) = ((𝑌↑2) + (𝑌↑2))) |
118 | 103, 106,
103 | ppncand 10776 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) = ((𝑌↑2) + (𝑌↑2))) |
119 | 117, 118 | eqtr4d 2817 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · (𝑌↑2)) = (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))))) |
120 | 106 | 2timesd 11630 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2 · ((𝑍↑2) − (𝑋↑2))) = (((𝑍↑2) − (𝑋↑2)) + ((𝑍↑2) − (𝑋↑2)))) |
121 | 103, 106,
106 | pnncand 10775 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) = (((𝑍↑2) − (𝑋↑2)) + ((𝑍↑2) − (𝑋↑2)))) |
122 | 120, 121 | eqtr4d 2817 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · ((𝑍↑2) − (𝑋↑2))) = (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))))) |
123 | 119, 122 | oveq12d 6942 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 · (𝑌↑2)) · (2 ·
((𝑍↑2) − (𝑋↑2)))) = ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) · (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))))) |
124 | | 2t2e4 11551 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· 2) = 4 |
125 | 124, 71 | syl5eqel 2863 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2 · 2) ∈
ℂ) |
126 | 125, 103,
106 | mulassd 10402 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((2 · 2) ·
(𝑌↑2)) ·
((𝑍↑2) − (𝑋↑2))) = ((2 · 2)
· ((𝑌↑2)
· ((𝑍↑2)
− (𝑋↑2))))) |
127 | 125, 103 | mulcld 10399 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((2 · 2) ·
(𝑌↑2)) ∈
ℂ) |
128 | 127, 104,
105 | subdid 10834 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((2 · 2) ·
(𝑌↑2)) ·
((𝑍↑2) − (𝑋↑2))) = ((((2 · 2)
· (𝑌↑2))
· (𝑍↑2))
− (((2 · 2) · (𝑌↑2)) · (𝑋↑2)))) |
129 | 52 | sqvald 13329 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (2↑2) = (2 ·
2)) |
130 | 47, 85 | sqmuld 13344 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑌 · 𝑍)↑2) = ((𝑌↑2) · (𝑍↑2))) |
131 | 129, 130 | oveq12d 6942 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((2↑2) ·
((𝑌 · 𝑍)↑2)) = ((2 · 2)
· ((𝑌↑2)
· (𝑍↑2)))) |
132 | 52, 100 | sqmuld 13344 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) = ((2↑2) · ((𝑌 · 𝑍)↑2))) |
133 | 125, 103,
104 | mulassd 10402 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((2 · 2) ·
(𝑌↑2)) · (𝑍↑2)) = ((2 · 2)
· ((𝑌↑2)
· (𝑍↑2)))) |
134 | 131, 132,
133 | 3eqtr4d 2824 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) = (((2 · 2) ·
(𝑌↑2)) · (𝑍↑2))) |
135 | 46, 47 | sqmuld 13344 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑋 · 𝑌)↑2) = ((𝑋↑2) · (𝑌↑2))) |
136 | 105, 103 | mulcomd 10400 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑋↑2) · (𝑌↑2)) = ((𝑌↑2) · (𝑋↑2))) |
137 | 135, 136 | eqtrd 2814 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑋 · 𝑌)↑2) = ((𝑌↑2) · (𝑋↑2))) |
138 | 129, 137 | oveq12d 6942 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((2↑2) ·
((𝑋 · 𝑌)↑2)) = ((2 · 2)
· ((𝑌↑2)
· (𝑋↑2)))) |
139 | 125, 103,
105 | mulassd 10402 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((2 · 2) ·
(𝑌↑2)) · (𝑋↑2)) = ((2 · 2)
· ((𝑌↑2)
· (𝑋↑2)))) |
140 | 138, 92, 139 | 3eqtr4d 2824 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = (((2 · 2) ·
(𝑌↑2)) · (𝑋↑2))) |
141 | 134, 140 | oveq12d 6942 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((((2 · 2) ·
(𝑌↑2)) · (𝑍↑2)) − (((2 ·
2) · (𝑌↑2))
· (𝑋↑2)))) |
142 | 128, 141 | eqtr4d 2817 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((2 · 2) ·
(𝑌↑2)) ·
((𝑍↑2) − (𝑋↑2))) = (((2 ·
(𝑌 · 𝑍))↑2) − ((2 ·
(𝑋 · 𝑌))↑2))) |
143 | 52, 52, 103, 106 | mul4d 10590 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 · 2) ·
((𝑌↑2) ·
((𝑍↑2) − (𝑋↑2)))) = ((2 ·
(𝑌↑2)) · (2
· ((𝑍↑2)
− (𝑋↑2))))) |
144 | 126, 142,
143 | 3eqtr3d 2822 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((2 · (𝑌↑2)) · (2 ·
((𝑍↑2) − (𝑋↑2))))) |
145 | 103, 106 | subcld 10736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) ∈ ℂ) |
146 | | subsq 13296 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) ∈ ℂ ∧ ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) ∈ ℂ)
→ ((((𝑌↑2) +
((𝑍↑2) − (𝑋↑2)))↑2) −
(((𝑌↑2) −
((𝑍↑2) − (𝑋↑2)))↑2)) = ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) · (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))))) |
147 | 107, 145,
146 | syl2anc 579 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) − (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2)) = ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) · (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))))) |
148 | 123, 144,
147 | 3eqtr4d 2824 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) − (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2))) |
149 | 148 | oveq2d 6940 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2))) = (((2 · (𝑌 · 𝑍))↑2) − ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) − (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2)))) |
150 | 102, 98 | nncand 10741 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2))) = ((2 · (𝑋 · 𝑌))↑2)) |
151 | 145 | sqcld 13330 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2) ∈
ℂ) |
152 | 102, 108,
151 | subsubd 10764 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) − (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2))) = ((((2
· (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2))) |
153 | 149, 150,
152 | 3eqtr3d 2822 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = ((((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2))) |
154 | 98 | mulid1d 10396 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · 1) = ((2 · (𝑋 · 𝑌))↑2)) |
155 | 105, 103 | addcld 10398 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑋↑2) + (𝑌↑2)) ∈ ℂ) |
156 | 48, 110 | mulcld 10399 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑋 · 𝑌) · (cos‘𝑂)) ∈ ℂ) |
157 | 52, 156 | mulcld 10399 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2 · ((𝑋 · 𝑌) · (cos‘𝑂))) ∈ ℂ) |
158 | 155, 157 | nncand 10741 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))) = (2 · ((𝑋 · 𝑌) · (cos‘𝑂)))) |
159 | 103, 104 | subcld 10736 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑌↑2) − (𝑍↑2)) ∈ ℂ) |
160 | 159, 105 | addcomd 10580 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((𝑌↑2) − (𝑍↑2)) + (𝑋↑2)) = ((𝑋↑2) + ((𝑌↑2) − (𝑍↑2)))) |
161 | 103, 104,
105 | subsubd 10764 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑌↑2) − (𝑍↑2)) + (𝑋↑2))) |
162 | 105, 103,
104 | addsubassd 10756 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2)) = ((𝑋↑2) + ((𝑌↑2) − (𝑍↑2)))) |
163 | 160, 161,
162 | 3eqtr4d 2824 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2))) |
164 | 18, 3, 9, 74, 16 | lawcos 25005 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝑍↑2) = (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))) |
165 | 10, 4, 5, 21, 19, 164 | syl32anc 1446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑍↑2) = (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))) |
166 | 165 | oveq2d 6940 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2)) = (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂)))))) |
167 | 163, 166 | eqtrd 2814 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂)))))) |
168 | 52, 48, 110 | mulassd 10402 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 · (𝑋 · 𝑌)) · (cos‘𝑂)) = (2 · ((𝑋 · 𝑌) · (cos‘𝑂)))) |
169 | 158, 167,
168 | 3eqtr4d 2824 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = ((2 · (𝑋 · 𝑌)) · (cos‘𝑂))) |
170 | 169 | oveq1d 6939 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2) = (((2 · (𝑋 · 𝑌)) · (cos‘𝑂))↑2)) |
171 | 97, 110 | sqmuld 13344 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2 · (𝑋 · 𝑌)) · (cos‘𝑂))↑2) = (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2))) |
172 | 170, 171 | eqtr2d 2815 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)) = (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2)) |
173 | 172 | oveq2d 6940 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2))) = ((((2 ·
(𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2))) |
174 | 153, 154,
173 | 3eqtr4d 2824 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · 1) = ((((2 ·
(𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)))) |
175 | 115, 116,
174 | 3eqtr3d 2822 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) + (((2 ·
(𝑋 · 𝑌))↑2) ·
((cos‘𝑂)↑2))) =
((((2 · (𝑌 ·
𝑍))↑2) −
(((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((2
· (𝑋 · 𝑌))↑2) ·
((cos‘𝑂)↑2)))) |
176 | 99, 109, 112, 175 | addcan2ad 10584 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = (((2 ·
(𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2))) |
177 | | subsq 13296 |
. . . . . . . . . . 11
⊢ (((2
· (𝑌 · 𝑍)) ∈ ℂ ∧ ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) ∈ ℂ) → (((2
· (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) · ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))))) |
178 | 101, 107,
177 | syl2anc 579 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) · ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))))) |
179 | 103, 104 | addcld 10398 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌↑2) + (𝑍↑2)) ∈ ℂ) |
180 | 101, 179,
105 | addsubassd 10756 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2)) = ((2 · (𝑌 · 𝑍)) + (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2)))) |
181 | 103, 104,
105 | addsubassd 10756 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2)) = ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) |
182 | 181 | oveq2d 6940 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))) |
183 | 180, 182 | eqtr2d 2815 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2))) |
184 | | binom2 13303 |
. . . . . . . . . . . . . . 15
⊢ ((𝑌 ∈ ℂ ∧ 𝑍 ∈ ℂ) → ((𝑌 + 𝑍)↑2) = (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2))) |
185 | 47, 85, 184 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 + 𝑍)↑2) = (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2))) |
186 | 103, 101,
104 | add32d 10605 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2)) = (((𝑌↑2) + (𝑍↑2)) + (2 · (𝑌 · 𝑍)))) |
187 | 179, 101 | addcomd 10580 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) + (2 · (𝑌 · 𝑍))) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2)))) |
188 | 185, 186,
187 | 3eqtrd 2818 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 + 𝑍)↑2) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2)))) |
189 | 188 | oveq1d 6939 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2))) |
190 | 47, 85 | addcld 10398 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌 + 𝑍) ∈ ℂ) |
191 | | subsq 13296 |
. . . . . . . . . . . . . . 15
⊢ (((𝑌 + 𝑍) ∈ ℂ ∧ 𝑋 ∈ ℂ) → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋))) |
192 | 190, 46, 191 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋))) |
193 | 72 | oveq2i 6935 |
. . . . . . . . . . . . . . . . 17
⊢ (2
· 𝑆) = (2 ·
(((𝑋 + 𝑌) + 𝑍) / 2)) |
194 | 78 | recnd 10407 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) ∈ ℂ) |
195 | 194, 52, 54 | divcan2d 11156 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · (((𝑋 + 𝑌) + 𝑍) / 2)) = ((𝑋 + 𝑌) + 𝑍)) |
196 | 193, 195 | syl5eq 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 · 𝑆) = ((𝑋 + 𝑌) + 𝑍)) |
197 | 46, 47, 85 | addassd 10401 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
198 | 46, 190 | addcomd 10580 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋 + (𝑌 + 𝑍)) = ((𝑌 + 𝑍) + 𝑋)) |
199 | 196, 197,
198 | 3eqtrd 2818 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 · 𝑆) = ((𝑌 + 𝑍) + 𝑋)) |
200 | 52, 81, 46 | subdid 10834 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 · (𝑆 − 𝑋)) = ((2 · 𝑆) − (2 · 𝑋))) |
201 | 196, 197 | eqtrd 2814 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · 𝑆) = (𝑋 + (𝑌 + 𝑍))) |
202 | 46 | 2timesd 11630 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · 𝑋) = (𝑋 + 𝑋)) |
203 | 201, 202 | oveq12d 6942 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑋)) = ((𝑋 + (𝑌 + 𝑍)) − (𝑋 + 𝑋))) |
204 | 46, 190, 46 | pnpcand 10773 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑋 + (𝑌 + 𝑍)) − (𝑋 + 𝑋)) = ((𝑌 + 𝑍) − 𝑋)) |
205 | 200, 203,
204 | 3eqtrd 2818 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 · (𝑆 − 𝑋)) = ((𝑌 + 𝑍) − 𝑋)) |
206 | 199, 205 | oveq12d 6942 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 · 𝑆) · (2 · (𝑆 − 𝑋))) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋))) |
207 | 192, 206 | eqtr4d 2817 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = ((2 · 𝑆) · (2 · (𝑆 − 𝑋)))) |
208 | 52, 81, 52, 82 | mul4d 10590 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 𝑆) · (2 · (𝑆 − 𝑋))) = ((2 · 2) · (𝑆 · (𝑆 − 𝑋)))) |
209 | 124 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 · 2) =
4) |
210 | 209 | oveq1d 6939 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 2) ·
(𝑆 · (𝑆 − 𝑋))) = (4 · (𝑆 · (𝑆 − 𝑋)))) |
211 | 207, 208,
210 | 3eqtrd 2818 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (4 · (𝑆 · (𝑆 − 𝑋)))) |
212 | 183, 189,
211 | 3eqtr2d 2820 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (4 · (𝑆 · (𝑆 − 𝑋)))) |
213 | 101, 179 | subcld 10736 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) ∈ ℂ) |
214 | 213, 105 | addcomd 10580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2)) = ((𝑋↑2) + ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))))) |
215 | 181 | oveq2d 6940 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))) |
216 | 101, 179,
105 | subsubd 10764 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2))) |
217 | 215, 216 | eqtr3d 2816 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2))) |
218 | 105, 179,
101 | subsub2d 10765 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍)))) = ((𝑋↑2) + ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))))) |
219 | 214, 217,
218 | 3eqtr4d 2824 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))))) |
220 | 103, 104,
101 | addsubassd 10756 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = ((𝑌↑2) + ((𝑍↑2) − (2 · (𝑌 · 𝑍))))) |
221 | 104, 101 | subcld 10736 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑍↑2) − (2 · (𝑌 · 𝑍))) ∈ ℂ) |
222 | 103, 221 | addcomd 10580 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑌↑2) + ((𝑍↑2) − (2 · (𝑌 · 𝑍)))) = (((𝑍↑2) − (2 · (𝑌 · 𝑍))) + (𝑌↑2))) |
223 | 47, 85 | mulcomd 10400 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑌 · 𝑍) = (𝑍 · 𝑌)) |
224 | 223 | oveq2d 6940 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · (𝑌 · 𝑍)) = (2 · (𝑍 · 𝑌))) |
225 | 224 | oveq2d 6940 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑍↑2) − (2 · (𝑌 · 𝑍))) = ((𝑍↑2) − (2 · (𝑍 · 𝑌)))) |
226 | 225 | oveq1d 6939 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑍↑2) − (2 · (𝑌 · 𝑍))) + (𝑌↑2)) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2))) |
227 | 220, 222,
226 | 3eqtrd 2818 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2))) |
228 | | binom2sub 13305 |
. . . . . . . . . . . . . . 15
⊢ ((𝑍 ∈ ℂ ∧ 𝑌 ∈ ℂ) → ((𝑍 − 𝑌)↑2) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2))) |
229 | 85, 47, 228 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑍 − 𝑌)↑2) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2))) |
230 | 227, 229 | eqtr4d 2817 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = ((𝑍 − 𝑌)↑2)) |
231 | 230 | oveq2d 6940 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍)))) = ((𝑋↑2) − ((𝑍 − 𝑌)↑2))) |
232 | 85, 47 | subcld 10736 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑍 − 𝑌) ∈ ℂ) |
233 | | subsq 13296 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ ℂ ∧ (𝑍 − 𝑌) ∈ ℂ) → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌)))) |
234 | 46, 232, 233 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌)))) |
235 | 52, 81, 47 | subdid 10834 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 · (𝑆 − 𝑌)) = ((2 · 𝑆) − (2 · 𝑌))) |
236 | 46, 47, 85 | add32d 10605 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌)) |
237 | 196, 236 | eqtrd 2814 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · 𝑆) = ((𝑋 + 𝑍) + 𝑌)) |
238 | 47 | 2timesd 11630 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · 𝑌) = (𝑌 + 𝑌)) |
239 | 237, 238 | oveq12d 6942 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑌)) = (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌))) |
240 | 46, 85 | addcld 10398 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑋 + 𝑍) ∈ ℂ) |
241 | 240, 47, 47 | pnpcan2d 10774 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌)) = ((𝑋 + 𝑍) − 𝑌)) |
242 | 46, 85, 47, 241 | assraddsubd 10792 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌)) = (𝑋 + (𝑍 − 𝑌))) |
243 | 235, 239,
242 | 3eqtrd 2818 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 · (𝑆 − 𝑌)) = (𝑋 + (𝑍 − 𝑌))) |
244 | 52, 81, 85 | subdid 10834 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 · (𝑆 − 𝑍)) = ((2 · 𝑆) − (2 · 𝑍))) |
245 | 85 | 2timesd 11630 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · 𝑍) = (𝑍 + 𝑍)) |
246 | 196, 245 | oveq12d 6942 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑍)) = (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍))) |
247 | 46, 47 | addcld 10398 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑋 + 𝑌) ∈ ℂ) |
248 | 247, 85, 85 | pnpcan2d 10774 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍)) = ((𝑋 + 𝑌) − 𝑍)) |
249 | 46, 85, 47 | subsub3d 10766 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑋 − (𝑍 − 𝑌)) = ((𝑋 + 𝑌) − 𝑍)) |
250 | 248, 249 | eqtr4d 2817 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍)) = (𝑋 − (𝑍 − 𝑌))) |
251 | 244, 246,
250 | 3eqtrd 2818 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 · (𝑆 − 𝑍)) = (𝑋 − (𝑍 − 𝑌))) |
252 | 243, 251 | oveq12d 6942 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍))) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌)))) |
253 | 234, 252 | eqtr4d 2817 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍)))) |
254 | 52, 84, 52, 86 | mul4d 10590 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍))) = ((2 · 2) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) |
255 | 209 | oveq1d 6939 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 2) ·
((𝑆 − 𝑌) · (𝑆 − 𝑍))) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) |
256 | 253, 254,
255 | 3eqtrd 2818 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) |
257 | 219, 231,
256 | 3eqtrd 2818 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) |
258 | 212, 257 | oveq12d 6942 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) · ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))) = ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))) |
259 | 176, 178,
258 | 3eqtrd 2818 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))) |
260 | 71, 87 | mulcld 10399 |
. . . . . . . . . 10
⊢ (𝜑 → (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ) |
261 | 71, 83, 260 | mulassd 10402 |
. . . . . . . . 9
⊢ (𝜑 → ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) = (4 · ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))) |
262 | 83, 71, 87 | mul12d 10587 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) = (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))) |
263 | 262 | oveq2d 6940 |
. . . . . . . . 9
⊢ (𝜑 → (4 · ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))) = (4 · (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))) |
264 | 259, 261,
263 | 3eqtrd 2818 |
. . . . . . . 8
⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = (4 · (4
· ((𝑆 ·
(𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))) |
265 | 95, 96, 264 | 3eqtr3d 2822 |
. . . . . . 7
⊢ (𝜑 → (4 · (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2))) = (4 · (4
· ((𝑆 ·
(𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))) |
266 | 69, 89, 71, 91, 265 | mulcanad 11013 |
. . . . . 6
⊢ (𝜑 → (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) = (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))) |
267 | 266 | oveq1d 6939 |
. . . . 5
⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) / 4) = ((4 ·
((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) / 4)) |
268 | 67, 68, 71, 91 | div23d 11191 |
. . . . 5
⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) / 4) = ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2))) |
269 | 80, 8 | resubcld 10806 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 − 𝑋) ∈ ℝ) |
270 | 80, 269 | remulcld 10409 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 · (𝑆 − 𝑋)) ∈ ℝ) |
271 | 80, 13 | resubcld 10806 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 − 𝑌) ∈ ℝ) |
272 | 80, 77 | resubcld 10806 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 − 𝑍) ∈ ℝ) |
273 | 271, 272 | remulcld 10409 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆 − 𝑌) · (𝑆 − 𝑍)) ∈ ℝ) |
274 | 270, 273 | remulcld 10409 |
. . . . . . 7
⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℝ) |
275 | 274 | recnd 10407 |
. . . . . 6
⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ) |
276 | 275, 71, 91 | divcan3d 11159 |
. . . . 5
⊢ (𝜑 → ((4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) / 4) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) |
277 | 267, 268,
276 | 3eqtr3d 2822 |
. . . 4
⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2)) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) |
278 | 51, 66, 277 | 3eqtrd 2818 |
. . 3
⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) |
279 | 278 | fveq2d 6452 |
. 2
⊢ (𝜑 → (√‘((((1 / 2)
· (𝑋 · 𝑌)) ·
(abs‘(sin‘𝑂)))↑2)) = (√‘((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))) |
280 | 43, 279 | eqtr3d 2816 |
1
⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))) = (√‘((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))) |