Theorem expneg

Description: Value of a complex number raised to a nonpositive integer power. When A = 0 and N is nonzero, both sides have the "value" ( 1 / 0 ) ; relying on that should be avoid in applications. (Contributed by Mario Carneiro, 4-Jun-2014)

	Ref	Expression
Assertion	expneg	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
3	2	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝑁 ≠ 0 )
4		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
5	4	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
6	5	negeq0d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 = 0 ↔ - 𝑁 = 0 ) )
7	6	necon3abid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ≠ 0 ↔ ¬ - 𝑁 = 0 ) )
8	3 7	mpbid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ¬ - 𝑁 = 0 )
9	8	iffalsed	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → if ( - 𝑁 = 0 , 1 , if ( 0 < - 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) ) ) = if ( 0 < - 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) ) )
10		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
11	10	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
12		nn0nlt0	⊢ ( 𝑁 ∈ ℕ0 → ¬ 𝑁 < 0 )
13	11 12	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ¬ 𝑁 < 0 )
14	11	nn0red	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
15	14	lt0neg1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 < 0 ↔ 0 < - 𝑁 ) )
16	13 15	mtbid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ¬ 0 < - 𝑁 )
17	16	iffalsed	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → if ( 0 < - 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) ) = ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) )
18	5	negnegd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → - - 𝑁 = 𝑁 )
19	18	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) = ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) )
20	19	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) = ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) ) )
21	9 17 20	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → if ( - 𝑁 = 0 , 1 , if ( 0 < - 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) ) ) = ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) ) )
22		nnnegz	⊢ ( 𝑁 ∈ ℕ → - 𝑁 ∈ ℤ )
23		expval	⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝑁 ∈ ℤ ) → ( 𝐴 ↑ - 𝑁 ) = if ( - 𝑁 = 0 , 1 , if ( 0 < - 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) ) ) )
24	22 23	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ - 𝑁 ) = if ( - 𝑁 = 0 , 1 , if ( 0 < - 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) ) ) )
25		expnnval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) = ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) )
26	25	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 1 / ( 𝐴 ↑ 𝑁 ) ) = ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) ) )
27	21 24 26	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )
28		1div1e1	⊢ ( 1 / 1 ) = 1
29	28	eqcomi	⊢ 1 = ( 1 / 1 )
30		negeq	⊢ ( 𝑁 = 0 → - 𝑁 = - 0 )
31		neg0	⊢ - 0 = 0
32	30 31	eqtrdi	⊢ ( 𝑁 = 0 → - 𝑁 = 0 )
33	32	oveq2d	⊢ ( 𝑁 = 0 → ( 𝐴 ↑ - 𝑁 ) = ( 𝐴 ↑ 0 ) )
34		exp0	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
35	33 34	sylan9eqr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( 𝐴 ↑ - 𝑁 ) = 1 )
36		oveq2	⊢ ( 𝑁 = 0 → ( 𝐴 ↑ 𝑁 ) = ( 𝐴 ↑ 0 ) )
37	36 34	sylan9eqr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 𝑁 ) = 1 )
38	37	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( 1 / ( 𝐴 ↑ 𝑁 ) ) = ( 1 / 1 ) )
39	29 35 38	3eqtr4a	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )
40	27 39	jaodan	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )
41	1 40	sylan2b	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )