Step | Hyp | Ref
| Expression |
1 | | pellfundval 41921 |
. . 3
β’ (π· β (β β
β»NN) β (PellFundβπ·) = inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < )) |
2 | 1 | 3ad2ant1 1132 |
. 2
β’ ((π· β (β β
β»NN) β§ π΄ β (Pell14QRβπ·) β§ 1 < π΄) β (PellFundβπ·) = inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < )) |
3 | | ssrab2 4078 |
. . . . 5
β’ {π β (Pell14QRβπ·) β£ 1 < π} β (Pell14QRβπ·) |
4 | | pell14qrre 41898 |
. . . . . . 7
β’ ((π· β (β β
β»NN) β§ π β (Pell14QRβπ·)) β π β β) |
5 | 4 | ex 412 |
. . . . . 6
β’ (π· β (β β
β»NN) β (π β (Pell14QRβπ·) β π β β)) |
6 | 5 | ssrdv 3989 |
. . . . 5
β’ (π· β (β β
β»NN) β (Pell14QRβπ·) β β) |
7 | 3, 6 | sstrid 3994 |
. . . 4
β’ (π· β (β β
β»NN) β {π β (Pell14QRβπ·) β£ 1 < π} β β) |
8 | 7 | 3ad2ant1 1132 |
. . 3
β’ ((π· β (β β
β»NN) β§ π΄ β (Pell14QRβπ·) β§ 1 < π΄) β {π β (Pell14QRβπ·) β£ 1 < π} β β) |
9 | | 1re 11219 |
. . . 4
β’ 1 β
β |
10 | | breq2 5153 |
. . . . . . . 8
β’ (π = π β (1 < π β 1 < π)) |
11 | 10 | elrab 3684 |
. . . . . . 7
β’ (π β {π β (Pell14QRβπ·) β£ 1 < π} β (π β (Pell14QRβπ·) β§ 1 < π)) |
12 | | pell14qrre 41898 |
. . . . . . . . 9
β’ ((π· β (β β
β»NN) β§ π β (Pell14QRβπ·)) β π β β) |
13 | | ltle 11307 |
. . . . . . . . 9
β’ ((1
β β β§ π
β β) β (1 < π β 1 β€ π)) |
14 | 9, 12, 13 | sylancr 586 |
. . . . . . . 8
β’ ((π· β (β β
β»NN) β§ π β (Pell14QRβπ·)) β (1 < π β 1 β€ π)) |
15 | 14 | expimpd 453 |
. . . . . . 7
β’ (π· β (β β
β»NN) β ((π β (Pell14QRβπ·) β§ 1 < π) β 1 β€ π)) |
16 | 11, 15 | biimtrid 241 |
. . . . . 6
β’ (π· β (β β
β»NN) β (π β {π β (Pell14QRβπ·) β£ 1 < π} β 1 β€ π)) |
17 | 16 | ralrimiv 3144 |
. . . . 5
β’ (π· β (β β
β»NN) β βπ β {π β (Pell14QRβπ·) β£ 1 < π}1 β€ π) |
18 | 17 | 3ad2ant1 1132 |
. . . 4
β’ ((π· β (β β
β»NN) β§ π΄ β (Pell14QRβπ·) β§ 1 < π΄) β βπ β {π β (Pell14QRβπ·) β£ 1 < π}1 β€ π) |
19 | | breq1 5152 |
. . . . . 6
β’ (π = 1 β (π β€ π β 1 β€ π)) |
20 | 19 | ralbidv 3176 |
. . . . 5
β’ (π = 1 β (βπ β {π β (Pell14QRβπ·) β£ 1 < π}π β€ π β βπ β {π β (Pell14QRβπ·) β£ 1 < π}1 β€ π)) |
21 | 20 | rspcev 3613 |
. . . 4
β’ ((1
β β β§ βπ β {π β (Pell14QRβπ·) β£ 1 < π}1 β€ π) β βπ β β βπ β {π β (Pell14QRβπ·) β£ 1 < π}π β€ π) |
22 | 9, 18, 21 | sylancr 586 |
. . 3
β’ ((π· β (β β
β»NN) β§ π΄ β (Pell14QRβπ·) β§ 1 < π΄) β βπ β β βπ β {π β (Pell14QRβπ·) β£ 1 < π}π β€ π) |
23 | | simp2 1136 |
. . . 4
β’ ((π· β (β β
β»NN) β§ π΄ β (Pell14QRβπ·) β§ 1 < π΄) β π΄ β (Pell14QRβπ·)) |
24 | | simp3 1137 |
. . . 4
β’ ((π· β (β β
β»NN) β§ π΄ β (Pell14QRβπ·) β§ 1 < π΄) β 1 < π΄) |
25 | | breq2 5153 |
. . . . 5
β’ (π = π΄ β (1 < π β 1 < π΄)) |
26 | 25 | elrab 3684 |
. . . 4
β’ (π΄ β {π β (Pell14QRβπ·) β£ 1 < π} β (π΄ β (Pell14QRβπ·) β§ 1 < π΄)) |
27 | 23, 24, 26 | sylanbrc 582 |
. . 3
β’ ((π· β (β β
β»NN) β§ π΄ β (Pell14QRβπ·) β§ 1 < π΄) β π΄ β {π β (Pell14QRβπ·) β£ 1 < π}) |
28 | | infrelb 12204 |
. . 3
β’ (({π β (Pell14QRβπ·) β£ 1 < π} β β β§
βπ β β
βπ β {π β (Pell14QRβπ·) β£ 1 < π}π β€ π β§ π΄ β {π β (Pell14QRβπ·) β£ 1 < π}) β inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < ) β€ π΄) |
29 | 8, 22, 27, 28 | syl3anc 1370 |
. 2
β’ ((π· β (β β
β»NN) β§ π΄ β (Pell14QRβπ·) β§ 1 < π΄) β inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < ) β€ π΄) |
30 | 2, 29 | eqbrtrd 5171 |
1
β’ ((π· β (β β
β»NN) β§ π΄ β (Pell14QRβπ·) β§ 1 < π΄) β (PellFundβπ·) β€ π΄) |