Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-erq | Structured version Visualization version GIF version |
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 9631. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-erq | ⊢ [Q] = ( ~Q ∩ ((N × N) × Q)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cerq 9555 | . 2 class [Q] | |
2 | ceq 9552 | . . 3 class ~Q | |
3 | cnpi 9545 | . . . . 5 class N | |
4 | 3, 3 | cxp 5036 | . . . 4 class (N × N) |
5 | cnq 9553 | . . . 4 class Q | |
6 | 4, 5 | cxp 5036 | . . 3 class ((N × N) × Q) |
7 | 2, 6 | cin 3539 | . 2 class ( ~Q ∩ ((N × N) × Q)) |
8 | 1, 7 | wceq 1475 | 1 wff [Q] = ( ~Q ∩ ((N × N) × Q)) |
Colors of variables: wff setvar class |
This definition is referenced by: nqerf 9631 nqerrel 9633 nqerid 9634 |
Copyright terms: Public domain | W3C validator |