Metamath Proof Explorer


Theorem archnq

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 A𝑸x𝑵A<𝑸x1𝑜

Proof

Step Hyp Ref Expression
1 elpqn A𝑸A𝑵×𝑵
2 xp1st A𝑵×𝑵1stA𝑵
3 1 2 syl A𝑸1stA𝑵
4 1pi 1𝑜𝑵
5 addclpi 1stA𝑵1𝑜𝑵1stA+𝑵1𝑜𝑵
6 3 4 5 sylancl A𝑸1stA+𝑵1𝑜𝑵
7 xp2nd A𝑵×𝑵2ndA𝑵
8 1 7 syl A𝑸2ndA𝑵
9 mulclpi 1stA+𝑵1𝑜𝑵2ndA𝑵1stA+𝑵1𝑜𝑵2ndA𝑵
10 6 8 9 syl2anc A𝑸1stA+𝑵1𝑜𝑵2ndA𝑵
11 eqid 1stA+𝑵1𝑜=1stA+𝑵1𝑜
12 oveq2 x=1𝑜1stA+𝑵x=1stA+𝑵1𝑜
13 12 eqeq1d x=1𝑜1stA+𝑵x=1stA+𝑵1𝑜1stA+𝑵1𝑜=1stA+𝑵1𝑜
14 13 rspcev 1𝑜𝑵1stA+𝑵1𝑜=1stA+𝑵1𝑜x𝑵1stA+𝑵x=1stA+𝑵1𝑜
15 4 11 14 mp2an x𝑵1stA+𝑵x=1stA+𝑵1𝑜
16 ltexpi 1stA𝑵1stA+𝑵1𝑜𝑵1stA<𝑵1stA+𝑵1𝑜x𝑵1stA+𝑵x=1stA+𝑵1𝑜
17 15 16 mpbiri 1stA𝑵1stA+𝑵1𝑜𝑵1stA<𝑵1stA+𝑵1𝑜
18 3 6 17 syl2anc A𝑸1stA<𝑵1stA+𝑵1𝑜
19 nlt1pi ¬2ndA<𝑵1𝑜
20 ltmpi 1stA+𝑵1𝑜𝑵2ndA<𝑵1𝑜1stA+𝑵1𝑜𝑵2ndA<𝑵1stA+𝑵1𝑜𝑵1𝑜
21 6 20 syl A𝑸2ndA<𝑵1𝑜1stA+𝑵1𝑜𝑵2ndA<𝑵1stA+𝑵1𝑜𝑵1𝑜
22 mulidpi 1stA+𝑵1𝑜𝑵1stA+𝑵1𝑜𝑵1𝑜=1stA+𝑵1𝑜
23 6 22 syl A𝑸1stA+𝑵1𝑜𝑵1𝑜=1stA+𝑵1𝑜
24 23 breq2d A𝑸1stA+𝑵1𝑜𝑵2ndA<𝑵1stA+𝑵1𝑜𝑵1𝑜1stA+𝑵1𝑜𝑵2ndA<𝑵1stA+𝑵1𝑜
25 21 24 bitrd A𝑸2ndA<𝑵1𝑜1stA+𝑵1𝑜𝑵2ndA<𝑵1stA+𝑵1𝑜
26 19 25 mtbii A𝑸¬1stA+𝑵1𝑜𝑵2ndA<𝑵1stA+𝑵1𝑜
27 ltsopi <𝑵Or𝑵
28 ltrelpi <𝑵𝑵×𝑵
29 27 28 sotri3 1stA+𝑵1𝑜𝑵2ndA𝑵1stA<𝑵1stA+𝑵1𝑜¬1stA+𝑵1𝑜𝑵2ndA<𝑵1stA+𝑵1𝑜1stA<𝑵1stA+𝑵1𝑜𝑵2ndA
30 10 18 26 29 syl3anc A𝑸1stA<𝑵1stA+𝑵1𝑜𝑵2ndA
31 pinq 1stA+𝑵1𝑜𝑵1stA+𝑵1𝑜1𝑜𝑸
32 6 31 syl A𝑸1stA+𝑵1𝑜1𝑜𝑸
33 ordpinq A𝑸1stA+𝑵1𝑜1𝑜𝑸A<𝑸1stA+𝑵1𝑜1𝑜1stA𝑵2nd1stA+𝑵1𝑜1𝑜<𝑵1st1stA+𝑵1𝑜1𝑜𝑵2ndA
34 32 33 mpdan A𝑸A<𝑸1stA+𝑵1𝑜1𝑜1stA𝑵2nd1stA+𝑵1𝑜1𝑜<𝑵1st1stA+𝑵1𝑜1𝑜𝑵2ndA
35 ovex 1stA+𝑵1𝑜V
36 1oex 1𝑜V
37 35 36 op2nd 2nd1stA+𝑵1𝑜1𝑜=1𝑜
38 37 oveq2i 1stA𝑵2nd1stA+𝑵1𝑜1𝑜=1stA𝑵1𝑜
39 mulidpi 1stA𝑵1stA𝑵1𝑜=1stA
40 3 39 syl A𝑸1stA𝑵1𝑜=1stA
41 38 40 eqtrid A𝑸1stA𝑵2nd1stA+𝑵1𝑜1𝑜=1stA
42 35 36 op1st 1st1stA+𝑵1𝑜1𝑜=1stA+𝑵1𝑜
43 42 oveq1i 1st1stA+𝑵1𝑜1𝑜𝑵2ndA=1stA+𝑵1𝑜𝑵2ndA
44 43 a1i A𝑸1st1stA+𝑵1𝑜1𝑜𝑵2ndA=1stA+𝑵1𝑜𝑵2ndA
45 41 44 breq12d A𝑸1stA𝑵2nd1stA+𝑵1𝑜1𝑜<𝑵1st1stA+𝑵1𝑜1𝑜𝑵2ndA1stA<𝑵1stA+𝑵1𝑜𝑵2ndA
46 34 45 bitrd A𝑸A<𝑸1stA+𝑵1𝑜1𝑜1stA<𝑵1stA+𝑵1𝑜𝑵2ndA
47 30 46 mpbird A𝑸A<𝑸1stA+𝑵1𝑜1𝑜
48 opeq1 x=1stA+𝑵1𝑜x1𝑜=1stA+𝑵1𝑜1𝑜
49 48 breq2d x=1stA+𝑵1𝑜A<𝑸x1𝑜A<𝑸1stA+𝑵1𝑜1𝑜
50 49 rspcev 1stA+𝑵1𝑜𝑵A<𝑸1stA+𝑵1𝑜1𝑜x𝑵A<𝑸x1𝑜
51 6 47 50 syl2anc A𝑸x𝑵A<𝑸x1𝑜