Metamath Proof Explorer


Theorem expclzlem

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

Ref Expression
Assertion expclzlem ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴𝑁 ) ∈ ( ℂ ∖ { 0 } ) )

Proof

Step Hyp Ref Expression
1 eldifsn ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
2 difss ( ℂ ∖ { 0 } ) ⊆ ℂ
3 eldifsn ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
4 eldifsn ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
5 mulcl ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
6 5 ad2ant2r ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
7 mulne0 ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
8 eldifsn ( ( 𝑥 · 𝑦 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑥 · 𝑦 ) ∈ ℂ ∧ ( 𝑥 · 𝑦 ) ≠ 0 ) )
9 6 7 8 sylanbrc ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ∈ ( ℂ ∖ { 0 } ) )
10 3 4 9 syl2anb ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ( ℂ ∖ { 0 } ) )
11 ax-1cn 1 ∈ ℂ
12 ax-1ne0 1 ≠ 0
13 eldifsn ( 1 ∈ ( ℂ ∖ { 0 } ) ↔ ( 1 ∈ ℂ ∧ 1 ≠ 0 ) )
14 11 12 13 mpbir2an 1 ∈ ( ℂ ∖ { 0 } )
15 reccl ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ ℂ )
16 recne0 ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ≠ 0 )
17 15 16 jca ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( ( 1 / 𝑥 ) ∈ ℂ ∧ ( 1 / 𝑥 ) ≠ 0 ) )
18 eldifsn ( ( 1 / 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 1 / 𝑥 ) ∈ ℂ ∧ ( 1 / 𝑥 ) ≠ 0 ) )
19 17 3 18 3imtr4i ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → ( 1 / 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
20 19 adantr ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
21 2 10 14 20 expcl2lem ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴𝑁 ) ∈ ( ℂ ∖ { 0 } ) )
22 21 3expia ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐴 ≠ 0 ) → ( 𝑁 ∈ ℤ → ( 𝐴𝑁 ) ∈ ( ℂ ∖ { 0 } ) ) )
23 1 22 sylanbr ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≠ 0 ) → ( 𝑁 ∈ ℤ → ( 𝐴𝑁 ) ∈ ( ℂ ∖ { 0 } ) ) )
24 23 anabss3 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑁 ∈ ℤ → ( 𝐴𝑁 ) ∈ ( ℂ ∖ { 0 } ) ) )
25 24 3impia ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴𝑁 ) ∈ ( ℂ ∖ { 0 } ) )