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 syl5bir
 |-  ( 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 )