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