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 ) )