Proof of Theorem mod2xnegi
Step | Hyp | Ref
| Expression |
1 | | mod2xnegi.8 |
. . 3
⊢ (𝐿 + 𝐾) = 𝑁 |
2 | | mod2xnegi.6 |
. . . 4
⊢ 𝐿 ∈
ℕ0 |
3 | | mod2xnegi.4 |
. . . 4
⊢ 𝐾 ∈ ℕ |
4 | | nn0nnaddcl 12264 |
. . . 4
⊢ ((𝐿 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ (𝐿 + 𝐾) ∈
ℕ) |
5 | 2, 3, 4 | mp2an 689 |
. . 3
⊢ (𝐿 + 𝐾) ∈ ℕ |
6 | 1, 5 | eqeltrri 2838 |
. 2
⊢ 𝑁 ∈ ℕ |
7 | | mod2xnegi.1 |
. 2
⊢ 𝐴 ∈ ℕ |
8 | | mod2xnegi.2 |
. 2
⊢ 𝐵 ∈
ℕ0 |
9 | 6 | nnzi 12344 |
. . . 4
⊢ 𝑁 ∈ ℤ |
10 | | mod2xnegi.3 |
. . . 4
⊢ 𝐷 ∈ ℤ |
11 | | zaddcl 12360 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝑁 + 𝐷) ∈ ℤ) |
12 | 9, 10, 11 | mp2an 689 |
. . 3
⊢ (𝑁 + 𝐷) ∈ ℤ |
13 | 3 | nnnn0i 12241 |
. . . . 5
⊢ 𝐾 ∈
ℕ0 |
14 | 13, 13 | nn0addcli 12270 |
. . . 4
⊢ (𝐾 + 𝐾) ∈
ℕ0 |
15 | 14 | nn0zi 12345 |
. . 3
⊢ (𝐾 + 𝐾) ∈ ℤ |
16 | | zsubcl 12362 |
. . 3
⊢ (((𝑁 + 𝐷) ∈ ℤ ∧ (𝐾 + 𝐾) ∈ ℤ) → ((𝑁 + 𝐷) − (𝐾 + 𝐾)) ∈ ℤ) |
17 | 12, 15, 16 | mp2an 689 |
. 2
⊢ ((𝑁 + 𝐷) − (𝐾 + 𝐾)) ∈ ℤ |
18 | | mod2xnegi.5 |
. 2
⊢ 𝑀 ∈
ℕ0 |
19 | | mod2xnegi.10 |
. 2
⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐿 mod 𝑁) |
20 | | mod2xnegi.7 |
. 2
⊢ (2
· 𝐵) = 𝐸 |
21 | 6 | nncni 11983 |
. . . . . 6
⊢ 𝑁 ∈ ℂ |
22 | | zcn 12324 |
. . . . . . 7
⊢ (𝐷 ∈ ℤ → 𝐷 ∈
ℂ) |
23 | 10, 22 | ax-mp 5 |
. . . . . 6
⊢ 𝐷 ∈ ℂ |
24 | 21, 23 | addcli 10982 |
. . . . 5
⊢ (𝑁 + 𝐷) ∈ ℂ |
25 | 3 | nncni 11983 |
. . . . . 6
⊢ 𝐾 ∈ ℂ |
26 | 25, 25 | addcli 10982 |
. . . . 5
⊢ (𝐾 + 𝐾) ∈ ℂ |
27 | 24, 26, 21 | subdiri 11425 |
. . . 4
⊢ (((𝑁 + 𝐷) − (𝐾 + 𝐾)) · 𝑁) = (((𝑁 + 𝐷) · 𝑁) − ((𝐾 + 𝐾) · 𝑁)) |
28 | 27 | oveq1i 7281 |
. . 3
⊢ ((((𝑁 + 𝐷) − (𝐾 + 𝐾)) · 𝑁) + 𝑀) = ((((𝑁 + 𝐷) · 𝑁) − ((𝐾 + 𝐾) · 𝑁)) + 𝑀) |
29 | 24, 21 | mulcli 10983 |
. . . 4
⊢ ((𝑁 + 𝐷) · 𝑁) ∈ ℂ |
30 | 18 | nn0cni 12245 |
. . . 4
⊢ 𝑀 ∈ ℂ |
31 | 26, 21 | mulcli 10983 |
. . . 4
⊢ ((𝐾 + 𝐾) · 𝑁) ∈ ℂ |
32 | 29, 30, 31 | addsubi 11313 |
. . 3
⊢ ((((𝑁 + 𝐷) · 𝑁) + 𝑀) − ((𝐾 + 𝐾) · 𝑁)) = ((((𝑁 + 𝐷) · 𝑁) − ((𝐾 + 𝐾) · 𝑁)) + 𝑀) |
33 | | mod2xnegi.9 |
. . . . . . 7
⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾) |
34 | 33 | oveq2i 7282 |
. . . . . 6
⊢ ((𝑁 · 𝑁) + ((𝐷 · 𝑁) + 𝑀)) = ((𝑁 · 𝑁) + (𝐾 · 𝐾)) |
35 | 21, 25, 25 | adddii 10988 |
. . . . . 6
⊢ (𝑁 · (𝐾 + 𝐾)) = ((𝑁 · 𝐾) + (𝑁 · 𝐾)) |
36 | 34, 35 | oveq12i 7283 |
. . . . 5
⊢ (((𝑁 · 𝑁) + ((𝐷 · 𝑁) + 𝑀)) − (𝑁 · (𝐾 + 𝐾))) = (((𝑁 · 𝑁) + (𝐾 · 𝐾)) − ((𝑁 · 𝐾) + (𝑁 · 𝐾))) |
37 | 21, 23, 21 | adddiri 10989 |
. . . . . . . 8
⊢ ((𝑁 + 𝐷) · 𝑁) = ((𝑁 · 𝑁) + (𝐷 · 𝑁)) |
38 | 37 | oveq1i 7281 |
. . . . . . 7
⊢ (((𝑁 + 𝐷) · 𝑁) + 𝑀) = (((𝑁 · 𝑁) + (𝐷 · 𝑁)) + 𝑀) |
39 | 21, 21 | mulcli 10983 |
. . . . . . . 8
⊢ (𝑁 · 𝑁) ∈ ℂ |
40 | 23, 21 | mulcli 10983 |
. . . . . . . 8
⊢ (𝐷 · 𝑁) ∈ ℂ |
41 | 39, 40, 30 | addassi 10986 |
. . . . . . 7
⊢ (((𝑁 · 𝑁) + (𝐷 · 𝑁)) + 𝑀) = ((𝑁 · 𝑁) + ((𝐷 · 𝑁) + 𝑀)) |
42 | 38, 41 | eqtr2i 2769 |
. . . . . 6
⊢ ((𝑁 · 𝑁) + ((𝐷 · 𝑁) + 𝑀)) = (((𝑁 + 𝐷) · 𝑁) + 𝑀) |
43 | 21, 26 | mulcomi 10984 |
. . . . . 6
⊢ (𝑁 · (𝐾 + 𝐾)) = ((𝐾 + 𝐾) · 𝑁) |
44 | 42, 43 | oveq12i 7283 |
. . . . 5
⊢ (((𝑁 · 𝑁) + ((𝐷 · 𝑁) + 𝑀)) − (𝑁 · (𝐾 + 𝐾))) = ((((𝑁 + 𝐷) · 𝑁) + 𝑀) − ((𝐾 + 𝐾) · 𝑁)) |
45 | 36, 44 | eqtr3i 2770 |
. . . 4
⊢ (((𝑁 · 𝑁) + (𝐾 · 𝐾)) − ((𝑁 · 𝐾) + (𝑁 · 𝐾))) = ((((𝑁 + 𝐷) · 𝑁) + 𝑀) − ((𝐾 + 𝐾) · 𝑁)) |
46 | | mulsub 11418 |
. . . . . 6
⊢ (((𝑁 ∈ ℂ ∧ 𝐾 ∈ ℂ) ∧ (𝑁 ∈ ℂ ∧ 𝐾 ∈ ℂ)) → ((𝑁 − 𝐾) · (𝑁 − 𝐾)) = (((𝑁 · 𝑁) + (𝐾 · 𝐾)) − ((𝑁 · 𝐾) + (𝑁 · 𝐾)))) |
47 | 21, 25, 21, 25, 46 | mp4an 690 |
. . . . 5
⊢ ((𝑁 − 𝐾) · (𝑁 − 𝐾)) = (((𝑁 · 𝑁) + (𝐾 · 𝐾)) − ((𝑁 · 𝐾) + (𝑁 · 𝐾))) |
48 | 2 | nn0cni 12245 |
. . . . . . . 8
⊢ 𝐿 ∈ ℂ |
49 | 21, 25, 48 | subadd2i 11309 |
. . . . . . 7
⊢ ((𝑁 − 𝐾) = 𝐿 ↔ (𝐿 + 𝐾) = 𝑁) |
50 | 1, 49 | mpbir 230 |
. . . . . 6
⊢ (𝑁 − 𝐾) = 𝐿 |
51 | 50, 50 | oveq12i 7283 |
. . . . 5
⊢ ((𝑁 − 𝐾) · (𝑁 − 𝐾)) = (𝐿 · 𝐿) |
52 | 47, 51 | eqtr3i 2770 |
. . . 4
⊢ (((𝑁 · 𝑁) + (𝐾 · 𝐾)) − ((𝑁 · 𝐾) + (𝑁 · 𝐾))) = (𝐿 · 𝐿) |
53 | 45, 52 | eqtr3i 2770 |
. . 3
⊢ ((((𝑁 + 𝐷) · 𝑁) + 𝑀) − ((𝐾 + 𝐾) · 𝑁)) = (𝐿 · 𝐿) |
54 | 28, 32, 53 | 3eqtr2i 2774 |
. 2
⊢ ((((𝑁 + 𝐷) − (𝐾 + 𝐾)) · 𝑁) + 𝑀) = (𝐿 · 𝐿) |
55 | 6, 7, 8, 17, 2, 18, 19, 20, 54 | mod2xi 16768 |
1
⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁) |