Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Initial properties of the complex numbers
addneintrd
Metamath Proof Explorer
Description: Introducing a term on the left-hand side of a sum in a negated
equality. Contrapositive of addcanad . Consequence of addcand .
(Contributed by David Moews , 28-Feb-2017)
Ref
Expression
Hypotheses
muld.1
⊢ ( 𝜑 → 𝐴 ∈ ℂ )
addcomd.2
⊢ ( 𝜑 → 𝐵 ∈ ℂ )
addcand.3
⊢ ( 𝜑 → 𝐶 ∈ ℂ )
addneintrd.4
⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
Assertion
addneintrd
⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ≠ ( 𝐴 + 𝐶 ) )
Proof
Step
Hyp
Ref
Expression
1
muld.1
⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2
addcomd.2
⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3
addcand.3
⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4
addneintrd.4
⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
5
1 2 3
addcand
⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) = ( 𝐴 + 𝐶 ) ↔ 𝐵 = 𝐶 ) )
6
5
necon3bid
⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) ≠ ( 𝐴 + 𝐶 ) ↔ 𝐵 ≠ 𝐶 ) )
7
4 6
mpbird
⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ≠ ( 𝐴 + 𝐶 ) )