Metamath Proof Explorer


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 fld Archi

Proof

Step Hyp Ref Expression
1 reofld fld oField
2 rebase = Base fld
3 eqid ℤRHom fld = ℤRHom fld
4 relt < = < fld
5 2 3 4 isarchiofld fld oField fld Archi x n x < ℤRHom fld n
6 1 5 ax-mp fld Archi x n x < ℤRHom fld n
7 arch x n x < n
8 nnz n n
9 refld fld Field
10 isfld fld Field fld DivRing fld CRing
11 10 simplbi fld Field fld DivRing
12 drngring fld DivRing fld Ring
13 9 11 12 mp2b fld Ring
14 eqid fld = fld
15 re1r 1 = 1 fld
16 3 14 15 zrhmulg fld Ring n ℤRHom fld n = n fld 1
17 13 16 mpan n ℤRHom fld n = n fld 1
18 1re 1
19 remulg n 1 n fld 1 = n 1
20 18 19 mpan2 n n fld 1 = n 1
21 zcn n n
22 21 mulid1d n n 1 = n
23 17 20 22 3eqtrd n ℤRHom fld n = n
24 23 breq2d n x < ℤRHom fld n x < n
25 8 24 syl n x < ℤRHom fld n x < n
26 25 rexbiia n x < ℤRHom fld n n x < n
27 7 26 sylibr x n x < ℤRHom fld n
28 6 27 mprgbir fld Archi