Proof of Theorem p1modz1
Step | Hyp | Ref
| Expression |
1 | | dvdszrcl 11754 |
. . 3
⊢ (𝑀 ∥ 𝐴 → (𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ)) |
2 | | 0red 7921 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 1 <
𝑀) → 0 ∈
ℝ) |
3 | | 1red 7935 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 1 <
𝑀) → 1 ∈
ℝ) |
4 | | zre 9216 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
5 | 4 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 1 <
𝑀) → 𝑀 ∈ ℝ) |
6 | 2, 3, 5 | 3jca 1172 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 1 <
𝑀) → (0 ∈ ℝ
∧ 1 ∈ ℝ ∧ 𝑀 ∈ ℝ)) |
7 | | 0lt1 8046 |
. . . . . . . . . . . . . . 15
⊢ 0 <
1 |
8 | 7 | a1i 9 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℤ → 0 <
1) |
9 | 8 | anim1i 338 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 1 <
𝑀) → (0 < 1 ∧ 1
< 𝑀)) |
10 | | lttr 7993 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((0 < 1 ∧ 1
< 𝑀) → 0 < 𝑀)) |
11 | 6, 9, 10 | sylc 62 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 1 <
𝑀) → 0 < 𝑀) |
12 | 11 | ex 114 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → (1 <
𝑀 → 0 < 𝑀)) |
13 | | elnnz 9222 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℤ ∧ 0 <
𝑀)) |
14 | 13 | simplbi2 383 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → (0 <
𝑀 → 𝑀 ∈ ℕ)) |
15 | 12, 14 | syld 45 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → (1 <
𝑀 → 𝑀 ∈ ℕ)) |
16 | 15 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (1 <
𝑀 → 𝑀 ∈ ℕ)) |
17 | 16 | imp 123 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 1 <
𝑀) → 𝑀 ∈ ℕ) |
18 | | dvdsmod0 11755 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑀 ∥ 𝐴) → (𝐴 mod 𝑀) = 0) |
19 | 17, 18 | sylan 281 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 1 <
𝑀) ∧ 𝑀 ∥ 𝐴) → (𝐴 mod 𝑀) = 0) |
20 | 19 | ex 114 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 1 <
𝑀) → (𝑀 ∥ 𝐴 → (𝐴 mod 𝑀) = 0)) |
21 | | oveq1 5860 |
. . . . . . . . . . 11
⊢ ((𝐴 mod 𝑀) = 0 → ((𝐴 mod 𝑀) + 1) = (0 + 1)) |
22 | | 0p1e1 8992 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
23 | 21, 22 | eqtrdi 2219 |
. . . . . . . . . 10
⊢ ((𝐴 mod 𝑀) = 0 → ((𝐴 mod 𝑀) + 1) = 1) |
24 | 23 | oveq1d 5868 |
. . . . . . . . 9
⊢ ((𝐴 mod 𝑀) = 0 → (((𝐴 mod 𝑀) + 1) mod 𝑀) = (1 mod 𝑀)) |
25 | 24 | adantl 275 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 1 <
𝑀) ∧ (𝐴 mod 𝑀) = 0) → (((𝐴 mod 𝑀) + 1) mod 𝑀) = (1 mod 𝑀)) |
26 | | zq 9585 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℚ) |
27 | 26 | ad3antlr 490 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 1 <
𝑀) ∧ (𝐴 mod 𝑀) = 0) → 𝐴 ∈ ℚ) |
28 | | 1z 9238 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
29 | | zq 9585 |
. . . . . . . . . 10
⊢ (1 ∈
ℤ → 1 ∈ ℚ) |
30 | 28, 29 | mp1i 10 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 1 <
𝑀) ∧ (𝐴 mod 𝑀) = 0) → 1 ∈
ℚ) |
31 | | zq 9585 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℚ) |
32 | 31 | ad3antrrr 489 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 1 <
𝑀) ∧ (𝐴 mod 𝑀) = 0) → 𝑀 ∈ ℚ) |
33 | 11 | ad4ant13 510 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 1 <
𝑀) ∧ (𝐴 mod 𝑀) = 0) → 0 < 𝑀) |
34 | | modqaddmod 10319 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℚ ∧ 1 ∈
ℚ) ∧ (𝑀 ∈
ℚ ∧ 0 < 𝑀))
→ (((𝐴 mod 𝑀) + 1) mod 𝑀) = ((𝐴 + 1) mod 𝑀)) |
35 | 27, 30, 32, 33, 34 | syl22anc 1234 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 1 <
𝑀) ∧ (𝐴 mod 𝑀) = 0) → (((𝐴 mod 𝑀) + 1) mod 𝑀) = ((𝐴 + 1) mod 𝑀)) |
36 | 31 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) → 𝑀 ∈
ℚ) |
37 | | q1mod 10312 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℚ ∧ 1 <
𝑀) → (1 mod 𝑀) = 1) |
38 | 36, 37 | sylan 281 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 1 <
𝑀) → (1 mod 𝑀) = 1) |
39 | 38 | adantr 274 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 1 <
𝑀) ∧ (𝐴 mod 𝑀) = 0) → (1 mod 𝑀) = 1) |
40 | 25, 35, 39 | 3eqtr3d 2211 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 1 <
𝑀) ∧ (𝐴 mod 𝑀) = 0) → ((𝐴 + 1) mod 𝑀) = 1) |
41 | 40 | ex 114 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 1 <
𝑀) → ((𝐴 mod 𝑀) = 0 → ((𝐴 + 1) mod 𝑀) = 1)) |
42 | 20, 41 | syld 45 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 1 <
𝑀) → (𝑀 ∥ 𝐴 → ((𝐴 + 1) mod 𝑀) = 1)) |
43 | 42 | ex 114 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (1 <
𝑀 → (𝑀 ∥ 𝐴 → ((𝐴 + 1) mod 𝑀) = 1))) |
44 | 43 | com23 78 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑀 ∥ 𝐴 → (1 < 𝑀 → ((𝐴 + 1) mod 𝑀) = 1))) |
45 | 1, 44 | mpcom 36 |
. 2
⊢ (𝑀 ∥ 𝐴 → (1 < 𝑀 → ((𝐴 + 1) mod 𝑀) = 1)) |
46 | 45 | imp 123 |
1
⊢ ((𝑀 ∥ 𝐴 ∧ 1 < 𝑀) → ((𝐴 + 1) mod 𝑀) = 1) |