This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem redivrec2d

Description: Relationship between division and reciprocal. (Contributed by SN, 9-Apr-2026)

Ref Expression
Hypotheses redivrec2d.a 
|- ( ph -> A e. RR )
redivrec2d.b 
|- ( ph -> B e. RR )
redivrec2d.z 
|- ( ph -> B =/= 0 )
Assertion redivrec2d 
|- ( ph -> ( A /R B ) = ( ( 1 /R B ) x. A ) )

Proof

Step Hyp Ref Expression
1 redivrec2d.a 
 |-  ( ph -> A e. RR )
2 redivrec2d.b 
 |-  ( ph -> B e. RR )
3 redivrec2d.z 
 |-  ( ph -> B =/= 0 )
4 2 3 rerecidd 
 |-  ( ph -> ( B x. ( 1 /R B ) ) = 1 )
5 4 oveq1d 
 |-  ( ph -> ( ( B x. ( 1 /R B ) ) x. A ) = ( 1 x. A ) )
6 2 recnd 
 |-  ( ph -> B e. CC )
7 2 3 sn-rereccld 
 |-  ( ph -> ( 1 /R B ) e. RR )
8 7 recnd 
 |-  ( ph -> ( 1 /R B ) e. CC )
9 1 recnd 
 |-  ( ph -> A e. CC )
10 6 8 9 mulassd 
 |-  ( ph -> ( ( B x. ( 1 /R B ) ) x. A ) = ( B x. ( ( 1 /R B ) x. A ) ) )
11 remullid 
 |-  ( A e. RR -> ( 1 x. A ) = A )
12 1 11 syl 
 |-  ( ph -> ( 1 x. A ) = A )
13 5 10 12 3eqtr3d 
 |-  ( ph -> ( B x. ( ( 1 /R B ) x. A ) ) = A )
14 7 1 remulcld 
 |-  ( ph -> ( ( 1 /R B ) x. A ) e. RR )
15 1 14 2 3 redivmuld 
 |-  ( ph -> ( ( A /R B ) = ( ( 1 /R B ) x. A ) <-> ( B x. ( ( 1 /R B ) x. A ) ) = A ) )
16 13 15 mpbird 
 |-  ( ph -> ( A /R B ) = ( ( 1 /R B ) x. A ) )