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

Metamath Proof Explorer

Theorem xnegeq

Description: Equality of two extended numbers with -e in front of them. (Contributed by FL, 26-Dec-2011) (Proof shortened by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xnegeq	⊢ ( 𝐴 = 𝐵 → -_𝑒 𝐴 = -_𝑒 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 = +∞ ↔ 𝐵 = +∞ ) )
2		eqeq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 = -∞ ↔ 𝐵 = -∞ ) )
3		negeq	⊢ ( 𝐴 = 𝐵 → - 𝐴 = - 𝐵 )
4	2 3	ifbieq2d	⊢ ( 𝐴 = 𝐵 → if ( 𝐴 = -∞ , +∞ , - 𝐴 ) = if ( 𝐵 = -∞ , +∞ , - 𝐵 ) )
5	1 4	ifbieq2d	⊢ ( 𝐴 = 𝐵 → if ( 𝐴 = +∞ , -∞ , if ( 𝐴 = -∞ , +∞ , - 𝐴 ) ) = if ( 𝐵 = +∞ , -∞ , if ( 𝐵 = -∞ , +∞ , - 𝐵 ) ) )
6		df-xneg	⊢ -_𝑒 𝐴 = if ( 𝐴 = +∞ , -∞ , if ( 𝐴 = -∞ , +∞ , - 𝐴 ) )
7		df-xneg	⊢ -_𝑒 𝐵 = if ( 𝐵 = +∞ , -∞ , if ( 𝐵 = -∞ , +∞ , - 𝐵 ) )
8	5 6 7	3eqtr4g	⊢ ( 𝐴 = 𝐵 → -_𝑒 𝐴 = -_𝑒 𝐵 )