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

Metamath Proof Explorer

Theorem repnpcan

Description: Cancellation law for addition and real subtraction. Compare pnpcan . (Contributed by Steven Nguyen, 19-May-2023)

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

Proof

Step Hyp Ref Expression
1 readdcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
2 resubsub4 ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) −ℝ 𝐶 ) = ( ( 𝐴 + 𝐵 ) −ℝ ( 𝐴 + 𝐶 ) ) )
3 1 2 stoic4a ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) −ℝ 𝐶 ) = ( ( 𝐴 + 𝐵 ) −ℝ ( 𝐴 + 𝐶 ) ) )
4 repncan2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) = 𝐵 )
5 4 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) = 𝐵 )
6 5 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) )
7 3 6 eqtr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) −ℝ ( 𝐴 + 𝐶 ) ) = ( 𝐵 −ℝ 𝐶 ) )