Theorem ssscongptld

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 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)

	Ref	Expression
Hypotheses	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	ssscongptld	⊢ ( 𝜑 → ( cos ‘ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) ) = ( cos ‘ ( ( 𝐷 − 𝐸 ) 𝐹 ( 𝐺 − 𝐸 ) ) ) )

Proof

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