This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) → ℤ ⊆ 𝑅 )