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	$⊢ φ \to A \in ℝ$
		redivrec2d.b	$⊢ φ \to B \in ℝ$
		redivrec2d.z	$⊢ φ \to B \neq 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	$⊢ φ \to A \in ℝ$
2		redivrec2d.b	$⊢ φ \to B \in ℝ$
3		redivrec2d.z	$⊢ φ \to B \neq 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	$⊢ φ \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	$⊢ φ \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 1 A = A$
12	1 11	syl	$⊢ φ \to 1 A = 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 \|-