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 26783

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 11246	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
2	1	rehalfcld 12490	. . . . 5 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
3		heron.x	. . . . . . 7 ⊢ 𝑋 = (abs‘(𝐵 − 𝐶))
4		heron.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5		heron.c	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℂ)
6	4, 5	subcld 11602	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
7	6	abscld 15416	. . . . . . 7 ⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) ∈ ℝ)
8	3, 7	eqeltrid 2833	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℝ)
9		heron.y	. . . . . . 7 ⊢ 𝑌 = (abs‘(𝐴 − 𝐶))
10		heron.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℂ)
11	10, 5	subcld 11602	. . . . . . . 8 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ)
12	11	abscld 15416	. . . . . . 7 ⊢ (𝜑 → (abs‘(𝐴 − 𝐶)) ∈ ℝ)
13	9, 12	eqeltrid 2833	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ ℝ)
14	8, 13	remulcld 11275	. . . . 5 ⊢ (𝜑 → (𝑋 · 𝑌) ∈ ℝ)
15	2, 14	remulcld 11275	. . . 4 ⊢ (𝜑 → ((1 / 2) · (𝑋 · 𝑌)) ∈ ℝ)
16		heron.o	. . . . . . 7 ⊢ 𝑂 = ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶))
17		negpitopissre 26487	. . . . . . . . 9 ⊢ (-π(,]π) ⊆ ℝ
18		heron.f	. . . . . . . . . 10 ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))
19		heron.bc	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
20	4, 5, 19	subne0d 11611	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐶) ≠ 0)
21		heron.ac	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
22	10, 5, 21	subne0d 11611	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 − 𝐶) ≠ 0)
23	18, 6, 20, 11, 22	angcld 26750	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ (-π(,]π))
24	17, 23	sselid 3978	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ ℝ)
25	24	recnd 11273	. . . . . . 7 ⊢ (𝜑 → ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ∈ ℂ)
26	16, 25	eqeltrid 2833	. . . . . 6 ⊢ (𝜑 → 𝑂 ∈ ℂ)
27	26	sincld 16107	. . . . 5 ⊢ (𝜑 → (sin‘𝑂) ∈ ℂ)
28	27	abscld 15416	. . . 4 ⊢ (𝜑 → (abs‘(sin‘𝑂)) ∈ ℝ)
29	15, 28	remulcld 11275	. . 3 ⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))) ∈ ℝ)
30		halfge0 12460	. . . . . 6 ⊢ 0 ≤ (1 / 2)
31	30	a1i 11	. . . . 5 ⊢ (𝜑 → 0 ≤ (1 / 2))
32	6	absge0d 15424	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (abs‘(𝐵 − 𝐶)))
33	32, 3	breqtrrdi 5190	. . . . . 6 ⊢ (𝜑 → 0 ≤ 𝑋)
34	11	absge0d 15424	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (abs‘(𝐴 − 𝐶)))
35	34, 9	breqtrrdi 5190	. . . . . 6 ⊢ (𝜑 → 0 ≤ 𝑌)
36	8, 13, 33, 35	mulge0d 11822	. . . . 5 ⊢ (𝜑 → 0 ≤ (𝑋 · 𝑌))
37	2, 14, 31, 36	mulge0d 11822	. . . 4 ⊢ (𝜑 → 0 ≤ ((1 / 2) · (𝑋 · 𝑌)))
38	27	absge0d 15424	. . . 4 ⊢ (𝜑 → 0 ≤ (abs‘(sin‘𝑂)))
39	15, 28, 37, 38	mulge0d 11822	. . 3 ⊢ (𝜑 → 0 ≤ (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))))
40	29, 39	sqrtsqd 15399	. 2 ⊢ (𝜑 → (√‘((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2)) = (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))))
41		halfcn 12458	. . . . . . 7 ⊢ (1 / 2) ∈ ℂ
42	41	a1i 11	. . . . . 6 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
43	8	recnd 11273	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℂ)
44	13	recnd 11273	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ ℂ)
45	43, 44	mulcld 11265	. . . . . 6 ⊢ (𝜑 → (𝑋 · 𝑌) ∈ ℂ)
46	42, 45	mulcld 11265	. . . . 5 ⊢ (𝜑 → ((1 / 2) · (𝑋 · 𝑌)) ∈ ℂ)
47	28	recnd 11273	. . . . 5 ⊢ (𝜑 → (abs‘(sin‘𝑂)) ∈ ℂ)
48	46, 47	sqmuld 14155	. . . 4 ⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2) = ((((1 / 2) · (𝑋 · 𝑌))↑2) · ((abs‘(sin‘𝑂))↑2)))
49		2cnd 12321	. . . . . . 7 ⊢ (𝜑 → 2 ∈ ℂ)
50		2ne0 12347	. . . . . . . 8 ⊢ 2 ≠ 0
51	50	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ≠ 0)
52	45, 49, 51	sqdivd 14156	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌) / 2)↑2) = (((𝑋 · 𝑌)↑2) / (2↑2)))
53	45, 49, 51	divrec2d 12025	. . . . . . 7 ⊢ (𝜑 → ((𝑋 · 𝑌) / 2) = ((1 / 2) · (𝑋 · 𝑌)))
54	53	oveq1d 7435	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌) / 2)↑2) = (((1 / 2) · (𝑋 · 𝑌))↑2))
55		sq2 14193	. . . . . . . 8 ⊢ (2↑2) = 4
56	55	a1i 11	. . . . . . 7 ⊢ (𝜑 → (2↑2) = 4)
57	56	oveq2d 7436	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌)↑2) / (2↑2)) = (((𝑋 · 𝑌)↑2) / 4))
58	52, 54, 57	3eqtr3d 2776	. . . . 5 ⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌))↑2) = (((𝑋 · 𝑌)↑2) / 4))
59	16, 24	eqeltrid 2833	. . . . . . 7 ⊢ (𝜑 → 𝑂 ∈ ℝ)
60	59	resincld 16120	. . . . . 6 ⊢ (𝜑 → (sin‘𝑂) ∈ ℝ)
61		absresq 15282	. . . . . 6 ⊢ ((sin‘𝑂) ∈ ℝ → ((abs‘(sin‘𝑂))↑2) = ((sin‘𝑂)↑2))
62	60, 61	syl 17	. . . . 5 ⊢ (𝜑 → ((abs‘(sin‘𝑂))↑2) = ((sin‘𝑂)↑2))
63	58, 62	oveq12d 7438	. . . 4 ⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌))↑2) · ((abs‘(sin‘𝑂))↑2)) = ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2)))
64	45	sqcld 14141	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 · 𝑌)↑2) ∈ ℂ)
65	27	sqcld 14141	. . . . . . . 8 ⊢ (𝜑 → ((sin‘𝑂)↑2) ∈ ℂ)
66	64, 65	mulcld 11265	. . . . . . 7 ⊢ (𝜑 → (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) ∈ ℂ)
67		4cn 12328	. . . . . . . . 9 ⊢ 4 ∈ ℂ
68	67	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 4 ∈ ℂ)
69		heron.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (((𝑋 + 𝑌) + 𝑍) / 2)
70	8, 13	readdcld 11274	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ ℝ)
71		heron.z	. . . . . . . . . . . . . . 15 ⊢ 𝑍 = (abs‘(𝐴 − 𝐵))
72	10, 4	subcld 11602	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)
73	72	abscld 15416	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ∈ ℝ)
74	71, 73	eqeltrid 2833	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑍 ∈ ℝ)
75	70, 74	readdcld 11274	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) ∈ ℝ)
76	75	rehalfcld 12490	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) / 2) ∈ ℝ)
77	69, 76	eqeltrid 2833	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ ℝ)
78	77	recnd 11273	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ ℂ)
79	78, 43	subcld 11602	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 − 𝑋) ∈ ℂ)
80	78, 79	mulcld 11265	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 · (𝑆 − 𝑋)) ∈ ℂ)
81	78, 44	subcld 11602	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 − 𝑌) ∈ ℂ)
82	74	recnd 11273	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ ℂ)
83	78, 82	subcld 11602	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 − 𝑍) ∈ ℂ)
84	81, 83	mulcld 11265	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 − 𝑌) · (𝑆 − 𝑍)) ∈ ℂ)
85	80, 84	mulcld 11265	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ)
86	68, 85	mulcld 11265	. . . . . . 7 ⊢ (𝜑 → (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) ∈ ℂ)
87		4ne0 12351	. . . . . . . 8 ⊢ 4 ≠ 0
88	87	a1i 11	. . . . . . 7 ⊢ (𝜑 → 4 ≠ 0)
89	49, 45	sqmuld 14155	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = ((2↑2) · ((𝑋 · 𝑌)↑2)))
90	56	oveq1d 7435	. . . . . . . . . 10 ⊢ (𝜑 → ((2↑2) · ((𝑋 · 𝑌)↑2)) = (4 · ((𝑋 · 𝑌)↑2)))
91	89, 90	eqtr2d 2769	. . . . . . . . 9 ⊢ (𝜑 → (4 · ((𝑋 · 𝑌)↑2)) = ((2 · (𝑋 · 𝑌))↑2))
92	91	oveq1d 7435	. . . . . . . 8 ⊢ (𝜑 → ((4 · ((𝑋 · 𝑌)↑2)) · ((sin‘𝑂)↑2)) = (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)))
93	68, 64, 65	mulassd 11268	. . . . . . . 8 ⊢ (𝜑 → ((4 · ((𝑋 · 𝑌)↑2)) · ((sin‘𝑂)↑2)) = (4 · (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2))))
94	49, 45	mulcld 11265	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑋 · 𝑌)) ∈ ℂ)
95	94	sqcld 14141	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) ∈ ℂ)
96	95, 65	mulcld 11265	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) ∈ ℂ)
97	44, 82	mulcld 11265	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 · 𝑍) ∈ ℂ)
98	49, 97	mulcld 11265	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑌 · 𝑍)) ∈ ℂ)
99	98	sqcld 14141	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) ∈ ℂ)
100	44	sqcld 14141	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌↑2) ∈ ℂ)
101	82	sqcld 14141	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍↑2) ∈ ℂ)
102	43	sqcld 14141	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
103	101, 102	subcld 11602	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑍↑2) − (𝑋↑2)) ∈ ℂ)
104	100, 103	addcld 11264	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) ∈ ℂ)
105	104	sqcld 14141	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) ∈ ℂ)
106	99, 105	subcld 11602	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) ∈ ℂ)
107	26	coscld 16108	. . . . . . . . . . . . 13 ⊢ (𝜑 → (cos‘𝑂) ∈ ℂ)
108	107	sqcld 14141	. . . . . . . . . . . 12 ⊢ (𝜑 → ((cos‘𝑂)↑2) ∈ ℂ)
109	95, 108	mulcld 11265	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)) ∈ ℂ)
110		sincossq 16153	. . . . . . . . . . . . . 14 ⊢ (𝑂 ∈ ℂ → (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2)) = 1)
111	26, 110	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2)) = 1)
112	111	oveq2d 7436	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2))) = (((2 · (𝑋 · 𝑌))↑2) · 1))
113	95, 65, 108	adddid 11269	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · (((sin‘𝑂)↑2) + ((cos‘𝑂)↑2))) = ((((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) + (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2))))
114	100	2timesd 12486	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · (𝑌↑2)) = ((𝑌↑2) + (𝑌↑2)))
115	100, 103, 100	ppncand 11642	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) = ((𝑌↑2) + (𝑌↑2)))
116	114, 115	eqtr4d 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑌↑2)) = (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))))
117	103	2timesd 12486	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · ((𝑍↑2) − (𝑋↑2))) = (((𝑍↑2) − (𝑋↑2)) + ((𝑍↑2) − (𝑋↑2))))
118	100, 103, 103	pnncand 11641	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) = (((𝑍↑2) − (𝑋↑2)) + ((𝑍↑2) − (𝑋↑2))))
119	117, 118	eqtr4d 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · ((𝑍↑2) − (𝑋↑2))) = (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))))
120	116, 119	oveq12d 7438	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · (𝑌↑2)) · (2 · ((𝑍↑2) − (𝑋↑2)))) = ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) + ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))) · (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))) − ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))))))
121		2t2e4 12407	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 · 2) = 4
122	121, 68	eqeltrid 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · 2) ∈ ℂ)
123	122, 100, 103	mulassd 11268	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · ((𝑍↑2) − (𝑋↑2))) = ((2 · 2) · ((𝑌↑2) · ((𝑍↑2) − (𝑋↑2)))))
124	122, 100	mulcld 11265	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 · 2) · (𝑌↑2)) ∈ ℂ)
125	124, 101, 102	subdid 11701	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · ((𝑍↑2) − (𝑋↑2))) = ((((2 · 2) · (𝑌↑2)) · (𝑍↑2)) − (((2 · 2) · (𝑌↑2)) · (𝑋↑2))))
126	49	sqvald 14140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (2↑2) = (2 · 2))
127	44, 82	sqmuld 14155	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑌 · 𝑍)↑2) = ((𝑌↑2) · (𝑍↑2)))
128	126, 127	oveq12d 7438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2↑2) · ((𝑌 · 𝑍)↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑍↑2))))
129	49, 97	sqmuld 14155	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) = ((2↑2) · ((𝑌 · 𝑍)↑2)))
130	122, 100, 101	mulassd 11268	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · (𝑍↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑍↑2))))
131	128, 129, 130	3eqtr4d 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍))↑2) = (((2 · 2) · (𝑌↑2)) · (𝑍↑2)))
132	43, 44	sqmuld 14155	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑋 · 𝑌)↑2) = ((𝑋↑2) · (𝑌↑2)))
133	102, 100	mulcomd 11266	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑋↑2) · (𝑌↑2)) = ((𝑌↑2) · (𝑋↑2)))
134	132, 133	eqtrd 2768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑋 · 𝑌)↑2) = ((𝑌↑2) · (𝑋↑2)))
135	126, 134	oveq12d 7438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2↑2) · ((𝑋 · 𝑌)↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑋↑2))))
136	122, 100, 102	mulassd 11268	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · (𝑋↑2)) = ((2 · 2) · ((𝑌↑2) · (𝑋↑2))))
137	135, 89, 136	3eqtr4d 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = (((2 · 2) · (𝑌↑2)) · (𝑋↑2)))
138	131, 137	oveq12d 7438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((((2 · 2) · (𝑌↑2)) · (𝑍↑2)) − (((2 · 2) · (𝑌↑2)) · (𝑋↑2))))
139	125, 138	eqtr4d 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2 · 2) · (𝑌↑2)) · ((𝑍↑2) − (𝑋↑2))) = (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)))
140	49, 49, 100, 103	mul4d 11457	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · 2) · ((𝑌↑2) · ((𝑍↑2) − (𝑋↑2)))) = ((2 · (𝑌↑2)) · (2 · ((𝑍↑2) − (𝑋↑2)))))
141	123, 139, 140	3eqtr3d 2776	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((2 · (𝑌↑2)) · (2 · ((𝑍↑2) − (𝑋↑2)))))
142	100, 103	subcld 11602	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) ∈ ℂ)
143		subsq 14206	. . . . . . . . . . . . . . . . 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 2778	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2)) = ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) − (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2)))
146	145	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2))) = (((2 · (𝑌 · 𝑍))↑2) − ((((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2) − (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2))))
147	99, 95	nncand 11607	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍))↑2) − (((2 · (𝑌 · 𝑍))↑2) − ((2 · (𝑋 · 𝑌))↑2))) = ((2 · (𝑋 · 𝑌))↑2))
148	142	sqcld 14141	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2) ∈ ℂ)
149	99, 105, 148	subsubd 11630	. . . . . . . . . . . . . 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 2776	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌))↑2) = ((((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2)))
151	95	mulridd 11262	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · 1) = ((2 · (𝑋 · 𝑌))↑2))
152	102, 100	addcld 11264	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋↑2) + (𝑌↑2)) ∈ ℂ)
153	45, 107	mulcld 11265	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑋 · 𝑌) · (cos‘𝑂)) ∈ ℂ)
154	49, 153	mulcld 11265	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · ((𝑋 · 𝑌) · (cos‘𝑂))) ∈ ℂ)
155	152, 154	nncand 11607	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))) = (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))
156	100, 101	subcld 11602	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑌↑2) − (𝑍↑2)) ∈ ℂ)
157	156, 102	addcomd 11447	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑌↑2) − (𝑍↑2)) + (𝑋↑2)) = ((𝑋↑2) + ((𝑌↑2) − (𝑍↑2))))
158	100, 101, 102	subsubd 11630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑌↑2) − (𝑍↑2)) + (𝑋↑2)))
159	102, 100, 101	addsubassd 11622	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2)) = ((𝑋↑2) + ((𝑌↑2) − (𝑍↑2))))
160	157, 158, 159	3eqtr4d 2778	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2)))
161	18, 3, 9, 71, 16	lawcos 26761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝑍↑2) = (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂)))))
162	10, 4, 5, 21, 19, 161	syl32anc 1376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑍↑2) = (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂)))))
163	162	oveq2d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑋↑2) + (𝑌↑2)) − (𝑍↑2)) = (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))))
164	160, 163	eqtrd 2768	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = (((𝑋↑2) + (𝑌↑2)) − (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))))
165	49, 45, 107	mulassd 11268	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · (𝑋 · 𝑌)) · (cos‘𝑂)) = (2 · ((𝑋 · 𝑌) · (cos‘𝑂))))
166	155, 164, 165	3eqtr4d 2778	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑌↑2) − ((𝑍↑2) − (𝑋↑2))) = ((2 · (𝑋 · 𝑌)) · (cos‘𝑂)))
167	166	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2) = (((2 · (𝑋 · 𝑌)) · (cos‘𝑂))↑2))
168	94, 107	sqmuld 14155	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌)) · (cos‘𝑂))↑2) = (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)))
169	167, 168	eqtr2d 2769	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2)) = (((𝑌↑2) − ((𝑍↑2) − (𝑋↑2)))↑2))
170	169	oveq2d 7436	. . . . . . . . . . . . 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 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · 1) = ((((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)) + (((2 · (𝑋 · 𝑌))↑2) · ((cos‘𝑂)↑2))))
172	112, 113, 171	3eqtr3d 2776	. . . . . . . . . . 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 11451	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = (((2 · (𝑌 · 𝑍))↑2) − (((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))↑2)))
174		subsq 14206	. . . . . . . . . . 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 11264	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌↑2) + (𝑍↑2)) ∈ ℂ)
177	98, 176, 102	addsubassd 11622	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2)) = ((2 · (𝑌 · 𝑍)) + (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))))
178	100, 101, 102	addsubassd 11622	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2)) = ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))
179	178	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))))
180	177, 179	eqtr2d 2769	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2)))
181		binom2 14213	. . . . . . . . . . . . . . 15 ⊢ ((𝑌 ∈ ℂ ∧ 𝑍 ∈ ℂ) → ((𝑌 + 𝑍)↑2) = (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2)))
182	44, 82, 181	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 + 𝑍)↑2) = (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2)))
183	100, 98, 101	add32d 11472	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (2 · (𝑌 · 𝑍))) + (𝑍↑2)) = (((𝑌↑2) + (𝑍↑2)) + (2 · (𝑌 · 𝑍))))
184	176, 98	addcomd 11447	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) + (2 · (𝑌 · 𝑍))) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))))
185	182, 183, 184	3eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌 + 𝑍)↑2) = ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))))
186	185	oveq1d 7435	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + (𝑍↑2))) − (𝑋↑2)))
187	44, 82	addcld 11264	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 + 𝑍) ∈ ℂ)
188		subsq 14206	. . . . . . . . . . . . . . 15 ⊢ (((𝑌 + 𝑍) ∈ ℂ ∧ 𝑋 ∈ ℂ) → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋)))
189	187, 43, 188	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋)))
190	69	oveq2i 7431	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 𝑆) = (2 · (((𝑋 + 𝑌) + 𝑍) / 2))
191	75	recnd 11273	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) ∈ ℂ)
192	191, 49, 51	divcan2d 12023	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (((𝑋 + 𝑌) + 𝑍) / 2)) = ((𝑋 + 𝑌) + 𝑍))
193	190, 192	eqtrid 2780	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · 𝑆) = ((𝑋 + 𝑌) + 𝑍))
194	43, 44, 82	addassd 11267	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
195	43, 187	addcomd 11447	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 + (𝑌 + 𝑍)) = ((𝑌 + 𝑍) + 𝑋))
196	193, 194, 195	3eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · 𝑆) = ((𝑌 + 𝑍) + 𝑋))
197	49, 78, 43	subdid 11701	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (𝑆 − 𝑋)) = ((2 · 𝑆) − (2 · 𝑋)))
198	193, 194	eqtrd 2768	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑆) = (𝑋 + (𝑌 + 𝑍)))
199	43	2timesd 12486	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑋) = (𝑋 + 𝑋))
200	198, 199	oveq12d 7438	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑋)) = ((𝑋 + (𝑌 + 𝑍)) − (𝑋 + 𝑋)))
201	43, 187, 43	pnpcand 11639	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑋 + (𝑌 + 𝑍)) − (𝑋 + 𝑋)) = ((𝑌 + 𝑍) − 𝑋))
202	197, 200, 201	3eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝑆 − 𝑋)) = ((𝑌 + 𝑍) − 𝑋))
203	196, 202	oveq12d 7438	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · 𝑆) · (2 · (𝑆 − 𝑋))) = (((𝑌 + 𝑍) + 𝑋) · ((𝑌 + 𝑍) − 𝑋)))
204	189, 203	eqtr4d 2771	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = ((2 · 𝑆) · (2 · (𝑆 − 𝑋))))
205	49, 78, 49, 79	mul4d 11457	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝑆) · (2 · (𝑆 − 𝑋))) = ((2 · 2) · (𝑆 · (𝑆 − 𝑋))))
206	121	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · 2) = 4)
207	206	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 2) · (𝑆 · (𝑆 − 𝑋))) = (4 · (𝑆 · (𝑆 − 𝑋))))
208	204, 205, 207	3eqtrd 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌 + 𝑍)↑2) − (𝑋↑2)) = (4 · (𝑆 · (𝑆 − 𝑋))))
209	180, 186, 208	3eqtr2d 2774	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (4 · (𝑆 · (𝑆 − 𝑋))))
210	98, 176	subcld 11602	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) ∈ ℂ)
211	210, 102	addcomd 11447	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2)) = ((𝑋↑2) + ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2)))))
212	178	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))))
213	98, 176, 102	subsubd 11630	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − (((𝑌↑2) + (𝑍↑2)) − (𝑋↑2))) = (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2)))
214	212, 213	eqtr3d 2770	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2))) + (𝑋↑2)))
215	102, 176, 98	subsub2d 11631	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍)))) = ((𝑋↑2) + ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + (𝑍↑2)))))
216	211, 214, 215	3eqtr4d 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍)))))
217	100, 101, 98	addsubassd 11622	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = ((𝑌↑2) + ((𝑍↑2) − (2 · (𝑌 · 𝑍)))))
218	101, 98	subcld 11602	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑍↑2) − (2 · (𝑌 · 𝑍))) ∈ ℂ)
219	100, 218	addcomd 11447	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌↑2) + ((𝑍↑2) − (2 · (𝑌 · 𝑍)))) = (((𝑍↑2) − (2 · (𝑌 · 𝑍))) + (𝑌↑2)))
220	44, 82	mulcomd 11266	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑌 · 𝑍) = (𝑍 · 𝑌))
221	220	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑌 · 𝑍)) = (2 · (𝑍 · 𝑌)))
222	221	oveq2d 7436	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑍↑2) − (2 · (𝑌 · 𝑍))) = ((𝑍↑2) − (2 · (𝑍 · 𝑌))))
223	222	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑍↑2) − (2 · (𝑌 · 𝑍))) + (𝑌↑2)) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
224	217, 219, 223	3eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
225		binom2sub 14215	. . . . . . . . . . . . . . 15 ⊢ ((𝑍 ∈ ℂ ∧ 𝑌 ∈ ℂ) → ((𝑍 − 𝑌)↑2) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
226	82, 44, 225	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑍 − 𝑌)↑2) = (((𝑍↑2) − (2 · (𝑍 · 𝑌))) + (𝑌↑2)))
227	224, 226	eqtr4d 2771	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍))) = ((𝑍 − 𝑌)↑2))
228	227	oveq2d 7436	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋↑2) − (((𝑌↑2) + (𝑍↑2)) − (2 · (𝑌 · 𝑍)))) = ((𝑋↑2) − ((𝑍 − 𝑌)↑2)))
229	82, 44	subcld 11602	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍 − 𝑌) ∈ ℂ)
230		subsq 14206	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ ℂ ∧ (𝑍 − 𝑌) ∈ ℂ) → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌))))
231	43, 229, 230	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌))))
232	49, 78, 44	subdid 11701	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (𝑆 − 𝑌)) = ((2 · 𝑆) − (2 · 𝑌)))
233	43, 44, 82	add32d 11472	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌))
234	193, 233	eqtrd 2768	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑆) = ((𝑋 + 𝑍) + 𝑌))
235	44	2timesd 12486	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑌) = (𝑌 + 𝑌))
236	234, 235	oveq12d 7438	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑌)) = (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌)))
237	43, 82	addcld 11264	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 + 𝑍) ∈ ℂ)
238	237, 44, 44	pnpcan2d 11640	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌)) = ((𝑋 + 𝑍) − 𝑌))
239	43, 82, 44, 238	assraddsubd 11659	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑋 + 𝑍) + 𝑌) − (𝑌 + 𝑌)) = (𝑋 + (𝑍 − 𝑌)))
240	232, 236, 239	3eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝑆 − 𝑌)) = (𝑋 + (𝑍 − 𝑌)))
241	49, 78, 82	subdid 11701	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (𝑆 − 𝑍)) = ((2 · 𝑆) − (2 · 𝑍)))
242	82	2timesd 12486	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑍) = (𝑍 + 𝑍))
243	193, 242	oveq12d 7438	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 𝑆) − (2 · 𝑍)) = (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍)))
244	43, 44	addcld 11264	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ ℂ)
245	244, 82, 82	pnpcan2d 11640	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍)) = ((𝑋 + 𝑌) − 𝑍))
246	43, 82, 44	subsub3d 11632	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 − (𝑍 − 𝑌)) = ((𝑋 + 𝑌) − 𝑍))
247	245, 246	eqtr4d 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) − (𝑍 + 𝑍)) = (𝑋 − (𝑍 − 𝑌)))
248	241, 243, 247	3eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝑆 − 𝑍)) = (𝑋 − (𝑍 − 𝑌)))
249	240, 248	oveq12d 7438	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍))) = ((𝑋 + (𝑍 − 𝑌)) · (𝑋 − (𝑍 − 𝑌))))
250	231, 249	eqtr4d 2771	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍))))
251	49, 81, 49, 83	mul4d 11457	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · (𝑆 − 𝑌)) · (2 · (𝑆 − 𝑍))) = ((2 · 2) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
252	206	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 2) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
253	250, 251, 252	3eqtrd 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋↑2) − ((𝑍 − 𝑌)↑2)) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
254	216, 228, 253	3eqtrd 2772	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) = (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
255	209, 254	oveq12d 7438	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (𝑌 · 𝑍)) + ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2)))) · ((2 · (𝑌 · 𝑍)) − ((𝑌↑2) + ((𝑍↑2) − (𝑋↑2))))) = ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
256	173, 175, 255	3eqtrd 2772	. . . . . . . . 9 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
257	68, 84	mulcld 11265	. . . . . . . . . 10 ⊢ (𝜑 → (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ)
258	68, 80, 257	mulassd 11268	. . . . . . . . 9 ⊢ (𝜑 → ((4 · (𝑆 · (𝑆 − 𝑋))) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) = (4 · ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
259	80, 68, 84	mul12d 11454	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) = (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
260	259	oveq2d 7436	. . . . . . . . 9 ⊢ (𝜑 → (4 · ((𝑆 · (𝑆 − 𝑋)) · (4 · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))) = (4 · (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
261	256, 258, 260	3eqtrd 2772	. . . . . . . 8 ⊢ (𝜑 → (((2 · (𝑋 · 𝑌))↑2) · ((sin‘𝑂)↑2)) = (4 · (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
262	92, 93, 261	3eqtr3d 2776	. . . . . . 7 ⊢ (𝜑 → (4 · (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2))) = (4 · (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))))
263	66, 86, 68, 88, 262	mulcanad 11880	. . . . . 6 ⊢ (𝜑 → (((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) = (4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
264	263	oveq1d 7435	. . . . 5 ⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) / 4) = ((4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) / 4))
265	64, 65, 68, 88	div23d 12058	. . . . 5 ⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) · ((sin‘𝑂)↑2)) / 4) = ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2)))
266	77, 8	resubcld 11673	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 − 𝑋) ∈ ℝ)
267	77, 266	remulcld 11275	. . . . . . . 8 ⊢ (𝜑 → (𝑆 · (𝑆 − 𝑋)) ∈ ℝ)
268	77, 13	resubcld 11673	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 − 𝑌) ∈ ℝ)
269	77, 74	resubcld 11673	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 − 𝑍) ∈ ℝ)
270	268, 269	remulcld 11275	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 − 𝑌) · (𝑆 − 𝑍)) ∈ ℝ)
271	267, 270	remulcld 11275	. . . . . . 7 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℝ)
272	271	recnd 11273	. . . . . 6 ⊢ (𝜑 → ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))) ∈ ℂ)
273	272, 68, 88	divcan3d 12026	. . . . 5 ⊢ (𝜑 → ((4 · ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))) / 4) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
274	264, 265, 273	3eqtr3d 2776	. . . 4 ⊢ (𝜑 → ((((𝑋 · 𝑌)↑2) / 4) · ((sin‘𝑂)↑2)) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
275	48, 63, 274	3eqtrd 2772	. . 3 ⊢ (𝜑 → ((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2) = ((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))
276	275	fveq2d 6901	. 2 ⊢ (𝜑 → (√‘((((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂)))↑2)) = (√‘((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
277	40, 276	eqtr3d 2770	1 ⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))) = (√‘((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1534 ∈ wcel 2099 ≠ wne 2937 ∖ cdif 3944 {csn 4629 class class class wbr 5148 ‘cfv 6548 (class class class)co 7420 ∈ cmpo 7422 ℂcc 11137 ℝcr 11138 0cc0 11139 1c1 11140 + caddc 11142 · cmul 11144 ≤ cle 11280 − cmin 11475 -cneg 11476 / cdiv 11902 2c2 12298 4c4 12300 (,]cioc 13358 ↑cexp 14059 ℑcim 15078 √csqrt 15213 abscabs 15214 sincsin 16040 cosccos 16041 πcpi 16043 logclog 26501

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5365 ax-pr 5429 ax-un 7740 ax-inf2 9665 ax-cnex 11195 ax-resscn 11196 ax-1cn 11197 ax-icn 11198 ax-addcl 11199 ax-addrcl 11200 ax-mulcl 11201 ax-mulrcl 11202 ax-mulcom 11203 ax-addass 11204 ax-mulass 11205 ax-distr 11206 ax-i2m1 11207 ax-1ne0 11208 ax-1rid 11209 ax-rnegex 11210 ax-rrecex 11211 ax-cnre 11212 ax-pre-lttri 11213 ax-pre-lttrn 11214 ax-pre-ltadd 11215 ax-pre-mulgt0 11216 ax-pre-sup 11217 ax-addf 11218

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3373 df-reu 3374 df-rab 3430 df-v 3473 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4909 df-int 4950 df-iun 4998 df-iin 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-se 5634 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-pred 6305 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6500 df-fun 6550 df-fn 6551 df-f 6552 df-f1 6553 df-fo 6554 df-f1o 6555 df-fv 6556 df-isom 6557 df-riota 7376 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7685 df-om 7871 df-1st 7993 df-2nd 7994 df-supp 8166 df-frecs 8287 df-wrecs 8318 df-recs 8392 df-rdg 8431 df-1o 8487 df-2o 8488 df-er 8725 df-map 8847 df-pm 8848 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fsupp 9387 df-fi 9435 df-sup 9466 df-inf 9467 df-oi 9534 df-card 9963 df-pnf 11281 df-mnf 11282 df-xr 11283 df-ltxr 11284 df-le 11285 df-sub 11477 df-neg 11478 df-div 11903 df-nn 12244 df-2 12306 df-3 12307 df-4 12308 df-5 12309 df-6 12310 df-7 12311 df-8 12312 df-9 12313 df-n0 12504 df-z 12590 df-dec 12709 df-uz 12854 df-q 12964 df-rp 13008 df-xneg 13125 df-xadd 13126 df-xmul 13127 df-ioo 13361 df-ioc 13362 df-ico 13363 df-icc 13364 df-fz 13518 df-fzo 13661 df-fl 13790 df-mod 13868 df-seq 14000 df-exp 14060 df-fac 14266 df-bc 14295 df-hash 14323 df-shft 15047 df-cj 15079 df-re 15080 df-im 15081 df-sqrt 15215 df-abs 15216 df-limsup 15448 df-clim 15465 df-rlim 15466 df-sum 15666 df-ef 16044 df-sin 16046 df-cos 16047 df-pi 16049 df-struct 17116 df-sets 17133 df-slot 17151 df-ndx 17163 df-base 17181 df-ress 17210 df-plusg 17246 df-mulr 17247 df-starv 17248 df-sca 17249 df-vsca 17250 df-ip 17251 df-tset 17252 df-ple 17253 df-ds 17255 df-unif 17256 df-hom 17257 df-cco 17258 df-rest 17404 df-topn 17405 df-0g 17423 df-gsum 17424 df-topgen 17425 df-pt 17426 df-prds 17429 df-xrs 17484 df-qtop 17489 df-imas 17490 df-xps 17492 df-mre 17566 df-mrc 17567 df-acs 17569 df-mgm 18600 df-sgrp 18679 df-mnd 18695 df-submnd 18741 df-mulg 19024 df-cntz 19268 df-cmn 19737 df-psmet 21271 df-xmet 21272 df-met 21273 df-bl 21274 df-mopn 21275 df-fbas 21276 df-fg 21277 df-cnfld 21280 df-top 22809 df-topon 22826 df-topsp 22848 df-bases 22862 df-cld 22936 df-ntr 22937 df-cls 22938 df-nei 23015 df-lp 23053 df-perf 23054 df-cn 23144 df-cnp 23145 df-haus 23232 df-tx 23479 df-hmeo 23672 df-fil 23763 df-fm 23855 df-flim 23856 df-flf 23857 df-xms 24239 df-ms 24240 df-tms 24241 df-cncf 24811 df-limc 25808 df-dv 25809 df-log 26503

This theorem is referenced by: (None)

W3C validator

	
		OSZAR »