Theorem mod2xnegi

Description: Version of mod2xi where A ^ B does not equal K (mod N ) but instead the negative of K (mod N ). (Contributed by Mario Carneiro, 21-Feb-2014)

	Ref	Expression
Hypotheses	mod2xnegi.1	⊢ 𝐴 ∈ ℕ
	mod2xnegi.2	⊢ 𝐵 ∈ ℕ0
	mod2xnegi.3	⊢ 𝐷 ∈ ℤ
	mod2xnegi.4	⊢ 𝐾 ∈ ℕ
	mod2xnegi.5	⊢ 𝑀 ∈ ℕ0
	mod2xnegi.6	⊢ 𝐿 ∈ ℕ0
	mod2xnegi.10	⊢ ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐿 mod 𝑁 )
	mod2xnegi.7	⊢ ( 2 · 𝐵 ) = 𝐸
	mod2xnegi.8	⊢ ( 𝐿 + 𝐾 ) = 𝑁
	mod2xnegi.9	⊢ ( ( 𝐷 · 𝑁 ) + 𝑀 ) = ( 𝐾 · 𝐾 )
Assertion	mod2xnegi	⊢ ( ( 𝐴 ↑ 𝐸 ) mod 𝑁 ) = ( 𝑀 mod 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		mod2xnegi.1	⊢ 𝐴 ∈ ℕ
2		mod2xnegi.2	⊢ 𝐵 ∈ ℕ0
3		mod2xnegi.3	⊢ 𝐷 ∈ ℤ
4		mod2xnegi.4	⊢ 𝐾 ∈ ℕ
5		mod2xnegi.5	⊢ 𝑀 ∈ ℕ0
6		mod2xnegi.6	⊢ 𝐿 ∈ ℕ0
7		mod2xnegi.10	⊢ ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐿 mod 𝑁 )
8		mod2xnegi.7	⊢ ( 2 · 𝐵 ) = 𝐸
9		mod2xnegi.8	⊢ ( 𝐿 + 𝐾 ) = 𝑁
10		mod2xnegi.9	⊢ ( ( 𝐷 · 𝑁 ) + 𝑀 ) = ( 𝐾 · 𝐾 )
11		nn0nnaddcl	⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) → ( 𝐿 + 𝐾 ) ∈ ℕ )
12	6 4 11	mp2an	⊢ ( 𝐿 + 𝐾 ) ∈ ℕ
13	9 12	eqeltrri	⊢ 𝑁 ∈ ℕ
14	13	nnzi	⊢ 𝑁 ∈ ℤ
15		zaddcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( 𝑁 + 𝐷 ) ∈ ℤ )
16	14 3 15	mp2an	⊢ ( 𝑁 + 𝐷 ) ∈ ℤ
17	4	nnnn0i	⊢ 𝐾 ∈ ℕ0
18	17 17	nn0addcli	⊢ ( 𝐾 + 𝐾 ) ∈ ℕ0
19	18	nn0zi	⊢ ( 𝐾 + 𝐾 ) ∈ ℤ
20		zsubcl	⊢ ( ( ( 𝑁 + 𝐷 ) ∈ ℤ ∧ ( 𝐾 + 𝐾 ) ∈ ℤ ) → ( ( 𝑁 + 𝐷 ) − ( 𝐾 + 𝐾 ) ) ∈ ℤ )
21	16 19 20	mp2an	⊢ ( ( 𝑁 + 𝐷 ) − ( 𝐾 + 𝐾 ) ) ∈ ℤ
22	13	nncni	⊢ 𝑁 ∈ ℂ
23		zcn	⊢ ( 𝐷 ∈ ℤ → 𝐷 ∈ ℂ )
24	3 23	ax-mp	⊢ 𝐷 ∈ ℂ
25	22 24	addcli	⊢ ( 𝑁 + 𝐷 ) ∈ ℂ
26	4	nncni	⊢ 𝐾 ∈ ℂ
27	26 26	addcli	⊢ ( 𝐾 + 𝐾 ) ∈ ℂ
28	25 27 22	subdiri	⊢ ( ( ( 𝑁 + 𝐷 ) − ( 𝐾 + 𝐾 ) ) · 𝑁 ) = ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) − ( ( 𝐾 + 𝐾 ) · 𝑁 ) )
29	28	oveq1i	⊢ ( ( ( ( 𝑁 + 𝐷 ) − ( 𝐾 + 𝐾 ) ) · 𝑁 ) + 𝑀 ) = ( ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) − ( ( 𝐾 + 𝐾 ) · 𝑁 ) ) + 𝑀 )
30	25 22	mulcli	⊢ ( ( 𝑁 + 𝐷 ) · 𝑁 ) ∈ ℂ
31	5	nn0cni	⊢ 𝑀 ∈ ℂ
32	27 22	mulcli	⊢ ( ( 𝐾 + 𝐾 ) · 𝑁 ) ∈ ℂ
33	30 31 32	addsubi	⊢ ( ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) + 𝑀 ) − ( ( 𝐾 + 𝐾 ) · 𝑁 ) ) = ( ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) − ( ( 𝐾 + 𝐾 ) · 𝑁 ) ) + 𝑀 )
34	10	oveq2i	⊢ ( ( 𝑁 · 𝑁 ) + ( ( 𝐷 · 𝑁 ) + 𝑀 ) ) = ( ( 𝑁 · 𝑁 ) + ( 𝐾 · 𝐾 ) )
35	22 26 26	adddii	⊢ ( 𝑁 · ( 𝐾 + 𝐾 ) ) = ( ( 𝑁 · 𝐾 ) + ( 𝑁 · 𝐾 ) )
36	34 35	oveq12i	⊢ ( ( ( 𝑁 · 𝑁 ) + ( ( 𝐷 · 𝑁 ) + 𝑀 ) ) − ( 𝑁 · ( 𝐾 + 𝐾 ) ) ) = ( ( ( 𝑁 · 𝑁 ) + ( 𝐾 · 𝐾 ) ) − ( ( 𝑁 · 𝐾 ) + ( 𝑁 · 𝐾 ) ) )
37	22 24 22	adddiri	⊢ ( ( 𝑁 + 𝐷 ) · 𝑁 ) = ( ( 𝑁 · 𝑁 ) + ( 𝐷 · 𝑁 ) )
38	37	oveq1i	⊢ ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) + 𝑀 ) = ( ( ( 𝑁 · 𝑁 ) + ( 𝐷 · 𝑁 ) ) + 𝑀 )
39	22 22	mulcli	⊢ ( 𝑁 · 𝑁 ) ∈ ℂ
40	24 22	mulcli	⊢ ( 𝐷 · 𝑁 ) ∈ ℂ
41	39 40 31	addassi	⊢ ( ( ( 𝑁 · 𝑁 ) + ( 𝐷 · 𝑁 ) ) + 𝑀 ) = ( ( 𝑁 · 𝑁 ) + ( ( 𝐷 · 𝑁 ) + 𝑀 ) )
42	38 41	eqtr2i	⊢ ( ( 𝑁 · 𝑁 ) + ( ( 𝐷 · 𝑁 ) + 𝑀 ) ) = ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) + 𝑀 )
43	22 27	mulcomi	⊢ ( 𝑁 · ( 𝐾 + 𝐾 ) ) = ( ( 𝐾 + 𝐾 ) · 𝑁 )
44	42 43	oveq12i	⊢ ( ( ( 𝑁 · 𝑁 ) + ( ( 𝐷 · 𝑁 ) + 𝑀 ) ) − ( 𝑁 · ( 𝐾 + 𝐾 ) ) ) = ( ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) + 𝑀 ) − ( ( 𝐾 + 𝐾 ) · 𝑁 ) )
45	36 44	eqtr3i	⊢ ( ( ( 𝑁 · 𝑁 ) + ( 𝐾 · 𝐾 ) ) − ( ( 𝑁 · 𝐾 ) + ( 𝑁 · 𝐾 ) ) ) = ( ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) + 𝑀 ) − ( ( 𝐾 + 𝐾 ) · 𝑁 ) )
46		mulsub	⊢ ( ( ( 𝑁 ∈ ℂ ∧ 𝐾 ∈ ℂ ) ∧ ( 𝑁 ∈ ℂ ∧ 𝐾 ∈ ℂ ) ) → ( ( 𝑁 − 𝐾 ) · ( 𝑁 − 𝐾 ) ) = ( ( ( 𝑁 · 𝑁 ) + ( 𝐾 · 𝐾 ) ) − ( ( 𝑁 · 𝐾 ) + ( 𝑁 · 𝐾 ) ) ) )
47	22 26 22 26 46	mp4an	⊢ ( ( 𝑁 − 𝐾 ) · ( 𝑁 − 𝐾 ) ) = ( ( ( 𝑁 · 𝑁 ) + ( 𝐾 · 𝐾 ) ) − ( ( 𝑁 · 𝐾 ) + ( 𝑁 · 𝐾 ) ) )
48	6	nn0cni	⊢ 𝐿 ∈ ℂ
49	22 26 48	subadd2i	⊢ ( ( 𝑁 − 𝐾 ) = 𝐿 ↔ ( 𝐿 + 𝐾 ) = 𝑁 )
50	9 49	mpbir	⊢ ( 𝑁 − 𝐾 ) = 𝐿
51	50 50	oveq12i	⊢ ( ( 𝑁 − 𝐾 ) · ( 𝑁 − 𝐾 ) ) = ( 𝐿 · 𝐿 )
52	47 51	eqtr3i	⊢ ( ( ( 𝑁 · 𝑁 ) + ( 𝐾 · 𝐾 ) ) − ( ( 𝑁 · 𝐾 ) + ( 𝑁 · 𝐾 ) ) ) = ( 𝐿 · 𝐿 )
53	45 52	eqtr3i	⊢ ( ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) + 𝑀 ) − ( ( 𝐾 + 𝐾 ) · 𝑁 ) ) = ( 𝐿 · 𝐿 )
54	29 33 53	3eqtr2i	⊢ ( ( ( ( 𝑁 + 𝐷 ) − ( 𝐾 + 𝐾 ) ) · 𝑁 ) + 𝑀 ) = ( 𝐿 · 𝐿 )
55	13 1 2 21 6 5 7 8 54	mod2xi	⊢ ( ( 𝐴 ↑ 𝐸 ) mod 𝑁 ) = ( 𝑀 mod 𝑁 )