heron - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > heron		Structured version Visualization version GIF version

Theorem heron 26748

Description: Heron's formula gives the area of a triangle given only the side lengths. If points A, B, C form a triangle, then the area of the triangle, represented here as (1 / 2) · 𝑋 · 𝑌 · abs(sin𝑂), is equal to the square root of 𝑆 · (𝑆 − 𝑋) · (𝑆 − 𝑌) · (𝑆 − 𝑍), where 𝑆 = (𝑋 + 𝑌 + 𝑍) / 2 is half the perimeter of the triangle. Based on work by Jon Pennant. This is Metamath 100 proof #57. (Contributed by Mario Carneiro, 10-Mar-2019.)

**Hypotheses**
Ref	Expression
heron.f	⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))
heron.x	⊢ 𝑋 = (abs‘(𝐵 − 𝐶))
heron.y	⊢ 𝑌 = (abs‘(𝐴 − 𝐶))
heron.z	⊢ 𝑍 = (abs‘(𝐴 − 𝐵))
heron.o	⊢ 𝑂 = ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶))
heron.s	⊢ 𝑆 = (((𝑋 + 𝑌) + 𝑍) / 2)
heron.a	⊢ (𝜑 → 𝐴 ∈ ℂ)
heron.b	⊢ (𝜑 → 𝐵 ∈ ℂ)
heron.c	⊢ (𝜑 → 𝐶 ∈ ℂ)
heron.ac	⊢ (𝜑 → 𝐴 ≠ 𝐶)
heron.bc	⊢ (𝜑 → 𝐵 ≠ 𝐶)

**Assertion**
Ref	Expression
heron	⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))) = (√‘((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))

Distinct variable groups: 𝑥,𝐴,𝑦 𝑥,𝐵,𝑦 𝑥,𝐶,𝑦 Allowed substitution hints: 𝜑(𝑥,𝑦) 𝑆(𝑥,𝑦) 𝐹(𝑥,𝑦) 𝑂(𝑥,𝑦) 𝑋(𝑥,𝑦) 𝑌(𝑥,𝑦) 𝑍(𝑥,𝑦)

**Proof of Theorem heron**
Step	Hyp	Ref	Expression
1		1red 11175	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
2	1	rehalfcld 12429	. . . . 5 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
3		heron.x	. . . . . . 7 ⊢ 𝑋 = (abs‘(𝐵 − 𝐶))
4		heron.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5		heron.c	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℂ)
6	4, 5	subcld 11533	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
7	6	abscld 15405	. . . . . . 7 ⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) ∈ ℝ)
8	3, 7	eqeltrid 2832	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℝ)
9		heron.y	. . . . . . 7 ⊢ 𝑌 = (abs‘(𝐴 − 𝐶))
10		heron.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℂ)
11	10, 5	subcld 11533	. . . . . . . 8 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ)
12	11	abscld 15405	. . . . . . 7 ⊢ (𝜑 → (abs‘(𝐴 − 𝐶)) ∈ ℝ)
13	9, 12	eqeltrid 2832	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ ℝ)
14	8, 13	remulcld 11204	. . . . 5 ⊢ (𝜑 → (𝑋 · 𝑌) ∈ ℝ)
15	2, 14	remulcld 11204	. . . 4 ⊢ (𝜑 → ((1 / 2) · (𝑋 · 𝑌)) ∈ ℝ)
16		heron.o	. . . . . . 7 ⊢ 𝑂 = ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶))
17		negpitopissre 26449	. . . . . . . . 9 ⊢ (-π(,]π) ⊆ ℝ
18		heron.f	. . . . . . . . . 10 ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))
19		heron.bc	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
20	4, 5, 19	subne0d 11542	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐶) ≠ 0)
21		heron.ac	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
22	10, 5, 21	subne0d 11542	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 − 𝐶) ≠ 0)
23	18, 6, 20, 11, 22	angcld 26715	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ (-π(,]π))
24	17, 23	sselid 3944	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ ℝ)
25	24	recnd 11202	. . . . . . 7 ⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ ℂ)
26	16, 25	eqeltrid 2832	. . . . . 6 ⊢ (𝜑 → 𝑂 ∈ ℂ)
27	26	sincld 16098	. . . . 5 ⊢ (𝜑 → (sin‘𝑂) ∈ ℂ)
28	27	abscld 15405	. . . 4 ⊢ (𝜑 → (abs‘(sin‘𝑂)) ∈ ℝ)
29	15, 28	remulcld 11204	. . 3 ⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))) ∈ ℝ)
30		halfge0 12398	. . . . . 6 ⊢ 0 ≤ (1 / 2)
31	30	a1i 11	. . . . 5 ⊢ (𝜑 → 0 ≤ (1 / 2))
32	6	absge0d 15413	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (abs‘(𝐵 − 𝐶)))
33	32, 3	breqtrrdi 5149	. . . . . 6 ⊢ (𝜑 → 0 ≤ 𝑋)
34	11	absge0d 15413	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (abs‘(𝐴 − 𝐶)))
35	34, 9	breqtrrdi 5149	. . . . . 6 ⊢ (𝜑 → 0 ≤ 𝑌)
36	8, 13, 33, 35	mulge0d 11755	. . . . 5 ⊢ (𝜑 → 0 ≤ (𝑋 · 𝑌))
37	2, 14, 31, 36	mulge0d 11755	. . . 4 ⊢ (𝜑 → 0 ≤ ((1 / 2) · (𝑋 · 𝑌)))
38	27	absge0d 15413	. . . 4 ⊢ (𝜑 → 0 ≤ (abs‘(sin‘𝑂)))
39	15, 28, 37, 38	mulge0d 11755	. . 3 ⊢ (𝜑 → 0 ≤ (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))))
40	29, 39	sqrtsqd 15386	. 2 ⊢ (𝜑 → (√‘((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2)) = (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))))
41		halfcn 12396	. . . . . . 7 ⊢ (1 / 2) ∈ ℂ
42	41	a1i 11	. . . . . 6 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
43	8	recnd 11202	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℂ)
44	13	recnd 11202	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ ℂ)
45	43, 44	mulcld 11194	. . . . . 6 ⊢ (𝜑 → (𝑋 · 𝑌) ∈ ℂ)
46	42, 45	mulcld 11194	. . . . 5 ⊢ (𝜑 → ((1 / 2) · (𝑋 · 𝑌)) ∈ ℂ)
47	28	recnd 11202	. . . . 5 ⊢ (𝜑 → (abs‘(sin‘𝑂)) ∈ ℂ)
48	46, 47	sqmuld 14123	. . . 4 ⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2) = ((((1 / 2) · (𝑋 · 𝑌))↑2) · ((abs‘(sin‘𝑂))↑2)))
49		2cnd 12264	. . . . . . 7 ⊢ (𝜑 → 2 ∈ ℂ)
50		2ne0 12290	. . . . . . . 8 ⊢ 2 ≠ 0
51	50	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ≠ 0)
52	45, 49, 51	sqdivd 14124	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌) / 2)↑2) = (((𝑋 · 𝑌)↑2) / (2↑2)))
53	45, 49, 51	divrec2d 11962	. . . . . . 7 ⊢ (𝜑 → ((𝑋 · 𝑌) / 2) = ((1 / 2) · (𝑋 · 𝑌)))
54	53	oveq1d 7402	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌) / 2)↑2) = (((1 / 2) · (𝑋 · 𝑌))↑2))
55		sq2 14162	. . . . . . . 8 ⊢ (2↑2) = 4
56	55	a1i 11	. . . . . . 7 ⊢ (𝜑 → (2↑2) = 4)
57	56	oveq2d 7403	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌)↑2) / (2↑2)) = (((𝑋 · 𝑌)↑2) / 4))
58	52, 54, 57	3eqtr3d 2772	. . . . 5 ⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌))↑2) = (((𝑋 · 𝑌)↑2) / 4))
59	16, 24	eqeltrid 2832	. . . . . . 7 ⊢ (𝜑 → 𝑂 ∈ ℝ)
60	59	resincld 16111	. . . . . 6 ⊢ (𝜑 → (sin‘𝑂) ∈ ℝ)
61		absresq 15268	. . . . . 6 ⊢ ((sin‘𝑂) ∈ ℝ → ((abs‘(sin‘𝑂))↑2) = ((sin‘𝑂)↑2))
62	60, 61	syl 17	. . . . 5 ⊢ (𝜑 → ((abs‘(sin‘𝑂))↑2) = ((sin‘𝑂)↑2))
63	58, 62	oveq12d 7405	. . . 4 ⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌))↑2) · ((abs‘(sin‘𝑂))↑2)) = ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2)))
64	45	sqcld 14109	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 · 𝑌)↑2) ∈ ℂ)
65	27	sqcld 14109	. . . . . . . 8 ⊢ (𝜑 → ((sin‘𝑂)↑2) ∈ ℂ)
66	64, 65	mulcld 11194	. . . . . . 7 ⊢ (𝜑 → (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) ∈ ℂ)
67		4cn 12271	. . . . . . . . 9 ⊢ 4 ∈ ℂ
68	67	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 4 ∈ ℂ)
69		heron.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (((𝑋 + 𝑌) + 𝑍) / 2)
70	8, 13	readdcld 11203	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ ℝ)
71		heron.z	. . . . . . . . . . . . . . 15 ⊢ 𝑍 = (abs‘(𝐴 − 𝐵))
72	10, 4	subcld 11533	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)
73	72	abscld 15405	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ∈ ℝ)
74	71, 73	eqeltrid 2832	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑍 ∈ ℝ)
75	70, 74	readdcld 11203	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) ∈ ℝ)
76	75	rehalfcld 12429	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) / 2) ∈ ℝ)
77	69, 76	eqeltrid 2832	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ ℝ)
78	77	recnd 11202	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ ℂ)
79	78, 43	subcld 11533	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 − 𝑋) ∈ ℂ)
80	78, 79	mulcld 11194	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 · (𝑆 − 𝑋)) ∈ ℂ)
81	78, 44	subcld 11533	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 − 𝑌) ∈ ℂ)
82	74	recnd 11202	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ ℂ)
83	78, 82	subcld 11533	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 − 𝑍) ∈ ℂ)
84	81, 83	mulcld 11194	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 − 𝑌) · (𝑆 − 𝑍)) ∈ ℂ)
85	80, 84	mulcld 11194	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ)
86	68, 85	mulcld 11194	. . . . . . 7 ⊢ (𝜑 → (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) ∈ ℂ)
87		4ne0 12294	. . . . . . . 8 ⊢ 4 ≠ 0
88	87	a1i 11	. . . . . . 7 ⊢ (𝜑 → 4 ≠ 0)
89	49, 45	sqmuld 14123	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = ((2↑2) · ((𝑋 · 𝑌)↑2)))
90	56	oveq1d 7402	. . . . . . . . . 10 ⊢ (𝜑 → ((2↑2) · ((𝑋 · 𝑌)↑2)) = (4 · ((𝑋 · 𝑌)↑2)))
91	89, 90	eqtr2d 2765	. . . . . . . . 9 ⊢ (𝜑 → (4 · ((𝑋 · 𝑌)↑2)) = ((2 · (𝑋 · 𝑌))↑2))
92	91	oveq1d 7402	. . . . . . . 8 ⊢ (𝜑 → ((4 · ((𝑋 · 𝑌)↑2)) · ((sin‘𝑂)↑2)) = (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)))
93	68, 64, 65	mulassd 11197	. . . . . . . 8 ⊢ (𝜑 → ((4 · ((𝑋 · 𝑌)↑2)) · ((sin‘𝑂)↑2)) = (4 · (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2))))
94	49, 45	mulcld 11194	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑋 · 𝑌)) ∈ ℂ)
95	94	sqcld 14109	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) ∈ ℂ)
96	95, 65	mulcld 11194	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) ∈ ℂ)
97	44, 82	mulcld 11194	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 · 𝑍) ∈ ℂ)
98	49, 97	mulcld 11194	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑌 · 𝑍)) ∈ ℂ)
99	98	sqcld 14109	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) ∈ ℂ)
100	44	sqcld 14109	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌↑2) ∈ ℂ)
101	82	sqcld 14109	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍↑2) ∈ ℂ)
102	43	sqcld 14109	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
103	101, 102	subcld 11533	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑍↑2) − (𝑋↑2)) ∈ ℂ)
104	100, 103	addcld 11193	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) ∈ ℂ)
105	104	sqcld 14109	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) ∈ ℂ)
106	99, 105	subcld 11533	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) ∈ ℂ)
107	26	coscld 16099	. . . . . . . . . . . . 13 ⊢ (𝜑 → (cos‘𝑂) ∈ ℂ)
108	107	sqcld 14109	. . . . . . . . . . . 12 ⊢ (𝜑 → ((cos‘𝑂)↑2) ∈ ℂ)
109	95, 108	mulcld 11194	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)) ∈ ℂ)
110		sincossq 16144	. . . . . . . . . . . . . 14 ⊢ (𝑂 ∈ ℂ → (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2)) = 1)
111	26, 110	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2)) = 1)
112	111	oveq2d 7403	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2))) = (((2 · (𝑋 · 𝑌))↑2) · 1))
113	95, 65, 108	adddid 11198	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2))) = ((((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) + (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2))))
114	100	2timesd 12425	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · (𝑌↑2)) = ((𝑌↑2) + (𝑌↑2)))
115	100, 103, 100	ppncand 11573	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) = ((𝑌↑2) + (𝑌↑2)))
116	114, 115	eqtr4d 2767	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑌↑2)) = (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))))
117	103	2timesd 12425	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · ((𝑍↑2) − (𝑋↑2))) = (((𝑍↑2) − (𝑋↑2)) + ((𝑍↑2) − (𝑋↑2))))
118	100, 103, 103	pnncand 11572	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) = (((𝑍↑2) − (𝑋↑2)) + ((𝑍↑2) − (𝑋↑2))))
119	117, 118	eqtr4d 2767	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · ((𝑍↑2) − (𝑋↑2))) = (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))))
120	116, 119	oveq12d 7405	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · (𝑌↑2)) · (2 · ((𝑍↑2) − (𝑋↑2)))) = ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) · (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))))))
121		2t2e4 12345	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 · 2) = 4
122	121, 68	eqeltrid 2832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · 2) ∈ ℂ)
123	122, 100, 103	mulassd 11197	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · ((𝑍↑2) − (𝑋↑2))) = ((2 · 2) · ((𝑌↑2) · ((𝑍↑2) − (𝑋↑2)))))
124	122, 100	mulcld 11194	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 · 2) · (𝑌↑2)) ∈ ℂ)
125	124, 101, 102	subdid 11634	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · ((𝑍↑2) − (𝑋↑2))) = ((((2 · 2) · (𝑌↑2)) · (𝑍↑2)) − (((2 · 2) · (𝑌↑2)) · (𝑋↑2))))
126	49	sqvald 14108	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (2↑2) = (2 · 2))
127	44, 82	sqmuld 14123	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑌 · 𝑍)↑2) = ((𝑌↑2) · (𝑍↑2)))
128	126, 127	oveq12d 7405	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2↑2) · ((𝑌 · 𝑍)↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑍↑2))))
129	49, 97	sqmuld 14123	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) = ((2↑2) · ((𝑌 · 𝑍)↑2)))
130	122, 100, 101	mulassd 11197	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · (𝑍↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑍↑2))))
131	128, 129, 130	3eqtr4d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) = (((2 · 2) · (𝑌↑2)) · (𝑍↑2)))
132	43, 44	sqmuld 14123	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑋 · 𝑌)↑2) = ((𝑋↑2) · (𝑌↑2)))
133	102, 100	mulcomd 11195	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑋↑2) · (𝑌↑2)) = ((𝑌↑2) · (𝑋↑2)))
134	132, 133	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑋 · 𝑌)↑2) = ((𝑌↑2) · (𝑋↑2)))
135	126, 134	oveq12d 7405	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2↑2) · ((𝑋 · 𝑌)↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑋↑2))))
136	122, 100, 102	mulassd 11197	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · (𝑋↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑋↑2))))
137	135, 89, 136	3eqtr4d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = (((2 · 2) · (𝑌↑2)) · (𝑋↑2)))
138	131, 137	oveq12d 7405	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((((2 · 2) · (𝑌↑2)) · (𝑍↑2)) − (((2 · 2) · (𝑌↑2)) · (𝑋↑2))))
139	125, 138	eqtr4d 2767	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · ((𝑍↑2) − (𝑋↑2))) = (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)))
140	49, 49, 100, 103	mul4d 11386	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · 2) · ((𝑌↑2) · ((𝑍↑2) − (𝑋↑2)))) = ((2 · (𝑌↑2)) · (2 · ((𝑍↑2) − (𝑋↑2)))))
141	123, 139, 140	3eqtr3d 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((2 · (𝑌↑2)) · (2 · ((𝑍↑2) − (𝑋↑2)))))
142	100, 103	subcld 11533	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) ∈ ℂ)
143		subsq 14175	. . . . . . . . . . . . . . . . 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))))))
144	104, 142, 143	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) − (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2)) = ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) · (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))))))
145	120, 141, 144	3eqtr4d 2774	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) − (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2)))
146	145	oveq2d 7403	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2))) = (((2 · (𝑌 · 𝑍))↑2) − ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) − (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2))))
147	99, 95	nncand 11538	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2))) = ((2 · (𝑋 · 𝑌))↑2))
148	142	sqcld 14109	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2) ∈ ℂ)
149	99, 105, 148	subsubd 11561	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) − (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2))) = ((((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2)))
150	146, 147, 149	3eqtr3d 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = ((((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2)))
151	95	mulridd 11191	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · 1) = ((2 · (𝑋 · 𝑌))↑2))
152	102, 100	addcld 11193	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋↑2) + (𝑌↑2)) ∈ ℂ)
153	45, 107	mulcld 11194	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑋 · 𝑌) · (cos‘𝑂)) ∈ ℂ)
154	49, 153	mulcld 11194	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · ((𝑋 · 𝑌) · (cos‘𝑂))) ∈ ℂ)
155	152, 154	nncand 11538	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))) = (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))
156	100, 101	subcld 11533	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑌↑2) − (𝑍↑2)) ∈ ℂ)
157	156, 102	addcomd 11376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑌↑2) − (𝑍↑2)) + (𝑋↑2)) = ((𝑋↑2) + ((𝑌↑2) − (𝑍↑2))))
158	100, 101, 102	subsubd 11561	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑌↑2) − (𝑍↑2)) + (𝑋↑2)))
159	102, 100, 101	addsubassd 11553	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2)) = ((𝑋↑2) + ((𝑌↑2) − (𝑍↑2))))
160	157, 158, 159	3eqtr4d 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2)))
161	18, 3, 9, 71, 16	lawcos 26726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝑍↑2) = (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂)))))
162	10, 4, 5, 21, 19, 161	syl32anc 1380	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑍↑2) = (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂)))))
163	162	oveq2d 7403	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2)) = (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))))
164	160, 163	eqtrd 2764	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))))
165	49, 45, 107	mulassd 11197	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌)) · (cos‘𝑂)) = (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))
166	155, 164, 165	3eqtr4d 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = ((2 · (𝑋 · 𝑌)) · (cos‘𝑂)))
167	166	oveq1d 7402	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2) = (((2 · (𝑋 · 𝑌)) · (cos‘𝑂))↑2))
168	94, 107	sqmuld 14123	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌)) · (cos‘𝑂))↑2) = (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)))
169	167, 168	eqtr2d 2765	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)) = (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2))
170	169	oveq2d 7403	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2))) = ((((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2)))
171	150, 151, 170	3eqtr4d 2774	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · 1) = ((((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2))))
172	112, 113, 171	3eqtr3d 2772	. . . . . . . . . . 11 ⊢ (𝜑 → ((((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) + (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2))) = ((((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2))))
173	96, 106, 109, 172	addcan2ad 11380	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)))
174		subsq 14175	. . . . . . . . . . 11 ⊢ (((2 · (𝑌 · 𝑍)) ∈ ℂ ∧ ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) ∈ ℂ) → (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) · ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))))
175	98, 104, 174	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) · ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))))
176	100, 101	addcld 11193	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌↑2) + (𝑍↑2)) ∈ ℂ)
177	98, 176, 102	addsubassd 11553	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2)) = ((2 · (𝑌 · 𝑍)) + (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))))
178	100, 101, 102	addsubassd 11553	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2)) = ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))
179	178	oveq2d 7403	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))))
180	177, 179	eqtr2d 2765	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2)))
181		binom2 14182	. . . . . . . . . . . . . . 15 ⊢ ((𝑌 ∈ ℂ ∧ 𝑍 ∈ ℂ) → ((𝑌 + 𝑍)↑2) = (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2)))
182	44, 82, 181	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 + 𝑍)↑2) = (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2)))
183	100, 98, 101	add32d 11402	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2)) = (((𝑌↑2) + (𝑍↑2)) + (2 · (𝑌 · 𝑍))))
184	176, 98	addcomd 11376	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) + (2 · (𝑌 · 𝑍))) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))))
185	182, 183, 184	3eqtrd 2768	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌 + 𝑍)↑2) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))))
186	185	oveq1d 7402	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2)))
187	44, 82	addcld 11193	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 + 𝑍) ∈ ℂ)
188		subsq 14175	. . . . . . . . . . . . . . 15 ⊢ (((𝑌 + 𝑍) ∈ ℂ ∧ 𝑋 ∈ ℂ) → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋)))
189	187, 43, 188	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋)))
190	69	oveq2i 7398	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 𝑆) = (2 · (((𝑋 + 𝑌) + 𝑍) / 2))
191	75	recnd 11202	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) ∈ ℂ)
192	191, 49, 51	divcan2d 11960	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (((𝑋 + 𝑌) + 𝑍) / 2)) = ((𝑋 + 𝑌) + 𝑍))
193	190, 192	eqtrid 2776	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · 𝑆) = ((𝑋 + 𝑌) + 𝑍))
194	43, 44, 82	addassd 11196	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
195	43, 187	addcomd 11376	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 + (𝑌 + 𝑍)) = ((𝑌 + 𝑍) + 𝑋))
196	193, 194, 195	3eqtrd 2768	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · 𝑆) = ((𝑌 + 𝑍) + 𝑋))
197	49, 78, 43	subdid 11634	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (𝑆 − 𝑋)) = ((2 · 𝑆) − (2 · 𝑋)))
198	193, 194	eqtrd 2764	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑆) = (𝑋 + (𝑌 + 𝑍)))
199	43	2timesd 12425	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑋) = (𝑋 + 𝑋))
200	198, 199	oveq12d 7405	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑋)) = ((𝑋 + (𝑌 + 𝑍)) − (𝑋 + 𝑋)))
201	43, 187, 43	pnpcand 11570	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑋 + (𝑌 + 𝑍)) − (𝑋 + 𝑋)) = ((𝑌 + 𝑍) − 𝑋))
202	197, 200, 201	3eqtrd 2768	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝑆 − 𝑋)) = ((𝑌 + 𝑍) − 𝑋))
203	196, 202	oveq12d 7405	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · 𝑆) · (2 · (𝑆 − 𝑋))) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋)))
204	189, 203	eqtr4d 2767	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = ((2 · 𝑆) · (2 · (𝑆 − 𝑋))))
205	49, 78, 49, 79	mul4d 11386	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝑆) · (2 · (𝑆 − 𝑋))) = ((2 · 2) · (𝑆 · (𝑆 − 𝑋))))
206	121	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · 2) = 4)
207	206	oveq1d 7402	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 2) · (𝑆 · (𝑆 − 𝑋))) = (4 · (𝑆 · (𝑆 − 𝑋))))
208	204, 205, 207	3eqtrd 2768	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (4 · (𝑆 · (𝑆 − 𝑋))))
209	180, 186, 208	3eqtr2d 2770	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (4 · (𝑆 · (𝑆 − 𝑋))))
210	98, 176	subcld 11533	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) ∈ ℂ)
211	210, 102	addcomd 11376	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2)) = ((𝑋↑2) + ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2)))))
212	178	oveq2d 7403	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))))
213	98, 176, 102	subsubd 11561	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2)))
214	212, 213	eqtr3d 2766	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2)))
215	102, 176, 98	subsub2d 11562	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍)))) = ((𝑋↑2) + ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2)))))
216	211, 214, 215	3eqtr4d 2774	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍)))))
217	100, 101, 98	addsubassd 11553	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = ((𝑌↑2) + ((𝑍↑2) − (2 · (𝑌 · 𝑍)))))
218	101, 98	subcld 11533	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑍↑2) − (2 · (𝑌 · 𝑍))) ∈ ℂ)
219	100, 218	addcomd 11376	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌↑2) + ((𝑍↑2) − (2 · (𝑌 · 𝑍)))) = (((𝑍↑2) − (2 · (𝑌 · 𝑍))) + (𝑌↑2)))
220	44, 82	mulcomd 11195	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑌 · 𝑍) = (𝑍 · 𝑌))
221	220	oveq2d 7403	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑌 · 𝑍)) = (2 · (𝑍 · 𝑌)))
222	221	oveq2d 7403	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑍↑2) − (2 · (𝑌 · 𝑍))) = ((𝑍↑2) − (2 · (𝑍 · 𝑌))))
223	222	oveq1d 7402	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑍↑2) − (2 · (𝑌 · 𝑍))) + (𝑌↑2)) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
224	217, 219, 223	3eqtrd 2768	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
225		binom2sub 14185	. . . . . . . . . . . . . . 15 ⊢ ((𝑍 ∈ ℂ ∧ 𝑌 ∈ ℂ) → ((𝑍 − 𝑌)↑2) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
226	82, 44, 225	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑍 − 𝑌)↑2) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
227	224, 226	eqtr4d 2767	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = ((𝑍 − 𝑌)↑2))
228	227	oveq2d 7403	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍)))) = ((𝑋↑2) − ((𝑍 − 𝑌)↑2)))
229	82, 44	subcld 11533	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍 − 𝑌) ∈ ℂ)
230		subsq 14175	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ ℂ ∧ (𝑍 − 𝑌) ∈ ℂ) → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌))))
231	43, 229, 230	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌))))
232	49, 78, 44	subdid 11634	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (𝑆 − 𝑌)) = ((2 · 𝑆) − (2 · 𝑌)))
233	43, 44, 82	add32d 11402	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌))
234	193, 233	eqtrd 2764	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑆) = ((𝑋 + 𝑍) + 𝑌))
235	44	2timesd 12425	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑌) = (𝑌 + 𝑌))
236	234, 235	oveq12d 7405	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑌)) = (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌)))
237	43, 82	addcld 11193	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 + 𝑍) ∈ ℂ)
238	237, 44, 44	pnpcan2d 11571	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌)) = ((𝑋 + 𝑍) − 𝑌))
239	43, 82, 44, 238	assraddsubd 11592	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌)) = (𝑋 + (𝑍 − 𝑌)))
240	232, 236, 239	3eqtrd 2768	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝑆 − 𝑌)) = (𝑋 + (𝑍 − 𝑌)))
241	49, 78, 82	subdid 11634	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (𝑆 − 𝑍)) = ((2 · 𝑆) − (2 · 𝑍)))
242	82	2timesd 12425	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑍) = (𝑍 + 𝑍))
243	193, 242	oveq12d 7405	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑍)) = (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍)))
244	43, 44	addcld 11193	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ ℂ)
245	244, 82, 82	pnpcan2d 11571	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍)) = ((𝑋 + 𝑌) − 𝑍))
246	43, 82, 44	subsub3d 11563	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 − (𝑍 − 𝑌)) = ((𝑋 + 𝑌) − 𝑍))
247	245, 246	eqtr4d 2767	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍)) = (𝑋 − (𝑍 − 𝑌)))
248	241, 243, 247	3eqtrd 2768	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝑆 − 𝑍)) = (𝑋 − (𝑍 − 𝑌)))
249	240, 248	oveq12d 7405	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍))) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌))))
250	231, 249	eqtr4d 2767	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍))))
251	49, 81, 49, 83	mul4d 11386	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍))) = ((2 · 2) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
252	206	oveq1d 7402	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 2) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
253	250, 251, 252	3eqtrd 2768	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
254	216, 228, 253	3eqtrd 2768	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
255	209, 254	oveq12d 7405	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) · ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))) = ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
256	173, 175, 255	3eqtrd 2768	. . . . . . . . 9 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
257	68, 84	mulcld 11194	. . . . . . . . . 10 ⊢ (𝜑 → (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ)
258	68, 80, 257	mulassd 11197	. . . . . . . . 9 ⊢ (𝜑 → ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) = (4 · ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
259	80, 68, 84	mul12d 11383	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) = (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
260	259	oveq2d 7403	. . . . . . . . 9 ⊢ (𝜑 → (4 · ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))) = (4 · (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
261	256, 258, 260	3eqtrd 2768	. . . . . . . 8 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = (4 · (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
262	92, 93, 261	3eqtr3d 2772	. . . . . . 7 ⊢ (𝜑 → (4 · (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2))) = (4 · (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
263	66, 86, 68, 88, 262	mulcanad 11813	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) = (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
264	263	oveq1d 7402	. . . . 5 ⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) / 4) = ((4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) / 4))
265	64, 65, 68, 88	div23d 11995	. . . . 5 ⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) / 4) = ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2)))
266	77, 8	resubcld 11606	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 − 𝑋) ∈ ℝ)
267	77, 266	remulcld 11204	. . . . . . . 8 ⊢ (𝜑 → (𝑆 · (𝑆 − 𝑋)) ∈ ℝ)
268	77, 13	resubcld 11606	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 − 𝑌) ∈ ℝ)
269	77, 74	resubcld 11606	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 − 𝑍) ∈ ℝ)
270	268, 269	remulcld 11204	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 − 𝑌) · (𝑆 − 𝑍)) ∈ ℝ)
271	267, 270	remulcld 11204	. . . . . . 7 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℝ)
272	271	recnd 11202	. . . . . 6 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ)
273	272, 68, 88	divcan3d 11963	. . . . 5 ⊢ (𝜑 → ((4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) / 4) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
274	264, 265, 273	3eqtr3d 2772	. . . 4 ⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2)) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
275	48, 63, 274	3eqtrd 2768	. . 3 ⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
276	275	fveq2d 6862	. 2 ⊢ (𝜑 → (√‘((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2)) = (√‘((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
277	40, 276	eqtr3d 2766	1 ⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))) = (√‘((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∖ cdif 3911 {csn 4589 class class class wbr 5107 ‘cfv 6511 (class class class)co 7387 ∈ cmpo 7389 ℂcc 11066 ℝcr 11067 0cc0 11068 1c1 11069 + caddc 11071 · cmul 11073 ≤ cle 11209 − cmin 11405 -cneg 11406 / cdiv 11835 2c2 12241 4c4 12243 (,]cioc 13307 ↑cexp 14026 ℑcim 15064 √csqrt 15199 abscabs 15200 sincsin 16029 cosccos 16030 πcpi 16032 logclog 26463

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146 ax-addf 11147

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-iin 4958 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-of 7653 df-om 7843 df-1st 7968 df-2nd 7969 df-supp 8140 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-2o 8435 df-er 8671 df-map 8801 df-pm 8802 df-ixp 8871 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-fsupp 9313 df-fi 9362 df-sup 9393 df-inf 9394 df-oi 9463 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-4 12251 df-5 12252 df-6 12253 df-7 12254 df-8 12255 df-9 12256 df-n0 12443 df-z 12530 df-dec 12650 df-uz 12794 df-q 12908 df-rp 12952 df-xneg 13072 df-xadd 13073 df-xmul 13074 df-ioo 13310 df-ioc 13311 df-ico 13312 df-icc 13313 df-fz 13469 df-fzo 13616 df-fl 13754 df-mod 13832 df-seq 13967 df-exp 14027 df-fac 14239 df-bc 14268 df-hash 14296 df-shft 15033 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-limsup 15437 df-clim 15454 df-rlim 15455 df-sum 15653 df-ef 16033 df-sin 16035 df-cos 16036 df-pi 16038 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-rest 17385 df-topn 17386 df-0g 17404 df-gsum 17405 df-topgen 17406 df-pt 17407 df-prds 17410 df-xrs 17465 df-qtop 17470 df-imas 17471 df-xps 17473 df-mre 17547 df-mrc 17548 df-acs 17550 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-submnd 18711 df-mulg 19000 df-cntz 19249 df-cmn 19712 df-psmet 21256 df-xmet 21257 df-met 21258 df-bl 21259 df-mopn 21260 df-fbas 21261 df-fg 21262 df-cnfld 21265 df-top 22781 df-topon 22798 df-topsp 22820 df-bases 22833 df-cld 22906 df-ntr 22907 df-cls 22908 df-nei 22985 df-lp 23023 df-perf 23024 df-cn 23114 df-cnp 23115 df-haus 23202 df-tx 23449 df-hmeo 23642 df-fil 23733 df-fm 23825 df-flim 23826 df-flf 23827 df-xms 24208 df-ms 24209 df-tms 24210 df-cncf 24771 df-limc 25767 df-dv 25768 df-log 26465

This theorem is referenced by: (None)

W3C validator