Description: Rotate the variables left in an equation with subtraction on the left, converting it into an addition.
EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | lsubrotld.a | ⊢ ( 𝜑 → 𝐴 ∈ ℂ ) | |
| lsubrotld.b | ⊢ ( 𝜑 → 𝐵 ∈ ℂ ) | ||
| lsubrotld.1 | ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = 𝐶 ) | ||
| Assertion | lsubrotld | ⊢ ( 𝜑 → ( 𝐵 + 𝐶 ) = 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lsubrotld.a | ⊢ ( 𝜑 → 𝐴 ∈ ℂ ) | |
| 2 | lsubrotld.b | ⊢ ( 𝜑 → 𝐵 ∈ ℂ ) | |
| 3 | lsubrotld.1 | ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = 𝐶 ) | |
| 4 | 1 2 | subcld | ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ ) |
| 5 | 3 4 | eqeltrrd | ⊢ ( 𝜑 → 𝐶 ∈ ℂ ) |
| 6 | 2 5 | addcld | ⊢ ( 𝜑 → ( 𝐵 + 𝐶 ) ∈ ℂ ) |
| 7 | 2 5 | pncan2d | ⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) − 𝐵 ) = 𝐶 ) |
| 8 | 7 3 | eqtr4d | ⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) − 𝐵 ) = ( 𝐴 − 𝐵 ) ) |
| 9 | 6 1 2 8 | subcan2d | ⊢ ( 𝜑 → ( 𝐵 + 𝐶 ) = 𝐴 ) |