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

Metamath Proof Explorer

Definition df-erq

Description: Define a convenience function that "reduces" a fraction to lowest terms. Note that in this form, it is not obviously a function; we prove this in nqerf . (Contributed by NM, 27-Aug-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-erq	$⊢ /_{𝑸} = ~_{𝑸} \cap ((𝑵 \times 𝑵) \times 𝑸)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cerq	$class /_{𝑸}$
1		ceq	$class ~_{𝑸}$
2		cnpi	$class 𝑵$
3	2 2	cxp	$class (𝑵 \times 𝑵)$
4		cnq	$class 𝑸$
5	3 4	cxp	$class ((𝑵 \times 𝑵) \times 𝑸)$
6	1 5	cin	$class (~_{𝑸} \cap ((𝑵 \times 𝑵) \times 𝑸))$
7	0 6	wceq	$wff /_{𝑸} = ~_{𝑸} \cap ((𝑵 \times 𝑵) \times 𝑸)$