Metamath Proof Explorer


Theorem qdenval

Description: Value of the canonical denominator function. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion qdenval AdenomA=2ndιx×|1stxgcd2ndx=1A=1stx2ndx

Proof

Step Hyp Ref Expression
1 eqeq1 a=Aa=1stx2ndxA=1stx2ndx
2 1 anbi2d a=A1stxgcd2ndx=1a=1stx2ndx1stxgcd2ndx=1A=1stx2ndx
3 2 riotabidv a=Aιx×|1stxgcd2ndx=1a=1stx2ndx=ιx×|1stxgcd2ndx=1A=1stx2ndx
4 3 fveq2d a=A2ndιx×|1stxgcd2ndx=1a=1stx2ndx=2ndιx×|1stxgcd2ndx=1A=1stx2ndx
5 df-denom denom=a2ndιx×|1stxgcd2ndx=1a=1stx2ndx
6 fvex 2ndιx×|1stxgcd2ndx=1A=1stx2ndxV
7 4 5 6 fvmpt AdenomA=2ndιx×|1stxgcd2ndx=1A=1stx2ndx