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

Metamath Proof Explorer

Theorem expclzlem

Description: Lemma for expclz . (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 } ) )