Metamath Proof Explorer

Theorem expclzlem

Description: Closure law for integer exponentiation. (Contributed by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expclzlem 
|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. ( CC \ { 0 } ) )

Proof

Step Hyp Ref Expression
1 eldifsn 
 |-  ( A e. ( CC \ { 0 } ) <-> ( A e. CC /\ A =/= 0 ) )
2 difss 
 |-  ( CC \ { 0 } ) C_ CC
3 eldifsn 
 |-  ( x e. ( CC \ { 0 } ) <-> ( x e. CC /\ x =/= 0 ) )
4 eldifsn 
 |-  ( y e. ( CC \ { 0 } ) <-> ( y e. CC /\ y =/= 0 ) )
5 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
6 5 ad2ant2r 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( x x. y ) e. CC )
7 mulne0 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( x x. y ) =/= 0 )
8 eldifsn 
 |-  ( ( x x. y ) e. ( CC \ { 0 } ) <-> ( ( x x. y ) e. CC /\ ( x x. y ) =/= 0 ) )
9 6 7 8 sylanbrc 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( x x. y ) e. ( CC \ { 0 } ) )
10 3 4 9 syl2anb 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( x x. y ) e. ( CC \ { 0 } ) )
11 ax-1cn 
 |-  1 e. CC
12 ax-1ne0 
 |-  1 =/= 0
13 eldifsn 
 |-  ( 1 e. ( CC \ { 0 } ) <-> ( 1 e. CC /\ 1 =/= 0 ) )
14 11 12 13 mpbir2an 
 |-  1 e. ( CC \ { 0 } )
15 reccl 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( 1 / x ) e. CC )
16 recne0 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( 1 / x ) =/= 0 )
17 15 16 jca 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( ( 1 / x ) e. CC /\ ( 1 / x ) =/= 0 ) )
18 eldifsn 
 |-  ( ( 1 / x ) e. ( CC \ { 0 } ) <-> ( ( 1 / x ) e. CC /\ ( 1 / x ) =/= 0 ) )
19 17 3 18 3imtr4i 
 |-  ( x e. ( CC \ { 0 } ) -> ( 1 / x ) e. ( CC \ { 0 } ) )
20 19 adantr 
 |-  ( ( x e. ( CC \ { 0 } ) /\ x =/= 0 ) -> ( 1 / x ) e. ( CC \ { 0 } ) )
21 2 10 14 20 expcl2lem 
 |-  ( ( A e. ( CC \ { 0 } ) /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. ( CC \ { 0 } ) )
22 21 3expia 
 |-  ( ( A e. ( CC \ { 0 } ) /\ A =/= 0 ) -> ( N e. ZZ -> ( A ^ N ) e. ( CC \ { 0 } ) ) )
23 1 22 sylanbr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ A =/= 0 ) -> ( N e. ZZ -> ( A ^ N ) e. ( CC \ { 0 } ) ) )
24 23 anabss3 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( N e. ZZ -> ( A ^ N ) e. ( CC \ { 0 } ) ) )
25 24 3impia 
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. ( CC \ { 0 } ) )