Metamath Proof Explorer

Theorem zsssubrg

Description: The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion zsssubrg 
|- ( R e. ( SubRing ` CCfld ) -> ZZ C_ R )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ x e. ZZ ) -> x e. ZZ )
2 ax-1cn 
 |-  1 e. CC
3 cnfldmulg 
 |-  ( ( x e. ZZ /\ 1 e. CC ) -> ( x ( .g ` CCfld ) 1 ) = ( x x. 1 ) )
4 1 2 3 sylancl 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ x e. ZZ ) -> ( x ( .g ` CCfld ) 1 ) = ( x x. 1 ) )
5 zcn 
 |-  ( x e. ZZ -> x e. CC )
6 5 adantl 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ x e. ZZ ) -> x e. CC )
7 6 mulid1d 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ x e. ZZ ) -> ( x x. 1 ) = x )
8 4 7 eqtrd 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ x e. ZZ ) -> ( x ( .g ` CCfld ) 1 ) = x )
9 subrgsubg 
 |-  ( R e. ( SubRing ` CCfld ) -> R e. ( SubGrp ` CCfld ) )
10 9 adantr 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ x e. ZZ ) -> R e. ( SubGrp ` CCfld ) )
11 cnfld1 
 |-  1 = ( 1r ` CCfld )
12 11 subrg1cl 
 |-  ( R e. ( SubRing ` CCfld ) -> 1 e. R )
13 12 adantr 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ x e. ZZ ) -> 1 e. R )
14 eqid 
 |-  ( .g ` CCfld ) = ( .g ` CCfld )
15 14 subgmulgcl 
 |-  ( ( R e. ( SubGrp ` CCfld ) /\ x e. ZZ /\ 1 e. R ) -> ( x ( .g ` CCfld ) 1 ) e. R )
16 10 1 13 15 syl3anc 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ x e. ZZ ) -> ( x ( .g ` CCfld ) 1 ) e. R )
17 8 16 eqeltrrd 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ x e. ZZ ) -> x e. R )
18 17 ex 
 |-  ( R e. ( SubRing ` CCfld ) -> ( x e. ZZ -> x e. R ) )
19 18 ssrdv 
 |-  ( R e. ( SubRing ` CCfld ) -> ZZ C_ R )