Description: For any fraction, there is an integer that is greater than it. This is also known as the "archimedean property". (Contributed by Mario Carneiro, 10-May-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | archnq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpqn | |
|
2 | xp1st | |
|
3 | 1 2 | syl | |
4 | 1pi | |
|
5 | addclpi | |
|
6 | 3 4 5 | sylancl | |
7 | xp2nd | |
|
8 | 1 7 | syl | |
9 | mulclpi | |
|
10 | 6 8 9 | syl2anc | |
11 | eqid | |
|
12 | oveq2 | |
|
13 | 12 | eqeq1d | |
14 | 13 | rspcev | |
15 | 4 11 14 | mp2an | |
16 | ltexpi | |
|
17 | 15 16 | mpbiri | |
18 | 3 6 17 | syl2anc | |
19 | nlt1pi | |
|
20 | ltmpi | |
|
21 | 6 20 | syl | |
22 | mulidpi | |
|
23 | 6 22 | syl | |
24 | 23 | breq2d | |
25 | 21 24 | bitrd | |
26 | 19 25 | mtbii | |
27 | ltsopi | |
|
28 | ltrelpi | |
|
29 | 27 28 | sotri3 | |
30 | 10 18 26 29 | syl3anc | |
31 | pinq | |
|
32 | 6 31 | syl | |
33 | ordpinq | |
|
34 | 32 33 | mpdan | |
35 | ovex | |
|
36 | 1oex | |
|
37 | 35 36 | op2nd | |
38 | 37 | oveq2i | |
39 | mulidpi | |
|
40 | 3 39 | syl | |
41 | 38 40 | eqtrid | |
42 | 35 36 | op1st | |
43 | 42 | oveq1i | |
44 | 43 | a1i | |
45 | 41 44 | breq12d | |
46 | 34 45 | bitrd | |
47 | 30 46 | mpbird | |
48 | opeq1 | |
|
49 | 48 | breq2d | |
50 | 49 | rspcev | |
51 | 6 47 50 | syl2anc | |