Metamath Proof Explorer


Theorem rediv

Description: Real part of a division. Related to remul2 . (Contributed by David A. Wheeler, 10-Jun-2015)

Ref Expression
Assertion rediv ABB0AB=AB

Proof

Step Hyp Ref Expression
1 ancom BB0AABB0
2 3anass ABB0ABB0
3 1 2 bitr4i BB0AABB0
4 rereccl BB01B
5 4 anim1i BB0A1BA
6 3 5 sylbir ABB01BA
7 remul2 1BA1BA=1BA
8 6 7 syl ABB01BA=1BA
9 recn BB
10 divrec2 ABB0AB=1BA
11 10 fveq2d ABB0AB=1BA
12 9 11 syl3an2 ABB0AB=1BA
13 recl AA
14 13 recnd AA
15 14 3ad2ant1 ABB0A
16 9 3ad2ant2 ABB0B
17 simp3 ABB0B0
18 15 16 17 divrec2d ABB0AB=1BA
19 8 12 18 3eqtr4d ABB0AB=AB