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 } ) ) |