This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐵 = ( 𝐶 −ℝ 𝐴 ) )