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

Metamath Proof Explorer

Theorem addlsub

Description: Left-subtraction: Subtraction of the left summand from the result of an addition. (Contributed by BJ, 6-Jun-2019)

		Ref	Expression
	Hypotheses	addlsub.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
		addlsub.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
		addlsub.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	Assertion	addlsub	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) = 𝐶 ↔ 𝐴 = ( 𝐶 − 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		addlsub.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		addlsub.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		addlsub.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		oveq1	⊢ ( ( 𝐴 + 𝐵 ) = 𝐶 → ( ( 𝐴 + 𝐵 ) − 𝐵 ) = ( 𝐶 − 𝐵 ) )
5	1 2	pncand	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 )
6		eqtr2	⊢ ( ( ( ( 𝐴 + 𝐵 ) − 𝐵 ) = ( 𝐶 − 𝐵 ) ∧ ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 ) → ( 𝐶 − 𝐵 ) = 𝐴 )
7	6	eqcomd	⊢ ( ( ( ( 𝐴 + 𝐵 ) − 𝐵 ) = ( 𝐶 − 𝐵 ) ∧ ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 ) → 𝐴 = ( 𝐶 − 𝐵 ) )
8	7	a1i	⊢ ( 𝜑 → ( ( ( ( 𝐴 + 𝐵 ) − 𝐵 ) = ( 𝐶 − 𝐵 ) ∧ ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 ) → 𝐴 = ( 𝐶 − 𝐵 ) ) )
9	5 8	mpan2d	⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) − 𝐵 ) = ( 𝐶 − 𝐵 ) → 𝐴 = ( 𝐶 − 𝐵 ) ) )
10	4 9	syl5	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) = 𝐶 → 𝐴 = ( 𝐶 − 𝐵 ) ) )
11		oveq1	⊢ ( 𝐴 = ( 𝐶 − 𝐵 ) → ( 𝐴 + 𝐵 ) = ( ( 𝐶 − 𝐵 ) + 𝐵 ) )
12	3 2	npcand	⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) + 𝐵 ) = 𝐶 )
13		eqtr	⊢ ( ( ( 𝐴 + 𝐵 ) = ( ( 𝐶 − 𝐵 ) + 𝐵 ) ∧ ( ( 𝐶 − 𝐵 ) + 𝐵 ) = 𝐶 ) → ( 𝐴 + 𝐵 ) = 𝐶 )
14	13	a1i	⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) = ( ( 𝐶 − 𝐵 ) + 𝐵 ) ∧ ( ( 𝐶 − 𝐵 ) + 𝐵 ) = 𝐶 ) → ( 𝐴 + 𝐵 ) = 𝐶 ) )
15	12 14	mpan2d	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) = ( ( 𝐶 − 𝐵 ) + 𝐵 ) → ( 𝐴 + 𝐵 ) = 𝐶 ) )
16	11 15	syl5	⊢ ( 𝜑 → ( 𝐴 = ( 𝐶 − 𝐵 ) → ( 𝐴 + 𝐵 ) = 𝐶 ) )
17	10 16	impbid	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) = 𝐶 ↔ 𝐴 = ( 𝐶 − 𝐵 ) ) )