Metamath Proof Explorer

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 ⊢F=x∈ℂ∖0,y∈ℂ∖0⟼ℑ⁡log⁡yx
ssscongptld.1 ⊢φ→A∈ℂ
ssscongptld.2 ⊢φ→B∈ℂ
ssscongptld.3 ⊢φ→C∈ℂ
ssscongptld.4 ⊢φ→D∈ℂ
ssscongptld.5 ⊢φ→E∈ℂ
ssscongptld.6 ⊢φ→G∈ℂ
ssscongptld.7 ⊢φ→A≠B
ssscongptld.8 ⊢φ→B≠C
ssscongptld.9 ⊢φ→D≠E
ssscongptld.10 ⊢φ→E≠G
ssscongptld.11 ⊢φ→A−B=D−E
ssscongptld.12 ⊢φ→B−C=E−G
ssscongptld.13 ⊢φ→C−A=G−D
Assertion ssscongptld ⊢φ→cos⁡A−BFC−B=cos⁡D−EFG−E

Proof

Step Hyp Ref Expression
1 ssscongptld.angdef ⊢F=x∈ℂ∖0,y∈ℂ∖0⟼ℑ⁡log⁡yx
2 ssscongptld.1 ⊢φ→A∈ℂ
3 ssscongptld.2 ⊢φ→B∈ℂ
4 ssscongptld.3 ⊢φ→C∈ℂ
5 ssscongptld.4 ⊢φ→D∈ℂ
6 ssscongptld.5 ⊢φ→E∈ℂ
7 ssscongptld.6 ⊢φ→G∈ℂ
8 ssscongptld.7 ⊢φ→A≠B
9 ssscongptld.8 ⊢φ→B≠C
10 ssscongptld.9 ⊢φ→D≠E
11 ssscongptld.10 ⊢φ→E≠G
12 ssscongptld.11 ⊢φ→A−B=D−E
13 ssscongptld.12 ⊢φ→B−C=E−G
14 ssscongptld.13 ⊢φ→C−A=G−D
15 negpitopissre ⊢−ππ⊆ℝ
16 ax-resscn ⊢ℝ⊆ℂ
17 15 16 sstri ⊢−ππ⊆ℂ
18 2 3 subcld ⊢φ→A−B∈ℂ
19 2 3 8 subne0d ⊢φ→A−B≠0
20 4 3 subcld ⊢φ→C−B∈ℂ
21 9 necomd ⊢φ→C≠B
22 4 3 21 subne0d ⊢φ→C−B≠0
23 1 18 19 20 22 angcld ⊢φ→A−BFC−B∈−ππ
24 17 23 sselid ⊢φ→A−BFC−B∈ℂ
25 24 coscld ⊢φ→cos⁡A−BFC−B∈ℂ
26 5 6 subcld ⊢φ→D−E∈ℂ
27 5 6 10 subne0d ⊢φ→D−E≠0
28 7 6 subcld ⊢φ→G−E∈ℂ
29 11 necomd ⊢φ→G≠E
30 7 6 29 subne0d ⊢φ→G−E≠0
31 1 26 27 28 30 angcld ⊢φ→D−EFG−E∈−ππ
32 17 31 sselid ⊢φ→D−EFG−E∈ℂ
33 32 coscld ⊢φ→cos⁡D−EFG−E∈ℂ
34 26 abscld ⊢φ→D−E∈ℝ
35 34 recnd ⊢φ→D−E∈ℂ
36 28 abscld ⊢φ→G−E∈ℝ
37 36 recnd ⊢φ→G−E∈ℂ
38 35 37 mulcld ⊢φ→D−E⁢G−E∈ℂ
39 26 27 absne0d ⊢φ→D−E≠0
40 28 30 absne0d ⊢φ→G−E≠0
41 35 37 39 40 mulne0d ⊢φ→D−E⁢G−E≠0
42 4 3 abssubd ⊢φ→C−B=B−C
43 7 6 abssubd ⊢φ→G−E=E−G
44 13 42 43 3eqtr4d ⊢φ→C−B=G−E
45 12 44 oveq12d ⊢φ→A−B⁢C−B=D−E⁢G−E
46 45 oveq1d ⊢φ→A−B⁢C−B⁢cos⁡A−BFC−B=D−E⁢G−E⁢cos⁡A−BFC−B
47 12 35 eqeltrd ⊢φ→A−B∈ℂ
48 44 37 eqeltrd ⊢φ→C−B∈ℂ
49 47 48 mulcld ⊢φ→A−B⁢C−B∈ℂ
50 49 25 mulcld ⊢φ→A−B⁢C−B⁢cos⁡A−BFC−B∈ℂ
51 38 33 mulcld ⊢φ→D−E⁢G−E⁢cos⁡D−EFG−E∈ℂ
52 2cnd ⊢φ→2∈ℂ
53 2ne0 ⊢2≠0
54 53 a1i ⊢φ→2≠0
55 35 sqcld ⊢φ→D−E2∈ℂ
56 37 sqcld ⊢φ→G−E2∈ℂ
57 55 56 addcld ⊢φ→D−E2+G−E2∈ℂ
58 52 50 mulcld ⊢φ→2⁢A−B⁢C−B⁢cos⁡A−BFC−B∈ℂ
59 52 51 mulcld ⊢φ→2⁢D−E⁢G−E⁢cos⁡D−EFG−E∈ℂ
60 12 oveq1d ⊢φ→A−B2=D−E2
61 44 oveq1d ⊢φ→C−B2=G−E2
62 60 61 oveq12d ⊢φ→A−B2+C−B2=D−E2+G−E2
63 62 oveq1d ⊢φ→A−B2+C−B2-2⁢A−B⁢C−B⁢cos⁡A−BFC−B=D−E2+G−E2-2⁢A−B⁢C−B⁢cos⁡A−BFC−B
64 14 oveq1d ⊢φ→C−A2=G−D2
65 eqid ⊢A−B=A−B
66 eqid ⊢C−B=C−B
67 eqid ⊢C−A=C−A
68 eqid ⊢A−BFC−B=A−BFC−B
69 1 65 66 67 68 lawcos ⊢C∈ℂ∧A∈ℂ∧B∈ℂ∧C≠B∧A≠B→C−A2=A−B2+C−B2-2⁢A−B⁢C−B⁢cos⁡A−BFC−B
70 4 2 3 21 8 69 syl32anc ⊢φ→C−A2=A−B2+C−B2-2⁢A−B⁢C−B⁢cos⁡A−BFC−B
71 eqid ⊢D−E=D−E
72 eqid ⊢G−E=G−E
73 eqid ⊢G−D=G−D
74 eqid ⊢D−EFG−E=D−EFG−E
75 1 71 72 73 74 lawcos ⊢G∈ℂ∧D∈ℂ∧E∈ℂ∧G≠E∧D≠E→G−D2=D−E2+G−E2-2⁢D−E⁢G−E⁢cos⁡D−EFG−E
76 7 5 6 29 10 75 syl32anc ⊢φ→G−D2=D−E2+G−E2-2⁢D−E⁢G−E⁢cos⁡D−EFG−E
77 64 70 76 3eqtr3d ⊢φ→A−B2+C−B2-2⁢A−B⁢C−B⁢cos⁡A−BFC−B=D−E2+G−E2-2⁢D−E⁢G−E⁢cos⁡D−EFG−E
78 63 77 eqtr3d ⊢φ→D−E2+G−E2-2⁢A−B⁢C−B⁢cos⁡A−BFC−B=D−E2+G−E2-2⁢D−E⁢G−E⁢cos⁡D−EFG−E
79 57 58 59 78 subcand ⊢φ→2⁢A−B⁢C−B⁢cos⁡A−BFC−B=2⁢D−E⁢G−E⁢cos⁡D−EFG−E
80 50 51 52 54 79 mulcanad ⊢φ→A−B⁢C−B⁢cos⁡A−BFC−B=D−E⁢G−E⁢cos⁡D−EFG−E
81 46 80 eqtr3d ⊢φ→D−E⁢G−E⁢cos⁡A−BFC−B=D−E⁢G−E⁢cos⁡D−EFG−E
82 25 33 38 41 81 mulcanad ⊢φ→cos⁡A−BFC−B=cos⁡D−EFG−E