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 ⋅ ℂ fld 1 = x ⋅ 1
4 1 2 3 sylancl ⊢ R ∈ SubRing ⁡ ℂ fld ∧ x ∈ ℤ → x ⋅ ℂ fld 1 = x ⋅ 1
5 zcn ⊢ x ∈ ℤ → x ∈ ℂ
6 5 adantl ⊢ R ∈ SubRing ⁡ ℂ fld ∧ x ∈ ℤ → x ∈ ℂ
7 6 mulid1d ⊢ R ∈ SubRing ⁡ ℂ fld ∧ x ∈ ℤ → x ⋅ 1 = x
8 4 7 eqtrd ⊢ R ∈ SubRing ⁡ ℂ fld ∧ x ∈ ℤ → x ⋅ ℂ fld 1 = 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 ⋅ ℂ fld 1 ∈ R
16 10 1 13 15 syl3anc ⊢ R ∈ SubRing ⁡ ℂ fld ∧ x ∈ ℤ → x ⋅ ℂ fld 1 ∈ 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