Proof of Theorem mulp1mod1
Step | Hyp | Ref
| Expression |
1 | | eluzelcn 9498 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℂ) |
2 | 1 | adantl 275 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → 𝑁 ∈ ℂ) |
3 | | simpl 108 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → 𝐴 ∈ ℤ) |
4 | 3 | zcnd 9335 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → 𝐴 ∈ ℂ) |
5 | 2, 4 | mulcomd 7941 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → (𝑁 · 𝐴) = (𝐴 · 𝑁)) |
6 | 5 | oveq1d 5868 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → ((𝑁 · 𝐴) mod 𝑁) = ((𝐴 · 𝑁) mod 𝑁)) |
7 | | eluzelz 9496 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℤ) |
8 | | zq 9585 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℚ) |
9 | 7, 8 | syl 14 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℚ) |
10 | 9 | adantl 275 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → 𝑁 ∈ ℚ) |
11 | | 0red 7921 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → 0 ∈ ℝ) |
12 | | 2re 8948 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
13 | 12 | a1i 9 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → 2 ∈ ℝ) |
14 | 7 | adantl 275 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → 𝑁 ∈ ℤ) |
15 | 14 | zred 9334 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → 𝑁 ∈ ℝ) |
16 | | 2pos 8969 |
. . . . . . . . 9
⊢ 0 <
2 |
17 | 16 | a1i 9 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → 0 < 2) |
18 | | eluzle 9499 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ≤ 𝑁) |
19 | 18 | adantl 275 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → 2 ≤ 𝑁) |
20 | 11, 13, 15, 17, 19 | ltletrd 8342 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → 0 < 𝑁) |
21 | | mulqmod0 10286 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℚ ∧ 0 <
𝑁) → ((𝐴 · 𝑁) mod 𝑁) = 0) |
22 | 3, 10, 20, 21 | syl3anc 1233 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → ((𝐴 · 𝑁) mod 𝑁) = 0) |
23 | 6, 22 | eqtrd 2203 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → ((𝑁 · 𝐴) mod 𝑁) = 0) |
24 | 23 | oveq1d 5868 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → (((𝑁 · 𝐴) mod 𝑁) + 1) = (0 + 1)) |
25 | | 0p1e1 8992 |
. . . 4
⊢ (0 + 1) =
1 |
26 | 24, 25 | eqtrdi 2219 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → (((𝑁 · 𝐴) mod 𝑁) + 1) = 1) |
27 | 26 | oveq1d 5868 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → ((((𝑁 · 𝐴) mod 𝑁) + 1) mod 𝑁) = (1 mod 𝑁)) |
28 | | zq 9585 |
. . . . 5
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℚ) |
29 | 3, 28 | syl 14 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → 𝐴 ∈ ℚ) |
30 | | qmulcl 9596 |
. . . 4
⊢ ((𝑁 ∈ ℚ ∧ 𝐴 ∈ ℚ) → (𝑁 · 𝐴) ∈ ℚ) |
31 | 10, 29, 30 | syl2anc 409 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → (𝑁 · 𝐴) ∈ ℚ) |
32 | | 1z 9238 |
. . . 4
⊢ 1 ∈
ℤ |
33 | | zq 9585 |
. . . 4
⊢ (1 ∈
ℤ → 1 ∈ ℚ) |
34 | 32, 33 | mp1i 10 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → 1 ∈ ℚ) |
35 | | modqaddmod 10319 |
. . 3
⊢ ((((𝑁 · 𝐴) ∈ ℚ ∧ 1 ∈ ℚ)
∧ (𝑁 ∈ ℚ
∧ 0 < 𝑁)) →
((((𝑁 · 𝐴) mod 𝑁) + 1) mod 𝑁) = (((𝑁 · 𝐴) + 1) mod 𝑁)) |
36 | 31, 34, 10, 20, 35 | syl22anc 1234 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → ((((𝑁 · 𝐴) mod 𝑁) + 1) mod 𝑁) = (((𝑁 · 𝐴) + 1) mod 𝑁)) |
37 | | eluz2gt1 9561 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 < 𝑁) |
38 | 37 | adantl 275 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → 1 < 𝑁) |
39 | | q1mod 10312 |
. . 3
⊢ ((𝑁 ∈ ℚ ∧ 1 <
𝑁) → (1 mod 𝑁) = 1) |
40 | 10, 38, 39 | syl2anc 409 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → (1 mod 𝑁) = 1) |
41 | 27, 36, 40 | 3eqtr3d 2211 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘2)) → (((𝑁 · 𝐴) + 1) mod 𝑁) = 1) |