This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. Q. -> E. x e. N. A . )

Proof

Step Hyp Ref Expression
1 elpqn 
 |-  ( A e. Q. -> A e. ( N. X. N. ) )
2 xp1st 
 |-  ( A e. ( N. X. N. ) -> ( 1st ` A ) e. N. )
3 1 2 syl 
 |-  ( A e. Q. -> ( 1st ` A ) e. N. )
4 1pi 
 |-  1o e. N.
5 addclpi 
 |-  ( ( ( 1st ` A ) e. N. /\ 1o e. N. ) -> ( ( 1st ` A ) +N 1o ) e. N. )
6 3 4 5 sylancl 
 |-  ( A e. Q. -> ( ( 1st ` A ) +N 1o ) e. N. )
7 xp2nd 
 |-  ( A e. ( N. X. N. ) -> ( 2nd ` A ) e. N. )
8 1 7 syl 
 |-  ( A e. Q. -> ( 2nd ` A ) e. N. )
9 mulclpi 
 |-  ( ( ( ( 1st ` A ) +N 1o ) e. N. /\ ( 2nd ` A ) e. N. ) -> ( ( ( 1st ` A ) +N 1o ) .N ( 2nd ` A ) ) e. N. )
10 6 8 9 syl2anc 
 |-  ( A e. Q. -> ( ( ( 1st ` A ) +N 1o ) .N ( 2nd ` A ) ) e. N. )
11 eqid 
 |-  ( ( 1st ` A ) +N 1o ) = ( ( 1st ` A ) +N 1o )
12 oveq2 
 |-  ( x = 1o -> ( ( 1st ` A ) +N x ) = ( ( 1st ` A ) +N 1o ) )
13 12 eqeq1d 
 |-  ( x = 1o -> ( ( ( 1st ` A ) +N x ) = ( ( 1st ` A ) +N 1o ) <-> ( ( 1st ` A ) +N 1o ) = ( ( 1st ` A ) +N 1o ) ) )
14 13 rspcev 
 |-  ( ( 1o e. N. /\ ( ( 1st ` A ) +N 1o ) = ( ( 1st ` A ) +N 1o ) ) -> E. x e. N. ( ( 1st ` A ) +N x ) = ( ( 1st ` A ) +N 1o ) )
15 4 11 14 mp2an 
 |-  E. x e. N. ( ( 1st ` A ) +N x ) = ( ( 1st ` A ) +N 1o )
16 ltexpi 
 |-  ( ( ( 1st ` A ) e. N. /\ ( ( 1st ` A ) +N 1o ) e. N. ) -> ( ( 1st ` A )  E. x e. N. ( ( 1st ` A ) +N x ) = ( ( 1st ` A ) +N 1o ) ) )
17 15 16 mpbiri 
 |-  ( ( ( 1st ` A ) e. N. /\ ( ( 1st ` A ) +N 1o ) e. N. ) -> ( 1st ` A )
18 3 6 17 syl2anc 
 |-  ( A e. Q. -> ( 1st ` A )
19 nlt1pi 
 |-  -. ( 2nd ` A )
20 ltmpi 
 |-  ( ( ( 1st ` A ) +N 1o ) e. N. -> ( ( 2nd ` A )  ( ( ( 1st ` A ) +N 1o ) .N ( 2nd ` A ) )
21 6 20 syl 
 |-  ( A e. Q. -> ( ( 2nd ` A )  ( ( ( 1st ` A ) +N 1o ) .N ( 2nd ` A ) )
22 mulidpi 
 |-  ( ( ( 1st ` A ) +N 1o ) e. N. -> ( ( ( 1st ` A ) +N 1o ) .N 1o ) = ( ( 1st ` A ) +N 1o ) )
23 6 22 syl 
 |-  ( A e. Q. -> ( ( ( 1st ` A ) +N 1o ) .N 1o ) = ( ( 1st ` A ) +N 1o ) )
24 23 breq2d 
 |-  ( A e. Q. -> ( ( ( ( 1st ` A ) +N 1o ) .N ( 2nd ` A ) )  ( ( ( 1st ` A ) +N 1o ) .N ( 2nd ` A ) )
25 21 24 bitrd 
 |-  ( A e. Q. -> ( ( 2nd ` A )  ( ( ( 1st ` A ) +N 1o ) .N ( 2nd ` A ) )
26 19 25 mtbii 
 |-  ( A e. Q. -> -. ( ( ( 1st ` A ) +N 1o ) .N ( 2nd ` A ) )
27 ltsopi 
 |-
28 ltrelpi 
 |-
29 27 28 sotri3 
 |-  ( ( ( ( ( 1st ` A ) +N 1o ) .N ( 2nd ` A ) ) e. N. /\ ( 1st ` A )  ( 1st ` A )
30 10 18 26 29 syl3anc 
 |-  ( A e. Q. -> ( 1st ` A )
31 pinq 
 |-  ( ( ( 1st ` A ) +N 1o ) e. N. -> <. ( ( 1st ` A ) +N 1o ) , 1o >. e. Q. )
32 6 31 syl 
 |-  ( A e. Q. -> <. ( ( 1st ` A ) +N 1o ) , 1o >. e. Q. )
33 ordpinq 
 |-  ( ( A e. Q. /\ <. ( ( 1st ` A ) +N 1o ) , 1o >. e. Q. ) -> ( A . <-> ( ( 1st ` A ) .N ( 2nd ` <. ( ( 1st ` A ) +N 1o ) , 1o >. ) ) . ) .N ( 2nd ` A ) ) ) )
34 32 33 mpdan 
 |-  ( A e. Q. -> ( A . <-> ( ( 1st ` A ) .N ( 2nd ` <. ( ( 1st ` A ) +N 1o ) , 1o >. ) ) . ) .N ( 2nd ` A ) ) ) )
35 ovex 
 |-  ( ( 1st ` A ) +N 1o ) e. _V
36 1oex 
 |-  1o e. _V
37 35 36 op2nd 
 |-  ( 2nd ` <. ( ( 1st ` A ) +N 1o ) , 1o >. ) = 1o
38 37 oveq2i 
 |-  ( ( 1st ` A ) .N ( 2nd ` <. ( ( 1st ` A ) +N 1o ) , 1o >. ) ) = ( ( 1st ` A ) .N 1o )
39 mulidpi 
 |-  ( ( 1st ` A ) e. N. -> ( ( 1st ` A ) .N 1o ) = ( 1st ` A ) )
40 3 39 syl 
 |-  ( A e. Q. -> ( ( 1st ` A ) .N 1o ) = ( 1st ` A ) )
41 38 40 eqtrid 
 |-  ( A e. Q. -> ( ( 1st ` A ) .N ( 2nd ` <. ( ( 1st ` A ) +N 1o ) , 1o >. ) ) = ( 1st ` A ) )
42 35 36 op1st 
 |-  ( 1st ` <. ( ( 1st ` A ) +N 1o ) , 1o >. ) = ( ( 1st ` A ) +N 1o )
43 42 oveq1i 
 |-  ( ( 1st ` <. ( ( 1st ` A ) +N 1o ) , 1o >. ) .N ( 2nd ` A ) ) = ( ( ( 1st ` A ) +N 1o ) .N ( 2nd ` A ) )
44 43 a1i 
 |-  ( A e. Q. -> ( ( 1st ` <. ( ( 1st ` A ) +N 1o ) , 1o >. ) .N ( 2nd ` A ) ) = ( ( ( 1st ` A ) +N 1o ) .N ( 2nd ` A ) ) )
45 41 44 breq12d 
 |-  ( A e. Q. -> ( ( ( 1st ` A ) .N ( 2nd ` <. ( ( 1st ` A ) +N 1o ) , 1o >. ) ) . ) .N ( 2nd ` A ) ) <-> ( 1st ` A )
46 34 45 bitrd 
 |-  ( A e. Q. -> ( A . <-> ( 1st ` A )
47 30 46 mpbird 
 |-  ( A e. Q. -> A . )
48 opeq1 
 |-  ( x = ( ( 1st ` A ) +N 1o ) -> <. x , 1o >. = <. ( ( 1st ` A ) +N 1o ) , 1o >. )
49 48 breq2d 
 |-  ( x = ( ( 1st ` A ) +N 1o ) -> ( A . <-> A . ) )
50 49 rspcev 
 |-  ( ( ( ( 1st ` A ) +N 1o ) e. N. /\ A . ) -> E. x e. N. A . )
51 6 47 50 syl2anc 
 |-  ( A e. Q. -> E. x e. N. A . )