Metamath Proof Explorer

Theorem mulresr

Description: Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996) (New usage is discouraged.)

Ref Expression
Assertion mulresr ⊢A∈𝑹∧B∈𝑹→A0𝑹⁢B0𝑹=A⋅𝑹B0𝑹

Proof

Step Hyp Ref Expression
1 0r ⊢0𝑹∈𝑹
2 mulcnsr ⊢A∈𝑹∧0𝑹∈𝑹∧B∈𝑹∧0𝑹∈𝑹→A0𝑹⁢B0𝑹=A⋅𝑹B+𝑹-1𝑹⋅𝑹0𝑹⋅𝑹0𝑹0𝑹⋅𝑹B+𝑹A⋅𝑹0𝑹
3 2 an4s ⊢A∈𝑹∧B∈𝑹∧0𝑹∈𝑹∧0𝑹∈𝑹→A0𝑹⁢B0𝑹=A⋅𝑹B+𝑹-1𝑹⋅𝑹0𝑹⋅𝑹0𝑹0𝑹⋅𝑹B+𝑹A⋅𝑹0𝑹
4 1 1 3 mpanr12 ⊢A∈𝑹∧B∈𝑹→A0𝑹⁢B0𝑹=A⋅𝑹B+𝑹-1𝑹⋅𝑹0𝑹⋅𝑹0𝑹0𝑹⋅𝑹B+𝑹A⋅𝑹0𝑹
5 00sr ⊢0𝑹∈𝑹→0𝑹⋅𝑹0𝑹=0𝑹
6 1 5 ax-mp ⊢0𝑹⋅𝑹0𝑹=0𝑹
7 6 oveq2i ⊢-1𝑹⋅𝑹0𝑹⋅𝑹0𝑹=-1𝑹⋅𝑹0𝑹
8 m1r ⊢-1𝑹∈𝑹
9 00sr ⊢-1𝑹∈𝑹→-1𝑹⋅𝑹0𝑹=0𝑹
10 8 9 ax-mp ⊢-1𝑹⋅𝑹0𝑹=0𝑹
11 7 10 eqtri ⊢-1𝑹⋅𝑹0𝑹⋅𝑹0𝑹=0𝑹
12 11 oveq2i ⊢A⋅𝑹B+𝑹-1𝑹⋅𝑹0𝑹⋅𝑹0𝑹=A⋅𝑹B+𝑹0𝑹
13 mulclsr ⊢A∈𝑹∧B∈𝑹→A⋅𝑹B∈𝑹
14 0idsr ⊢A⋅𝑹B∈𝑹→A⋅𝑹B+𝑹0𝑹=A⋅𝑹B
15 13 14 syl ⊢A∈𝑹∧B∈𝑹→A⋅𝑹B+𝑹0𝑹=A⋅𝑹B
16 12 15 eqtrid ⊢A∈𝑹∧B∈𝑹→A⋅𝑹B+𝑹-1𝑹⋅𝑹0𝑹⋅𝑹0𝑹=A⋅𝑹B
17 mulcomsr ⊢0𝑹⋅𝑹B=B⋅𝑹0𝑹
18 00sr ⊢B∈𝑹→B⋅𝑹0𝑹=0𝑹
19 17 18 eqtrid ⊢B∈𝑹→0𝑹⋅𝑹B=0𝑹
20 00sr ⊢A∈𝑹→A⋅𝑹0𝑹=0𝑹
21 19 20 oveqan12rd ⊢A∈𝑹∧B∈𝑹→0𝑹⋅𝑹B+𝑹A⋅𝑹0𝑹=0𝑹+𝑹0𝑹
22 0idsr ⊢0𝑹∈𝑹→0𝑹+𝑹0𝑹=0𝑹
23 1 22 ax-mp ⊢0𝑹+𝑹0𝑹=0𝑹
24 21 23 eqtrdi ⊢A∈𝑹∧B∈𝑹→0𝑹⋅𝑹B+𝑹A⋅𝑹0𝑹=0𝑹
25 16 24 opeq12d ⊢A∈𝑹∧B∈𝑹→A⋅𝑹B+𝑹-1𝑹⋅𝑹0𝑹⋅𝑹0𝑹0𝑹⋅𝑹B+𝑹A⋅𝑹0𝑹=A⋅𝑹B0𝑹
26 4 25 eqtrd ⊢A∈𝑹∧B∈𝑹→A0𝑹⁢B0𝑹=A⋅𝑹B0𝑹