Theorem m1expcl2

Description: Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Assertion	m1expcl2	⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } )

Proof

Step	Hyp	Ref	Expression
1		negex	⊢ - 1 ∈ V
2	1	prid1	⊢ - 1 ∈ { - 1 , 1 }
3		neg1ne0	⊢ - 1 ≠ 0
4		neg1cn	⊢ - 1 ∈ ℂ
5		ax-1cn	⊢ 1 ∈ ℂ
6		prssi	⊢ ( ( - 1 ∈ ℂ ∧ 1 ∈ ℂ ) → { - 1 , 1 } ⊆ ℂ )
7	4 5 6	mp2an	⊢ { - 1 , 1 } ⊆ ℂ
8		elpri	⊢ ( 𝑥 ∈ { - 1 , 1 } → ( 𝑥 = - 1 ∨ 𝑥 = 1 ) )
9	7	sseli	⊢ ( 𝑦 ∈ { - 1 , 1 } → 𝑦 ∈ ℂ )
10	9	mulm1d	⊢ ( 𝑦 ∈ { - 1 , 1 } → ( - 1 · 𝑦 ) = - 𝑦 )
11		elpri	⊢ ( 𝑦 ∈ { - 1 , 1 } → ( 𝑦 = - 1 ∨ 𝑦 = 1 ) )
12		negeq	⊢ ( 𝑦 = - 1 → - 𝑦 = - - 1 )
13		negneg1e1	⊢ - - 1 = 1
14		1ex	⊢ 1 ∈ V
15	14	prid2	⊢ 1 ∈ { - 1 , 1 }
16	13 15	eqeltri	⊢ - - 1 ∈ { - 1 , 1 }
17	12 16	eqeltrdi	⊢ ( 𝑦 = - 1 → - 𝑦 ∈ { - 1 , 1 } )
18		negeq	⊢ ( 𝑦 = 1 → - 𝑦 = - 1 )
19	18 2	eqeltrdi	⊢ ( 𝑦 = 1 → - 𝑦 ∈ { - 1 , 1 } )
20	17 19	jaoi	⊢ ( ( 𝑦 = - 1 ∨ 𝑦 = 1 ) → - 𝑦 ∈ { - 1 , 1 } )
21	11 20	syl	⊢ ( 𝑦 ∈ { - 1 , 1 } → - 𝑦 ∈ { - 1 , 1 } )
22	10 21	eqeltrd	⊢ ( 𝑦 ∈ { - 1 , 1 } → ( - 1 · 𝑦 ) ∈ { - 1 , 1 } )
23		oveq1	⊢ ( 𝑥 = - 1 → ( 𝑥 · 𝑦 ) = ( - 1 · 𝑦 ) )
24	23	eleq1d	⊢ ( 𝑥 = - 1 → ( ( 𝑥 · 𝑦 ) ∈ { - 1 , 1 } ↔ ( - 1 · 𝑦 ) ∈ { - 1 , 1 } ) )
25	22 24	syl5ibr	⊢ ( 𝑥 = - 1 → ( 𝑦 ∈ { - 1 , 1 } → ( 𝑥 · 𝑦 ) ∈ { - 1 , 1 } ) )
26	9	mulid2d	⊢ ( 𝑦 ∈ { - 1 , 1 } → ( 1 · 𝑦 ) = 𝑦 )
27		id	⊢ ( 𝑦 ∈ { - 1 , 1 } → 𝑦 ∈ { - 1 , 1 } )
28	26 27	eqeltrd	⊢ ( 𝑦 ∈ { - 1 , 1 } → ( 1 · 𝑦 ) ∈ { - 1 , 1 } )
29		oveq1	⊢ ( 𝑥 = 1 → ( 𝑥 · 𝑦 ) = ( 1 · 𝑦 ) )
30	29	eleq1d	⊢ ( 𝑥 = 1 → ( ( 𝑥 · 𝑦 ) ∈ { - 1 , 1 } ↔ ( 1 · 𝑦 ) ∈ { - 1 , 1 } ) )
31	28 30	syl5ibr	⊢ ( 𝑥 = 1 → ( 𝑦 ∈ { - 1 , 1 } → ( 𝑥 · 𝑦 ) ∈ { - 1 , 1 } ) )
32	25 31	jaoi	⊢ ( ( 𝑥 = - 1 ∨ 𝑥 = 1 ) → ( 𝑦 ∈ { - 1 , 1 } → ( 𝑥 · 𝑦 ) ∈ { - 1 , 1 } ) )
33	8 32	syl	⊢ ( 𝑥 ∈ { - 1 , 1 } → ( 𝑦 ∈ { - 1 , 1 } → ( 𝑥 · 𝑦 ) ∈ { - 1 , 1 } ) )
34	33	imp	⊢ ( ( 𝑥 ∈ { - 1 , 1 } ∧ 𝑦 ∈ { - 1 , 1 } ) → ( 𝑥 · 𝑦 ) ∈ { - 1 , 1 } )
35		oveq2	⊢ ( 𝑥 = - 1 → ( 1 / 𝑥 ) = ( 1 / - 1 ) )
36		ax-1ne0	⊢ 1 ≠ 0
37		divneg2	⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0 ) → - ( 1 / 1 ) = ( 1 / - 1 ) )
38	5 5 36 37	mp3an	⊢ - ( 1 / 1 ) = ( 1 / - 1 )
39		1div1e1	⊢ ( 1 / 1 ) = 1
40	39	negeqi	⊢ - ( 1 / 1 ) = - 1
41	38 40	eqtr3i	⊢ ( 1 / - 1 ) = - 1
42	41 2	eqeltri	⊢ ( 1 / - 1 ) ∈ { - 1 , 1 }
43	35 42	eqeltrdi	⊢ ( 𝑥 = - 1 → ( 1 / 𝑥 ) ∈ { - 1 , 1 } )
44		oveq2	⊢ ( 𝑥 = 1 → ( 1 / 𝑥 ) = ( 1 / 1 ) )
45	39 15	eqeltri	⊢ ( 1 / 1 ) ∈ { - 1 , 1 }
46	44 45	eqeltrdi	⊢ ( 𝑥 = 1 → ( 1 / 𝑥 ) ∈ { - 1 , 1 } )
47	43 46	jaoi	⊢ ( ( 𝑥 = - 1 ∨ 𝑥 = 1 ) → ( 1 / 𝑥 ) ∈ { - 1 , 1 } )
48	8 47	syl	⊢ ( 𝑥 ∈ { - 1 , 1 } → ( 1 / 𝑥 ) ∈ { - 1 , 1 } )
49	48	adantr	⊢ ( ( 𝑥 ∈ { - 1 , 1 } ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ { - 1 , 1 } )
50	7 34 15 49	expcl2lem	⊢ ( ( - 1 ∈ { - 1 , 1 } ∧ - 1 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } )
51	2 3 50	mp3an12	⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } )