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

Metamath Proof Explorer

Theorem resubadd

Description: Relation between real subtraction and addition. Based on subadd . (Contributed by Steven Nguyen, 7-Jan-2023)

Ref Expression
Assertion resubadd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐵 ) = 𝐶 ↔ ( 𝐵 + 𝐶 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 resubval ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 −ℝ 𝐵 ) = ( ℩ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 ) )
2 1 eqeq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐵 ) = 𝐶 ↔ ( ℩ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 ) = 𝐶 ) )
3 2 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐵 ) = 𝐶 ↔ ( ℩ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 ) = 𝐶 ) )
4 resubeu ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ∃! 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 )
5 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐵 + 𝑥 ) = ( 𝐵 + 𝐶 ) )
6 5 eqeq1d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐵 + 𝑥 ) = 𝐴 ↔ ( 𝐵 + 𝐶 ) = 𝐴 ) )
7 6 riota2 ⊢ ( ( 𝐶 ∈ ℝ ∧ ∃! 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 ) → ( ( 𝐵 + 𝐶 ) = 𝐴 ↔ ( ℩ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 ) = 𝐶 ) )
8 4 7 sylan2 ⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) → ( ( 𝐵 + 𝐶 ) = 𝐴 ↔ ( ℩ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 ) = 𝐶 ) )
9 8 3impb ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 + 𝐶 ) = 𝐴 ↔ ( ℩ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 ) = 𝐶 ) )
10 9 3com13 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 + 𝐶 ) = 𝐴 ↔ ( ℩ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 ) = 𝐶 ) )
11 3 10 bitr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐵 ) = 𝐶 ↔ ( 𝐵 + 𝐶 ) = 𝐴 ) )