Step | Hyp | Ref
| Expression |
1 | | pellfundval 41250 |
. 2
β’ (π· β (β β
β»NN) β (PellFundβπ·) = inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < )) |
2 | | ssrab2 4041 |
. . . 4
β’ {π β (Pell14QRβπ·) β£ 1 < π} β (Pell14QRβπ·) |
3 | | pell14qrre 41227 |
. . . . . 6
β’ ((π· β (β β
β»NN) β§ π β (Pell14QRβπ·)) β π β β) |
4 | 3 | ex 414 |
. . . . 5
β’ (π· β (β β
β»NN) β (π β (Pell14QRβπ·) β π β β)) |
5 | 4 | ssrdv 3954 |
. . . 4
β’ (π· β (β β
β»NN) β (Pell14QRβπ·) β β) |
6 | 2, 5 | sstrid 3959 |
. . 3
β’ (π· β (β β
β»NN) β {π β (Pell14QRβπ·) β£ 1 < π} β β) |
7 | | pell1qrss14 41238 |
. . . . 5
β’ (π· β (β β
β»NN) β (Pell1QRβπ·) β (Pell14QRβπ·)) |
8 | | pellqrex 41249 |
. . . . 5
β’ (π· β (β β
β»NN) β βπ β (Pell1QRβπ·)1 < π) |
9 | | ssrexv 4015 |
. . . . 5
β’
((Pell1QRβπ·)
β (Pell14QRβπ·)
β (βπ β
(Pell1QRβπ·)1 <
π β βπ β (Pell14QRβπ·)1 < π)) |
10 | 7, 8, 9 | sylc 65 |
. . . 4
β’ (π· β (β β
β»NN) β βπ β (Pell14QRβπ·)1 < π) |
11 | | rabn0 4349 |
. . . 4
β’ ({π β (Pell14QRβπ·) β£ 1 < π} β β
β
βπ β
(Pell14QRβπ·)1 <
π) |
12 | 10, 11 | sylibr 233 |
. . 3
β’ (π· β (β β
β»NN) β {π β (Pell14QRβπ·) β£ 1 < π} β β
) |
13 | | 1re 11163 |
. . . 4
β’ 1 β
β |
14 | | breq2 5113 |
. . . . . . 7
β’ (π = π β (1 < π β 1 < π)) |
15 | 14 | elrab 3649 |
. . . . . 6
β’ (π β {π β (Pell14QRβπ·) β£ 1 < π} β (π β (Pell14QRβπ·) β§ 1 < π)) |
16 | | pell14qrre 41227 |
. . . . . . . 8
β’ ((π· β (β β
β»NN) β§ π β (Pell14QRβπ·)) β π β β) |
17 | | ltle 11251 |
. . . . . . . 8
β’ ((1
β β β§ π
β β) β (1 < π β 1 β€ π)) |
18 | 13, 16, 17 | sylancr 588 |
. . . . . . 7
β’ ((π· β (β β
β»NN) β§ π β (Pell14QRβπ·)) β (1 < π β 1 β€ π)) |
19 | 18 | expimpd 455 |
. . . . . 6
β’ (π· β (β β
β»NN) β ((π β (Pell14QRβπ·) β§ 1 < π) β 1 β€ π)) |
20 | 15, 19 | biimtrid 241 |
. . . . 5
β’ (π· β (β β
β»NN) β (π β {π β (Pell14QRβπ·) β£ 1 < π} β 1 β€ π)) |
21 | 20 | ralrimiv 3139 |
. . . 4
β’ (π· β (β β
β»NN) β βπ β {π β (Pell14QRβπ·) β£ 1 < π}1 β€ π) |
22 | | breq1 5112 |
. . . . . 6
β’ (π = 1 β (π β€ π β 1 β€ π)) |
23 | 22 | ralbidv 3171 |
. . . . 5
β’ (π = 1 β (βπ β {π β (Pell14QRβπ·) β£ 1 < π}π β€ π β βπ β {π β (Pell14QRβπ·) β£ 1 < π}1 β€ π)) |
24 | 23 | rspcev 3583 |
. . . 4
β’ ((1
β β β§ βπ β {π β (Pell14QRβπ·) β£ 1 < π}1 β€ π) β βπ β β βπ β {π β (Pell14QRβπ·) β£ 1 < π}π β€ π) |
25 | 13, 21, 24 | sylancr 588 |
. . 3
β’ (π· β (β β
β»NN) β βπ β β βπ β {π β (Pell14QRβπ·) β£ 1 < π}π β€ π) |
26 | | infrecl 12145 |
. . 3
β’ (({π β (Pell14QRβπ·) β£ 1 < π} β β β§ {π β (Pell14QRβπ·) β£ 1 < π} β β
β§
βπ β β
βπ β {π β (Pell14QRβπ·) β£ 1 < π}π β€ π) β inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < ) β
β) |
27 | 6, 12, 25, 26 | syl3anc 1372 |
. 2
β’ (π· β (β β
β»NN) β inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < ) β
β) |
28 | 1, 27 | eqeltrd 2834 |
1
β’ (π· β (β β
β»NN) β (PellFundβπ·) β β) |