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 )