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

Metamath Proof Explorer

Theorem resubcan2

Description: Cancellation law for real subtraction. Compare subcan2 . (Contributed by Steven Nguyen, 8-Jan-2023)

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

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) )
2 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → 𝐴 ∈ ℝ )
3 simpl3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → 𝐶 ∈ ℝ )
4 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → 𝐵 ∈ ℝ )
5 rersubcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 −ℝ 𝐶 ) ∈ ℝ )
6 4 3 5 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → ( 𝐵 −ℝ 𝐶 ) ∈ ℝ )
7 2 3 6 resubaddd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → ( ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ↔ ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐴 ) )
8 1 7 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐴 )
9 repncan3 ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐵 )
10 3 4 9 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐵 )
11 8 10 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → 𝐴 = 𝐵 )
12 11 ex ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) → 𝐴 = 𝐵 ) )
13 oveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) )
14 12 13 impbid1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ↔ 𝐴 = 𝐵 ) )