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	⊢ [Q] = ( ~_Q ∩ ( ( N × N ) × Q ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cerq	⊢ [Q]
1		ceq	⊢ ~_Q
2		cnpi	⊢ N
3	2 2	cxp	⊢ ( N × N )
4		cnq	⊢ Q
5	3 4	cxp	⊢ ( ( N × N ) × Q )
6	1 5	cin	⊢ ( ~_Q ∩ ( ( N × N ) × Q ) )
7	0 6	wceq	⊢ [Q] = ( ~_Q ∩ ( ( N × N ) × Q ) )