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