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	mulid1d	⊢ ( ( 𝑅 ∈ ( 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 ) → ℤ ⊆ 𝑅 )