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∈SubRing⁡ℂfld→ℤ⊆R

Proof

Step Hyp Ref Expression
1 simpr ⊢R∈SubRing⁡ℂfld∧x∈ℤ→x∈ℤ
2 ax-1cn ⊢1∈ℂ
3 cnfldmulg ⊢x∈ℤ∧1∈ℂ→x⋅ℂfld1=x⋅1
4 1 2 3 sylancl ⊢R∈SubRing⁡ℂfld∧x∈ℤ→x⋅ℂfld1=x⋅1
5 zcn ⊢x∈ℤ→x∈ℂ
6 5 adantl ⊢R∈SubRing⁡ℂfld∧x∈ℤ→x∈ℂ
7 6 mulridd ⊢R∈SubRing⁡ℂfld∧x∈ℤ→x⋅1=x
8 4 7 eqtrd ⊢R∈SubRing⁡ℂfld∧x∈ℤ→x⋅ℂfld1=x
9 subrgsubg ⊢R∈SubRing⁡ℂfld→R∈SubGrp⁡ℂfld
10 9 adantr ⊢R∈SubRing⁡ℂfld∧x∈ℤ→R∈SubGrp⁡ℂfld
11 cnfld1 ⊢1=1ℂfld
12 11 subrg1cl ⊢R∈SubRing⁡ℂfld→1∈R
13 12 adantr ⊢R∈SubRing⁡ℂfld∧x∈ℤ→1∈R
14 eqid ⊢⋅ℂfld=⋅ℂfld
15 14 subgmulgcl ⊢R∈SubGrp⁡ℂfld∧x∈ℤ∧1∈R→x⋅ℂfld1∈R
16 10 1 13 15 syl3anc ⊢R∈SubRing⁡ℂfld∧x∈ℤ→x⋅ℂfld1∈R
17 8 16 eqeltrrd ⊢R∈SubRing⁡ℂfld∧x∈ℤ→x∈R
18 17 ex ⊢R∈SubRing⁡ℂfld→x∈ℤ→x∈R
19 18 ssrdv ⊢R∈SubRing⁡ℂfld→ℤ⊆R