Metamath Proof Explorer


Theorem fden

Description: Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion fden denom:

Proof

Step Hyp Ref Expression
1 df-denom denom=a2ndιb×|1stbgcd2ndb=1a=1stb2ndb
2 qdenval adenoma=2ndιb×|1stbgcd2ndb=1a=1stb2ndb
3 qdencl adenoma
4 2 3 eqeltrrd a2ndιb×|1stbgcd2ndb=1a=1stb2ndb
5 1 4 fmpti denom: