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

Metamath Proof Explorer

Theorem expcllem

Description: Lemma for proving nonnegative integer exponentiation closure laws. (Contributed by NM, 14-Dec-2005)

Ref Expression
Hypotheses expcllem.1 
|- F C_ CC
expcllem.2 
|- ( ( x e. F /\ y e. F ) -> ( x x. y ) e. F )
expcllem.3 
|- 1 e. F
Assertion expcllem 
|- ( ( A e. F /\ B e. NN0 ) -> ( A ^ B ) e. F )

Proof

Step Hyp Ref Expression
1 expcllem.1 
 |-  F C_ CC
2 expcllem.2 
 |-  ( ( x e. F /\ y e. F ) -> ( x x. y ) e. F )
3 expcllem.3 
 |-  1 e. F
4 elnn0 
 |-  ( B e. NN0 <-> ( B e. NN \/ B = 0 ) )
5 oveq2 
 |-  ( z = 1 -> ( A ^ z ) = ( A ^ 1 ) )
6 5 eleq1d 
 |-  ( z = 1 -> ( ( A ^ z ) e. F <-> ( A ^ 1 ) e. F ) )
7 6 imbi2d 
 |-  ( z = 1 -> ( ( A e. F -> ( A ^ z ) e. F ) <-> ( A e. F -> ( A ^ 1 ) e. F ) ) )
8 oveq2 
 |-  ( z = w -> ( A ^ z ) = ( A ^ w ) )
9 8 eleq1d 
 |-  ( z = w -> ( ( A ^ z ) e. F <-> ( A ^ w ) e. F ) )
10 9 imbi2d 
 |-  ( z = w -> ( ( A e. F -> ( A ^ z ) e. F ) <-> ( A e. F -> ( A ^ w ) e. F ) ) )
11 oveq2 
 |-  ( z = ( w + 1 ) -> ( A ^ z ) = ( A ^ ( w + 1 ) ) )
12 11 eleq1d 
 |-  ( z = ( w + 1 ) -> ( ( A ^ z ) e. F <-> ( A ^ ( w + 1 ) ) e. F ) )
13 12 imbi2d 
 |-  ( z = ( w + 1 ) -> ( ( A e. F -> ( A ^ z ) e. F ) <-> ( A e. F -> ( A ^ ( w + 1 ) ) e. F ) ) )
14 oveq2 
 |-  ( z = B -> ( A ^ z ) = ( A ^ B ) )
15 14 eleq1d 
 |-  ( z = B -> ( ( A ^ z ) e. F <-> ( A ^ B ) e. F ) )
16 15 imbi2d 
 |-  ( z = B -> ( ( A e. F -> ( A ^ z ) e. F ) <-> ( A e. F -> ( A ^ B ) e. F ) ) )
17 1 sseli 
 |-  ( A e. F -> A e. CC )
18 exp1 
 |-  ( A e. CC -> ( A ^ 1 ) = A )
19 17 18 syl 
 |-  ( A e. F -> ( A ^ 1 ) = A )
20 19 eleq1d 
 |-  ( A e. F -> ( ( A ^ 1 ) e. F <-> A e. F ) )
21 20 ibir 
 |-  ( A e. F -> ( A ^ 1 ) e. F )
22 2 caovcl 
 |-  ( ( ( A ^ w ) e. F /\ A e. F ) -> ( ( A ^ w ) x. A ) e. F )
23 22 ancoms 
 |-  ( ( A e. F /\ ( A ^ w ) e. F ) -> ( ( A ^ w ) x. A ) e. F )
24 23 adantlr 
 |-  ( ( ( A e. F /\ w e. NN ) /\ ( A ^ w ) e. F ) -> ( ( A ^ w ) x. A ) e. F )
25 nnnn0 
 |-  ( w e. NN -> w e. NN0 )
26 expp1 
 |-  ( ( A e. CC /\ w e. NN0 ) -> ( A ^ ( w + 1 ) ) = ( ( A ^ w ) x. A ) )
27 17 25 26 syl2an 
 |-  ( ( A e. F /\ w e. NN ) -> ( A ^ ( w + 1 ) ) = ( ( A ^ w ) x. A ) )
28 27 eleq1d 
 |-  ( ( A e. F /\ w e. NN ) -> ( ( A ^ ( w + 1 ) ) e. F <-> ( ( A ^ w ) x. A ) e. F ) )
29 28 adantr 
 |-  ( ( ( A e. F /\ w e. NN ) /\ ( A ^ w ) e. F ) -> ( ( A ^ ( w + 1 ) ) e. F <-> ( ( A ^ w ) x. A ) e. F ) )
30 24 29 mpbird 
 |-  ( ( ( A e. F /\ w e. NN ) /\ ( A ^ w ) e. F ) -> ( A ^ ( w + 1 ) ) e. F )
31 30 exp31 
 |-  ( A e. F -> ( w e. NN -> ( ( A ^ w ) e. F -> ( A ^ ( w + 1 ) ) e. F ) ) )
32 31 com12 
 |-  ( w e. NN -> ( A e. F -> ( ( A ^ w ) e. F -> ( A ^ ( w + 1 ) ) e. F ) ) )
33 32 a2d 
 |-  ( w e. NN -> ( ( A e. F -> ( A ^ w ) e. F ) -> ( A e. F -> ( A ^ ( w + 1 ) ) e. F ) ) )
34 7 10 13 16 21 33 nnind 
 |-  ( B e. NN -> ( A e. F -> ( A ^ B ) e. F ) )
35 34 impcom 
 |-  ( ( A e. F /\ B e. NN ) -> ( A ^ B ) e. F )
36 oveq2 
 |-  ( B = 0 -> ( A ^ B ) = ( A ^ 0 ) )
37 exp0 
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
38 17 37 syl 
 |-  ( A e. F -> ( A ^ 0 ) = 1 )
39 36 38 sylan9eqr 
 |-  ( ( A e. F /\ B = 0 ) -> ( A ^ B ) = 1 )
40 39 3 eqeltrdi 
 |-  ( ( A e. F /\ B = 0 ) -> ( A ^ B ) e. F )
41 35 40 jaodan 
 |-  ( ( A e. F /\ ( B e. NN \/ B = 0 ) ) -> ( A ^ B ) e. F )
42 4 41 sylan2b 
 |-  ( ( A e. F /\ B e. NN0 ) -> ( A ^ B ) e. F )