Theorem redivrec2d

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

	Ref	Expression
Hypotheses	redivrec2d.a	$$⊢\phi \to A\in ℝ$$
	redivrec2d.b	$$⊢\phi \to B\in ℝ$$
	redivrec2d.z	$$⊢\phi \to B\ne 0$$
Assertion	redivrec2d	Could not format assertion : No typesetting found for |- ( ph -> ( A /R B ) = ( ( 1 /R B ) x. A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		redivrec2d.a	$$⊢\phi \to A\in ℝ$$
2		redivrec2d.b	$$⊢\phi \to B\in ℝ$$
3		redivrec2d.z	$$⊢\phi \to B\ne 0$$
4	2 3	rerecidd	Could not format ( ph -> ( B x. ( 1 /R B ) ) = 1 ) : No typesetting found for |- ( ph -> ( B x. ( 1 /R B ) ) = 1 ) with typecode |-
5	4	oveq1d	Could not format ( ph -> ( ( B x. ( 1 /R B ) ) x. A ) = ( 1 x. A ) ) : No typesetting found for |- ( ph -> ( ( B x. ( 1 /R B ) ) x. A ) = ( 1 x. A ) ) with typecode |-
6	2	recnd	$$⊢\phi \to B\in ℂ$$
7	2 3	sn-rereccld	Could not format ( ph -> ( 1 /R B ) e. RR ) : No typesetting found for |- ( ph -> ( 1 /R B ) e. RR ) with typecode |-
8	7	recnd	Could not format ( ph -> ( 1 /R B ) e. CC ) : No typesetting found for |- ( ph -> ( 1 /R B ) e. CC ) with typecode |-
9	1	recnd	$$⊢\phi \to A\in ℂ$$
10	6 8 9	mulassd	Could not format ( ph -> ( ( B x. ( 1 /R B ) ) x. A ) = ( B x. ( ( 1 /R B ) x. A ) ) ) : No typesetting found for |- ( ph -> ( ( B x. ( 1 /R B ) ) x. A ) = ( B x. ( ( 1 /R B ) x. A ) ) ) with typecode |-
11		remullid	$$⊢A\in ℝ\to 1A=A$$
12	1 11	syl	$$⊢\phi \to 1A=A$$
13	5 10 12	3eqtr3d	Could not format ( ph -> ( B x. ( ( 1 /R B ) x. A ) ) = A ) : No typesetting found for |- ( ph -> ( B x. ( ( 1 /R B ) x. A ) ) = A ) with typecode |-
14	7 1	remulcld	Could not format ( ph -> ( ( 1 /R B ) x. A ) e. RR ) : No typesetting found for |- ( ph -> ( ( 1 /R B ) x. A ) e. RR ) with typecode |-
15	1 14 2 3	redivmuld	Could not format ( ph -> ( ( A /R B ) = ( ( 1 /R B ) x. A ) <-> ( B x. ( ( 1 /R B ) x. A ) ) = A ) ) : No typesetting found for |- ( ph -> ( ( A /R B ) = ( ( 1 /R B ) x. A ) <-> ( B x. ( ( 1 /R B ) x. A ) ) = A ) ) with typecode |-
16	13 15	mpbird	Could not format ( ph -> ( A /R B ) = ( ( 1 /R B ) x. A ) ) : No typesetting found for |- ( ph -> ( A /R B ) = ( ( 1 /R B ) x. A ) ) with typecode |-