Theorem cnsrexpcl

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

	Ref	Expression
Hypotheses	cnsrexpcl.s	$$⊢\phi \to S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
	cnsrexpcl.x	$$⊢\phi \to X\in S$$
	cnsrexpcl.y	$$⊢\phi \to Y\in {\mathbb{N}}_0$$
Assertion	cnsrexpcl	$$⊢\phi \to X^Y\in S$$

Proof

Step	Hyp	Ref	Expression
1		cnsrexpcl.s	$$⊢\phi \to S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
2		cnsrexpcl.x	$$⊢\phi \to X\in S$$
3		cnsrexpcl.y	$$⊢\phi \to Y\in {\mathbb{N}}_0$$
4		oveq2	$$⊢a=0\to X^a=X^0$$
5	4	eleq1d	$$⊢a=0\to \left(X^a\in S\leftrightarrow X^0\in S\right)$$
6	5	imbi2d	$$⊢a=0\to \left(\left(\phi \to X^a\in S\right)\leftrightarrow \left(\phi \to X^0\in S\right)\right)$$
7		oveq2	$$⊢a=b\to X^a=X^b$$
8	7	eleq1d	$$⊢a=b\to \left(X^a\in S\leftrightarrow X^b\in S\right)$$
9	8	imbi2d	$$⊢a=b\to \left(\left(\phi \to X^a\in S\right)\leftrightarrow \left(\phi \to X^b\in S\right)\right)$$
10		oveq2	$$⊢a=b+1\to X^a=X^{b+1}$$
11	10	eleq1d	$$⊢a=b+1\to \left(X^a\in S\leftrightarrow X^{b+1}\in S\right)$$
12	11	imbi2d	$$⊢a=b+1\to \left(\left(\phi \to X^a\in S\right)\leftrightarrow \left(\phi \to X^{b+1}\in S\right)\right)$$
13		oveq2	$$⊢a=Y\to X^a=X^Y$$
14	13	eleq1d	$$⊢a=Y\to \left(X^a\in S\leftrightarrow X^Y\in S\right)$$
15	14	imbi2d	$$⊢a=Y\to \left(\left(\phi \to X^a\in S\right)\leftrightarrow \left(\phi \to X^Y\in S\right)\right)$$
16		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
17	16	subrgss	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to S\subseteq ℂ$$
18	1 17	syl	$$⊢\phi \to S\subseteq ℂ$$
19	18 2	sseldd	$$⊢\phi \to X\in ℂ$$
20	19	exp0d	$$⊢\phi \to X^0=1$$
21		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
22	21	subrg1cl	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to 1\in S$$
23	1 22	syl	$$⊢\phi \to 1\in S$$
24	20 23	eqeltrd	$$⊢\phi \to X^0\in S$$
25	19	3ad2ant2	$$⊢\left(b\in {\mathbb{N}}_0\wedge \phi \wedge X^b\in S\right)\to X\in ℂ$$
26		simp1	$$⊢\left(b\in {\mathbb{N}}_0\wedge \phi \wedge X^b\in S\right)\to b\in {\mathbb{N}}_0$$
27	25 26	expp1d	$$⊢\left(b\in {\mathbb{N}}_0\wedge \phi \wedge X^b\in S\right)\to X^{b+1}=X^{b}X$$
28	1	3ad2ant2	$$⊢\left(b\in {\mathbb{N}}_0\wedge \phi \wedge X^b\in S\right)\to S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
29		simp3	$$⊢\left(b\in {\mathbb{N}}_0\wedge \phi \wedge X^b\in S\right)\to X^b\in S$$
30	2	3ad2ant2	$$⊢\left(b\in {\mathbb{N}}_0\wedge \phi \wedge X^b\in S\right)\to X\in S$$
31		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
32	31	subrgmcl	$$⊢\left(S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge X^b\in S\wedge X\in S\right)\to X^{b}X\in S$$
33	28 29 30 32	syl3anc	$$⊢\left(b\in {\mathbb{N}}_0\wedge \phi \wedge X^b\in S\right)\to X^{b}X\in S$$
34	27 33	eqeltrd	$$⊢\left(b\in {\mathbb{N}}_0\wedge \phi \wedge X^b\in S\right)\to X^{b+1}\in S$$
35	34	3exp	$$⊢b\in {\mathbb{N}}_0\to \left(\phi \to \left(X^b\in S\to X^{b+1}\in S\right)\right)$$
36	35	a2d	$$⊢b\in {\mathbb{N}}_0\to \left(\left(\phi \to X^b\in S\right)\to \left(\phi \to X^{b+1}\in S\right)\right)$$
37	6 9 12 15 24 36	nn0ind	$$⊢Y\in {\mathbb{N}}_0\to \left(\phi \to X^Y\in S\right)$$
38	3 37	mpcom	$$⊢\phi \to X^Y\in S$$