Metamath Proof Explorer

Theorem nn0archi

Description: The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018)

Ref Expression
Assertion nn0archi 
|- ( CCfld |`s NN0 ) e. Archi

Proof

Step Hyp Ref Expression
1 df-refld 
 |-  RRfld = ( CCfld |`s RR )
2 1 oveq1i 
 |-  ( RRfld |`s NN0 ) = ( ( CCfld |`s RR ) |`s NN0 )
3 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
4 3 simpli 
 |-  RR e. ( SubRing ` CCfld )
5 nn0ssre 
 |-  NN0 C_ RR
6 ressabs 
 |-  ( ( RR e. ( SubRing ` CCfld ) /\ NN0 C_ RR ) -> ( ( CCfld |`s RR ) |`s NN0 ) = ( CCfld |`s NN0 ) )
7 4 5 6 mp2an 
 |-  ( ( CCfld |`s RR ) |`s NN0 ) = ( CCfld |`s NN0 )
8 2 7 eqtri 
 |-  ( RRfld |`s NN0 ) = ( CCfld |`s NN0 )
9 retos 
 |-  RRfld e. Toset
10 rearchi 
 |-  RRfld e. Archi
11 9 10 pm3.2i 
 |-  ( RRfld e. Toset /\ RRfld e. Archi )
12 nn0subm 
 |-  NN0 e. ( SubMnd ` CCfld )
13 subrgsubg 
 |-  ( RR e. ( SubRing ` CCfld ) -> RR e. ( SubGrp ` CCfld ) )
14 subgsubm 
 |-  ( RR e. ( SubGrp ` CCfld ) -> RR e. ( SubMnd ` CCfld ) )
15 4 13 14 mp2b 
 |-  RR e. ( SubMnd ` CCfld )
16 1 subsubm 
 |-  ( RR e. ( SubMnd ` CCfld ) -> ( NN0 e. ( SubMnd ` RRfld ) <-> ( NN0 e. ( SubMnd ` CCfld ) /\ NN0 C_ RR ) ) )
17 15 16 ax-mp 
 |-  ( NN0 e. ( SubMnd ` RRfld ) <-> ( NN0 e. ( SubMnd ` CCfld ) /\ NN0 C_ RR ) )
18 12 5 17 mpbir2an 
 |-  NN0 e. ( SubMnd ` RRfld )
19 submarchi 
 |-  ( ( ( RRfld e. Toset /\ RRfld e. Archi ) /\ NN0 e. ( SubMnd ` RRfld ) ) -> ( RRfld |`s NN0 ) e. Archi )
20 11 18 19 mp2an 
 |-  ( RRfld |`s NN0 ) e. Archi
21 8 20 eqeltrri 
 |-  ( CCfld |`s NN0 ) e. Archi