Metamath Proof Explorer


Theorem reladdrsub

Description: Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023)

Ref Expression
Hypotheses reladdrsub.1 ( 𝜑𝐴 ∈ ℝ )
reladdrsub.2 ( 𝜑𝐵 ∈ ℝ )
reladdrsub.3 ( 𝜑 → ( 𝐴 + 𝐵 ) = 𝐶 )
Assertion reladdrsub ( 𝜑𝐵 = ( 𝐶 𝐴 ) )

Proof

Step Hyp Ref Expression
1 reladdrsub.1 ( 𝜑𝐴 ∈ ℝ )
2 reladdrsub.2 ( 𝜑𝐵 ∈ ℝ )
3 reladdrsub.3 ( 𝜑 → ( 𝐴 + 𝐵 ) = 𝐶 )
4 1 2 readdcld ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
5 3 4 eqeltrrd ( 𝜑𝐶 ∈ ℝ )
6 resubadd ( ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐶 𝐴 ) = 𝐵 ↔ ( 𝐴 + 𝐵 ) = 𝐶 ) )
7 3 6 syl5ibrcom ( 𝜑 → ( ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 𝐴 ) = 𝐵 ) )
8 5 1 2 7 mp3and ( 𝜑 → ( 𝐶 𝐴 ) = 𝐵 )
9 8 eqcomd ( 𝜑𝐵 = ( 𝐶 𝐴 ) )