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 ( ๐‘… โˆˆ ( SubRing โ€˜ โ„‚fld ) โ†’ โ„ค โŠ† ๐‘… )

Proof

Step Hyp Ref Expression
1 simpr โŠข ( ( ๐‘… โˆˆ ( SubRing โ€˜ โ„‚fld ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ๐‘ฅ โˆˆ โ„ค )
2 ax-1cn โŠข 1 โˆˆ โ„‚
3 cnfldmulg โŠข ( ( ๐‘ฅ โˆˆ โ„ค โˆง 1 โˆˆ โ„‚ ) โ†’ ( ๐‘ฅ ( .g โ€˜ โ„‚fld ) 1 ) = ( ๐‘ฅ ยท 1 ) )
4 1 2 3 sylancl โŠข ( ( ๐‘… โˆˆ ( SubRing โ€˜ โ„‚fld ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ๐‘ฅ ( .g โ€˜ โ„‚fld ) 1 ) = ( ๐‘ฅ ยท 1 ) )
5 zcn โŠข ( ๐‘ฅ โˆˆ โ„ค โ†’ ๐‘ฅ โˆˆ โ„‚ )
6 5 adantl โŠข ( ( ๐‘… โˆˆ ( SubRing โ€˜ โ„‚fld ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
7 6 mulridd โŠข ( ( ๐‘… โˆˆ ( SubRing โ€˜ โ„‚fld ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ๐‘ฅ ยท 1 ) = ๐‘ฅ )
8 4 7 eqtrd โŠข ( ( ๐‘… โˆˆ ( SubRing โ€˜ โ„‚fld ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ๐‘ฅ ( .g โ€˜ โ„‚fld ) 1 ) = ๐‘ฅ )
9 subrgsubg โŠข ( ๐‘… โˆˆ ( SubRing โ€˜ โ„‚fld ) โ†’ ๐‘… โˆˆ ( SubGrp โ€˜ โ„‚fld ) )
10 9 adantr โŠข ( ( ๐‘… โˆˆ ( SubRing โ€˜ โ„‚fld ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ๐‘… โˆˆ ( SubGrp โ€˜ โ„‚fld ) )
11 cnfld1 โŠข 1 = ( 1r โ€˜ โ„‚fld )
12 11 subrg1cl โŠข ( ๐‘… โˆˆ ( SubRing โ€˜ โ„‚fld ) โ†’ 1 โˆˆ ๐‘… )
13 12 adantr โŠข ( ( ๐‘… โˆˆ ( SubRing โ€˜ โ„‚fld ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ 1 โˆˆ ๐‘… )
14 eqid โŠข ( .g โ€˜ โ„‚fld ) = ( .g โ€˜ โ„‚fld )
15 14 subgmulgcl โŠข ( ( ๐‘… โˆˆ ( SubGrp โ€˜ โ„‚fld ) โˆง ๐‘ฅ โˆˆ โ„ค โˆง 1 โˆˆ ๐‘… ) โ†’ ( ๐‘ฅ ( .g โ€˜ โ„‚fld ) 1 ) โˆˆ ๐‘… )
16 10 1 13 15 syl3anc โŠข ( ( ๐‘… โˆˆ ( SubRing โ€˜ โ„‚fld ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ๐‘ฅ ( .g โ€˜ โ„‚fld ) 1 ) โˆˆ ๐‘… )
17 8 16 eqeltrrd โŠข ( ( ๐‘… โˆˆ ( SubRing โ€˜ โ„‚fld ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ๐‘ฅ โˆˆ ๐‘… )
18 17 ex โŠข ( ๐‘… โˆˆ ( SubRing โ€˜ โ„‚fld ) โ†’ ( ๐‘ฅ โˆˆ โ„ค โ†’ ๐‘ฅ โˆˆ ๐‘… ) )
19 18 ssrdv โŠข ( ๐‘… โˆˆ ( SubRing โ€˜ โ„‚fld ) โ†’ โ„ค โŠ† ๐‘… )