Theorem ssscongptld 26770

Description: If two triangles have equal sides, one angle in one triangle has the same cosine as the corresponding angle in the other triangle. This is a partial form of the SSS congruence theorem.

This theorem is proven by using lawcos 26764 on both triangles to express one side in terms of the other two, and then equating these expressions and reducing this algebraically to get an equality of cosines of angles. (Contributed by David Moews, 28-Feb-2017.)

Hypotheses

Ref	Expression
ssscongptld.angdef	⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))
ssscongptld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
ssscongptld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
ssscongptld.3	⊢ (𝜑 → 𝐶 ∈ ℂ)
ssscongptld.4	⊢ (𝜑 → 𝐷 ∈ ℂ)
ssscongptld.5	⊢ (𝜑 → 𝐸 ∈ ℂ)
ssscongptld.6	⊢ (𝜑 → 𝐺 ∈ ℂ)
ssscongptld.7	⊢ (𝜑 → 𝐴 ≠ 𝐵)
ssscongptld.8	⊢ (𝜑 → 𝐵 ≠ 𝐶)
ssscongptld.9	⊢ (𝜑 → 𝐷 ≠ 𝐸)
ssscongptld.10	⊢ (𝜑 → 𝐸 ≠ 𝐺)
ssscongptld.11	⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) = (abs‘(𝐷 − 𝐸)))
ssscongptld.12	⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) = (abs‘(𝐸 − 𝐺)))
ssscongptld.13	⊢ (𝜑 → (abs‘(𝐶 − 𝐴)) = (abs‘(𝐺 − 𝐷)))

Assertion

Ref	Expression
ssscongptld	⊢ (𝜑 → (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))) = (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝐸,𝑦   𝑥,𝐺,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem ssscongptld

Step	Hyp	Ref	Expression
1		negpitopissre 26487	. . . . 5 ⊢ (-π(,]π) ⊆ ℝ
2		ax-resscn 11179	. . . . 5 ⊢ ℝ ⊆ ℂ
3	1, 2	sstri 3966	. . . 4 ⊢ (-π(,]π) ⊆ ℂ
4		ssscongptld.angdef	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))
5		ssscongptld.1	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℂ)
6		ssscongptld.2	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℂ)
7	5, 6	subcld 11587	. . . . 5 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)
8		ssscongptld.7	. . . . . 6 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
9	5, 6, 8	subne0d 11596	. . . . 5 ⊢ (𝜑 → (𝐴 − 𝐵) ≠ 0)
10		ssscongptld.3	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ ℂ)
11	10, 6	subcld 11587	. . . . 5 ⊢ (𝜑 → (𝐶 − 𝐵) ∈ ℂ)
12		ssscongptld.8	. . . . . . 7 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
13	12	necomd 2986	. . . . . 6 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
14	10, 6, 13	subne0d 11596	. . . . 5 ⊢ (𝜑 → (𝐶 − 𝐵) ≠ 0)
15	4, 7, 9, 11, 14	angcld 26753	. . . 4 ⊢ (𝜑 → ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) ∈ (-π(,]π))
16	3, 15	sselid 3954	. . 3 ⊢ (𝜑 → ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) ∈ ℂ)
17	16	coscld 16136	. 2 ⊢ (𝜑 → (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))) ∈ ℂ)
18		ssscongptld.4	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ ℂ)
19		ssscongptld.5	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ ℂ)
20	18, 19	subcld 11587	. . . . 5 ⊢ (𝜑 → (𝐷 − 𝐸) ∈ ℂ)
21		ssscongptld.9	. . . . . 6 ⊢ (𝜑 → 𝐷 ≠ 𝐸)
22	18, 19, 21	subne0d 11596	. . . . 5 ⊢ (𝜑 → (𝐷 − 𝐸) ≠ 0)
23		ssscongptld.6	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ ℂ)
24	23, 19	subcld 11587	. . . . 5 ⊢ (𝜑 → (𝐺 − 𝐸) ∈ ℂ)
25		ssscongptld.10	. . . . . . 7 ⊢ (𝜑 → 𝐸 ≠ 𝐺)
26	25	necomd 2986	. . . . . 6 ⊢ (𝜑 → 𝐺 ≠ 𝐸)
27	23, 19, 26	subne0d 11596	. . . . 5 ⊢ (𝜑 → (𝐺 − 𝐸) ≠ 0)
28	4, 20, 22, 24, 27	angcld 26753	. . . 4 ⊢ (𝜑 → ((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)) ∈ (-π(,]π))
29	3, 28	sselid 3954	. . 3 ⊢ (𝜑 → ((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)) ∈ ℂ)
30	29	coscld 16136	. 2 ⊢ (𝜑 → (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))) ∈ ℂ)
31	20	abscld 15444	. . . 4 ⊢ (𝜑 → (abs‘(𝐷 − 𝐸)) ∈ ℝ)
32	31	recnd 11256	. . 3 ⊢ (𝜑 → (abs‘(𝐷 − 𝐸)) ∈ ℂ)
33	24	abscld 15444	. . . 4 ⊢ (𝜑 → (abs‘(𝐺 − 𝐸)) ∈ ℝ)
34	33	recnd 11256	. . 3 ⊢ (𝜑 → (abs‘(𝐺 − 𝐸)) ∈ ℂ)
35	32, 34	mulcld 11248	. 2 ⊢ (𝜑 → ((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) ∈ ℂ)
36	20, 22	absne0d 15455	. . 3 ⊢ (𝜑 → (abs‘(𝐷 − 𝐸)) ≠ 0)
37	24, 27	absne0d 15455	. . 3 ⊢ (𝜑 → (abs‘(𝐺 − 𝐸)) ≠ 0)
38	32, 34, 36, 37	mulne0d 11882	. 2 ⊢ (𝜑 → ((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) ≠ 0)
39		ssscongptld.11	. . . . 5 ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) = (abs‘(𝐷 − 𝐸)))
40		ssscongptld.12	. . . . . 6 ⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) = (abs‘(𝐸 − 𝐺)))
41	10, 6	abssubd 15461	. . . . . 6 ⊢ (𝜑 → (abs‘(𝐶 − 𝐵)) = (abs‘(𝐵 − 𝐶)))
42	23, 19	abssubd 15461	. . . . . 6 ⊢ (𝜑 → (abs‘(𝐺 − 𝐸)) = (abs‘(𝐸 − 𝐺)))
43	40, 41, 42	3eqtr4d 2779	. . . . 5 ⊢ (𝜑 → (abs‘(𝐶 − 𝐵)) = (abs‘(𝐺 − 𝐸)))
44	39, 43	oveq12d 7418	. . . 4 ⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) = ((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))))
45	44	oveq1d 7415	. . 3 ⊢ (𝜑 → (((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))) = (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))))
46	39, 32	eqeltrd 2833	. . . . . 6 ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ∈ ℂ)
47	43, 34	eqeltrd 2833	. . . . . 6 ⊢ (𝜑 → (abs‘(𝐶 − 𝐵)) ∈ ℂ)
48	46, 47	mulcld 11248	. . . . 5 ⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) ∈ ℂ)
49	48, 17	mulcld 11248	. . . 4 ⊢ (𝜑 → (((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))) ∈ ℂ)
50	35, 30	mulcld 11248	. . . 4 ⊢ (𝜑 → (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)))) ∈ ℂ)
51		2cnd 12311	. . . 4 ⊢ (𝜑 → 2 ∈ ℂ)
52		2ne0 12337	. . . . 5 ⊢ 2 ≠ 0
53	52	a1i 11	. . . 4 ⊢ (𝜑 → 2 ≠ 0)
54	32	sqcld 14152	. . . . . 6 ⊢ (𝜑 → ((abs‘(𝐷 − 𝐸))↑2) ∈ ℂ)
55	34	sqcld 14152	. . . . . 6 ⊢ (𝜑 → ((abs‘(𝐺 − 𝐸))↑2) ∈ ℂ)
56	54, 55	addcld 11247	. . . . 5 ⊢ (𝜑 → (((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)) ∈ ℂ)
57	51, 49	mulcld 11248	. . . . 5 ⊢ (𝜑 → (2 · (((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))))) ∈ ℂ)
58	51, 50	mulcld 11248	. . . . 5 ⊢ (𝜑 → (2 · (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))))) ∈ ℂ)
59	39	oveq1d 7415	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐴 − 𝐵))↑2) = ((abs‘(𝐷 − 𝐸))↑2))
60	43	oveq1d 7415	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐶 − 𝐵))↑2) = ((abs‘(𝐺 − 𝐸))↑2))
61	59, 60	oveq12d 7418	. . . . . . 7 ⊢ (𝜑 → (((abs‘(𝐴 − 𝐵))↑2) + ((abs‘(𝐶 − 𝐵))↑2)) = (((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)))
62	61	oveq1d 7415	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 − 𝐵))↑2) + ((abs‘(𝐶 − 𝐵))↑2)) − (2 · (((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))))) = ((((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)) − (2 · (((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))))))
63		ssscongptld.13	. . . . . . . 8 ⊢ (𝜑 → (abs‘(𝐶 − 𝐴)) = (abs‘(𝐺 − 𝐷)))
64	63	oveq1d 7415	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐶 − 𝐴))↑2) = ((abs‘(𝐺 − 𝐷))↑2))
65		eqid 2734	. . . . . . . . 9 ⊢ (abs‘(𝐴 − 𝐵)) = (abs‘(𝐴 − 𝐵))
66		eqid 2734	. . . . . . . . 9 ⊢ (abs‘(𝐶 − 𝐵)) = (abs‘(𝐶 − 𝐵))
67		eqid 2734	. . . . . . . . 9 ⊢ (abs‘(𝐶 − 𝐴)) = (abs‘(𝐶 − 𝐴))
68		eqid 2734	. . . . . . . . 9 ⊢ ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) = ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))
69	4, 65, 66, 67, 68	lawcos 26764	. . . . . . . 8 ⊢ (((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) → ((abs‘(𝐶 − 𝐴))↑2) = ((((abs‘(𝐴 − 𝐵))↑2) + ((abs‘(𝐶 − 𝐵))↑2)) − (2 · (((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))))))
70	10, 5, 6, 13, 8, 69	syl32anc 1379	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐶 − 𝐴))↑2) = ((((abs‘(𝐴 − 𝐵))↑2) + ((abs‘(𝐶 − 𝐵))↑2)) − (2 · (((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))))))
71		eqid 2734	. . . . . . . . 9 ⊢ (abs‘(𝐷 − 𝐸)) = (abs‘(𝐷 − 𝐸))
72		eqid 2734	. . . . . . . . 9 ⊢ (abs‘(𝐺 − 𝐸)) = (abs‘(𝐺 − 𝐸))
73		eqid 2734	. . . . . . . . 9 ⊢ (abs‘(𝐺 − 𝐷)) = (abs‘(𝐺 − 𝐷))
74		eqid 2734	. . . . . . . . 9 ⊢ ((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)) = ((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))
75	4, 71, 72, 73, 74	lawcos 26764	. . . . . . . 8 ⊢ (((𝐺 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ) ∧ (𝐺 ≠ 𝐸 ∧ 𝐷 ≠ 𝐸)) → ((abs‘(𝐺 − 𝐷))↑2) = ((((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)) − (2 · (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)))))))
76	23, 18, 19, 26, 21, 75	syl32anc 1379	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐺 − 𝐷))↑2) = ((((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)) − (2 · (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)))))))
77	64, 70, 76	3eqtr3d 2777	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 − 𝐵))↑2) + ((abs‘(𝐶 − 𝐵))↑2)) − (2 · (((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))))) = ((((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)) − (2 · (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)))))))
78	62, 77	eqtr3d 2771	. . . . 5 ⊢ (𝜑 → ((((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)) − (2 · (((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))))) = ((((abs‘(𝐷 − 𝐸))↑2) + ((abs‘(𝐺 − 𝐸))↑2)) − (2 · (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)))))))
79	56, 57, 58, 78	subcand 11628	. . . 4 ⊢ (𝜑 → (2 · (((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))))) = (2 · (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))))))
80	49, 50, 51, 53, 79	mulcanad 11865	. . 3 ⊢ (𝜑 → (((abs‘(𝐴 − 𝐵)) · (abs‘(𝐶 − 𝐵))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))) = (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)))))
81	45, 80	eqtr3d 2771	. 2 ⊢ (𝜑 → (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))) = (((abs‘(𝐷 − 𝐸)) · (abs‘(𝐺 − 𝐸))) · (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸)))))
82	17, 30, 35, 38, 81	mulcanad 11865	1 ⊢ (𝜑 → (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))) = (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   ≠ wne 2931   ∖ cdif 3921  {csn 4599  ‘cfv 6528  (class class class)co 7400   ∈ cmpo 7402  ℂcc 11120  ℝcr 11121  0cc0 11122   + caddc 11125   · cmul 11127   − cmin 11459  -cneg 11460   / cdiv 11887  2c2 12288  (,]cioc 13355  ↑cexp 14069  ℑcim 15106  abscabs 15242  cosccos 16069  πcpi 16071  logclog 26501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5247  ax-sep 5264  ax-nul 5274  ax-pow 5333  ax-pr 5400  ax-un 7724  ax-inf2 9648  ax-cnex 11178  ax-resscn 11179  ax-1cn 11180  ax-icn 11181  ax-addcl 11182  ax-addrcl 11183  ax-mulcl 11184  ax-mulrcl 11185  ax-mulcom 11186  ax-addass 11187  ax-mulass 11188  ax-distr 11189  ax-i2m1 11190  ax-1ne0 11191  ax-1rid 11192  ax-rnegex 11193  ax-rrecex 11194  ax-cnre 11195  ax-pre-lttri 11196  ax-pre-lttrn 11197  ax-pre-ltadd 11198  ax-pre-mulgt0 11199  ax-pre-sup 11200  ax-addf 11201

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3357  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-pss 3944  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-tp 4604  df-op 4606  df-uni 4882  df-int 4921  df-iun 4967  df-iin 4968  df-br 5118  df-opab 5180  df-mpt 5200  df-tr 5228  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6288  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-isom 6537  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-of 7666  df-om 7857  df-1st 7983  df-2nd 7984  df-supp 8155  df-frecs 8275  df-wrecs 8306  df-recs 8380  df-rdg 8419  df-1o 8475  df-2o 8476  df-er 8714  df-map 8837  df-pm 8838  df-ixp 8907  df-en 8955  df-dom 8956  df-sdom 8957  df-fin 8958  df-fsupp 9369  df-fi 9418  df-sup 9449  df-inf 9450  df-oi 9517  df-card 9946  df-pnf 11264  df-mnf 11265  df-xr 11266  df-ltxr 11267  df-le 11268  df-sub 11461  df-neg 11462  df-div 11888  df-nn 12234  df-2 12296  df-3 12297  df-4 12298  df-5 12299  df-6 12300  df-7 12301  df-8 12302  df-9 12303  df-n0 12495  df-z 12582  df-dec 12702  df-uz 12846  df-q 12958  df-rp 13002  df-xneg 13121  df-xadd 13122  df-xmul 13123  df-ioo 13358  df-ioc 13359  df-ico 13360  df-icc 13361  df-fz 13515  df-fzo 13662  df-fl 13799  df-mod 13877  df-seq 14010  df-exp 14070  df-fac 14282  df-bc 14311  df-hash 14339  df-shft 15075  df-cj 15107  df-re 15108  df-im 15109  df-sqrt 15243  df-abs 15244  df-limsup 15476  df-clim 15493  df-rlim 15494  df-sum 15692  df-ef 16072  df-sin 16074  df-cos 16075  df-pi 16077  df-struct 17153  df-sets 17170  df-slot 17188  df-ndx 17200  df-base 17216  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 17503  df-qtop 17508  df-imas 17509  df-xps 17511  df-mre 17585  df-mrc 17586  df-acs 17588  df-mgm 18605  df-sgrp 18684  df-mnd 18700  df-submnd 18749  df-mulg 19038  df-cntz 19287  df-cmn 19750  df-psmet 21294  df-xmet 21295  df-met 21296  df-bl 21297  df-mopn 21298  df-fbas 21299  df-fg 21300  df-cnfld 21303  df-top 22819  df-topon 22836  df-topsp 22858  df-bases 22871  df-cld 22944  df-ntr 22945  df-cls 22946  df-nei 23023  df-lp 23061  df-perf 23062  df-cn 23152  df-cnp 23153  df-haus 23240  df-tx 23487  df-hmeo 23680  df-fil 23771  df-fm 23863  df-flim 23864  df-flf 23865  df-xms 24246  df-ms 24247  df-tms 24248  df-cncf 24809  df-limc 25806  df-dv 25807  df-log 26503

This theorem is referenced by:  chordthmlem  26780