Theorem cnsrexpcl

Description: Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014)

	Ref	Expression
Hypotheses	cnsrexpcl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ ℂfld ) )
	cnsrexpcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	cnsrexpcl.y	⊢ ( 𝜑 → 𝑌 ∈ ℕ0 )
Assertion	cnsrexpcl	⊢ ( 𝜑 → ( 𝑋 ↑ 𝑌 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		cnsrexpcl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ ℂfld ) )
2		cnsrexpcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
3		cnsrexpcl.y	⊢ ( 𝜑 → 𝑌 ∈ ℕ0 )
4		oveq2	⊢ ( 𝑎 = 0 → ( 𝑋 ↑ 𝑎 ) = ( 𝑋 ↑ 0 ) )
5	4	eleq1d	⊢ ( 𝑎 = 0 → ( ( 𝑋 ↑ 𝑎 ) ∈ 𝑆 ↔ ( 𝑋 ↑ 0 ) ∈ 𝑆 ) )
6	5	imbi2d	⊢ ( 𝑎 = 0 → ( ( 𝜑 → ( 𝑋 ↑ 𝑎 ) ∈ 𝑆 ) ↔ ( 𝜑 → ( 𝑋 ↑ 0 ) ∈ 𝑆 ) ) )
7		oveq2	⊢ ( 𝑎 = 𝑏 → ( 𝑋 ↑ 𝑎 ) = ( 𝑋 ↑ 𝑏 ) )
8	7	eleq1d	⊢ ( 𝑎 = 𝑏 → ( ( 𝑋 ↑ 𝑎 ) ∈ 𝑆 ↔ ( 𝑋 ↑ 𝑏 ) ∈ 𝑆 ) )
9	8	imbi2d	⊢ ( 𝑎 = 𝑏 → ( ( 𝜑 → ( 𝑋 ↑ 𝑎 ) ∈ 𝑆 ) ↔ ( 𝜑 → ( 𝑋 ↑ 𝑏 ) ∈ 𝑆 ) ) )
10		oveq2	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝑋 ↑ 𝑎 ) = ( 𝑋 ↑ ( 𝑏 + 1 ) ) )
11	10	eleq1d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝑋 ↑ 𝑎 ) ∈ 𝑆 ↔ ( 𝑋 ↑ ( 𝑏 + 1 ) ) ∈ 𝑆 ) )
12	11	imbi2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝜑 → ( 𝑋 ↑ 𝑎 ) ∈ 𝑆 ) ↔ ( 𝜑 → ( 𝑋 ↑ ( 𝑏 + 1 ) ) ∈ 𝑆 ) ) )
13		oveq2	⊢ ( 𝑎 = 𝑌 → ( 𝑋 ↑ 𝑎 ) = ( 𝑋 ↑ 𝑌 ) )
14	13	eleq1d	⊢ ( 𝑎 = 𝑌 → ( ( 𝑋 ↑ 𝑎 ) ∈ 𝑆 ↔ ( 𝑋 ↑ 𝑌 ) ∈ 𝑆 ) )
15	14	imbi2d	⊢ ( 𝑎 = 𝑌 → ( ( 𝜑 → ( 𝑋 ↑ 𝑎 ) ∈ 𝑆 ) ↔ ( 𝜑 → ( 𝑋 ↑ 𝑌 ) ∈ 𝑆 ) ) )
16		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
17	16	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝑆 ⊆ ℂ )
18	1 17	syl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
19	18 2	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
20	19	exp0d	⊢ ( 𝜑 → ( 𝑋 ↑ 0 ) = 1 )
21		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
22	21	subrg1cl	⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 1 ∈ 𝑆 )
23	1 22	syl	⊢ ( 𝜑 → 1 ∈ 𝑆 )
24	20 23	eqeltrd	⊢ ( 𝜑 → ( 𝑋 ↑ 0 ) ∈ 𝑆 )
25	19	3ad2ant2	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑋 ↑ 𝑏 ) ∈ 𝑆 ) → 𝑋 ∈ ℂ )
26		simp1	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑋 ↑ 𝑏 ) ∈ 𝑆 ) → 𝑏 ∈ ℕ0 )
27	25 26	expp1d	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑋 ↑ 𝑏 ) ∈ 𝑆 ) → ( 𝑋 ↑ ( 𝑏 + 1 ) ) = ( ( 𝑋 ↑ 𝑏 ) · 𝑋 ) )
28	1	3ad2ant2	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑋 ↑ 𝑏 ) ∈ 𝑆 ) → 𝑆 ∈ ( SubRing ‘ ℂfld ) )
29		simp3	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑋 ↑ 𝑏 ) ∈ 𝑆 ) → ( 𝑋 ↑ 𝑏 ) ∈ 𝑆 )
30	2	3ad2ant2	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑋 ↑ 𝑏 ) ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
31		cnfldmul	⊢ · = ( .r ‘ ℂfld )
32	31	subrgmcl	⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑋 ↑ 𝑏 ) ∈ 𝑆 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝑋 ↑ 𝑏 ) · 𝑋 ) ∈ 𝑆 )
33	28 29 30 32	syl3anc	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑋 ↑ 𝑏 ) ∈ 𝑆 ) → ( ( 𝑋 ↑ 𝑏 ) · 𝑋 ) ∈ 𝑆 )
34	27 33	eqeltrd	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑋 ↑ 𝑏 ) ∈ 𝑆 ) → ( 𝑋 ↑ ( 𝑏 + 1 ) ) ∈ 𝑆 )
35	34	3exp	⊢ ( 𝑏 ∈ ℕ0 → ( 𝜑 → ( ( 𝑋 ↑ 𝑏 ) ∈ 𝑆 → ( 𝑋 ↑ ( 𝑏 + 1 ) ) ∈ 𝑆 ) ) )
36	35	a2d	⊢ ( 𝑏 ∈ ℕ0 → ( ( 𝜑 → ( 𝑋 ↑ 𝑏 ) ∈ 𝑆 ) → ( 𝜑 → ( 𝑋 ↑ ( 𝑏 + 1 ) ) ∈ 𝑆 ) ) )
37	6 9 12 15 24 36	nn0ind	⊢ ( 𝑌 ∈ ℕ0 → ( 𝜑 → ( 𝑋 ↑ 𝑌 ) ∈ 𝑆 ) )
38	3 37	mpcom	⊢ ( 𝜑 → ( 𝑋 ↑ 𝑌 ) ∈ 𝑆 )