Step |
Hyp |
Ref |
Expression |
1 |
|
pellfundval |
|- ( D e. ( NN \ []NN ) -> ( PellFund ` D ) = inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) ) |
2 |
1
|
3ad2ant1 |
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( PellFund ` D ) = inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) ) |
3 |
|
ssrab2 |
|- { a e. ( Pell14QR ` D ) | 1 < a } C_ ( Pell14QR ` D ) |
4 |
|
pell14qrre |
|- ( ( D e. ( NN \ []NN ) /\ d e. ( Pell14QR ` D ) ) -> d e. RR ) |
5 |
4
|
ex |
|- ( D e. ( NN \ []NN ) -> ( d e. ( Pell14QR ` D ) -> d e. RR ) ) |
6 |
5
|
ssrdv |
|- ( D e. ( NN \ []NN ) -> ( Pell14QR ` D ) C_ RR ) |
7 |
3 6
|
sstrid |
|- ( D e. ( NN \ []NN ) -> { a e. ( Pell14QR ` D ) | 1 < a } C_ RR ) |
8 |
7
|
3ad2ant1 |
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> { a e. ( Pell14QR ` D ) | 1 < a } C_ RR ) |
9 |
|
1re |
|- 1 e. RR |
10 |
|
breq2 |
|- ( a = c -> ( 1 < a <-> 1 < c ) ) |
11 |
10
|
elrab |
|- ( c e. { a e. ( Pell14QR ` D ) | 1 < a } <-> ( c e. ( Pell14QR ` D ) /\ 1 < c ) ) |
12 |
|
pell14qrre |
|- ( ( D e. ( NN \ []NN ) /\ c e. ( Pell14QR ` D ) ) -> c e. RR ) |
13 |
|
ltle |
|- ( ( 1 e. RR /\ c e. RR ) -> ( 1 < c -> 1 <_ c ) ) |
14 |
9 12 13
|
sylancr |
|- ( ( D e. ( NN \ []NN ) /\ c e. ( Pell14QR ` D ) ) -> ( 1 < c -> 1 <_ c ) ) |
15 |
14
|
expimpd |
|- ( D e. ( NN \ []NN ) -> ( ( c e. ( Pell14QR ` D ) /\ 1 < c ) -> 1 <_ c ) ) |
16 |
11 15
|
syl5bi |
|- ( D e. ( NN \ []NN ) -> ( c e. { a e. ( Pell14QR ` D ) | 1 < a } -> 1 <_ c ) ) |
17 |
16
|
ralrimiv |
|- ( D e. ( NN \ []NN ) -> A. c e. { a e. ( Pell14QR ` D ) | 1 < a } 1 <_ c ) |
18 |
17
|
3ad2ant1 |
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> A. c e. { a e. ( Pell14QR ` D ) | 1 < a } 1 <_ c ) |
19 |
|
breq1 |
|- ( b = 1 -> ( b <_ c <-> 1 <_ c ) ) |
20 |
19
|
ralbidv |
|- ( b = 1 -> ( A. c e. { a e. ( Pell14QR ` D ) | 1 < a } b <_ c <-> A. c e. { a e. ( Pell14QR ` D ) | 1 < a } 1 <_ c ) ) |
21 |
20
|
rspcev |
|- ( ( 1 e. RR /\ A. c e. { a e. ( Pell14QR ` D ) | 1 < a } 1 <_ c ) -> E. b e. RR A. c e. { a e. ( Pell14QR ` D ) | 1 < a } b <_ c ) |
22 |
9 18 21
|
sylancr |
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> E. b e. RR A. c e. { a e. ( Pell14QR ` D ) | 1 < a } b <_ c ) |
23 |
|
simp2 |
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> A e. ( Pell14QR ` D ) ) |
24 |
|
simp3 |
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 1 < A ) |
25 |
|
breq2 |
|- ( a = A -> ( 1 < a <-> 1 < A ) ) |
26 |
25
|
elrab |
|- ( A e. { a e. ( Pell14QR ` D ) | 1 < a } <-> ( A e. ( Pell14QR ` D ) /\ 1 < A ) ) |
27 |
23 24 26
|
sylanbrc |
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> A e. { a e. ( Pell14QR ` D ) | 1 < a } ) |
28 |
|
infrelb |
|- ( ( { a e. ( Pell14QR ` D ) | 1 < a } C_ RR /\ E. b e. RR A. c e. { a e. ( Pell14QR ` D ) | 1 < a } b <_ c /\ A e. { a e. ( Pell14QR ` D ) | 1 < a } ) -> inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) <_ A ) |
29 |
8 22 27 28
|
syl3anc |
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) <_ A ) |
30 |
2 29
|
eqbrtrd |
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( PellFund ` D ) <_ A ) |