Description: Swap the second and third variables 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, 23-Aug-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | lsubswap23d.a | ⊢ ( 𝜑 → 𝐴 ∈ ℂ ) | |
| lsubswap23d.b | ⊢ ( 𝜑 → 𝐵 ∈ ℂ ) | ||
| lsubswap23d.1 | ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = 𝐶 ) | ||
| Assertion | lsubswap23d | ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lsubswap23d.a | ⊢ ( 𝜑 → 𝐴 ∈ ℂ ) | |
| 2 | lsubswap23d.b | ⊢ ( 𝜑 → 𝐵 ∈ ℂ ) | |
| 3 | lsubswap23d.1 | ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = 𝐶 ) | |
| 4 | 1 2 | subcld | ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ ) |
| 5 | 3 4 | eqeltrrd | ⊢ ( 𝜑 → 𝐶 ∈ ℂ ) |
| 6 | 1 5 | subcld | ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ∈ ℂ ) |
| 7 | 4 3 | subeq0bd | ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) − 𝐶 ) = 0 ) |
| 8 | 1 5 2 | sub32d | ⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) − 𝐵 ) = ( ( 𝐴 − 𝐵 ) − 𝐶 ) ) |
| 9 | 2 | subidd | ⊢ ( 𝜑 → ( 𝐵 − 𝐵 ) = 0 ) |
| 10 | 7 8 9 | 3eqtr4d | ⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) − 𝐵 ) = ( 𝐵 − 𝐵 ) ) |
| 11 | 6 2 2 10 | subcan2d | ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = 𝐵 ) |