Metamath Proof Explorer


Theorem irrapx1

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 A+y|0<yyA<denomy2

Proof

Step Hyp Ref Expression
1 qnnen
2 nnenom ω
3 1 2 entri ω
4 3 2 pm3.2i ωω
5 ssrab2 y|0<yyA<denomy2
6 qssre
7 5 6 sstri y|0<yyA<denomy2
8 7 a1i A+y|0<yyA<denomy2
9 eldifi A+A+
10 9 rpred A+A
11 eldifn A+¬A
12 elrabi Ay|0<yyA<denomy2A
13 11 12 nsyl A+¬Ay|0<yyA<denomy2
14 irrapxlem6 A+a+by|0<yyA<denomy2bA<a
15 9 14 sylan A+a+by|0<yyA<denomy2bA<a
16 15 ralrimiva A+a+by|0<yyA<denomy2bA<a
17 rencldnfi y|0<yyA<denomy2A¬Ay|0<yyA<denomy2a+by|0<yyA<denomy2bA<a¬y|0<yyA<denomy2Fin
18 8 10 13 16 17 syl31anc A+¬y|0<yyA<denomy2Fin
19 18 5 jctil A+y|0<yyA<denomy2¬y|0<yyA<denomy2Fin
20 ctbnfien ωωy|0<yyA<denomy2¬y|0<yyA<denomy2Finy|0<yyA<denomy2
21 4 19 20 sylancr A+y|0<yyA<denomy2