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 ∈ 𝑹 → A 0 𝑹 ⁢ B 0 𝑹 = A ⋅ 𝑹 B 0 𝑹

Proof

Step Hyp Ref Expression
1 0r ⊢ 0 𝑹 ∈ 𝑹
2 mulcnsr ⊢ A ∈ 𝑹 ∧ 0 𝑹 ∈ 𝑹 ∧ B ∈ 𝑹 ∧ 0 𝑹 ∈ 𝑹 → A 0 𝑹 ⁢ B 0 𝑹 = A ⋅ 𝑹 B + 𝑹 -1 𝑹 ⋅ 𝑹 0 𝑹 ⋅ 𝑹 0 𝑹 0 𝑹 ⋅ 𝑹 B + 𝑹 A ⋅ 𝑹 0 𝑹
3 2 an4s ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 ∧ 0 𝑹 ∈ 𝑹 ∧ 0 𝑹 ∈ 𝑹 → A 0 𝑹 ⁢ B 0 𝑹 = A ⋅ 𝑹 B + 𝑹 -1 𝑹 ⋅ 𝑹 0 𝑹 ⋅ 𝑹 0 𝑹 0 𝑹 ⋅ 𝑹 B + 𝑹 A ⋅ 𝑹 0 𝑹
4 1 1 3 mpanr12 ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 → A 0 𝑹 ⁢ B 0 𝑹 = 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 syl5eq ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 → A ⋅ 𝑹 B + 𝑹 -1 𝑹 ⋅ 𝑹 0 𝑹 ⋅ 𝑹 0 𝑹 = A ⋅ 𝑹 B
17 mulcomsr ⊢ 0 𝑹 ⋅ 𝑹 B = B ⋅ 𝑹 0 𝑹
18 00sr ⊢ B ∈ 𝑹 → B ⋅ 𝑹 0 𝑹 = 0 𝑹
19 17 18 syl5eq ⊢ 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 ⋅ 𝑹 B 0 𝑹
26 4 25 eqtrd ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 → A 0 𝑹 ⁢ B 0 𝑹 = A ⋅ 𝑹 B 0 𝑹