Proof of Theorem difmodm1lt
Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . 4
⊢ (((𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → (𝐴 mod 𝑁) = 1) |
2 | | zre 12180 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
3 | 2 | 3ad2ant1 1135 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → 𝐴 ∈ ℝ) |
4 | | nnre 11837 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
5 | 4 | 3ad2ant2 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → 𝑁 ∈ ℝ) |
6 | | 1lt2 12001 |
. . . . . . . . . . 11
⊢ 1 <
2 |
7 | | 1red 10834 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) |
8 | | 2re 11904 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ |
9 | 8 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ) |
10 | 7, 9, 4 | 3jca 1130 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (1 ∈
ℝ ∧ 2 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
11 | | lttr 10909 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((1 < 2 ∧ 2
< 𝑁) → 1 < 𝑁)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((1 <
2 ∧ 2 < 𝑁) → 1
< 𝑁)) |
13 | 6, 12 | mpani 696 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (2 <
𝑁 → 1 < 𝑁)) |
14 | 13 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ → (𝑁 ∈ ℕ → (2 <
𝑁 → 1 < 𝑁))) |
15 | 14 | 3imp 1113 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → 1 < 𝑁) |
16 | 3, 5, 15 | 3jca 1130 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → (𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁)) |
17 | 16 | adantl 485 |
. . . . . 6
⊢ (((𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → (𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 < 𝑁)) |
18 | | m1mod0mod1 44494 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → (((𝐴 − 1) mod 𝑁) = 0 ↔ (𝐴 mod 𝑁) = 1)) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ (((𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → (((𝐴 − 1) mod 𝑁) = 0 ↔ (𝐴 mod 𝑁) = 1)) |
20 | 1, 19 | mpbird 260 |
. . . 4
⊢ (((𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → ((𝐴 − 1) mod 𝑁) = 0) |
21 | 1, 20 | oveq12d 7231 |
. . 3
⊢ (((𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) = (1 − 0)) |
22 | | df-2 11893 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
23 | 22 | breq1i 5060 |
. . . . . . . . 9
⊢ (2 <
𝑁 ↔ (1 + 1) < 𝑁) |
24 | 23 | biimpi 219 |
. . . . . . . 8
⊢ (2 <
𝑁 → (1 + 1) < 𝑁) |
25 | 24 | adantl 485 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → (1 + 1) <
𝑁) |
26 | | 1red 10834 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → 1 ∈
ℝ) |
27 | 4 | adantr 484 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → 𝑁 ∈ ℝ) |
28 | 26, 26, 27 | ltaddsub2d 11433 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → ((1 + 1) <
𝑁 ↔ 1 < (𝑁 − 1))) |
29 | 25, 28 | mpbid 235 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → 1 < (𝑁 − 1)) |
30 | | 1m0e1 11951 |
. . . . . . 7
⊢ (1
− 0) = 1 |
31 | 30 | breq1i 5060 |
. . . . . 6
⊢ ((1
− 0) < (𝑁 −
1) ↔ 1 < (𝑁 −
1)) |
32 | 29, 31 | sylibr 237 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → (1 − 0)
< (𝑁 −
1)) |
33 | 32 | 3adant1 1132 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → (1 − 0)
< (𝑁 −
1)) |
34 | 33 | adantl 485 |
. . 3
⊢ (((𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → (1 − 0) <
(𝑁 −
1)) |
35 | 21, 34 | eqbrtrd 5075 |
. 2
⊢ (((𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) < (𝑁 − 1)) |
36 | | zmodfz 13466 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 mod 𝑁) ∈ (0...(𝑁 − 1))) |
37 | 36 | 3adant3 1134 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → (𝐴 mod 𝑁) ∈ (0...(𝑁 − 1))) |
38 | | elfzle2 13116 |
. . . . . 6
⊢ ((𝐴 mod 𝑁) ∈ (0...(𝑁 − 1)) → (𝐴 mod 𝑁) ≤ (𝑁 − 1)) |
39 | 37, 38 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → (𝐴 mod 𝑁) ≤ (𝑁 − 1)) |
40 | 39 | adantl 485 |
. . . 4
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → (𝐴 mod 𝑁) ≤ (𝑁 − 1)) |
41 | | nnrp 12597 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
42 | 41 | 3ad2ant2 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → 𝑁 ∈
ℝ+) |
43 | 3, 42 | modcld 13448 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → (𝐴 mod 𝑁) ∈ ℝ) |
44 | | peano2rem 11145 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
45 | 4, 44 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℝ) |
46 | 45 | 3ad2ant2 1136 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → (𝑁 − 1) ∈
ℝ) |
47 | | peano2zm 12220 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → (𝐴 − 1) ∈
ℤ) |
48 | 47 | zred 12282 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ → (𝐴 − 1) ∈
ℝ) |
49 | 48 | 3ad2ant1 1135 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → (𝐴 − 1) ∈
ℝ) |
50 | 49, 42 | modcld 13448 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → ((𝐴 − 1) mod 𝑁) ∈
ℝ) |
51 | 43, 46, 50 | 3jca 1130 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → ((𝐴 mod 𝑁) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ ((𝐴 − 1) mod 𝑁) ∈
ℝ)) |
52 | 51 | adantl 485 |
. . . . 5
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → ((𝐴 mod 𝑁) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ ((𝐴 − 1) mod 𝑁) ∈
ℝ)) |
53 | | lesub1 11326 |
. . . . 5
⊢ (((𝐴 mod 𝑁) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ ((𝐴 − 1) mod 𝑁) ∈ ℝ) → ((𝐴 mod 𝑁) ≤ (𝑁 − 1) ↔ ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) ≤ ((𝑁 − 1) − ((𝐴 − 1) mod 𝑁)))) |
54 | 52, 53 | syl 17 |
. . . 4
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → ((𝐴 mod 𝑁) ≤ (𝑁 − 1) ↔ ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) ≤ ((𝑁 − 1) − ((𝐴 − 1) mod 𝑁)))) |
55 | 40, 54 | mpbid 235 |
. . 3
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) ≤ ((𝑁 − 1) − ((𝐴 − 1) mod 𝑁))) |
56 | 49, 42 | jca 515 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → ((𝐴 − 1) ∈ ℝ ∧
𝑁 ∈
ℝ+)) |
57 | 56 | adantl 485 |
. . . . . . 7
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → ((𝐴 − 1) ∈ ℝ ∧ 𝑁 ∈
ℝ+)) |
58 | | modge0 13452 |
. . . . . . 7
⊢ (((𝐴 − 1) ∈ ℝ ∧
𝑁 ∈
ℝ+) → 0 ≤ ((𝐴 − 1) mod 𝑁)) |
59 | 57, 58 | syl 17 |
. . . . . 6
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → 0 ≤ ((𝐴 − 1) mod 𝑁)) |
60 | 16, 18 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → (((𝐴 − 1) mod 𝑁) = 0 ↔ (𝐴 mod 𝑁) = 1)) |
61 | 60 | bicomd 226 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → ((𝐴 mod 𝑁) = 1 ↔ ((𝐴 − 1) mod 𝑁) = 0)) |
62 | 61 | notbid 321 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → (¬ (𝐴 mod 𝑁) = 1 ↔ ¬ ((𝐴 − 1) mod 𝑁) = 0)) |
63 | 62 | biimpac 482 |
. . . . . . 7
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → ¬ ((𝐴 − 1) mod 𝑁) = 0) |
64 | 63 | neqned 2947 |
. . . . . 6
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → ((𝐴 − 1) mod 𝑁) ≠ 0) |
65 | 59, 64 | jca 515 |
. . . . 5
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → (0 ≤ ((𝐴 − 1) mod 𝑁) ∧ ((𝐴 − 1) mod 𝑁) ≠ 0)) |
66 | | 0red 10836 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → 0 ∈
ℝ) |
67 | 66, 50 | jca 515 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → (0 ∈ ℝ
∧ ((𝐴 − 1) mod
𝑁) ∈
ℝ)) |
68 | 67 | adantl 485 |
. . . . . 6
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → (0 ∈ ℝ
∧ ((𝐴 − 1) mod
𝑁) ∈
ℝ)) |
69 | | ltlen 10933 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ ((𝐴
− 1) mod 𝑁) ∈
ℝ) → (0 < ((𝐴
− 1) mod 𝑁) ↔ (0
≤ ((𝐴 − 1) mod
𝑁) ∧ ((𝐴 − 1) mod 𝑁) ≠ 0))) |
70 | 68, 69 | syl 17 |
. . . . 5
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → (0 < ((𝐴 − 1) mod 𝑁) ↔ (0 ≤ ((𝐴 − 1) mod 𝑁) ∧ ((𝐴 − 1) mod 𝑁) ≠ 0))) |
71 | 65, 70 | mpbird 260 |
. . . 4
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → 0 < ((𝐴 − 1) mod 𝑁)) |
72 | 50, 46 | jca 515 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → (((𝐴 − 1) mod 𝑁) ∈ ℝ ∧ (𝑁 − 1) ∈
ℝ)) |
73 | 72 | adantl 485 |
. . . . 5
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → (((𝐴 − 1) mod 𝑁) ∈ ℝ ∧ (𝑁 − 1) ∈
ℝ)) |
74 | | ltsubpos 11324 |
. . . . 5
⊢ ((((𝐴 − 1) mod 𝑁) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ)
→ (0 < ((𝐴 −
1) mod 𝑁) ↔ ((𝑁 − 1) − ((𝐴 − 1) mod 𝑁)) < (𝑁 − 1))) |
75 | 73, 74 | syl 17 |
. . . 4
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → (0 < ((𝐴 − 1) mod 𝑁) ↔ ((𝑁 − 1) − ((𝐴 − 1) mod 𝑁)) < (𝑁 − 1))) |
76 | 71, 75 | mpbid 235 |
. . 3
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → ((𝑁 − 1) − ((𝐴 − 1) mod 𝑁)) < (𝑁 − 1)) |
77 | 43, 50 | resubcld 11260 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) ∈ ℝ) |
78 | 46, 50 | resubcld 11260 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → ((𝑁 − 1) − ((𝐴 − 1) mod 𝑁)) ∈
ℝ) |
79 | 77, 78, 46 | 3jca 1130 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → (((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) ∈ ℝ ∧ ((𝑁 − 1) − ((𝐴 − 1) mod 𝑁)) ∈ ℝ ∧ (𝑁 − 1) ∈
ℝ)) |
80 | 79 | adantl 485 |
. . . 4
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → (((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) ∈ ℝ ∧ ((𝑁 − 1) − ((𝐴 − 1) mod 𝑁)) ∈ ℝ ∧ (𝑁 − 1) ∈
ℝ)) |
81 | | lelttr 10923 |
. . . 4
⊢ ((((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) ∈ ℝ ∧ ((𝑁 − 1) − ((𝐴 − 1) mod 𝑁)) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ) → ((((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) ≤ ((𝑁 − 1) − ((𝐴 − 1) mod 𝑁)) ∧ ((𝑁 − 1) − ((𝐴 − 1) mod 𝑁)) < (𝑁 − 1)) → ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) < (𝑁 − 1))) |
82 | 80, 81 | syl 17 |
. . 3
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → ((((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) ≤ ((𝑁 − 1) − ((𝐴 − 1) mod 𝑁)) ∧ ((𝑁 − 1) − ((𝐴 − 1) mod 𝑁)) < (𝑁 − 1)) → ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) < (𝑁 − 1))) |
83 | 55, 76, 82 | mp2and 699 |
. 2
⊢ ((¬
(𝐴 mod 𝑁) = 1 ∧ (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁)) → ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) < (𝑁 − 1)) |
84 | 35, 83 | pm2.61ian 812 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 <
𝑁) → ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) < (𝑁 − 1)) |