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 26594

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 11222	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
2	1	rehalfcld 12466	. . . . 5 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
3		heron.x	. . . . . . 7 ⊢ 𝑋 = (abs‘(𝐵 − 𝐶))
4		heron.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5		heron.c	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℂ)
6	4, 5	subcld 11578	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
7	6	abscld 15390	. . . . . . 7 ⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) ∈ ℝ)
8	3, 7	eqeltrid 2836	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℝ)
9		heron.y	. . . . . . 7 ⊢ 𝑌 = (abs‘(𝐴 − 𝐶))
10		heron.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℂ)
11	10, 5	subcld 11578	. . . . . . . 8 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ)
12	11	abscld 15390	. . . . . . 7 ⊢ (𝜑 → (abs‘(𝐴 − 𝐶)) ∈ ℝ)
13	9, 12	eqeltrid 2836	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ ℝ)
14	8, 13	remulcld 11251	. . . . 5 ⊢ (𝜑 → (𝑋 · 𝑌) ∈ ℝ)
15	2, 14	remulcld 11251	. . . 4 ⊢ (𝜑 → ((1 / 2) · (𝑋 · 𝑌)) ∈ ℝ)
16		heron.o	. . . . . . 7 ⊢ 𝑂 = ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶))
17		negpitopissre 26300	. . . . . . . . 9 ⊢ (-π(,]π) ⊆ ℝ
18		heron.f	. . . . . . . . . 10 ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))
19		heron.bc	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
20	4, 5, 19	subne0d 11587	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐶) ≠ 0)
21		heron.ac	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
22	10, 5, 21	subne0d 11587	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 − 𝐶) ≠ 0)
23	18, 6, 20, 11, 22	angcld 26561	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ (-π(,]π))
24	17, 23	sselid 3980	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ ℝ)
25	24	recnd 11249	. . . . . . 7 ⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ ℂ)
26	16, 25	eqeltrid 2836	. . . . . 6 ⊢ (𝜑 → 𝑂 ∈ ℂ)
27	26	sincld 16080	. . . . 5 ⊢ (𝜑 → (sin‘𝑂) ∈ ℂ)
28	27	abscld 15390	. . . 4 ⊢ (𝜑 → (abs‘(sin‘𝑂)) ∈ ℝ)
29	15, 28	remulcld 11251	. . 3 ⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))) ∈ ℝ)
30		halfge0 12436	. . . . . 6 ⊢ 0 ≤ (1 / 2)
31	30	a1i 11	. . . . 5 ⊢ (𝜑 → 0 ≤ (1 / 2))
32	6	absge0d 15398	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (abs‘(𝐵 − 𝐶)))
33	32, 3	breqtrrdi 5190	. . . . . 6 ⊢ (𝜑 → 0 ≤ 𝑋)
34	11	absge0d 15398	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (abs‘(𝐴 − 𝐶)))
35	34, 9	breqtrrdi 5190	. . . . . 6 ⊢ (𝜑 → 0 ≤ 𝑌)
36	8, 13, 33, 35	mulge0d 11798	. . . . 5 ⊢ (𝜑 → 0 ≤ (𝑋 · 𝑌))
37	2, 14, 31, 36	mulge0d 11798	. . . 4 ⊢ (𝜑 → 0 ≤ ((1 / 2) · (𝑋 · 𝑌)))
38	27	absge0d 15398	. . . 4 ⊢ (𝜑 → 0 ≤ (abs‘(sin‘𝑂)))
39	15, 28, 37, 38	mulge0d 11798	. . 3 ⊢ (𝜑 → 0 ≤ (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))))
40	29, 39	sqrtsqd 15373	. 2 ⊢ (𝜑 → (√‘((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2)) = (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))))
41		halfcn 12434	. . . . . . 7 ⊢ (1 / 2) ∈ ℂ
42	41	a1i 11	. . . . . 6 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
43	8	recnd 11249	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℂ)
44	13	recnd 11249	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ ℂ)
45	43, 44	mulcld 11241	. . . . . 6 ⊢ (𝜑 → (𝑋 · 𝑌) ∈ ℂ)
46	42, 45	mulcld 11241	. . . . 5 ⊢ (𝜑 → ((1 / 2) · (𝑋 · 𝑌)) ∈ ℂ)
47	28	recnd 11249	. . . . 5 ⊢ (𝜑 → (abs‘(sin‘𝑂)) ∈ ℂ)
48	46, 47	sqmuld 14130	. . . 4 ⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2) = ((((1 / 2) · (𝑋 · 𝑌))↑2) · ((abs‘(sin‘𝑂))↑2)))
49		2cnd 12297	. . . . . . 7 ⊢ (𝜑 → 2 ∈ ℂ)
50		2ne0 12323	. . . . . . . 8 ⊢ 2 ≠ 0
51	50	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ≠ 0)
52	45, 49, 51	sqdivd 14131	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌) / 2)↑2) = (((𝑋 · 𝑌)↑2) / (2↑2)))
53	45, 49, 51	divrec2d 12001	. . . . . . 7 ⊢ (𝜑 → ((𝑋 · 𝑌) / 2) = ((1 / 2) · (𝑋 · 𝑌)))
54	53	oveq1d 7427	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌) / 2)↑2) = (((1 / 2) · (𝑋 · 𝑌))↑2))
55		sq2 14168	. . . . . . . 8 ⊢ (2↑2) = 4
56	55	a1i 11	. . . . . . 7 ⊢ (𝜑 → (2↑2) = 4)
57	56	oveq2d 7428	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌)↑2) / (2↑2)) = (((𝑋 · 𝑌)↑2) / 4))
58	52, 54, 57	3eqtr3d 2779	. . . . 5 ⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌))↑2) = (((𝑋 · 𝑌)↑2) / 4))
59	16, 24	eqeltrid 2836	. . . . . . 7 ⊢ (𝜑 → 𝑂 ∈ ℝ)
60	59	resincld 16093	. . . . . 6 ⊢ (𝜑 → (sin‘𝑂) ∈ ℝ)
61		absresq 15256	. . . . . 6 ⊢ ((sin‘𝑂) ∈ ℝ → ((abs‘(sin‘𝑂))↑2) = ((sin‘𝑂)↑2))
62	60, 61	syl 17	. . . . 5 ⊢ (𝜑 → ((abs‘(sin‘𝑂))↑2) = ((sin‘𝑂)↑2))
63	58, 62	oveq12d 7430	. . . 4 ⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌))↑2) · ((abs‘(sin‘𝑂))↑2)) = ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2)))
64	45	sqcld 14116	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 · 𝑌)↑2) ∈ ℂ)
65	27	sqcld 14116	. . . . . . . 8 ⊢ (𝜑 → ((sin‘𝑂)↑2) ∈ ℂ)
66	64, 65	mulcld 11241	. . . . . . 7 ⊢ (𝜑 → (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) ∈ ℂ)
67		4cn 12304	. . . . . . . . 9 ⊢ 4 ∈ ℂ
68	67	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 4 ∈ ℂ)
69		heron.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (((𝑋 + 𝑌) + 𝑍) / 2)
70	8, 13	readdcld 11250	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ ℝ)
71		heron.z	. . . . . . . . . . . . . . 15 ⊢ 𝑍 = (abs‘(𝐴 − 𝐵))
72	10, 4	subcld 11578	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)
73	72	abscld 15390	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ∈ ℝ)
74	71, 73	eqeltrid 2836	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑍 ∈ ℝ)
75	70, 74	readdcld 11250	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) ∈ ℝ)
76	75	rehalfcld 12466	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) / 2) ∈ ℝ)
77	69, 76	eqeltrid 2836	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ ℝ)
78	77	recnd 11249	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ ℂ)
79	78, 43	subcld 11578	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 − 𝑋) ∈ ℂ)
80	78, 79	mulcld 11241	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 · (𝑆 − 𝑋)) ∈ ℂ)
81	78, 44	subcld 11578	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 − 𝑌) ∈ ℂ)
82	74	recnd 11249	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ ℂ)
83	78, 82	subcld 11578	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 − 𝑍) ∈ ℂ)
84	81, 83	mulcld 11241	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 − 𝑌) · (𝑆 − 𝑍)) ∈ ℂ)
85	80, 84	mulcld 11241	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ)
86	68, 85	mulcld 11241	. . . . . . 7 ⊢ (𝜑 → (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) ∈ ℂ)
87		4ne0 12327	. . . . . . . 8 ⊢ 4 ≠ 0
88	87	a1i 11	. . . . . . 7 ⊢ (𝜑 → 4 ≠ 0)
89	49, 45	sqmuld 14130	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = ((2↑2) · ((𝑋 · 𝑌)↑2)))
90	56	oveq1d 7427	. . . . . . . . . 10 ⊢ (𝜑 → ((2↑2) · ((𝑋 · 𝑌)↑2)) = (4 · ((𝑋 · 𝑌)↑2)))
91	89, 90	eqtr2d 2772	. . . . . . . . 9 ⊢ (𝜑 → (4 · ((𝑋 · 𝑌)↑2)) = ((2 · (𝑋 · 𝑌))↑2))
92	91	oveq1d 7427	. . . . . . . 8 ⊢ (𝜑 → ((4 · ((𝑋 · 𝑌)↑2)) · ((sin‘𝑂)↑2)) = (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)))
93	68, 64, 65	mulassd 11244	. . . . . . . 8 ⊢ (𝜑 → ((4 · ((𝑋 · 𝑌)↑2)) · ((sin‘𝑂)↑2)) = (4 · (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2))))
94	49, 45	mulcld 11241	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑋 · 𝑌)) ∈ ℂ)
95	94	sqcld 14116	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) ∈ ℂ)
96	95, 65	mulcld 11241	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) ∈ ℂ)
97	44, 82	mulcld 11241	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 · 𝑍) ∈ ℂ)
98	49, 97	mulcld 11241	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑌 · 𝑍)) ∈ ℂ)
99	98	sqcld 14116	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) ∈ ℂ)
100	44	sqcld 14116	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌↑2) ∈ ℂ)
101	82	sqcld 14116	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍↑2) ∈ ℂ)
102	43	sqcld 14116	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
103	101, 102	subcld 11578	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑍↑2) − (𝑋↑2)) ∈ ℂ)
104	100, 103	addcld 11240	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) ∈ ℂ)
105	104	sqcld 14116	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) ∈ ℂ)
106	99, 105	subcld 11578	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) ∈ ℂ)
107	26	coscld 16081	. . . . . . . . . . . . 13 ⊢ (𝜑 → (cos‘𝑂) ∈ ℂ)
108	107	sqcld 14116	. . . . . . . . . . . 12 ⊢ (𝜑 → ((cos‘𝑂)↑2) ∈ ℂ)
109	95, 108	mulcld 11241	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)) ∈ ℂ)
110		sincossq 16126	. . . . . . . . . . . . . 14 ⊢ (𝑂 ∈ ℂ → (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2)) = 1)
111	26, 110	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2)) = 1)
112	111	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2))) = (((2 · (𝑋 · 𝑌))↑2) · 1))
113	95, 65, 108	adddid 11245	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2))) = ((((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) + (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2))))
114	100	2timesd 12462	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · (𝑌↑2)) = ((𝑌↑2) + (𝑌↑2)))
115	100, 103, 100	ppncand 11618	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) = ((𝑌↑2) + (𝑌↑2)))
116	114, 115	eqtr4d 2774	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑌↑2)) = (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))))
117	103	2timesd 12462	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · ((𝑍↑2) − (𝑋↑2))) = (((𝑍↑2) − (𝑋↑2)) + ((𝑍↑2) − (𝑋↑2))))
118	100, 103, 103	pnncand 11617	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) = (((𝑍↑2) − (𝑋↑2)) + ((𝑍↑2) − (𝑋↑2))))
119	117, 118	eqtr4d 2774	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · ((𝑍↑2) − (𝑋↑2))) = (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))))
120	116, 119	oveq12d 7430	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · (𝑌↑2)) · (2 · ((𝑍↑2) − (𝑋↑2)))) = ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) · (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))))))
121		2t2e4 12383	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 · 2) = 4
122	121, 68	eqeltrid 2836	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · 2) ∈ ℂ)
123	122, 100, 103	mulassd 11244	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · ((𝑍↑2) − (𝑋↑2))) = ((2 · 2) · ((𝑌↑2) · ((𝑍↑2) − (𝑋↑2)))))
124	122, 100	mulcld 11241	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 · 2) · (𝑌↑2)) ∈ ℂ)
125	124, 101, 102	subdid 11677	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · ((𝑍↑2) − (𝑋↑2))) = ((((2 · 2) · (𝑌↑2)) · (𝑍↑2)) − (((2 · 2) · (𝑌↑2)) · (𝑋↑2))))
126	49	sqvald 14115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (2↑2) = (2 · 2))
127	44, 82	sqmuld 14130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑌 · 𝑍)↑2) = ((𝑌↑2) · (𝑍↑2)))
128	126, 127	oveq12d 7430	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2↑2) · ((𝑌 · 𝑍)↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑍↑2))))
129	49, 97	sqmuld 14130	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) = ((2↑2) · ((𝑌 · 𝑍)↑2)))
130	122, 100, 101	mulassd 11244	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · (𝑍↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑍↑2))))
131	128, 129, 130	3eqtr4d 2781	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) = (((2 · 2) · (𝑌↑2)) · (𝑍↑2)))
132	43, 44	sqmuld 14130	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑋 · 𝑌)↑2) = ((𝑋↑2) · (𝑌↑2)))
133	102, 100	mulcomd 11242	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑋↑2) · (𝑌↑2)) = ((𝑌↑2) · (𝑋↑2)))
134	132, 133	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑋 · 𝑌)↑2) = ((𝑌↑2) · (𝑋↑2)))
135	126, 134	oveq12d 7430	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2↑2) · ((𝑋 · 𝑌)↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑋↑2))))
136	122, 100, 102	mulassd 11244	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · (𝑋↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑋↑2))))
137	135, 89, 136	3eqtr4d 2781	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = (((2 · 2) · (𝑌↑2)) · (𝑋↑2)))
138	131, 137	oveq12d 7430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((((2 · 2) · (𝑌↑2)) · (𝑍↑2)) − (((2 · 2) · (𝑌↑2)) · (𝑋↑2))))
139	125, 138	eqtr4d 2774	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · ((𝑍↑2) − (𝑋↑2))) = (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)))
140	49, 49, 100, 103	mul4d 11433	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · 2) · ((𝑌↑2) · ((𝑍↑2) − (𝑋↑2)))) = ((2 · (𝑌↑2)) · (2 · ((𝑍↑2) − (𝑋↑2)))))
141	123, 139, 140	3eqtr3d 2779	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((2 · (𝑌↑2)) · (2 · ((𝑍↑2) − (𝑋↑2)))))
142	100, 103	subcld 11578	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) ∈ ℂ)
143		subsq 14181	. . . . . . . . . . . . . . . . 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 583	. . . . . . . . . . . . . . . 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 2781	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) − (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2)))
146	145	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2))) = (((2 · (𝑌 · 𝑍))↑2) − ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) − (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2))))
147	99, 95	nncand 11583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2))) = ((2 · (𝑋 · 𝑌))↑2))
148	142	sqcld 14116	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2) ∈ ℂ)
149	99, 105, 148	subsubd 11606	. . . . . . . . . . . . . 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 2779	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = ((((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2)))
151	95	mulridd 11238	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · 1) = ((2 · (𝑋 · 𝑌))↑2))
152	102, 100	addcld 11240	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋↑2) + (𝑌↑2)) ∈ ℂ)
153	45, 107	mulcld 11241	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑋 · 𝑌) · (cos‘𝑂)) ∈ ℂ)
154	49, 153	mulcld 11241	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · ((𝑋 · 𝑌) · (cos‘𝑂))) ∈ ℂ)
155	152, 154	nncand 11583	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))) = (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))
156	100, 101	subcld 11578	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑌↑2) − (𝑍↑2)) ∈ ℂ)
157	156, 102	addcomd 11423	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑌↑2) − (𝑍↑2)) + (𝑋↑2)) = ((𝑋↑2) + ((𝑌↑2) − (𝑍↑2))))
158	100, 101, 102	subsubd 11606	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑌↑2) − (𝑍↑2)) + (𝑋↑2)))
159	102, 100, 101	addsubassd 11598	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2)) = ((𝑋↑2) + ((𝑌↑2) − (𝑍↑2))))
160	157, 158, 159	3eqtr4d 2781	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2)))
161	18, 3, 9, 71, 16	lawcos 26572	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝑍↑2) = (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂)))))
162	10, 4, 5, 21, 19, 161	syl32anc 1377	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑍↑2) = (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂)))))
163	162	oveq2d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2)) = (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))))
164	160, 163	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))))
165	49, 45, 107	mulassd 11244	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌)) · (cos‘𝑂)) = (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))
166	155, 164, 165	3eqtr4d 2781	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = ((2 · (𝑋 · 𝑌)) · (cos‘𝑂)))
167	166	oveq1d 7427	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2) = (((2 · (𝑋 · 𝑌)) · (cos‘𝑂))↑2))
168	94, 107	sqmuld 14130	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌)) · (cos‘𝑂))↑2) = (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)))
169	167, 168	eqtr2d 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)) = (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2))
170	169	oveq2d 7428	. . . . . . . . . . . . 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 2781	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · 1) = ((((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2))))
172	112, 113, 171	3eqtr3d 2779	. . . . . . . . . . 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 11427	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)))
174		subsq 14181	. . . . . . . . . . 11 ⊢ (((2 · (𝑌 · 𝑍)) ∈ ℂ ∧ ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) ∈ ℂ) → (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) · ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))))
175	98, 104, 174	syl2anc 583	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) · ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))))
176	100, 101	addcld 11240	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌↑2) + (𝑍↑2)) ∈ ℂ)
177	98, 176, 102	addsubassd 11598	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2)) = ((2 · (𝑌 · 𝑍)) + (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))))
178	100, 101, 102	addsubassd 11598	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2)) = ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))
179	178	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))))
180	177, 179	eqtr2d 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2)))
181		binom2 14188	. . . . . . . . . . . . . . 15 ⊢ ((𝑌 ∈ ℂ ∧ 𝑍 ∈ ℂ) → ((𝑌 + 𝑍)↑2) = (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2)))
182	44, 82, 181	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 + 𝑍)↑2) = (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2)))
183	100, 98, 101	add32d 11448	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2)) = (((𝑌↑2) + (𝑍↑2)) + (2 · (𝑌 · 𝑍))))
184	176, 98	addcomd 11423	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) + (2 · (𝑌 · 𝑍))) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))))
185	182, 183, 184	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌 + 𝑍)↑2) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))))
186	185	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2)))
187	44, 82	addcld 11240	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 + 𝑍) ∈ ℂ)
188		subsq 14181	. . . . . . . . . . . . . . 15 ⊢ (((𝑌 + 𝑍) ∈ ℂ ∧ 𝑋 ∈ ℂ) → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋)))
189	187, 43, 188	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋)))
190	69	oveq2i 7423	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 𝑆) = (2 · (((𝑋 + 𝑌) + 𝑍) / 2))
191	75	recnd 11249	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) ∈ ℂ)
192	191, 49, 51	divcan2d 11999	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (((𝑋 + 𝑌) + 𝑍) / 2)) = ((𝑋 + 𝑌) + 𝑍))
193	190, 192	eqtrid 2783	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · 𝑆) = ((𝑋 + 𝑌) + 𝑍))
194	43, 44, 82	addassd 11243	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
195	43, 187	addcomd 11423	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 + (𝑌 + 𝑍)) = ((𝑌 + 𝑍) + 𝑋))
196	193, 194, 195	3eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · 𝑆) = ((𝑌 + 𝑍) + 𝑋))
197	49, 78, 43	subdid 11677	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (𝑆 − 𝑋)) = ((2 · 𝑆) − (2 · 𝑋)))
198	193, 194	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑆) = (𝑋 + (𝑌 + 𝑍)))
199	43	2timesd 12462	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑋) = (𝑋 + 𝑋))
200	198, 199	oveq12d 7430	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑋)) = ((𝑋 + (𝑌 + 𝑍)) − (𝑋 + 𝑋)))
201	43, 187, 43	pnpcand 11615	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑋 + (𝑌 + 𝑍)) − (𝑋 + 𝑋)) = ((𝑌 + 𝑍) − 𝑋))
202	197, 200, 201	3eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝑆 − 𝑋)) = ((𝑌 + 𝑍) − 𝑋))
203	196, 202	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · 𝑆) · (2 · (𝑆 − 𝑋))) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋)))
204	189, 203	eqtr4d 2774	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = ((2 · 𝑆) · (2 · (𝑆 − 𝑋))))
205	49, 78, 49, 79	mul4d 11433	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝑆) · (2 · (𝑆 − 𝑋))) = ((2 · 2) · (𝑆 · (𝑆 − 𝑋))))
206	121	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · 2) = 4)
207	206	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 2) · (𝑆 · (𝑆 − 𝑋))) = (4 · (𝑆 · (𝑆 − 𝑋))))
208	204, 205, 207	3eqtrd 2775	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (4 · (𝑆 · (𝑆 − 𝑋))))
209	180, 186, 208	3eqtr2d 2777	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (4 · (𝑆 · (𝑆 − 𝑋))))
210	98, 176	subcld 11578	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) ∈ ℂ)
211	210, 102	addcomd 11423	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2)) = ((𝑋↑2) + ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2)))))
212	178	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))))
213	98, 176, 102	subsubd 11606	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2)))
214	212, 213	eqtr3d 2773	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2)))
215	102, 176, 98	subsub2d 11607	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍)))) = ((𝑋↑2) + ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2)))))
216	211, 214, 215	3eqtr4d 2781	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍)))))
217	100, 101, 98	addsubassd 11598	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = ((𝑌↑2) + ((𝑍↑2) − (2 · (𝑌 · 𝑍)))))
218	101, 98	subcld 11578	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑍↑2) − (2 · (𝑌 · 𝑍))) ∈ ℂ)
219	100, 218	addcomd 11423	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌↑2) + ((𝑍↑2) − (2 · (𝑌 · 𝑍)))) = (((𝑍↑2) − (2 · (𝑌 · 𝑍))) + (𝑌↑2)))
220	44, 82	mulcomd 11242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑌 · 𝑍) = (𝑍 · 𝑌))
221	220	oveq2d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑌 · 𝑍)) = (2 · (𝑍 · 𝑌)))
222	221	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑍↑2) − (2 · (𝑌 · 𝑍))) = ((𝑍↑2) − (2 · (𝑍 · 𝑌))))
223	222	oveq1d 7427	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑍↑2) − (2 · (𝑌 · 𝑍))) + (𝑌↑2)) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
224	217, 219, 223	3eqtrd 2775	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
225		binom2sub 14190	. . . . . . . . . . . . . . 15 ⊢ ((𝑍 ∈ ℂ ∧ 𝑌 ∈ ℂ) → ((𝑍 − 𝑌)↑2) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
226	82, 44, 225	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑍 − 𝑌)↑2) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
227	224, 226	eqtr4d 2774	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = ((𝑍 − 𝑌)↑2))
228	227	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍)))) = ((𝑋↑2) − ((𝑍 − 𝑌)↑2)))
229	82, 44	subcld 11578	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍 − 𝑌) ∈ ℂ)
230		subsq 14181	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ ℂ ∧ (𝑍 − 𝑌) ∈ ℂ) → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌))))
231	43, 229, 230	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌))))
232	49, 78, 44	subdid 11677	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (𝑆 − 𝑌)) = ((2 · 𝑆) − (2 · 𝑌)))
233	43, 44, 82	add32d 11448	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌))
234	193, 233	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑆) = ((𝑋 + 𝑍) + 𝑌))
235	44	2timesd 12462	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑌) = (𝑌 + 𝑌))
236	234, 235	oveq12d 7430	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑌)) = (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌)))
237	43, 82	addcld 11240	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 + 𝑍) ∈ ℂ)
238	237, 44, 44	pnpcan2d 11616	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌)) = ((𝑋 + 𝑍) − 𝑌))
239	43, 82, 44, 238	assraddsubd 11635	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌)) = (𝑋 + (𝑍 − 𝑌)))
240	232, 236, 239	3eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝑆 − 𝑌)) = (𝑋 + (𝑍 − 𝑌)))
241	49, 78, 82	subdid 11677	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (𝑆 − 𝑍)) = ((2 · 𝑆) − (2 · 𝑍)))
242	82	2timesd 12462	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑍) = (𝑍 + 𝑍))
243	193, 242	oveq12d 7430	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑍)) = (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍)))
244	43, 44	addcld 11240	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ ℂ)
245	244, 82, 82	pnpcan2d 11616	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍)) = ((𝑋 + 𝑌) − 𝑍))
246	43, 82, 44	subsub3d 11608	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 − (𝑍 − 𝑌)) = ((𝑋 + 𝑌) − 𝑍))
247	245, 246	eqtr4d 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍)) = (𝑋 − (𝑍 − 𝑌)))
248	241, 243, 247	3eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝑆 − 𝑍)) = (𝑋 − (𝑍 − 𝑌)))
249	240, 248	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍))) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌))))
250	231, 249	eqtr4d 2774	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍))))
251	49, 81, 49, 83	mul4d 11433	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍))) = ((2 · 2) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
252	206	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 2) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
253	250, 251, 252	3eqtrd 2775	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
254	216, 228, 253	3eqtrd 2775	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
255	209, 254	oveq12d 7430	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) · ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))) = ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
256	173, 175, 255	3eqtrd 2775	. . . . . . . . 9 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
257	68, 84	mulcld 11241	. . . . . . . . . 10 ⊢ (𝜑 → (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ)
258	68, 80, 257	mulassd 11244	. . . . . . . . 9 ⊢ (𝜑 → ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) = (4 · ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
259	80, 68, 84	mul12d 11430	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) = (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
260	259	oveq2d 7428	. . . . . . . . 9 ⊢ (𝜑 → (4 · ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))) = (4 · (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
261	256, 258, 260	3eqtrd 2775	. . . . . . . 8 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = (4 · (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
262	92, 93, 261	3eqtr3d 2779	. . . . . . 7 ⊢ (𝜑 → (4 · (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2))) = (4 · (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
263	66, 86, 68, 88, 262	mulcanad 11856	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) = (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
264	263	oveq1d 7427	. . . . 5 ⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) / 4) = ((4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) / 4))
265	64, 65, 68, 88	div23d 12034	. . . . 5 ⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) / 4) = ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2)))
266	77, 8	resubcld 11649	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 − 𝑋) ∈ ℝ)
267	77, 266	remulcld 11251	. . . . . . . 8 ⊢ (𝜑 → (𝑆 · (𝑆 − 𝑋)) ∈ ℝ)
268	77, 13	resubcld 11649	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 − 𝑌) ∈ ℝ)
269	77, 74	resubcld 11649	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 − 𝑍) ∈ ℝ)
270	268, 269	remulcld 11251	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 − 𝑌) · (𝑆 − 𝑍)) ∈ ℝ)
271	267, 270	remulcld 11251	. . . . . . 7 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℝ)
272	271	recnd 11249	. . . . . 6 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ)
273	272, 68, 88	divcan3d 12002	. . . . 5 ⊢ (𝜑 → ((4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) / 4) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
274	264, 265, 273	3eqtr3d 2779	. . . 4 ⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2)) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
275	48, 63, 274	3eqtrd 2775	. . 3 ⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
276	275	fveq2d 6895	. 2 ⊢ (𝜑 → (√‘((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2)) = (√‘((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
277	40, 276	eqtr3d 2773	1 ⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))) = (√‘((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2105 ≠ wne 2939 ∖ cdif 3945 {csn 4628 class class class wbr 5148 ‘cfv 6543 (class class class)co 7412 ∈ cmpo 7414 ℂcc 11114 ℝcr 11115 0cc0 11116 1c1 11117 + caddc 11119 · cmul 11121 ≤ cle 11256 − cmin 11451 -cneg 11452 / cdiv 11878 2c2 12274 4c4 12276 (,]cioc 13332 ↑cexp 14034 ℑcim 15052 √csqrt 15187 abscabs 15188 sincsin 16014 cosccos 16015 πcpi 16017 logclog 26314

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-inf2 9642 ax-cnex 11172 ax-resscn 11173 ax-1cn 11174 ax-icn 11175 ax-addcl 11176 ax-addrcl 11177 ax-mulcl 11178 ax-mulrcl 11179 ax-mulcom 11180 ax-addass 11181 ax-mulass 11182 ax-distr 11183 ax-i2m1 11184 ax-1ne0 11185 ax-1rid 11186 ax-rnegex 11187 ax-rrecex 11188 ax-cnre 11189 ax-pre-lttri 11190 ax-pre-lttrn 11191 ax-pre-ltadd 11192 ax-pre-mulgt0 11193 ax-pre-sup 11194 ax-addf 11195

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7674 df-om 7860 df-1st 7979 df-2nd 7980 df-supp 8152 df-frecs 8272 df-wrecs 8303 df-recs 8377 df-rdg 8416 df-1o 8472 df-2o 8473 df-er 8709 df-map 8828 df-pm 8829 df-ixp 8898 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fsupp 9368 df-fi 9412 df-sup 9443 df-inf 9444 df-oi 9511 df-card 9940 df-pnf 11257 df-mnf 11258 df-xr 11259 df-ltxr 11260 df-le 11261 df-sub 11453 df-neg 11454 df-div 11879 df-nn 12220 df-2 12282 df-3 12283 df-4 12284 df-5 12285 df-6 12286 df-7 12287 df-8 12288 df-9 12289 df-n0 12480 df-z 12566 df-dec 12685 df-uz 12830 df-q 12940 df-rp 12982 df-xneg 13099 df-xadd 13100 df-xmul 13101 df-ioo 13335 df-ioc 13336 df-ico 13337 df-icc 13338 df-fz 13492 df-fzo 13635 df-fl 13764 df-mod 13842 df-seq 13974 df-exp 14035 df-fac 14241 df-bc 14270 df-hash 14298 df-shft 15021 df-cj 15053 df-re 15054 df-im 15055 df-sqrt 15189 df-abs 15190 df-limsup 15422 df-clim 15439 df-rlim 15440 df-sum 15640 df-ef 16018 df-sin 16020 df-cos 16021 df-pi 16023 df-struct 17087 df-sets 17104 df-slot 17122 df-ndx 17134 df-base 17152 df-ress 17181 df-plusg 17217 df-mulr 17218 df-starv 17219 df-sca 17220 df-vsca 17221 df-ip 17222 df-tset 17223 df-ple 17224 df-ds 17226 df-unif 17227 df-hom 17228 df-cco 17229 df-rest 17375 df-topn 17376 df-0g 17394 df-gsum 17395 df-topgen 17396 df-pt 17397 df-prds 17400 df-xrs 17455 df-qtop 17460 df-imas 17461 df-xps 17463 df-mre 17537 df-mrc 17538 df-acs 17540 df-mgm 18568 df-sgrp 18647 df-mnd 18663 df-submnd 18709 df-mulg 18991 df-cntz 19226 df-cmn 19695 df-psmet 21140 df-xmet 21141 df-met 21142 df-bl 21143 df-mopn 21144 df-fbas 21145 df-fg 21146 df-cnfld 21149 df-top 22629 df-topon 22646 df-topsp 22668 df-bases 22682 df-cld 22756 df-ntr 22757 df-cls 22758 df-nei 22835 df-lp 22873 df-perf 22874 df-cn 22964 df-cnp 22965 df-haus 23052 df-tx 23299 df-hmeo 23492 df-fil 23583 df-fm 23675 df-flim 23676 df-flf 23677 df-xms 24059 df-ms 24060 df-tms 24061 df-cncf 24631 df-limc 25628 df-dv 25629 df-log 26316

This theorem is referenced by: (None)

W3C validator