Step | Hyp | Ref
| Expression |
1 | | pellfundval 41921 |
. . . . . . 7
β’ (π· β (β β
β»NN) β (PellFundβπ·) = inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < )) |
2 | 1 | 3ad2ant1 1132 |
. . . . . 6
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β (PellFundβπ·) = inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < )) |
3 | | simp3 1137 |
. . . . . 6
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β (PellFundβπ·) < π΄) |
4 | 2, 3 | eqbrtrrd 5173 |
. . . . 5
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < ) < π΄) |
5 | | pellfundre 41922 |
. . . . . . . 8
β’ (π· β (β β
β»NN) β (PellFundβπ·) β β) |
6 | 5 | 3ad2ant1 1132 |
. . . . . . 7
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β (PellFundβπ·) β β) |
7 | 2, 6 | eqeltrrd 2833 |
. . . . . 6
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < ) β
β) |
8 | | simp2 1136 |
. . . . . 6
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β π΄ β β) |
9 | 7, 8 | ltnled 11366 |
. . . . 5
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β (inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < ) < π΄ β Β¬ π΄ β€ inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < ))) |
10 | 4, 9 | mpbid 231 |
. . . 4
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β Β¬ π΄ β€ inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < )) |
11 | | ssrab2 4078 |
. . . . . 6
β’ {π β (Pell14QRβπ·) β£ 1 < π} β (Pell14QRβπ·) |
12 | | pell14qrre 41898 |
. . . . . . . . 9
β’ ((π· β (β β
β»NN) β§ π β (Pell14QRβπ·)) β π β β) |
13 | 12 | ex 412 |
. . . . . . . 8
β’ (π· β (β β
β»NN) β (π β (Pell14QRβπ·) β π β β)) |
14 | 13 | ssrdv 3989 |
. . . . . . 7
β’ (π· β (β β
β»NN) β (Pell14QRβπ·) β β) |
15 | 14 | 3ad2ant1 1132 |
. . . . . 6
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β (Pell14QRβπ·) β β) |
16 | 11, 15 | sstrid 3994 |
. . . . 5
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β {π β (Pell14QRβπ·) β£ 1 < π} β β) |
17 | | pell1qrss14 41909 |
. . . . . . . 8
β’ (π· β (β β
β»NN) β (Pell1QRβπ·) β (Pell14QRβπ·)) |
18 | 17 | 3ad2ant1 1132 |
. . . . . . 7
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β (Pell1QRβπ·) β (Pell14QRβπ·)) |
19 | | pellqrex 41920 |
. . . . . . . 8
β’ (π· β (β β
β»NN) β βπ β (Pell1QRβπ·)1 < π) |
20 | 19 | 3ad2ant1 1132 |
. . . . . . 7
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β βπ β (Pell1QRβπ·)1 < π) |
21 | | ssrexv 4052 |
. . . . . . 7
β’
((Pell1QRβπ·)
β (Pell14QRβπ·)
β (βπ β
(Pell1QRβπ·)1 <
π β βπ β (Pell14QRβπ·)1 < π)) |
22 | 18, 20, 21 | sylc 65 |
. . . . . 6
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β βπ β (Pell14QRβπ·)1 < π) |
23 | | rabn0 4386 |
. . . . . 6
β’ ({π β (Pell14QRβπ·) β£ 1 < π} β β
β
βπ β
(Pell14QRβπ·)1 <
π) |
24 | 22, 23 | sylibr 233 |
. . . . 5
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β {π β (Pell14QRβπ·) β£ 1 < π} β β
) |
25 | | infmrgelbi 41919 |
. . . . . 6
β’ ((({π β (Pell14QRβπ·) β£ 1 < π} β β β§ {π β (Pell14QRβπ·) β£ 1 < π} β β
β§ π΄ β β) β§
βπ₯ β {π β (Pell14QRβπ·) β£ 1 < π}π΄ β€ π₯) β π΄ β€ inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < )) |
26 | 25 | ex 412 |
. . . . 5
β’ (({π β (Pell14QRβπ·) β£ 1 < π} β β β§ {π β (Pell14QRβπ·) β£ 1 < π} β β
β§ π΄ β β) β
(βπ₯ β {π β (Pell14QRβπ·) β£ 1 < π}π΄ β€ π₯ β π΄ β€ inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < ))) |
27 | 16, 24, 8, 26 | syl3anc 1370 |
. . . 4
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β (βπ₯ β {π β (Pell14QRβπ·) β£ 1 < π}π΄ β€ π₯ β π΄ β€ inf({π β (Pell14QRβπ·) β£ 1 < π}, β, < ))) |
28 | 10, 27 | mtod 197 |
. . 3
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β Β¬ βπ₯ β {π β (Pell14QRβπ·) β£ 1 < π}π΄ β€ π₯) |
29 | | rexnal 3099 |
. . 3
β’
(βπ₯ β
{π β
(Pell14QRβπ·) β£
1 < π} Β¬ π΄ β€ π₯ β Β¬ βπ₯ β {π β (Pell14QRβπ·) β£ 1 < π}π΄ β€ π₯) |
30 | 28, 29 | sylibr 233 |
. 2
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β βπ₯ β {π β (Pell14QRβπ·) β£ 1 < π} Β¬ π΄ β€ π₯) |
31 | | breq2 5153 |
. . . . 5
β’ (π = π₯ β (1 < π β 1 < π₯)) |
32 | 31 | elrab 3684 |
. . . 4
β’ (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β (π₯ β (Pell14QRβπ·) β§ 1 < π₯)) |
33 | | simprl 768 |
. . . . . 6
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β (Pell14QRβπ·) β§ 1 < π₯)) β π₯ β (Pell14QRβπ·)) |
34 | | 1red 11220 |
. . . . . . 7
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β (Pell14QRβπ·) β§ 1 < π₯)) β 1 β β) |
35 | | simpl1 1190 |
. . . . . . . 8
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β (Pell14QRβπ·) β§ 1 < π₯)) β π· β (β β
β»NN)) |
36 | | pell14qrre 41898 |
. . . . . . . 8
β’ ((π· β (β β
β»NN) β§ π₯ β (Pell14QRβπ·)) β π₯ β β) |
37 | 35, 33, 36 | syl2anc 583 |
. . . . . . 7
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β (Pell14QRβπ·) β§ 1 < π₯)) β π₯ β β) |
38 | | simprr 770 |
. . . . . . 7
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β (Pell14QRβπ·) β§ 1 < π₯)) β 1 < π₯) |
39 | 34, 37, 38 | ltled 11367 |
. . . . . 6
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β (Pell14QRβπ·) β§ 1 < π₯)) β 1 β€ π₯) |
40 | 33, 39 | jca 511 |
. . . . 5
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β (Pell14QRβπ·) β§ 1 < π₯)) β (π₯ β (Pell14QRβπ·) β§ 1 β€ π₯)) |
41 | | elpell1qr2 41913 |
. . . . . 6
β’ (π· β (β β
β»NN) β (π₯ β (Pell1QRβπ·) β (π₯ β (Pell14QRβπ·) β§ 1 β€ π₯))) |
42 | 35, 41 | syl 17 |
. . . . 5
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β (Pell14QRβπ·) β§ 1 < π₯)) β (π₯ β (Pell1QRβπ·) β (π₯ β (Pell14QRβπ·) β§ 1 β€ π₯))) |
43 | 40, 42 | mpbird 256 |
. . . 4
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β (Pell14QRβπ·) β§ 1 < π₯)) β π₯ β (Pell1QRβπ·)) |
44 | 32, 43 | sylan2b 593 |
. . 3
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ π₯ β {π β (Pell14QRβπ·) β£ 1 < π}) β π₯ β (Pell1QRβπ·)) |
45 | 44 | adantrr 714 |
. 2
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β§ Β¬ π΄ β€ π₯)) β π₯ β (Pell1QRβπ·)) |
46 | | simpl1 1190 |
. . . 4
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β§ Β¬ π΄ β€ π₯)) β π· β (β β
β»NN)) |
47 | | simprl 768 |
. . . . 5
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β§ Β¬ π΄ β€ π₯)) β π₯ β {π β (Pell14QRβπ·) β£ 1 < π}) |
48 | 11, 47 | sselid 3981 |
. . . 4
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β§ Β¬ π΄ β€ π₯)) β π₯ β (Pell14QRβπ·)) |
49 | | simpr 484 |
. . . . . . . 8
β’ ((π₯ β (Pell14QRβπ·) β§ 1 < π₯) β 1 < π₯) |
50 | 49 | a1i 11 |
. . . . . . 7
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β ((π₯ β (Pell14QRβπ·) β§ 1 < π₯) β 1 < π₯)) |
51 | 32, 50 | biimtrid 241 |
. . . . . 6
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β 1 < π₯)) |
52 | 51 | imp 406 |
. . . . 5
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ π₯ β {π β (Pell14QRβπ·) β£ 1 < π}) β 1 < π₯) |
53 | 52 | adantrr 714 |
. . . 4
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β§ Β¬ π΄ β€ π₯)) β 1 < π₯) |
54 | | pellfundlb 41925 |
. . . 4
β’ ((π· β (β β
β»NN) β§ π₯ β (Pell14QRβπ·) β§ 1 < π₯) β (PellFundβπ·) β€ π₯) |
55 | 46, 48, 53, 54 | syl3anc 1370 |
. . 3
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β§ Β¬ π΄ β€ π₯)) β (PellFundβπ·) β€ π₯) |
56 | | simprr 770 |
. . . 4
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β§ Β¬ π΄ β€ π₯)) β Β¬ π΄ β€ π₯) |
57 | 15 | adantr 480 |
. . . . . 6
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β§ Β¬ π΄ β€ π₯)) β (Pell14QRβπ·) β β) |
58 | 57, 48 | sseldd 3984 |
. . . . 5
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β§ Β¬ π΄ β€ π₯)) β π₯ β β) |
59 | | simpl2 1191 |
. . . . 5
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β§ Β¬ π΄ β€ π₯)) β π΄ β β) |
60 | 58, 59 | ltnled 11366 |
. . . 4
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β§ Β¬ π΄ β€ π₯)) β (π₯ < π΄ β Β¬ π΄ β€ π₯)) |
61 | 56, 60 | mpbird 256 |
. . 3
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β§ Β¬ π΄ β€ π₯)) β π₯ < π΄) |
62 | 55, 61 | jca 511 |
. 2
β’ (((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β§ (π₯ β {π β (Pell14QRβπ·) β£ 1 < π} β§ Β¬ π΄ β€ π₯)) β ((PellFundβπ·) β€ π₯ β§ π₯ < π΄)) |
63 | 30, 45, 62 | reximssdv 3171 |
1
β’ ((π· β (β β
β»NN) β§ π΄ β β β§ (PellFundβπ·) < π΄) β βπ₯ β (Pell1QRβπ·)((PellFundβπ·) β€ π₯ β§ π₯ < π΄)) |