Metamath Proof Explorer


Theorem xmul01

Description: Extended real version of mul01 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmul01 A * A 𝑒 0 = 0

Proof

Step Hyp Ref Expression
1 0xr 0 *
2 xmulval A * 0 * A 𝑒 0 = if A = 0 0 = 0 0 if 0 < 0 A = +∞ 0 < 0 A = −∞ 0 < A 0 = +∞ A < 0 0 = −∞ +∞ if 0 < 0 A = −∞ 0 < 0 A = +∞ 0 < A 0 = −∞ A < 0 0 = +∞ −∞ A 0
3 1 2 mpan2 A * A 𝑒 0 = if A = 0 0 = 0 0 if 0 < 0 A = +∞ 0 < 0 A = −∞ 0 < A 0 = +∞ A < 0 0 = −∞ +∞ if 0 < 0 A = −∞ 0 < 0 A = +∞ 0 < A 0 = −∞ A < 0 0 = +∞ −∞ A 0
4 eqid 0 = 0
5 4 olci A = 0 0 = 0
6 5 iftruei if A = 0 0 = 0 0 if 0 < 0 A = +∞ 0 < 0 A = −∞ 0 < A 0 = +∞ A < 0 0 = −∞ +∞ if 0 < 0 A = −∞ 0 < 0 A = +∞ 0 < A 0 = −∞ A < 0 0 = +∞ −∞ A 0 = 0
7 3 6 eqtrdi A * A 𝑒 0 = 0