Metamath Proof Explorer

Theorem cnsrexpcl

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

Ref Expression
Hypotheses cnsrexpcl.s 
|- ( ph -> S e. ( SubRing ` CCfld ) )
cnsrexpcl.x 
|- ( ph -> X e. S )
cnsrexpcl.y 
|- ( ph -> Y e. NN0 )
Assertion cnsrexpcl 
|- ( ph -> ( X ^ Y ) e. S )

Proof

Step Hyp Ref Expression
1 cnsrexpcl.s 
 |-  ( ph -> S e. ( SubRing ` CCfld ) )
2 cnsrexpcl.x 
 |-  ( ph -> X e. S )
3 cnsrexpcl.y 
 |-  ( ph -> Y e. NN0 )
4 oveq2 
 |-  ( a = 0 -> ( X ^ a ) = ( X ^ 0 ) )
5 4 eleq1d 
 |-  ( a = 0 -> ( ( X ^ a ) e. S <-> ( X ^ 0 ) e. S ) )
6 5 imbi2d 
 |-  ( a = 0 -> ( ( ph -> ( X ^ a ) e. S ) <-> ( ph -> ( X ^ 0 ) e. S ) ) )
7 oveq2 
 |-  ( a = b -> ( X ^ a ) = ( X ^ b ) )
8 7 eleq1d 
 |-  ( a = b -> ( ( X ^ a ) e. S <-> ( X ^ b ) e. S ) )
9 8 imbi2d 
 |-  ( a = b -> ( ( ph -> ( X ^ a ) e. S ) <-> ( ph -> ( X ^ b ) e. S ) ) )
10 oveq2 
 |-  ( a = ( b + 1 ) -> ( X ^ a ) = ( X ^ ( b + 1 ) ) )
11 10 eleq1d 
 |-  ( a = ( b + 1 ) -> ( ( X ^ a ) e. S <-> ( X ^ ( b + 1 ) ) e. S ) )
12 11 imbi2d 
 |-  ( a = ( b + 1 ) -> ( ( ph -> ( X ^ a ) e. S ) <-> ( ph -> ( X ^ ( b + 1 ) ) e. S ) ) )
13 oveq2 
 |-  ( a = Y -> ( X ^ a ) = ( X ^ Y ) )
14 13 eleq1d 
 |-  ( a = Y -> ( ( X ^ a ) e. S <-> ( X ^ Y ) e. S ) )
15 14 imbi2d 
 |-  ( a = Y -> ( ( ph -> ( X ^ a ) e. S ) <-> ( ph -> ( X ^ Y ) e. S ) ) )
16 cnfldbas 
 |-  CC = ( Base ` CCfld )
17 16 subrgss 
 |-  ( S e. ( SubRing ` CCfld ) -> S C_ CC )
18 1 17 syl 
 |-  ( ph -> S C_ CC )
19 18 2 sseldd 
 |-  ( ph -> X e. CC )
20 19 exp0d 
 |-  ( ph -> ( X ^ 0 ) = 1 )
21 cnfld1 
 |-  1 = ( 1r ` CCfld )
22 21 subrg1cl 
 |-  ( S e. ( SubRing ` CCfld ) -> 1 e. S )
23 1 22 syl 
 |-  ( ph -> 1 e. S )
24 20 23 eqeltrd 
 |-  ( ph -> ( X ^ 0 ) e. S )
25 19 3ad2ant2 
 |-  ( ( b e. NN0 /\ ph /\ ( X ^ b ) e. S ) -> X e. CC )
26 simp1 
 |-  ( ( b e. NN0 /\ ph /\ ( X ^ b ) e. S ) -> b e. NN0 )
27 25 26 expp1d 
 |-  ( ( b e. NN0 /\ ph /\ ( X ^ b ) e. S ) -> ( X ^ ( b + 1 ) ) = ( ( X ^ b ) x. X ) )
28 1 3ad2ant2 
 |-  ( ( b e. NN0 /\ ph /\ ( X ^ b ) e. S ) -> S e. ( SubRing ` CCfld ) )
29 simp3 
 |-  ( ( b e. NN0 /\ ph /\ ( X ^ b ) e. S ) -> ( X ^ b ) e. S )
30 2 3ad2ant2 
 |-  ( ( b e. NN0 /\ ph /\ ( X ^ b ) e. S ) -> X e. S )
31 cnfldmul 
 |-  x. = ( .r ` CCfld )
32 31 subrgmcl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( X ^ b ) e. S /\ X e. S ) -> ( ( X ^ b ) x. X ) e. S )
33 28 29 30 32 syl3anc 
 |-  ( ( b e. NN0 /\ ph /\ ( X ^ b ) e. S ) -> ( ( X ^ b ) x. X ) e. S )
34 27 33 eqeltrd 
 |-  ( ( b e. NN0 /\ ph /\ ( X ^ b ) e. S ) -> ( X ^ ( b + 1 ) ) e. S )
35 34 3exp 
 |-  ( b e. NN0 -> ( ph -> ( ( X ^ b ) e. S -> ( X ^ ( b + 1 ) ) e. S ) ) )
36 35 a2d 
 |-  ( b e. NN0 -> ( ( ph -> ( X ^ b ) e. S ) -> ( ph -> ( X ^ ( b + 1 ) ) e. S ) ) )
37 6 9 12 15 24 36 nn0ind 
 |-  ( Y e. NN0 -> ( ph -> ( X ^ Y ) e. S ) )
38 3 37 mpcom 
 |-  ( ph -> ( X ^ Y ) e. S )