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 ‘ ( ( 𝐷 − 𝐸 ) 𝐹 ( 𝐺 − 𝐸 ) ) ) ) |
| 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 | sseldi | ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) ∈ ℂ ) |
| 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 | sseldi | ⊢ ( 𝜑 → ( ( 𝐷 − 𝐸 ) 𝐹 ( 𝐺 − 𝐸 ) ) ∈ ℂ ) |
| 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 ‘ ( ( 𝐷 − 𝐸 ) 𝐹 ( 𝐺 − 𝐸 ) ) ) ) |