Proof of Theorem fldivp1
Step | Hyp | Ref
| Expression |
1 | | nnz 9224 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
2 | | nnne0 8899 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
3 | | peano2z 9241 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈
ℤ) |
4 | 3 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 1) ∈
ℤ) |
5 | | dvdsval2 11745 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ (𝑀 + 1) ∈ ℤ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) / 𝑁) ∈ ℤ)) |
6 | 1, 2, 4, 5 | syl2an23an 1294 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) / 𝑁) ∈ ℤ)) |
7 | 6 | biimpa 294 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑀 + 1) / 𝑁) ∈ ℤ) |
8 | | flid 10233 |
. . . . . . 7
⊢ (((𝑀 + 1) / 𝑁) ∈ ℤ →
(⌊‘((𝑀 + 1) /
𝑁)) = ((𝑀 + 1) / 𝑁)) |
9 | 7, 8 | syl 14 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 + 1) / 𝑁)) = ((𝑀 + 1) / 𝑁)) |
10 | | nnm1nn0 9169 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
11 | 10 | nn0red 9182 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℝ) |
12 | 10 | nn0ge0d 9184 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 ≤
(𝑁 −
1)) |
13 | | nnre 8878 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
14 | | nngt0 8896 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
15 | | divge0 8782 |
. . . . . . . . 9
⊢ ((((𝑁 − 1) ∈ ℝ ∧
0 ≤ (𝑁 − 1)) ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → 0 ≤
((𝑁 − 1) / 𝑁)) |
16 | 11, 12, 13, 14, 15 | syl22anc 1234 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 ≤
((𝑁 − 1) / 𝑁)) |
17 | 16 | ad2antlr 486 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → 0 ≤ ((𝑁 − 1) / 𝑁)) |
18 | 13 | ltm1d 8841 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁) |
19 | | nncn 8879 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
20 | 19 | mulid1d 7930 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 · 1) = 𝑁) |
21 | 18, 20 | breqtrrd 4015 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < (𝑁 · 1)) |
22 | | 1red 7928 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) |
23 | | ltdivmul 8785 |
. . . . . . . . . 10
⊢ (((𝑁 − 1) ∈ ℝ ∧
1 ∈ ℝ ∧ (𝑁
∈ ℝ ∧ 0 < 𝑁)) → (((𝑁 − 1) / 𝑁) < 1 ↔ (𝑁 − 1) < (𝑁 · 1))) |
24 | 11, 22, 13, 14, 23 | syl112anc 1237 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) / 𝑁) < 1 ↔ (𝑁 − 1) < (𝑁 · 1))) |
25 | 21, 24 | mpbird 166 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) / 𝑁) < 1) |
26 | 25 | ad2antlr 486 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑁 − 1) / 𝑁) < 1) |
27 | 10 | nn0zd 9325 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℤ) |
28 | | znq 9576 |
. . . . . . . . . 10
⊢ (((𝑁 − 1) ∈ ℤ ∧
𝑁 ∈ ℕ) →
((𝑁 − 1) / 𝑁) ∈
ℚ) |
29 | 27, 28 | mpancom 420 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) / 𝑁) ∈ ℚ) |
30 | 29 | ad2antlr 486 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑁 − 1) / 𝑁) ∈ ℚ) |
31 | | flqbi2 10240 |
. . . . . . . 8
⊢ ((((𝑀 + 1) / 𝑁) ∈ ℤ ∧ ((𝑁 − 1) / 𝑁) ∈ ℚ) →
((⌊‘(((𝑀 + 1) /
𝑁) + ((𝑁 − 1) / 𝑁))) = ((𝑀 + 1) / 𝑁) ↔ (0 ≤ ((𝑁 − 1) / 𝑁) ∧ ((𝑁 − 1) / 𝑁) < 1))) |
32 | 7, 30, 31 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = ((𝑀 + 1) / 𝑁) ↔ (0 ≤ ((𝑁 − 1) / 𝑁) ∧ ((𝑁 − 1) / 𝑁) < 1))) |
33 | 17, 26, 32 | mpbir2and 939 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = ((𝑀 + 1) / 𝑁)) |
34 | 9, 33 | eqtr4d 2206 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 + 1) / 𝑁)) = (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)))) |
35 | | zcn 9210 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
36 | 35 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℂ) |
37 | 19 | adantl 275 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
38 | | nnap0 8900 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 # 0) |
39 | 38 | adantl 275 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 # 0) |
40 | 36, 37, 37, 39 | divdirapd 8739 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 𝑁) / 𝑁) = ((𝑀 / 𝑁) + (𝑁 / 𝑁))) |
41 | | ax-1cn 7860 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
42 | 41 | a1i 9 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 1 ∈
ℂ) |
43 | 36, 42, 37 | ppncand 8263 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) + (𝑁 − 1)) = (𝑀 + 𝑁)) |
44 | 43 | oveq1d 5866 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) + (𝑁 − 1)) / 𝑁) = ((𝑀 + 𝑁) / 𝑁)) |
45 | 4 | zcnd 9328 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 1) ∈
ℂ) |
46 | | subcl 8111 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 −
1) ∈ ℂ) |
47 | 19, 41, 46 | sylancl 411 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℂ) |
48 | 47 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) ∈
ℂ) |
49 | 45, 48, 37, 39 | divdirapd 8739 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) + (𝑁 − 1)) / 𝑁) = (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) |
50 | 44, 49 | eqtr3d 2205 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 𝑁) / 𝑁) = (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) |
51 | 37, 39 | dividapd 8696 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 / 𝑁) = 1) |
52 | 51 | oveq2d 5867 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) + (𝑁 / 𝑁)) = ((𝑀 / 𝑁) + 1)) |
53 | 40, 50, 52 | 3eqtr3d 2211 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)) = ((𝑀 / 𝑁) + 1)) |
54 | 53 | fveq2d 5498 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘(((𝑀 + 1) /
𝑁) + ((𝑁 − 1) / 𝑁))) = (⌊‘((𝑀 / 𝑁) + 1))) |
55 | 54 | adantr 274 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = (⌊‘((𝑀 / 𝑁) + 1))) |
56 | | znq 9576 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℚ) |
57 | | 1z 9231 |
. . . . . . 7
⊢ 1 ∈
ℤ |
58 | | flqaddz 10246 |
. . . . . . 7
⊢ (((𝑀 / 𝑁) ∈ ℚ ∧ 1 ∈ ℤ)
→ (⌊‘((𝑀 /
𝑁) + 1)) =
((⌊‘(𝑀 / 𝑁)) + 1)) |
59 | 56, 57, 58 | sylancl 411 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑀 / 𝑁) + 1)) = ((⌊‘(𝑀 / 𝑁)) + 1)) |
60 | 59 | adantr 274 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 / 𝑁) + 1)) = ((⌊‘(𝑀 / 𝑁)) + 1)) |
61 | 34, 55, 60 | 3eqtrrd 2208 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘(𝑀 / 𝑁)) + 1) = (⌊‘((𝑀 + 1) / 𝑁))) |
62 | | znq 9576 |
. . . . . . . . 9
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) / 𝑁) ∈ ℚ) |
63 | 3, 62 | sylan 281 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) / 𝑁) ∈ ℚ) |
64 | 63 | flqcld 10226 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑀 + 1) /
𝑁)) ∈
ℤ) |
65 | 64 | zcnd 9328 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑀 + 1) /
𝑁)) ∈
ℂ) |
66 | 56 | flqcld 10226 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝑀 / 𝑁)) ∈
ℤ) |
67 | 66 | zcnd 9328 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝑀 / 𝑁)) ∈
ℂ) |
68 | 65, 67, 42 | subaddd 8241 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(((⌊‘((𝑀 + 1) /
𝑁)) −
(⌊‘(𝑀 / 𝑁))) = 1 ↔
((⌊‘(𝑀 / 𝑁)) + 1) = (⌊‘((𝑀 + 1) / 𝑁)))) |
69 | 68 | adantr 274 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 1 ↔ ((⌊‘(𝑀 / 𝑁)) + 1) = (⌊‘((𝑀 + 1) / 𝑁)))) |
70 | 61, 69 | mpbird 166 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 1) |
71 | | iftrue 3530 |
. . . 4
⊢ (𝑁 ∥ (𝑀 + 1) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 1) |
72 | 71 | adantl 275 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 1) |
73 | 70, 72 | eqtr4d 2206 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0)) |
74 | | zmodcl 10293 |
. . . . . . . . . . 11
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈
ℕ0) |
75 | 3, 74 | sylan 281 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈
ℕ0) |
76 | 75 | nn0red 9182 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈ ℝ) |
77 | | 1re 7912 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
78 | | resubcl 8176 |
. . . . . . . . 9
⊢ ((((𝑀 + 1) mod 𝑁) ∈ ℝ ∧ 1 ∈ ℝ)
→ (((𝑀 + 1) mod 𝑁) − 1) ∈
ℝ) |
79 | 76, 77, 78 | sylancl 411 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) ∈
ℝ) |
80 | 79 | adantr 274 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → (((𝑀 + 1) mod 𝑁) − 1) ∈
ℝ) |
81 | 75 | nn0zd 9325 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈ ℤ) |
82 | | elnndc 9564 |
. . . . . . . . . . . 12
⊢ (((𝑀 + 1) mod 𝑁) ∈ ℤ → DECID
((𝑀 + 1) mod 𝑁) ∈
ℕ) |
83 | 81, 82 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
DECID ((𝑀 +
1) mod 𝑁) ∈
ℕ) |
84 | | elnn0 9130 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 + 1) mod 𝑁) ∈ ℕ0 ↔ (((𝑀 + 1) mod 𝑁) ∈ ℕ ∨ ((𝑀 + 1) mod 𝑁) = 0)) |
85 | 75, 84 | sylib 121 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) ∈ ℕ ∨ ((𝑀 + 1) mod 𝑁) = 0)) |
86 | 85 | ord 719 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (¬
((𝑀 + 1) mod 𝑁) ∈ ℕ → ((𝑀 + 1) mod 𝑁) = 0)) |
87 | | id 19 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
88 | | dvdsval3 11746 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑀 + 1) ∈ ℤ) →
(𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) mod 𝑁) = 0)) |
89 | 87, 3, 88 | syl2anr 288 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) mod 𝑁) = 0)) |
90 | 86, 89 | sylibrd 168 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (¬
((𝑀 + 1) mod 𝑁) ∈ ℕ → 𝑁 ∥ (𝑀 + 1))) |
91 | | con1dc 851 |
. . . . . . . . . . 11
⊢
(DECID ((𝑀 + 1) mod 𝑁) ∈ ℕ → ((¬ ((𝑀 + 1) mod 𝑁) ∈ ℕ → 𝑁 ∥ (𝑀 + 1)) → (¬ 𝑁 ∥ (𝑀 + 1) → ((𝑀 + 1) mod 𝑁) ∈ ℕ))) |
92 | 83, 90, 91 | sylc 62 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (¬
𝑁 ∥ (𝑀 + 1) → ((𝑀 + 1) mod 𝑁) ∈ ℕ)) |
93 | 92 | imp 123 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → ((𝑀 + 1) mod 𝑁) ∈ ℕ) |
94 | | nnm1nn0 9169 |
. . . . . . . . 9
⊢ (((𝑀 + 1) mod 𝑁) ∈ ℕ → (((𝑀 + 1) mod 𝑁) − 1) ∈
ℕ0) |
95 | 93, 94 | syl 14 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → (((𝑀 + 1) mod 𝑁) − 1) ∈
ℕ0) |
96 | 95 | nn0ge0d 9184 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → 0 ≤ (((𝑀 + 1) mod 𝑁) − 1)) |
97 | 13, 14 | jca 304 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 0 <
𝑁)) |
98 | 97 | ad2antlr 486 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → (𝑁 ∈ ℝ ∧ 0 < 𝑁)) |
99 | | divge0 8782 |
. . . . . . 7
⊢
((((((𝑀 + 1) mod
𝑁) − 1) ∈
ℝ ∧ 0 ≤ (((𝑀 +
1) mod 𝑁) − 1)) ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → 0 ≤
((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) |
100 | 80, 96, 98, 99 | syl21anc 1232 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → 0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) |
101 | 13 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) |
102 | 76 | ltm1d 8841 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < ((𝑀 + 1) mod 𝑁)) |
103 | | zq 9578 |
. . . . . . . . . . . . 13
⊢ ((𝑀 + 1) ∈ ℤ →
(𝑀 + 1) ∈
ℚ) |
104 | 3, 103 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈
ℚ) |
105 | 104 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 1) ∈
ℚ) |
106 | | nnq 9585 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℚ) |
107 | 106 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℚ) |
108 | 14 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 0 <
𝑁) |
109 | | modqlt 10282 |
. . . . . . . . . . 11
⊢ (((𝑀 + 1) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 <
𝑁) → ((𝑀 + 1) mod 𝑁) < 𝑁) |
110 | 105, 107,
108, 109 | syl3anc 1233 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) < 𝑁) |
111 | 79, 76, 101, 102, 110 | lttrd 8038 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < 𝑁) |
112 | 37 | mulid1d 7930 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 1) = 𝑁) |
113 | 111, 112 | breqtrrd 4015 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < (𝑁 · 1)) |
114 | | 1red 7928 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 1 ∈
ℝ) |
115 | | ltdivmul 8785 |
. . . . . . . . 9
⊢
(((((𝑀 + 1) mod
𝑁) − 1) ∈
ℝ ∧ 1 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1 ↔ (((𝑀 + 1) mod 𝑁) − 1) < (𝑁 · 1))) |
116 | 79, 114, 101, 108, 115 | syl112anc 1237 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1 ↔ (((𝑀 + 1) mod 𝑁) − 1) < (𝑁 · 1))) |
117 | 113, 116 | mpbird 166 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1) |
118 | 117 | adantr 274 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1) |
119 | | peano2zm 9243 |
. . . . . . . . . 10
⊢ (((𝑀 + 1) mod 𝑁) ∈ ℤ → (((𝑀 + 1) mod 𝑁) − 1) ∈
ℤ) |
120 | 81, 119 | syl 14 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) ∈
ℤ) |
121 | | znq 9576 |
. . . . . . . . 9
⊢
(((((𝑀 + 1) mod
𝑁) − 1) ∈
ℤ ∧ 𝑁 ∈
ℕ) → ((((𝑀 + 1)
mod 𝑁) − 1) / 𝑁) ∈
ℚ) |
122 | 120, 121 | sylancom 418 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℚ) |
123 | | flqbi2 10240 |
. . . . . . . 8
⊢
(((⌊‘((𝑀
+ 1) / 𝑁)) ∈ ℤ
∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℚ) →
((⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁)) ↔ (0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1))) |
124 | 64, 122, 123 | syl2anc 409 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁)) ↔ (0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1))) |
125 | 124 | adantr 274 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
((⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁)) ↔ (0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1))) |
126 | 100, 118,
125 | mpbir2and 939 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
(⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁))) |
127 | | modqval 10273 |
. . . . . . . . . . . . 13
⊢ (((𝑀 + 1) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 <
𝑁) → ((𝑀 + 1) mod 𝑁) = ((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁))))) |
128 | 105, 107,
108, 127 | syl3anc 1233 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) = ((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁))))) |
129 | 128 | oveq1d 5866 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) = (((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) − 1)) |
130 | 37, 65 | mulcld 7933 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) ∈ ℂ) |
131 | 45, 42, 130 | sub32d 8255 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) − 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) = (((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) − 1)) |
132 | | pncan 8118 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 1) = 𝑀) |
133 | 36, 41, 132 | sylancl 411 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) − 1) = 𝑀) |
134 | 133 | oveq1d 5866 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) − 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) = (𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁))))) |
135 | 129, 131,
134 | 3eqtr2d 2209 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) = (𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁))))) |
136 | 135 | oveq1d 5866 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) = ((𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) / 𝑁)) |
137 | 36, 130, 37, 39 | divsubdirapd 8740 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) / 𝑁) = ((𝑀 / 𝑁) − ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁))) |
138 | 65, 37, 39 | divcanap3d 8705 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁) = (⌊‘((𝑀 + 1) / 𝑁))) |
139 | 138 | oveq2d 5867 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) − ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁)) = ((𝑀 / 𝑁) − (⌊‘((𝑀 + 1) / 𝑁)))) |
140 | 136, 137,
139 | 3eqtrrd 2208 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) − (⌊‘((𝑀 + 1) / 𝑁))) = ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) |
141 | | zre 9209 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
142 | | nndivre 8907 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℝ) |
143 | 141, 142 | sylan 281 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℝ) |
144 | 143 | recnd 7941 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℂ) |
145 | | nndivre 8907 |
. . . . . . . . . . 11
⊢
(((((𝑀 + 1) mod
𝑁) − 1) ∈
ℝ ∧ 𝑁 ∈
ℕ) → ((((𝑀 + 1)
mod 𝑁) − 1) / 𝑁) ∈
ℝ) |
146 | 79, 145 | sylancom 418 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℝ) |
147 | 146 | recnd 7941 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℂ) |
148 | 144, 65, 147 | subaddd 8241 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 / 𝑁) − (⌊‘((𝑀 + 1) / 𝑁))) = ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ↔ ((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) = (𝑀 / 𝑁))) |
149 | 140, 148 | mpbid 146 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((⌊‘((𝑀 + 1) /
𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) = (𝑀 / 𝑁)) |
150 | 149 | adantr 274 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
((⌊‘((𝑀 + 1) /
𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) = (𝑀 / 𝑁)) |
151 | 150 | fveq2d 5498 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
(⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘(𝑀 / 𝑁))) |
152 | 126, 151 | eqtr3d 2205 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
(⌊‘((𝑀 + 1) /
𝑁)) = (⌊‘(𝑀 / 𝑁))) |
153 | 65, 67 | subeq0ad 8233 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(((⌊‘((𝑀 + 1) /
𝑁)) −
(⌊‘(𝑀 / 𝑁))) = 0 ↔
(⌊‘((𝑀 + 1) /
𝑁)) = (⌊‘(𝑀 / 𝑁)))) |
154 | 153 | adantr 274 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
(((⌊‘((𝑀 + 1) /
𝑁)) −
(⌊‘(𝑀 / 𝑁))) = 0 ↔
(⌊‘((𝑀 + 1) /
𝑁)) = (⌊‘(𝑀 / 𝑁)))) |
155 | 152, 154 | mpbird 166 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
((⌊‘((𝑀 + 1) /
𝑁)) −
(⌊‘(𝑀 / 𝑁))) = 0) |
156 | | iffalse 3533 |
. . . 4
⊢ (¬
𝑁 ∥ (𝑀 + 1) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 0) |
157 | 156 | adantl 275 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 0) |
158 | 155, 157 | eqtr4d 2206 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
((⌊‘((𝑀 + 1) /
𝑁)) −
(⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0)) |
159 | | simpr 109 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ) |
160 | | dvdsdc 11753 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑀 + 1) ∈ ℤ) →
DECID 𝑁
∥ (𝑀 +
1)) |
161 | 159, 4, 160 | syl2anc 409 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
DECID 𝑁
∥ (𝑀 +
1)) |
162 | | exmiddc 831 |
. . 3
⊢
(DECID 𝑁 ∥ (𝑀 + 1) → (𝑁 ∥ (𝑀 + 1) ∨ ¬ 𝑁 ∥ (𝑀 + 1))) |
163 | 161, 162 | syl 14 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ (𝑀 + 1) ∨ ¬ 𝑁 ∥ (𝑀 + 1))) |
164 | 73, 158, 163 | mpjaodan 793 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((⌊‘((𝑀 + 1) /
𝑁)) −
(⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0)) |