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

Metamath Proof Explorer

Theorem arch

Description: Archimedean property of real numbers. For any real number, there is an integer greater than it. Theorem I.29 of Apostol p. 26. (Contributed by NM, 21-Jan-1997)

Ref Expression
Assertion arch 
|- ( A e. RR -> E. n e. NN A < n )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( y = A -> ( y < n <-> A < n ) )
2 1 rexbidv 
 |-  ( y = A -> ( E. n e. NN y < n <-> E. n e. NN A < n ) )
3 nnunb 
 |-  -. E. y e. RR A. n e. NN ( n < y \/ n = y )
4 ralnex 
 |-  ( A. y e. RR -. A. n e. NN ( n < y \/ n = y ) <-> -. E. y e. RR A. n e. NN ( n < y \/ n = y ) )
5 3 4 mpbir 
 |-  A. y e. RR -. A. n e. NN ( n < y \/ n = y )
6 rexnal 
 |-  ( E. n e. NN -. ( n < y \/ n = y ) <-> -. A. n e. NN ( n < y \/ n = y ) )
7 nnre 
 |-  ( n e. NN -> n e. RR )
8 axlttri 
 |-  ( ( y e. RR /\ n e. RR ) -> ( y < n <-> -. ( y = n \/ n < y ) ) )
9 7 8 sylan2 
 |-  ( ( y e. RR /\ n e. NN ) -> ( y < n <-> -. ( y = n \/ n < y ) ) )
10 equcom 
 |-  ( y = n <-> n = y )
11 10 orbi1i 
 |-  ( ( y = n \/ n < y ) <-> ( n = y \/ n < y ) )
12 orcom 
 |-  ( ( n = y \/ n < y ) <-> ( n < y \/ n = y ) )
13 11 12 bitri 
 |-  ( ( y = n \/ n < y ) <-> ( n < y \/ n = y ) )
14 13 notbii 
 |-  ( -. ( y = n \/ n < y ) <-> -. ( n < y \/ n = y ) )
15 9 14 bitrdi 
 |-  ( ( y e. RR /\ n e. NN ) -> ( y < n <-> -. ( n < y \/ n = y ) ) )
16 15 biimprd 
 |-  ( ( y e. RR /\ n e. NN ) -> ( -. ( n < y \/ n = y ) -> y < n ) )
17 16 reximdva 
 |-  ( y e. RR -> ( E. n e. NN -. ( n < y \/ n = y ) -> E. n e. NN y < n ) )
18 6 17 biimtrrid 
 |-  ( y e. RR -> ( -. A. n e. NN ( n < y \/ n = y ) -> E. n e. NN y < n ) )
19 18 ralimia 
 |-  ( A. y e. RR -. A. n e. NN ( n < y \/ n = y ) -> A. y e. RR E. n e. NN y < n )
20 5 19 ax-mp 
 |-  A. y e. RR E. n e. NN y < n
21 2 20 vtoclri 
 |-  ( A e. RR -> E. n e. NN A < n )