Metamath Proof Explorer

Theorem expcl2lem

Description: Lemma for proving integer exponentiation closure laws. (Contributed by Mario Carneiro, 4-Jun-2014) (Revised by Mario Carneiro, 9-Sep-2014)

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
expcl2lem.4 
|- ( ( x e. F /\ x =/= 0 ) -> ( 1 / x ) e. F )
Assertion expcl2lem 
|- ( ( A e. F /\ A =/= 0 /\ B e. ZZ ) -> ( 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 expcl2lem.4 
 |-  ( ( x e. F /\ x =/= 0 ) -> ( 1 / x ) e. F )
5 elznn0nn 
 |-  ( B e. ZZ <-> ( B e. NN0 \/ ( B e. RR /\ -u B e. NN ) ) )
6 1 2 3 expcllem 
 |-  ( ( A e. F /\ B e. NN0 ) -> ( A ^ B ) e. F )
7 6 ex 
 |-  ( A e. F -> ( B e. NN0 -> ( A ^ B ) e. F ) )
8 7 adantr 
 |-  ( ( A e. F /\ A =/= 0 ) -> ( B e. NN0 -> ( A ^ B ) e. F ) )
9 simpll 
 |-  ( ( ( A e. F /\ A =/= 0 ) /\ ( B e. RR /\ -u B e. NN ) ) -> A e. F )
10 1 9 sselid 
 |-  ( ( ( A e. F /\ A =/= 0 ) /\ ( B e. RR /\ -u B e. NN ) ) -> A e. CC )
11 simprl 
 |-  ( ( ( A e. F /\ A =/= 0 ) /\ ( B e. RR /\ -u B e. NN ) ) -> B e. RR )
12 11 recnd 
 |-  ( ( ( A e. F /\ A =/= 0 ) /\ ( B e. RR /\ -u B e. NN ) ) -> B e. CC )
13 nnnn0 
 |-  ( -u B e. NN -> -u B e. NN0 )
14 13 ad2antll 
 |-  ( ( ( A e. F /\ A =/= 0 ) /\ ( B e. RR /\ -u B e. NN ) ) -> -u B e. NN0 )
15 expneg2 
 |-  ( ( A e. CC /\ B e. CC /\ -u B e. NN0 ) -> ( A ^ B ) = ( 1 / ( A ^ -u B ) ) )
16 10 12 14 15 syl3anc 
 |-  ( ( ( A e. F /\ A =/= 0 ) /\ ( B e. RR /\ -u B e. NN ) ) -> ( A ^ B ) = ( 1 / ( A ^ -u B ) ) )
17 difss 
 |-  ( F \ { 0 } ) C_ F
18 eldifsn 
 |-  ( A e. ( F \ { 0 } ) <-> ( A e. F /\ A =/= 0 ) )
19 18 biranri 
 |-  ( ( ( A e. F /\ A =/= 0 ) /\ ( B e. RR /\ -u B e. NN ) ) -> A e. ( F \ { 0 } ) )
20 17 1 sstri 
 |-  ( F \ { 0 } ) C_ CC
21 17 sseli 
 |-  ( x e. ( F \ { 0 } ) -> x e. F )
22 17 sseli 
 |-  ( y e. ( F \ { 0 } ) -> y e. F )
23 21 22 2 syl2an 
 |-  ( ( x e. ( F \ { 0 } ) /\ y e. ( F \ { 0 } ) ) -> ( x x. y ) e. F )
24 eldifsn 
 |-  ( x e. ( F \ { 0 } ) <-> ( x e. F /\ x =/= 0 ) )
25 1 sseli 
 |-  ( x e. F -> x e. CC )
26 25 anim1i 
 |-  ( ( x e. F /\ x =/= 0 ) -> ( x e. CC /\ x =/= 0 ) )
27 24 26 sylbi 
 |-  ( x e. ( F \ { 0 } ) -> ( x e. CC /\ x =/= 0 ) )
28 eldifsn 
 |-  ( y e. ( F \ { 0 } ) <-> ( y e. F /\ y =/= 0 ) )
29 1 sseli 
 |-  ( y e. F -> y e. CC )
30 29 anim1i 
 |-  ( ( y e. F /\ y =/= 0 ) -> ( y e. CC /\ y =/= 0 ) )
31 28 30 sylbi 
 |-  ( y e. ( F \ { 0 } ) -> ( y e. CC /\ y =/= 0 ) )
32 mulne0 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( x x. y ) =/= 0 )
33 27 31 32 syl2an 
 |-  ( ( x e. ( F \ { 0 } ) /\ y e. ( F \ { 0 } ) ) -> ( x x. y ) =/= 0 )
34 eldifsn 
 |-  ( ( x x. y ) e. ( F \ { 0 } ) <-> ( ( x x. y ) e. F /\ ( x x. y ) =/= 0 ) )
35 23 33 34 sylanbrc 
 |-  ( ( x e. ( F \ { 0 } ) /\ y e. ( F \ { 0 } ) ) -> ( x x. y ) e. ( F \ { 0 } ) )
36 ax-1ne0 
 |-  1 =/= 0
37 eldifsn 
 |-  ( 1 e. ( F \ { 0 } ) <-> ( 1 e. F /\ 1 =/= 0 ) )
38 3 36 37 mpbir2an 
 |-  1 e. ( F \ { 0 } )
39 20 35 38 expcllem 
 |-  ( ( A e. ( F \ { 0 } ) /\ -u B e. NN0 ) -> ( A ^ -u B ) e. ( F \ { 0 } ) )
40 19 14 39 syl2anc 
 |-  ( ( ( A e. F /\ A =/= 0 ) /\ ( B e. RR /\ -u B e. NN ) ) -> ( A ^ -u B ) e. ( F \ { 0 } ) )
41 17 40 sselid 
 |-  ( ( ( A e. F /\ A =/= 0 ) /\ ( B e. RR /\ -u B e. NN ) ) -> ( A ^ -u B ) e. F )
42 eldifsn 
 |-  ( ( A ^ -u B ) e. ( F \ { 0 } ) <-> ( ( A ^ -u B ) e. F /\ ( A ^ -u B ) =/= 0 ) )
43 40 42 sylib 
 |-  ( ( ( A e. F /\ A =/= 0 ) /\ ( B e. RR /\ -u B e. NN ) ) -> ( ( A ^ -u B ) e. F /\ ( A ^ -u B ) =/= 0 ) )
44 43 simprd 
 |-  ( ( ( A e. F /\ A =/= 0 ) /\ ( B e. RR /\ -u B e. NN ) ) -> ( A ^ -u B ) =/= 0 )
45 neeq1 
 |-  ( x = ( A ^ -u B ) -> ( x =/= 0 <-> ( A ^ -u B ) =/= 0 ) )
46 oveq2 
 |-  ( x = ( A ^ -u B ) -> ( 1 / x ) = ( 1 / ( A ^ -u B ) ) )
47 46 eleq1d 
 |-  ( x = ( A ^ -u B ) -> ( ( 1 / x ) e. F <-> ( 1 / ( A ^ -u B ) ) e. F ) )
48 45 47 imbi12d 
 |-  ( x = ( A ^ -u B ) -> ( ( x =/= 0 -> ( 1 / x ) e. F ) <-> ( ( A ^ -u B ) =/= 0 -> ( 1 / ( A ^ -u B ) ) e. F ) ) )
49 4 ex 
 |-  ( x e. F -> ( x =/= 0 -> ( 1 / x ) e. F ) )
50 48 49 vtoclga 
 |-  ( ( A ^ -u B ) e. F -> ( ( A ^ -u B ) =/= 0 -> ( 1 / ( A ^ -u B ) ) e. F ) )
51 41 44 50 sylc 
 |-  ( ( ( A e. F /\ A =/= 0 ) /\ ( B e. RR /\ -u B e. NN ) ) -> ( 1 / ( A ^ -u B ) ) e. F )
52 16 51 eqeltrd 
 |-  ( ( ( A e. F /\ A =/= 0 ) /\ ( B e. RR /\ -u B e. NN ) ) -> ( A ^ B ) e. F )
53 52 ex 
 |-  ( ( A e. F /\ A =/= 0 ) -> ( ( B e. RR /\ -u B e. NN ) -> ( A ^ B ) e. F ) )
54 8 53 jaod 
 |-  ( ( A e. F /\ A =/= 0 ) -> ( ( B e. NN0 \/ ( B e. RR /\ -u B e. NN ) ) -> ( A ^ B ) e. F ) )
55 5 54 biimtrid 
 |-  ( ( A e. F /\ A =/= 0 ) -> ( B e. ZZ -> ( A ^ B ) e. F ) )
56 55 3impia 
 |-  ( ( A e. F /\ A =/= 0 /\ B e. ZZ ) -> ( A ^ B ) e. F )