| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ssrab2 4077 |
. . . 4
β’ {π β (Pell14QRβπ·) β£ 1 < π} β (Pell14QRβπ·) |
| 2 | | pell14qrre 41585 |
. . . . . 6
β’ ((π· β (β β
β»NN) β§ π β (Pell14QRβπ·)) β π β β) |
| 3 | 2 | ex 413 |
. . . . 5
β’ (π· β (β β
β»NN) β (π β (Pell14QRβπ·) β π β β)) |
| 4 | 3 | ssrdv 3988 |
. . . 4
β’ (π· β (β β
β»NN) β (Pell14QRβπ·) β β) |
| 5 | 1, 4 | sstrid 3993 |
. . 3
β’ (π· β (β β
β»NN) β {π β (Pell14QRβπ·) β£ 1 < π} β β) |
| 6 | | pell1qrss14 41596 |
. . . . 5
β’ (π· β (β β
β»NN) β (Pell1QRβπ·) β (Pell14QRβπ·)) |
| 7 | | pellqrex 41607 |
. . . . 5
β’ (π· β (β β
β»NN) β βπ β (Pell1QRβπ·)1 < π) |
| 8 | | ssrexv 4051 |
. . . . 5
β’
((Pell1QRβπ·)
β (Pell14QRβπ·)
β (βπ β
(Pell1QRβπ·)1 <
π β βπ β (Pell14QRβπ·)1 < π)) |
| 9 | 6, 7, 8 | sylc 65 |
. . . 4
β’ (π· β (β β
β»NN) β βπ β (Pell14QRβπ·)1 < π) |
| 10 | | rabn0 4385 |
. . . 4
β’ ({π β (Pell14QRβπ·) β£ 1 < π} β β
β
βπ β
(Pell14QRβπ·)1 <
π) |
| 11 | 9, 10 | sylibr 233 |
. . 3
β’ (π· β (β β
β»NN) β {π β (Pell14QRβπ·) β£ 1 < π} β β
) |
| 12 | | eldifi 4126 |
. . . . . . . 8
β’ (π· β (β β
β»NN) β π· β β) |
| 13 | 12 | peano2nnd 12228 |
. . . . . . 7
β’ (π· β (β β
β»NN) β (π· + 1) β β) |
| 14 | 13 | nnrpd 13013 |
. . . . . 6
β’ (π· β (β β
β»NN) β (π· + 1) β
β+) |
| 15 | 14 | rpsqrtcld 15357 |
. . . . 5
β’ (π· β (β β
β»NN) β (ββ(π· + 1)) β
β+) |
| 16 | 15 | rpred 13015 |
. . . 4
β’ (π· β (β β
β»NN) β (ββ(π· + 1)) β β) |
| 17 | 12 | nnrpd 13013 |
. . . . . 6
β’ (π· β (β β
β»NN) β π· β
β+) |
| 18 | 17 | rpsqrtcld 15357 |
. . . . 5
β’ (π· β (β β
β»NN) β (ββπ·) β
β+) |
| 19 | 18 | rpred 13015 |
. . . 4
β’ (π· β (β β
β»NN) β (ββπ·) β β) |
| 20 | 16, 19 | readdcld 11242 |
. . 3
β’ (π· β (β β
β»NN) β ((ββ(π· + 1)) + (ββπ·)) β β) |
| 21 | | breq2 5152 |
. . . . . 6
β’ (π = π β (1 < π β 1 < π)) |
| 22 | 21 | elrab 3683 |
. . . . 5
β’ (π β {π β (Pell14QRβπ·) β£ 1 < π} β (π β (Pell14QRβπ·) β§ 1 < π)) |
| 23 | | pell14qrgap 41603 |
. . . . . 6
β’ ((π· β (β β
β»NN) β§ π β (Pell14QRβπ·) β§ 1 < π) β ((ββ(π· + 1)) + (ββπ·)) β€ π) |
| 24 | 23 | 3expib 1122 |
. . . . 5
β’ (π· β (β β
β»NN) β ((π β (Pell14QRβπ·) β§ 1 < π) β ((ββ(π· + 1)) + (ββπ·)) β€ π)) |
| 25 | 22, 24 | biimtrid 241 |
. . . 4
β’ (π· β (β β
β»NN) β (π β {π β (Pell14QRβπ·) β£ 1 < π} β ((ββ(π· + 1)) + (ββπ·)) β€ π)) |
| 26 | 25 | ralrimiv 3145 |
. . 3
β’ (π· β (β β
β»NN) β βπ β {π β (Pell14QRβπ·) β£ 1 < π} ((ββ(π· + 1)) + (ββπ·)) β€ π) |
| 27 | | infmrgelbi 41606 |
. . 3
β’ ((({π β (Pell14QRβπ·) β£ 1 < π} β β β§ {π β (Pell14QRβπ·) β£ 1 < π} β β
β§
((ββ(π· + 1)) +
(ββπ·)) β
β) β§ βπ
β {π β
(Pell14QRβπ·) β£
1 < π}
((ββ(π· + 1)) +
(ββπ·)) β€
π) β
((ββ(π· + 1)) +
(ββπ·)) β€
inf({π β
(Pell14QRβπ·) β£
1 < π}, β, <
)) |
| 28 | 5, 11, 20, 26, 27 | syl31anc 1373 |
. 2
β’ (π· β (β β
β»NN) β ((ββ(π· + 1)) + (ββπ·)) β€ inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < )) |
| 29 | | pellfundval 41608 |
. 2
β’ (π· β (β β
β»NN) β (PellFundβπ·) = inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < )) |
| 30 | 28, 29 | breqtrrd 5176 |
1
β’ (π· β (β β
β»NN) β ((ββ(π· + 1)) + (ββπ·)) β€ (PellFundβπ·)) |
