Theorem rearchi

Description: The field of the real numbers is Archimedean. See also arch . (Contributed by Thierry Arnoux, 9-Apr-2018)

	Ref	Expression
Assertion	rearchi	|- RRfld e. Archi

Proof

Step	Hyp	Ref	Expression
1		reofld	|- RRfld e. oField
2		rebase	|- RR = ( Base ` RRfld )
3		eqid	|- ( ZRHom ` RRfld ) = ( ZRHom ` RRfld )
4		relt	|- < = ( lt ` RRfld )
5	2 3 4	isarchiofld	|- ( RRfld e. oField -> ( RRfld e. Archi <-> A. x e. RR E. n e. NN x < ( ( ZRHom ` RRfld ) ` n ) ) )
6	1 5	ax-mp	|- ( RRfld e. Archi <-> A. x e. RR E. n e. NN x < ( ( ZRHom ` RRfld ) ` n ) )
7		arch	|- ( x e. RR -> E. n e. NN x < n )
8		nnz	|- ( n e. NN -> n e. ZZ )
9		refld	|- RRfld e. Field
10		isfld	|- ( RRfld e. Field <-> ( RRfld e. DivRing /\ RRfld e. CRing ) )
11	10	simplbi	|- ( RRfld e. Field -> RRfld e. DivRing )
12		drngring	|- ( RRfld e. DivRing -> RRfld e. Ring )
13	9 11 12	mp2b	|- RRfld e. Ring
14		eqid	|- ( .g ` RRfld ) = ( .g ` RRfld )
15		re1r	|- 1 = ( 1r ` RRfld )
16	3 14 15	zrhmulg	|- ( ( RRfld e. Ring /\ n e. ZZ ) -> ( ( ZRHom ` RRfld ) ` n ) = ( n ( .g ` RRfld ) 1 ) )
17	13 16	mpan	|- ( n e. ZZ -> ( ( ZRHom ` RRfld ) ` n ) = ( n ( .g ` RRfld ) 1 ) )
18		1re	|- 1 e. RR
19		remulg	|- ( ( n e. ZZ /\ 1 e. RR ) -> ( n ( .g ` RRfld ) 1 ) = ( n x. 1 ) )
20	18 19	mpan2	|- ( n e. ZZ -> ( n ( .g ` RRfld ) 1 ) = ( n x. 1 ) )
21		zcn	|- ( n e. ZZ -> n e. CC )
22	21	mulid1d	|- ( n e. ZZ -> ( n x. 1 ) = n )
23	17 20 22	3eqtrd	|- ( n e. ZZ -> ( ( ZRHom ` RRfld ) ` n ) = n )
24	23	breq2d	|- ( n e. ZZ -> ( x < ( ( ZRHom ` RRfld ) ` n ) <-> x < n ) )
25	8 24	syl	|- ( n e. NN -> ( x < ( ( ZRHom ` RRfld ) ` n ) <-> x < n ) )
26	25	rexbiia	|- ( E. n e. NN x < ( ( ZRHom ` RRfld ) ` n ) <-> E. n e. NN x < n )
27	7 26	sylibr	|- ( x e. RR -> E. n e. NN x < ( ( ZRHom ` RRfld ) ` n ) )
28	6 27	mprgbir	|- RRfld e. Archi