Description: Dirichlet's approximation theorem. Every positive irrational number has infinitely many rational approximations which are closer than the inverse squares of their reduced denominators. Lemma 61 in vandenDries p. 42. (Contributed by Stefan O'Rear, 14-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | irrapx1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | qnnen | |
|
2 | nnenom | |
|
3 | 1 2 | entri | |
4 | 3 2 | pm3.2i | |
5 | ssrab2 | |
|
6 | qssre | |
|
7 | 5 6 | sstri | |
8 | 7 | a1i | |
9 | eldifi | |
|
10 | 9 | rpred | |
11 | eldifn | |
|
12 | elrabi | |
|
13 | 11 12 | nsyl | |
14 | irrapxlem6 | |
|
15 | 9 14 | sylan | |
16 | 15 | ralrimiva | |
17 | rencldnfi | |
|
18 | 8 10 13 16 17 | syl31anc | |
19 | 18 5 | jctil | |
20 | ctbnfien | |
|
21 | 4 19 20 | sylancr | |