Metamath Proof Explorer


Theorem qnumval

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

Ref Expression
Assertion qnumval AnumerA=1stι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=A1stιx×|1stxgcd2ndx=1a=1stx2ndx=1stιx×|1stxgcd2ndx=1A=1stx2ndx
5 df-numer numer=a1stιx×|1stxgcd2ndx=1a=1stx2ndx
6 fvex 1stιx×|1stxgcd2ndx=1A=1stx2ndxV
7 4 5 6 fvmpt AnumerA=1stιx×|1stxgcd2ndx=1A=1stx2ndx