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 26869

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 11168	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
2	1	rehalfcld 12454	. . . . 5 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
3		heron.x	. . . . . . 7 ⊢ 𝑋 = (abs‘(𝐵 − 𝐶))
4		heron.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5		heron.c	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℂ)
6	4, 5	subcld 11528	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
7	6	abscld 15438	. . . . . . 7 ⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) ∈ ℝ)
8	3, 7	eqeltrid 2856	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℝ)
9		heron.y	. . . . . . 7 ⊢ 𝑌 = (abs‘(𝐴 − 𝐶))
10		heron.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℂ)
11	10, 5	subcld 11528	. . . . . . . 8 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ)
12	11	abscld 15438	. . . . . . 7 ⊢ (𝜑 → (abs‘(𝐴 − 𝐶)) ∈ ℝ)
13	9, 12	eqeltrid 2856	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ ℝ)
14	8, 13	remulcld 11198	. . . . 5 ⊢ (𝜑 → (𝑋 · 𝑌) ∈ ℝ)
15	2, 14	remulcld 11198	. . . 4 ⊢ (𝜑 → ((1 / 2) · (𝑋 · 𝑌)) ∈ ℝ)
16		heron.o	. . . . . . 7 ⊢ 𝑂 = ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶))
17		negpitopissre 26571	. . . . . . . . 9 ⊢ (-π(,]π) ⊆ ℝ
18		heron.f	. . . . . . . . . 10 ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))
19		heron.bc	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
20	4, 5, 19	subne0d 11537	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐶) ≠ 0)
21		heron.ac	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
22	10, 5, 21	subne0d 11537	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 − 𝐶) ≠ 0)
23	18, 6, 20, 11, 22	angcld 26836	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ (-π(,]π))
24	17, 23	sselid 3925	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ ℝ)
25	24	recnd 11196	. . . . . . 7 ⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ ℂ)
26	16, 25	eqeltrid 2856	. . . . . 6 ⊢ (𝜑 → 𝑂 ∈ ℂ)
27	26	sincld 16134	. . . . 5 ⊢ (𝜑 → (sin‘𝑂) ∈ ℂ)
28	27	abscld 15438	. . . 4 ⊢ (𝜑 → (abs‘(sin‘𝑂)) ∈ ℝ)
29	15, 28	remulcld 11198	. . 3 ⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))) ∈ ℝ)
30		halfge0 12423	. . . . . 6 ⊢ 0 ≤ (1 / 2)
31	30	a1i 11	. . . . 5 ⊢ (𝜑 → 0 ≤ (1 / 2))
32	6	absge0d 15446	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (abs‘(𝐵 − 𝐶)))
33	32, 3	breqtrrdi 5132	. . . . . 6 ⊢ (𝜑 → 0 ≤ 𝑋)
34	11	absge0d 15446	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (abs‘(𝐴 − 𝐶)))
35	34, 9	breqtrrdi 5132	. . . . . 6 ⊢ (𝜑 → 0 ≤ 𝑌)
36	8, 13, 33, 35	mulge0d 11750	. . . . 5 ⊢ (𝜑 → 0 ≤ (𝑋 · 𝑌))
37	2, 14, 31, 36	mulge0d 11750	. . . 4 ⊢ (𝜑 → 0 ≤ ((1 / 2) · (𝑋 · 𝑌)))
38	27	absge0d 15446	. . . 4 ⊢ (𝜑 → 0 ≤ (abs‘(sin‘𝑂)))
39	15, 28, 37, 38	mulge0d 11750	. . 3 ⊢ (𝜑 → 0 ≤ (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))))
40	29, 39	sqrtsqd 15419	. 2 ⊢ (𝜑 → (√‘((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2)) = (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))))
41		halfcn 12421	. . . . . . 7 ⊢ (1 / 2) ∈ ℂ
42	41	a1i 11	. . . . . 6 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
43	8	recnd 11196	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℂ)
44	13	recnd 11196	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ ℂ)
45	43, 44	mulcld 11188	. . . . . 6 ⊢ (𝜑 → (𝑋 · 𝑌) ∈ ℂ)
46	42, 45	mulcld 11188	. . . . 5 ⊢ (𝜑 → ((1 / 2) · (𝑋 · 𝑌)) ∈ ℂ)
47	28	recnd 11196	. . . . 5 ⊢ (𝜑 → (abs‘(sin‘𝑂)) ∈ ℂ)
48	46, 47	sqmuld 14157	. . . 4 ⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2) = ((((1 / 2) · (𝑋 · 𝑌))↑2) · ((abs‘(sin‘𝑂))↑2)))
49		2cnd 12282	. . . . . . 7 ⊢ (𝜑 → 2 ∈ ℂ)
50		2ne0 12310	. . . . . . . 8 ⊢ 2 ≠ 0
51	50	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ≠ 0)
52	45, 49, 51	sqdivd 14158	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌) / 2)↑2) = (((𝑋 · 𝑌)↑2) / (2↑2)))
53	45, 49, 51	divrec2d 11957	. . . . . . 7 ⊢ (𝜑 → ((𝑋 · 𝑌) / 2) = ((1 / 2) · (𝑋 · 𝑌)))
54	53	oveq1d 7396	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌) / 2)↑2) = (((1 / 2) · (𝑋 · 𝑌))↑2))
55		sq2 14196	. . . . . . . 8 ⊢ (2↑2) = 4
56	55	a1i 11	. . . . . . 7 ⊢ (𝜑 → (2↑2) = 4)
57	56	oveq2d 7397	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌)↑2) / (2↑2)) = (((𝑋 · 𝑌)↑2) / 4))
58	52, 54, 57	3eqtr3d 2795	. . . . 5 ⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌))↑2) = (((𝑋 · 𝑌)↑2) / 4))
59	16, 24	eqeltrid 2856	. . . . . . 7 ⊢ (𝜑 → 𝑂 ∈ ℝ)
60	59	resincld 16147	. . . . . 6 ⊢ (𝜑 → (sin‘𝑂) ∈ ℝ)
61		absresq 15301	. . . . . 6 ⊢ ((sin‘𝑂) ∈ ℝ → ((abs‘(sin‘𝑂))↑2) = ((sin‘𝑂)↑2))
62	60, 61	syl 17	. . . . 5 ⊢ (𝜑 → ((abs‘(sin‘𝑂))↑2) = ((sin‘𝑂)↑2))
63	58, 62	oveq12d 7399	. . . 4 ⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌))↑2) · ((abs‘(sin‘𝑂))↑2)) = ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2)))
64	45	sqcld 14143	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 · 𝑌)↑2) ∈ ℂ)
65	27	sqcld 14143	. . . . . . . 8 ⊢ (𝜑 → ((sin‘𝑂)↑2) ∈ ℂ)
66	64, 65	mulcld 11188	. . . . . . 7 ⊢ (𝜑 → (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) ∈ ℂ)
67		4cn 12289	. . . . . . . . 9 ⊢ 4 ∈ ℂ
68	67	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 4 ∈ ℂ)
69		heron.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (((𝑋 + 𝑌) + 𝑍) / 2)
70	8, 13	readdcld 11197	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ ℝ)
71		heron.z	. . . . . . . . . . . . . . 15 ⊢ 𝑍 = (abs‘(𝐴 − 𝐵))
72	10, 4	subcld 11528	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)
73	72	abscld 15438	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ∈ ℝ)
74	71, 73	eqeltrid 2856	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑍 ∈ ℝ)
75	70, 74	readdcld 11197	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) ∈ ℝ)
76	75	rehalfcld 12454	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) / 2) ∈ ℝ)
77	69, 76	eqeltrid 2856	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ ℝ)
78	77	recnd 11196	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ ℂ)
79	78, 43	subcld 11528	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 − 𝑋) ∈ ℂ)
80	78, 79	mulcld 11188	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 · (𝑆 − 𝑋)) ∈ ℂ)
81	78, 44	subcld 11528	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 − 𝑌) ∈ ℂ)
82	74	recnd 11196	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ ℂ)
83	78, 82	subcld 11528	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 − 𝑍) ∈ ℂ)
84	81, 83	mulcld 11188	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 − 𝑌) · (𝑆 − 𝑍)) ∈ ℂ)
85	80, 84	mulcld 11188	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ)
86	68, 85	mulcld 11188	. . . . . . 7 ⊢ (𝜑 → (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) ∈ ℂ)
87		4ne0 12315	. . . . . . . 8 ⊢ 4 ≠ 0
88	87	a1i 11	. . . . . . 7 ⊢ (𝜑 → 4 ≠ 0)
89	49, 45	sqmuld 14157	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = ((2↑2) · ((𝑋 · 𝑌)↑2)))
90	56	oveq1d 7396	. . . . . . . . . 10 ⊢ (𝜑 → ((2↑2) · ((𝑋 · 𝑌)↑2)) = (4 · ((𝑋 · 𝑌)↑2)))
91	89, 90	eqtr2d 2788	. . . . . . . . 9 ⊢ (𝜑 → (4 · ((𝑋 · 𝑌)↑2)) = ((2 · (𝑋 · 𝑌))↑2))
92	91	oveq1d 7396	. . . . . . . 8 ⊢ (𝜑 → ((4 · ((𝑋 · 𝑌)↑2)) · ((sin‘𝑂)↑2)) = (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)))
93	68, 64, 65	mulassd 11191	. . . . . . . 8 ⊢ (𝜑 → ((4 · ((𝑋 · 𝑌)↑2)) · ((sin‘𝑂)↑2)) = (4 · (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2))))
94	49, 45	mulcld 11188	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑋 · 𝑌)) ∈ ℂ)
95	94	sqcld 14143	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) ∈ ℂ)
96	95, 65	mulcld 11188	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) ∈ ℂ)
97	44, 82	mulcld 11188	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 · 𝑍) ∈ ℂ)
98	49, 97	mulcld 11188	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑌 · 𝑍)) ∈ ℂ)
99	98	sqcld 14143	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) ∈ ℂ)
100	44	sqcld 14143	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌↑2) ∈ ℂ)
101	82	sqcld 14143	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍↑2) ∈ ℂ)
102	43	sqcld 14143	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
103	101, 102	subcld 11528	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑍↑2) − (𝑋↑2)) ∈ ℂ)
104	100, 103	addcld 11187	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) ∈ ℂ)
105	104	sqcld 14143	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) ∈ ℂ)
106	99, 105	subcld 11528	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) ∈ ℂ)
107	26	coscld 16135	. . . . . . . . . . . . 13 ⊢ (𝜑 → (cos‘𝑂) ∈ ℂ)
108	107	sqcld 14143	. . . . . . . . . . . 12 ⊢ (𝜑 → ((cos‘𝑂)↑2) ∈ ℂ)
109	95, 108	mulcld 11188	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)) ∈ ℂ)
110		sincossq 16180	. . . . . . . . . . . . . 14 ⊢ (𝑂 ∈ ℂ → (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2)) = 1)
111	26, 110	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2)) = 1)
112	111	oveq2d 7397	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2))) = (((2 · (𝑋 · 𝑌))↑2) · 1))
113	95, 65, 108	adddid 11192	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2))) = ((((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) + (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2))))
114	100	2timesd 12450	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · (𝑌↑2)) = ((𝑌↑2) + (𝑌↑2)))
115	100, 103, 100	ppncand 11568	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) = ((𝑌↑2) + (𝑌↑2)))
116	114, 115	eqtr4d 2790	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑌↑2)) = (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))))
117	103	2timesd 12450	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · ((𝑍↑2) − (𝑋↑2))) = (((𝑍↑2) − (𝑋↑2)) + ((𝑍↑2) − (𝑋↑2))))
118	100, 103, 103	pnncand 11567	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) = (((𝑍↑2) − (𝑋↑2)) + ((𝑍↑2) − (𝑋↑2))))
119	117, 118	eqtr4d 2790	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · ((𝑍↑2) − (𝑋↑2))) = (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))))
120	116, 119	oveq12d 7399	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · (𝑌↑2)) · (2 · ((𝑍↑2) − (𝑋↑2)))) = ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) · (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))))))
121		2t2e4 12367	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 · 2) = 4
122	121, 68	eqeltrid 2856	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · 2) ∈ ℂ)
123	122, 100, 103	mulassd 11191	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · ((𝑍↑2) − (𝑋↑2))) = ((2 · 2) · ((𝑌↑2) · ((𝑍↑2) − (𝑋↑2)))))
124	122, 100	mulcld 11188	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 · 2) · (𝑌↑2)) ∈ ℂ)
125	124, 101, 102	subdid 11629	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · ((𝑍↑2) − (𝑋↑2))) = ((((2 · 2) · (𝑌↑2)) · (𝑍↑2)) − (((2 · 2) · (𝑌↑2)) · (𝑋↑2))))
126	49	sqvald 14142	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (2↑2) = (2 · 2))
127	44, 82	sqmuld 14157	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑌 · 𝑍)↑2) = ((𝑌↑2) · (𝑍↑2)))
128	126, 127	oveq12d 7399	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2↑2) · ((𝑌 · 𝑍)↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑍↑2))))
129	49, 97	sqmuld 14157	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) = ((2↑2) · ((𝑌 · 𝑍)↑2)))
130	122, 100, 101	mulassd 11191	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · (𝑍↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑍↑2))))
131	128, 129, 130	3eqtr4d 2797	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) = (((2 · 2) · (𝑌↑2)) · (𝑍↑2)))
132	43, 44	sqmuld 14157	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑋 · 𝑌)↑2) = ((𝑋↑2) · (𝑌↑2)))
133	102, 100	mulcomd 11189	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑋↑2) · (𝑌↑2)) = ((𝑌↑2) · (𝑋↑2)))
134	132, 133	eqtrd 2787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑋 · 𝑌)↑2) = ((𝑌↑2) · (𝑋↑2)))
135	126, 134	oveq12d 7399	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2↑2) · ((𝑋 · 𝑌)↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑋↑2))))
136	122, 100, 102	mulassd 11191	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · (𝑋↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑋↑2))))
137	135, 89, 136	3eqtr4d 2797	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = (((2 · 2) · (𝑌↑2)) · (𝑋↑2)))
138	131, 137	oveq12d 7399	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((((2 · 2) · (𝑌↑2)) · (𝑍↑2)) − (((2 · 2) · (𝑌↑2)) · (𝑋↑2))))
139	125, 138	eqtr4d 2790	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · ((𝑍↑2) − (𝑋↑2))) = (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)))
140	49, 49, 100, 103	mul4d 11381	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · 2) · ((𝑌↑2) · ((𝑍↑2) − (𝑋↑2)))) = ((2 · (𝑌↑2)) · (2 · ((𝑍↑2) − (𝑋↑2)))))
141	123, 139, 140	3eqtr3d 2795	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((2 · (𝑌↑2)) · (2 · ((𝑍↑2) − (𝑋↑2)))))
142	100, 103	subcld 11528	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) ∈ ℂ)
143		subsq 14209	. . . . . . . . . . . . . . . . 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 592	. . . . . . . . . . . . . . . 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 2797	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) − (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2)))
146	145	oveq2d 7397	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2))) = (((2 · (𝑌 · 𝑍))↑2) − ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) − (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2))))
147	99, 95	nncand 11533	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2))) = ((2 · (𝑋 · 𝑌))↑2))
148	142	sqcld 14143	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2) ∈ ℂ)
149	99, 105, 148	subsubd 11556	. . . . . . . . . . . . . 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 2795	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = ((((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2)))
151	95	mulridd 11185	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · 1) = ((2 · (𝑋 · 𝑌))↑2))
152	102, 100	addcld 11187	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋↑2) + (𝑌↑2)) ∈ ℂ)
153	45, 107	mulcld 11188	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑋 · 𝑌) · (cos‘𝑂)) ∈ ℂ)
154	49, 153	mulcld 11188	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · ((𝑋 · 𝑌) · (cos‘𝑂))) ∈ ℂ)
155	152, 154	nncand 11533	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))) = (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))
156	100, 101	subcld 11528	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑌↑2) − (𝑍↑2)) ∈ ℂ)
157	156, 102	addcomd 11371	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑌↑2) − (𝑍↑2)) + (𝑋↑2)) = ((𝑋↑2) + ((𝑌↑2) − (𝑍↑2))))
158	100, 101, 102	subsubd 11556	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑌↑2) − (𝑍↑2)) + (𝑋↑2)))
159	102, 100, 101	addsubassd 11548	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2)) = ((𝑋↑2) + ((𝑌↑2) − (𝑍↑2))))
160	157, 158, 159	3eqtr4d 2797	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2)))
161	18, 3, 9, 71, 16	lawcos 26847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝑍↑2) = (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂)))))
162	10, 4, 5, 21, 19, 161	syl32anc 1389	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑍↑2) = (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂)))))
163	162	oveq2d 7397	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2)) = (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))))
164	160, 163	eqtrd 2787	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))))
165	49, 45, 107	mulassd 11191	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌)) · (cos‘𝑂)) = (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))
166	155, 164, 165	3eqtr4d 2797	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = ((2 · (𝑋 · 𝑌)) · (cos‘𝑂)))
167	166	oveq1d 7396	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2) = (((2 · (𝑋 · 𝑌)) · (cos‘𝑂))↑2))
168	94, 107	sqmuld 14157	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌)) · (cos‘𝑂))↑2) = (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)))
169	167, 168	eqtr2d 2788	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)) = (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2))
170	169	oveq2d 7397	. . . . . . . . . . . . 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 2797	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · 1) = ((((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2))))
172	112, 113, 171	3eqtr3d 2795	. . . . . . . . . . 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 11375	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)))
174		subsq 14209	. . . . . . . . . . 11 ⊢ (((2 · (𝑌 · 𝑍)) ∈ ℂ ∧ ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) ∈ ℂ) → (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) · ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))))
175	98, 104, 174	syl2anc 592	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) · ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))))
176	100, 101	addcld 11187	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌↑2) + (𝑍↑2)) ∈ ℂ)
177	98, 176, 102	addsubassd 11548	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2)) = ((2 · (𝑌 · 𝑍)) + (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))))
178	100, 101, 102	addsubassd 11548	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2)) = ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))
179	178	oveq2d 7397	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))))
180	177, 179	eqtr2d 2788	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2)))
181		binom2 14216	. . . . . . . . . . . . . . 15 ⊢ ((𝑌 ∈ ℂ ∧ 𝑍 ∈ ℂ) → ((𝑌 + 𝑍)↑2) = (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2)))
182	44, 82, 181	syl2anc 592	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 + 𝑍)↑2) = (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2)))
183	100, 98, 101	add32d 11397	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2)) = (((𝑌↑2) + (𝑍↑2)) + (2 · (𝑌 · 𝑍))))
184	176, 98	addcomd 11371	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) + (2 · (𝑌 · 𝑍))) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))))
185	182, 183, 184	3eqtrd 2791	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌 + 𝑍)↑2) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))))
186	185	oveq1d 7396	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2)))
187	44, 82	addcld 11187	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 + 𝑍) ∈ ℂ)
188		subsq 14209	. . . . . . . . . . . . . . 15 ⊢ (((𝑌 + 𝑍) ∈ ℂ ∧ 𝑋 ∈ ℂ) → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋)))
189	187, 43, 188	syl2anc 592	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋)))
190	69	oveq2i 7392	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 𝑆) = (2 · (((𝑋 + 𝑌) + 𝑍) / 2))
191	75	recnd 11196	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) ∈ ℂ)
192	191, 49, 51	divcan2d 11955	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (((𝑋 + 𝑌) + 𝑍) / 2)) = ((𝑋 + 𝑌) + 𝑍))
193	190, 192	eqtrid 2799	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · 𝑆) = ((𝑋 + 𝑌) + 𝑍))
194	43, 44, 82	addassd 11190	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
195	43, 187	addcomd 11371	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 + (𝑌 + 𝑍)) = ((𝑌 + 𝑍) + 𝑋))
196	193, 194, 195	3eqtrd 2791	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · 𝑆) = ((𝑌 + 𝑍) + 𝑋))
197	49, 78, 43	subdid 11629	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (𝑆 − 𝑋)) = ((2 · 𝑆) − (2 · 𝑋)))
198	193, 194	eqtrd 2787	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑆) = (𝑋 + (𝑌 + 𝑍)))
199	43	2timesd 12450	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑋) = (𝑋 + 𝑋))
200	198, 199	oveq12d 7399	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑋)) = ((𝑋 + (𝑌 + 𝑍)) − (𝑋 + 𝑋)))
201	43, 187, 43	pnpcand 11565	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑋 + (𝑌 + 𝑍)) − (𝑋 + 𝑋)) = ((𝑌 + 𝑍) − 𝑋))
202	197, 200, 201	3eqtrd 2791	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝑆 − 𝑋)) = ((𝑌 + 𝑍) − 𝑋))
203	196, 202	oveq12d 7399	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · 𝑆) · (2 · (𝑆 − 𝑋))) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋)))
204	189, 203	eqtr4d 2790	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = ((2 · 𝑆) · (2 · (𝑆 − 𝑋))))
205	49, 78, 49, 79	mul4d 11381	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝑆) · (2 · (𝑆 − 𝑋))) = ((2 · 2) · (𝑆 · (𝑆 − 𝑋))))
206	121	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · 2) = 4)
207	206	oveq1d 7396	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 2) · (𝑆 · (𝑆 − 𝑋))) = (4 · (𝑆 · (𝑆 − 𝑋))))
208	204, 205, 207	3eqtrd 2791	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (4 · (𝑆 · (𝑆 − 𝑋))))
209	180, 186, 208	3eqtr2d 2793	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (4 · (𝑆 · (𝑆 − 𝑋))))
210	98, 176	subcld 11528	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) ∈ ℂ)
211	210, 102	addcomd 11371	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2)) = ((𝑋↑2) + ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2)))))
212	178	oveq2d 7397	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))))
213	98, 176, 102	subsubd 11556	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2)))
214	212, 213	eqtr3d 2789	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2)))
215	102, 176, 98	subsub2d 11557	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍)))) = ((𝑋↑2) + ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2)))))
216	211, 214, 215	3eqtr4d 2797	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍)))))
217	100, 101, 98	addsubassd 11548	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = ((𝑌↑2) + ((𝑍↑2) − (2 · (𝑌 · 𝑍)))))
218	101, 98	subcld 11528	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑍↑2) − (2 · (𝑌 · 𝑍))) ∈ ℂ)
219	100, 218	addcomd 11371	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌↑2) + ((𝑍↑2) − (2 · (𝑌 · 𝑍)))) = (((𝑍↑2) − (2 · (𝑌 · 𝑍))) + (𝑌↑2)))
220	44, 82	mulcomd 11189	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑌 · 𝑍) = (𝑍 · 𝑌))
221	220	oveq2d 7397	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑌 · 𝑍)) = (2 · (𝑍 · 𝑌)))
222	221	oveq2d 7397	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑍↑2) − (2 · (𝑌 · 𝑍))) = ((𝑍↑2) − (2 · (𝑍 · 𝑌))))
223	222	oveq1d 7396	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑍↑2) − (2 · (𝑌 · 𝑍))) + (𝑌↑2)) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
224	217, 219, 223	3eqtrd 2791	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
225		binom2sub 14219	. . . . . . . . . . . . . . 15 ⊢ ((𝑍 ∈ ℂ ∧ 𝑌 ∈ ℂ) → ((𝑍 − 𝑌)↑2) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
226	82, 44, 225	syl2anc 592	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑍 − 𝑌)↑2) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
227	224, 226	eqtr4d 2790	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = ((𝑍 − 𝑌)↑2))
228	227	oveq2d 7397	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍)))) = ((𝑋↑2) − ((𝑍 − 𝑌)↑2)))
229	82, 44	subcld 11528	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍 − 𝑌) ∈ ℂ)
230		subsq 14209	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ ℂ ∧ (𝑍 − 𝑌) ∈ ℂ) → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌))))
231	43, 229, 230	syl2anc 592	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌))))
232	49, 78, 44	subdid 11629	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (𝑆 − 𝑌)) = ((2 · 𝑆) − (2 · 𝑌)))
233	43, 44, 82	add32d 11397	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌))
234	193, 233	eqtrd 2787	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑆) = ((𝑋 + 𝑍) + 𝑌))
235	44	2timesd 12450	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑌) = (𝑌 + 𝑌))
236	234, 235	oveq12d 7399	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑌)) = (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌)))
237	43, 82	addcld 11187	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 + 𝑍) ∈ ℂ)
238	237, 44, 44	pnpcan2d 11566	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌)) = ((𝑋 + 𝑍) − 𝑌))
239	43, 82, 44, 238	assraddsubd 11587	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌)) = (𝑋 + (𝑍 − 𝑌)))
240	232, 236, 239	3eqtrd 2791	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝑆 − 𝑌)) = (𝑋 + (𝑍 − 𝑌)))
241	49, 78, 82	subdid 11629	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (𝑆 − 𝑍)) = ((2 · 𝑆) − (2 · 𝑍)))
242	82	2timesd 12450	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑍) = (𝑍 + 𝑍))
243	193, 242	oveq12d 7399	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑍)) = (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍)))
244	43, 44	addcld 11187	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ ℂ)
245	244, 82, 82	pnpcan2d 11566	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍)) = ((𝑋 + 𝑌) − 𝑍))
246	43, 82, 44	subsub3d 11558	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 − (𝑍 − 𝑌)) = ((𝑋 + 𝑌) − 𝑍))
247	245, 246	eqtr4d 2790	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍)) = (𝑋 − (𝑍 − 𝑌)))
248	241, 243, 247	3eqtrd 2791	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝑆 − 𝑍)) = (𝑋 − (𝑍 − 𝑌)))
249	240, 248	oveq12d 7399	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍))) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌))))
250	231, 249	eqtr4d 2790	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍))))
251	49, 81, 49, 83	mul4d 11381	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍))) = ((2 · 2) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
252	206	oveq1d 7396	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 2) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
253	250, 251, 252	3eqtrd 2791	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
254	216, 228, 253	3eqtrd 2791	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
255	209, 254	oveq12d 7399	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) · ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))) = ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
256	173, 175, 255	3eqtrd 2791	. . . . . . . . 9 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
257	68, 84	mulcld 11188	. . . . . . . . . 10 ⊢ (𝜑 → (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ)
258	68, 80, 257	mulassd 11191	. . . . . . . . 9 ⊢ (𝜑 → ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) = (4 · ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
259	80, 68, 84	mul12d 11378	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) = (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
260	259	oveq2d 7397	. . . . . . . . 9 ⊢ (𝜑 → (4 · ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))) = (4 · (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
261	256, 258, 260	3eqtrd 2791	. . . . . . . 8 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = (4 · (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
262	92, 93, 261	3eqtr3d 2795	. . . . . . 7 ⊢ (𝜑 → (4 · (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2))) = (4 · (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
263	66, 86, 68, 88, 262	mulcanad 11808	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) = (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
264	263	oveq1d 7396	. . . . 5 ⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) / 4) = ((4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) / 4))
265	64, 65, 68, 88	div23d 11990	. . . . 5 ⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) / 4) = ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2)))
266	77, 8	resubcld 11601	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 − 𝑋) ∈ ℝ)
267	77, 266	remulcld 11198	. . . . . . . 8 ⊢ (𝜑 → (𝑆 · (𝑆 − 𝑋)) ∈ ℝ)
268	77, 13	resubcld 11601	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 − 𝑌) ∈ ℝ)
269	77, 74	resubcld 11601	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 − 𝑍) ∈ ℝ)
270	268, 269	remulcld 11198	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 − 𝑌) · (𝑆 − 𝑍)) ∈ ℝ)
271	267, 270	remulcld 11198	. . . . . . 7 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℝ)
272	271	recnd 11196	. . . . . 6 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ)
273	272, 68, 88	divcan3d 11958	. . . . 5 ⊢ (𝜑 → ((4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) / 4) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
274	264, 265, 273	3eqtr3d 2795	. . . 4 ⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2)) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
275	48, 63, 274	3eqtrd 2791	. . 3 ⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
276	275	fveq2d 6856	. 2 ⊢ (𝜑 → (√‘((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2)) = (√‘((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
277	40, 276	eqtr3d 2789	1 ⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))) = (√‘((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1550 ∈ wcel 2132 ≠ wne 2947 ∖ cdif 3892 {csn 4572 class class class wbr 5090 ‘cfv 6506 (class class class)co 7381 ∈ cmpo 7383 ℂcc 11057 ℝcr 11058 0cc0 11059 1c1 11060 + caddc 11062 · cmul 11064 ≤ cle 11203 − cmin 11400 -cneg 11401 / cdiv 11830 2c2 12258 4c4 12260 (,]cioc 13336 ↑cexp 14060 ℑcim 15097 √csqrt 15232 abscabs 15233 sincsin 16065 cosccos 16066 πcpi 16068 logclog 26585

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1805 ax-4 1819 ax-5 1920 ax-6 1977 ax-7 2018 ax-8 2134 ax-9 2142 ax-10 2165 ax-11 2181 ax-12 2202 ax-ext 2724 ax-rep 5217 ax-sep 5236 ax-nul 5246 ax-pow 5312 ax-pr 5380 ax-un 7703 ax-inf2 9582 ax-cnex 11115 ax-resscn 11116 ax-1cn 11117 ax-icn 11118 ax-addcl 11119 ax-addrcl 11120 ax-mulcl 11121 ax-mulrcl 11122 ax-mulcom 11123 ax-addass 11124 ax-mulass 11125 ax-distr 11126 ax-i2m1 11127 ax-1ne0 11128 ax-1rid 11129 ax-rnegex 11130 ax-rrecex 11131 ax-cnre 11132 ax-pre-lttri 11133 ax-pre-lttrn 11134 ax-pre-ltadd 11135 ax-pre-mulgt0 11136 ax-pre-sup 11137 ax-addf 11138

This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3or 1096 df-3an 1097 df-tru 1553 df-fal 1563 df-ex 1790 df-nf 1794 df-sb 2081 df-mo 2556 df-eu 2586 df-clab 2731 df-cleq 2744 df-clel 2827 df-nfc 2901 df-ne 2948 df-nel 3052 df-ral 3067 df-rex 3077 df-rmo 3357 df-reu 3358 df-rab 3405 df-v 3446 df-sbc 3736 df-csb 3844 df-dif 3898 df-un 3900 df-in 3902 df-ss 3912 df-pss 3915 df-nul 4277 df-if 4471 df-pw 4547 df-sn 4573 df-pr 4575 df-tp 4577 df-op 4579 df-uni 4856 df-int 4896 df-iun 4941 df-iin 4942 df-br 5091 df-opab 5153 df-mpt 5172 df-tr 5198 df-id 5531 df-eprel 5536 df-po 5544 df-so 5545 df-fr 5589 df-se 5590 df-we 5591 df-xp 5642 df-rel 5643 df-cnv 5644 df-co 5645 df-dm 5646 df-rn 5647 df-res 5648 df-ima 5649 df-pred 6273 df-ord 6334 df-on 6335 df-lim 6336 df-suc 6337 df-iota 6462 df-fun 6508 df-fn 6509 df-f 6510 df-f1 6511 df-fo 6512 df-f1o 6513 df-fv 6514 df-isom 6515 df-riota 7338 df-ov 7384 df-oprab 7385 df-mpo 7386 df-of 7645 df-om 7832 df-1st 7955 df-2nd 7956 df-supp 8125 df-frecs 8246 df-wrecs 8277 df-recs 8326 df-rdg 8365 df-1o 8421 df-2o 8422 df-er 8662 df-map 8794 df-pm 8795 df-ixp 8865 df-en 8913 df-dom 8914 df-sdom 8915 df-fin 8916 df-fsupp 9294 df-fi 9343 df-sup 9374 df-inf 9375 df-oi 9444 df-card 9883 df-pnf 11204 df-mnf 11205 df-xr 11206 df-ltxr 11207 df-le 11208 df-sub 11402 df-neg 11403 df-div 11831 df-nn 12197 df-2 12266 df-3 12267 df-4 12268 df-5 12269 df-6 12270 df-7 12271 df-8 12272 df-9 12273 df-n0 12468 df-z 12555 df-dec 12675 df-uz 12826 df-q 12936 df-rp 12980 df-xneg 13100 df-xadd 13101 df-xmul 13102 df-ioo 13339 df-ioc 13340 df-ico 13341 df-icc 13342 df-fz 13499 df-fzo 13646 df-fl 13788 df-mod 13866 df-seq 14001 df-exp 14061 df-fac 14273 df-bc 14302 df-hash 14330 df-shft 15066 df-cj 15098 df-re 15099 df-im 15100 df-sqrt 15234 df-abs 15235 df-limsup 15470 df-clim 15487 df-rlim 15488 df-sum 15686 df-ef 16069 df-sin 16071 df-cos 16072 df-pi 16074 df-struct 17155 df-sets 17172 df-slot 17190 df-ndx 17202 df-base 17218 df-ress 17239 df-plusg 17271 df-mulr 17272 df-starv 17273 df-sca 17274 df-vsca 17275 df-ip 17276 df-tset 17277 df-ple 17278 df-ds 17280 df-unif 17281 df-hom 17282 df-cco 17283 df-rest 17423 df-topn 17424 df-0g 17442 df-gsum 17443 df-topgen 17444 df-pt 17445 df-prds 17448 df-xrs 17504 df-qtop 17509 df-imas 17510 df-xps 17512 df-mre 17586 df-mrc 17587 df-acs 17589 df-mgm 18646 df-sgrp 18725 df-mnd 18741 df-submnd 18790 df-mulg 19082 df-cntz 19329 df-cmn 19794 df-psmet 21385 df-xmet 21386 df-met 21387 df-bl 21388 df-mopn 21389 df-fbas 21390 df-fg 21391 df-cnfld 21394 df-top 22923 df-topon 22940 df-topsp 22962 df-bases 22975 df-cld 23048 df-ntr 23049 df-cls 23050 df-nei 23127 df-lp 23165 df-perf 23166 df-cn 23256 df-cnp 23257 df-haus 23344 df-tx 23591 df-hmeo 23784 df-fil 23875 df-fm 23967 df-flim 23968 df-flf 23969 df-xms 24349 df-ms 24350 df-tms 24351 df-cncf 24909 df-limc 25897 df-dv 25898 df-log 26587

This theorem is referenced by: (None)

W3C validator