Metamath Proof Explorer

Theorem subadd

Description: Relationship between subtraction and addition. (Contributed by NM, 20-Jan-1997) (Revised by Mario Carneiro, 21-Dec-2013)

Ref Expression
Assertion subadd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B=C↔B+C=A

Proof

Step Hyp Ref Expression
1 subval ⊢A∈ℂ∧B∈ℂ→A−B=ιx∈ℂ|B+x=A
2 1 eqeq1d ⊢A∈ℂ∧B∈ℂ→A−B=C↔ιx∈ℂ|B+x=A=C
3 2 3adant3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B=C↔ιx∈ℂ|B+x=A=C
4 negeu ⊢B∈ℂ∧A∈ℂ→∃!x∈ℂB+x=A
5 oveq2 ⊢x=C→B+x=B+C
6 5 eqeq1d ⊢x=C→B+x=A↔B+C=A
7 6 riota2 ⊢C∈ℂ∧∃!x∈ℂB+x=A→B+C=A↔ιx∈ℂ|B+x=A=C
8 4 7 sylan2 ⊢C∈ℂ∧B∈ℂ∧A∈ℂ→B+C=A↔ιx∈ℂ|B+x=A=C
9 8 3impb ⊢C∈ℂ∧B∈ℂ∧A∈ℂ→B+C=A↔ιx∈ℂ|B+x=A=C
10 9 3com13 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B+C=A↔ιx∈ℂ|B+x=A=C
11 3 10 bitr4d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B=C↔B+C=A