Theorem addid0

Description: If adding a number to a another number yields the other number, the added number must be 0 . This shows that 0 is the unique (right) identity of the complex numbers. (Contributed by AV, 17-Jan-2021)

	Ref	Expression
Assertion	addid0	|- ( ( X e. CC /\ Y e. CC ) -> ( ( X + Y ) = X <-> Y = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( X e. CC /\ Y e. CC ) -> X e. CC )
2		simpr	|- ( ( X e. CC /\ Y e. CC ) -> Y e. CC )
3	1 1 2	subaddd	|- ( ( X e. CC /\ Y e. CC ) -> ( ( X - X ) = Y <-> ( X + Y ) = X ) )
4		eqcom	|- ( ( X - X ) = Y <-> Y = ( X - X ) )
5		simpr	|- ( ( X e. CC /\ Y = ( X - X ) ) -> Y = ( X - X ) )
6		subid	|- ( X e. CC -> ( X - X ) = 0 )
7	6	adantr	|- ( ( X e. CC /\ Y = ( X - X ) ) -> ( X - X ) = 0 )
8	5 7	eqtrd	|- ( ( X e. CC /\ Y = ( X - X ) ) -> Y = 0 )
9	8	ex	|- ( X e. CC -> ( Y = ( X - X ) -> Y = 0 ) )
10	4 9	syl5bi	|- ( X e. CC -> ( ( X - X ) = Y -> Y = 0 ) )
11	10	adantr	|- ( ( X e. CC /\ Y e. CC ) -> ( ( X - X ) = Y -> Y = 0 ) )
12	3 11	sylbird	|- ( ( X e. CC /\ Y e. CC ) -> ( ( X + Y ) = X -> Y = 0 ) )
13		oveq2	|- ( Y = 0 -> ( X + Y ) = ( X + 0 ) )
14		addid1	|- ( X e. CC -> ( X + 0 ) = X )
15	13 14	sylan9eqr	|- ( ( X e. CC /\ Y = 0 ) -> ( X + Y ) = X )
16	15	ex	|- ( X e. CC -> ( Y = 0 -> ( X + Y ) = X ) )
17	16	adantr	|- ( ( X e. CC /\ Y e. CC ) -> ( Y = 0 -> ( X + Y ) = X ) )
18	12 17	impbid	|- ( ( X e. CC /\ Y e. CC ) -> ( ( X + Y ) = X <-> Y = 0 ) )