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

Metamath Proof Explorer

Theorem rennncan2

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

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
2 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
3 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
4 rersubcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 −ℝ 𝐶 ) ∈ ℝ )
5 3 2 4 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 −ℝ 𝐶 ) ∈ ℝ )
6 resubsub4 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ ( 𝐵 −ℝ 𝐶 ) ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐶 ) −ℝ ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐴 −ℝ ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) ) )
7 1 2 5 6 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐶 ) −ℝ ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐴 −ℝ ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) ) )
8 repncan3 ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐵 )
9 2 3 8 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐵 )
10 9 oveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 −ℝ ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) ) = ( 𝐴 −ℝ 𝐵 ) )
11 7 10 eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐶 ) −ℝ ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐴 −ℝ 𝐵 ) )