Metamath Proof Explorer


Theorem xdivmul

Description: Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016)

Ref Expression
Assertion xdivmul A * B * C C 0 A ÷ 𝑒 C = B C 𝑒 B = A

Proof

Step Hyp Ref Expression
1 xdivval A * C C 0 A ÷ 𝑒 C = ι x * | C 𝑒 x = A
2 1 3expb A * C C 0 A ÷ 𝑒 C = ι x * | C 𝑒 x = A
3 2 3adant2 A * B * C C 0 A ÷ 𝑒 C = ι x * | C 𝑒 x = A
4 3 eqeq1d A * B * C C 0 A ÷ 𝑒 C = B ι x * | C 𝑒 x = A = B
5 simp2 A * B * C C 0 B *
6 xreceu A * C C 0 ∃! x * C 𝑒 x = A
7 6 3expb A * C C 0 ∃! x * C 𝑒 x = A
8 7 3adant2 A * B * C C 0 ∃! x * C 𝑒 x = A
9 oveq2 x = B C 𝑒 x = C 𝑒 B
10 9 eqeq1d x = B C 𝑒 x = A C 𝑒 B = A
11 10 riota2 B * ∃! x * C 𝑒 x = A C 𝑒 B = A ι x * | C 𝑒 x = A = B
12 5 8 11 syl2anc A * B * C C 0 C 𝑒 B = A ι x * | C 𝑒 x = A = B
13 4 12 bitr4d A * B * C C 0 A ÷ 𝑒 C = B C 𝑒 B = A