Metamath Proof Explorer

Theorem pellfundval

Description: Value of the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 18-Sep-2014) (Revised by AV, 17-Sep-2020)

Ref Expression
Assertion pellfundval 
|- ( D e. ( NN \ []NN ) -> ( PellFund ` D ) = inf ( { x e. ( Pell14QR ` D ) | 1 < x } , RR , < ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( a = D -> ( Pell14QR ` a ) = ( Pell14QR ` D ) )
2 rabeq 
 |-  ( ( Pell14QR ` a ) = ( Pell14QR ` D ) -> { x e. ( Pell14QR ` a ) | 1 < x } = { x e. ( Pell14QR ` D ) | 1 < x } )
3 1 2 syl 
 |-  ( a = D -> { x e. ( Pell14QR ` a ) | 1 < x } = { x e. ( Pell14QR ` D ) | 1 < x } )
4 3 infeq1d 
 |-  ( a = D -> inf ( { x e. ( Pell14QR ` a ) | 1 < x } , RR , < ) = inf ( { x e. ( Pell14QR ` D ) | 1 < x } , RR , < ) )
5 df-pellfund 
 |-  PellFund = ( a e. ( NN \ []NN ) |-> inf ( { x e. ( Pell14QR ` a ) | 1 < x } , RR , < ) )
6 ltso 
 |-  < Or RR
7 6 infex 
 |-  inf ( { x e. ( Pell14QR ` D ) | 1 < x } , RR , < ) e. _V
8 4 5 7 fvmpt 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) = inf ( { x e. ( Pell14QR ` D ) | 1 < x } , RR , < ) )