Proof of Theorem fldivp1
Step | Hyp | Ref
| Expression |
1 | | nnz 11399 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
2 | 1 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℤ) |
3 | | nnne0 11053 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
4 | 3 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ≠ 0) |
5 | | peano2z 11418 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈
ℤ) |
6 | 5 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 1) ∈
ℤ) |
7 | | dvdsval2 14986 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ (𝑀 + 1) ∈ ℤ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) / 𝑁) ∈ ℤ)) |
8 | 2, 4, 6, 7 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) / 𝑁) ∈ ℤ)) |
9 | 8 | biimpa 501 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑀 + 1) / 𝑁) ∈ ℤ) |
10 | | flid 12609 |
. . . . . . 7
⊢ (((𝑀 + 1) / 𝑁) ∈ ℤ →
(⌊‘((𝑀 + 1) /
𝑁)) = ((𝑀 + 1) / 𝑁)) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 + 1) / 𝑁)) = ((𝑀 + 1) / 𝑁)) |
12 | | nnm1nn0 11334 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
13 | 12 | nn0red 11352 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℝ) |
14 | 12 | nn0ge0d 11354 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 ≤
(𝑁 −
1)) |
15 | | nnre 11027 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
16 | | nngt0 11049 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
17 | | divge0 10892 |
. . . . . . . . 9
⊢ ((((𝑁 − 1) ∈ ℝ ∧
0 ≤ (𝑁 − 1)) ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → 0 ≤
((𝑁 − 1) / 𝑁)) |
18 | 13, 14, 15, 16, 17 | syl22anc 1327 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 ≤
((𝑁 − 1) / 𝑁)) |
19 | 18 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → 0 ≤ ((𝑁 − 1) / 𝑁)) |
20 | 15 | ltm1d 10956 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁) |
21 | | nncn 11028 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
22 | 21 | mulid1d 10057 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 · 1) = 𝑁) |
23 | 20, 22 | breqtrrd 4681 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < (𝑁 · 1)) |
24 | | 1re 10039 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) |
26 | | ltdivmul 10898 |
. . . . . . . . . 10
⊢ (((𝑁 − 1) ∈ ℝ ∧
1 ∈ ℝ ∧ (𝑁
∈ ℝ ∧ 0 < 𝑁)) → (((𝑁 − 1) / 𝑁) < 1 ↔ (𝑁 − 1) < (𝑁 · 1))) |
27 | 13, 25, 15, 16, 26 | syl112anc 1330 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) / 𝑁) < 1 ↔ (𝑁 − 1) < (𝑁 · 1))) |
28 | 23, 27 | mpbird 247 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) / 𝑁) < 1) |
29 | 28 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑁 − 1) / 𝑁) < 1) |
30 | | nndivre 11056 |
. . . . . . . . . 10
⊢ (((𝑁 − 1) ∈ ℝ ∧
𝑁 ∈ ℕ) →
((𝑁 − 1) / 𝑁) ∈
ℝ) |
31 | 13, 30 | mpancom 703 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) / 𝑁) ∈ ℝ) |
32 | 31 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑁 − 1) / 𝑁) ∈ ℝ) |
33 | | flbi2 12618 |
. . . . . . . 8
⊢ ((((𝑀 + 1) / 𝑁) ∈ ℤ ∧ ((𝑁 − 1) / 𝑁) ∈ ℝ) →
((⌊‘(((𝑀 + 1) /
𝑁) + ((𝑁 − 1) / 𝑁))) = ((𝑀 + 1) / 𝑁) ↔ (0 ≤ ((𝑁 − 1) / 𝑁) ∧ ((𝑁 − 1) / 𝑁) < 1))) |
34 | 9, 32, 33 | syl2anc 693 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = ((𝑀 + 1) / 𝑁) ↔ (0 ≤ ((𝑁 − 1) / 𝑁) ∧ ((𝑁 − 1) / 𝑁) < 1))) |
35 | 19, 29, 34 | mpbir2and 957 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = ((𝑀 + 1) / 𝑁)) |
36 | 11, 35 | eqtr4d 2659 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 + 1) / 𝑁)) = (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)))) |
37 | | zcn 11382 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
38 | 37 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℂ) |
39 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
40 | 39 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 1 ∈
ℂ) |
41 | 21 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
42 | 38, 40, 41 | ppncand 10432 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) + (𝑁 − 1)) = (𝑀 + 𝑁)) |
43 | 42 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) + (𝑁 − 1)) / 𝑁) = ((𝑀 + 𝑁) / 𝑁)) |
44 | 6 | zcnd 11483 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 1) ∈
ℂ) |
45 | | subcl 10280 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 −
1) ∈ ℂ) |
46 | 21, 39, 45 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℂ) |
47 | 46 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) ∈
ℂ) |
48 | 44, 47, 41, 4 | divdird 10839 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) + (𝑁 − 1)) / 𝑁) = (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) |
49 | 43, 48 | eqtr3d 2658 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 𝑁) / 𝑁) = (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) |
50 | 38, 41, 41, 4 | divdird 10839 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 𝑁) / 𝑁) = ((𝑀 / 𝑁) + (𝑁 / 𝑁))) |
51 | 49, 50 | eqtr3d 2658 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)) = ((𝑀 / 𝑁) + (𝑁 / 𝑁))) |
52 | 41, 4 | dividd 10799 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 / 𝑁) = 1) |
53 | 52 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) + (𝑁 / 𝑁)) = ((𝑀 / 𝑁) + 1)) |
54 | 51, 53 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)) = ((𝑀 / 𝑁) + 1)) |
55 | 54 | fveq2d 6195 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘(((𝑀 + 1) /
𝑁) + ((𝑁 − 1) / 𝑁))) = (⌊‘((𝑀 / 𝑁) + 1))) |
56 | 55 | adantr 481 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = (⌊‘((𝑀 / 𝑁) + 1))) |
57 | | zre 11381 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
58 | | nndivre 11056 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℝ) |
59 | 57, 58 | sylan 488 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℝ) |
60 | | 1z 11407 |
. . . . . . 7
⊢ 1 ∈
ℤ |
61 | | fladdz 12626 |
. . . . . . 7
⊢ (((𝑀 / 𝑁) ∈ ℝ ∧ 1 ∈ ℤ)
→ (⌊‘((𝑀 /
𝑁) + 1)) =
((⌊‘(𝑀 / 𝑁)) + 1)) |
62 | 59, 60, 61 | sylancl 694 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑀 / 𝑁) + 1)) = ((⌊‘(𝑀 / 𝑁)) + 1)) |
63 | 62 | adantr 481 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 / 𝑁) + 1)) = ((⌊‘(𝑀 / 𝑁)) + 1)) |
64 | 36, 56, 63 | 3eqtrrd 2661 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘(𝑀 / 𝑁)) + 1) = (⌊‘((𝑀 + 1) / 𝑁))) |
65 | | zre 11381 |
. . . . . . . . . 10
⊢ ((𝑀 + 1) ∈ ℤ →
(𝑀 + 1) ∈
ℝ) |
66 | 5, 65 | syl 17 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈
ℝ) |
67 | | nndivre 11056 |
. . . . . . . . 9
⊢ (((𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) / 𝑁) ∈ ℝ) |
68 | 66, 67 | sylan 488 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) / 𝑁) ∈ ℝ) |
69 | 68 | flcld 12599 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑀 + 1) /
𝑁)) ∈
ℤ) |
70 | 69 | zcnd 11483 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑀 + 1) /
𝑁)) ∈
ℂ) |
71 | 59 | flcld 12599 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝑀 / 𝑁)) ∈
ℤ) |
72 | 71 | zcnd 11483 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝑀 / 𝑁)) ∈
ℂ) |
73 | 70, 72, 40 | subaddd 10410 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(((⌊‘((𝑀 + 1) /
𝑁)) −
(⌊‘(𝑀 / 𝑁))) = 1 ↔
((⌊‘(𝑀 / 𝑁)) + 1) = (⌊‘((𝑀 + 1) / 𝑁)))) |
74 | 73 | adantr 481 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 1 ↔ ((⌊‘(𝑀 / 𝑁)) + 1) = (⌊‘((𝑀 + 1) / 𝑁)))) |
75 | 64, 74 | mpbird 247 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 1) |
76 | | iftrue 4092 |
. . . 4
⊢ (𝑁 ∥ (𝑀 + 1) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 1) |
77 | 76 | adantl 482 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 1) |
78 | 75, 77 | eqtr4d 2659 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0)) |
79 | | zmodcl 12690 |
. . . . . . . . . . 11
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈
ℕ0) |
80 | 5, 79 | sylan 488 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈
ℕ0) |
81 | 80 | nn0red 11352 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈ ℝ) |
82 | | resubcl 10345 |
. . . . . . . . 9
⊢ ((((𝑀 + 1) mod 𝑁) ∈ ℝ ∧ 1 ∈ ℝ)
→ (((𝑀 + 1) mod 𝑁) − 1) ∈
ℝ) |
83 | 81, 24, 82 | sylancl 694 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) ∈
ℝ) |
84 | 83 | adantr 481 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → (((𝑀 + 1) mod 𝑁) − 1) ∈
ℝ) |
85 | | elnn0 11294 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 + 1) mod 𝑁) ∈ ℕ0 ↔ (((𝑀 + 1) mod 𝑁) ∈ ℕ ∨ ((𝑀 + 1) mod 𝑁) = 0)) |
86 | 80, 85 | sylib 208 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) ∈ ℕ ∨ ((𝑀 + 1) mod 𝑁) = 0)) |
87 | 86 | ord 392 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (¬
((𝑀 + 1) mod 𝑁) ∈ ℕ → ((𝑀 + 1) mod 𝑁) = 0)) |
88 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
89 | | dvdsval3 14987 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑀 + 1) ∈ ℤ) →
(𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) mod 𝑁) = 0)) |
90 | 88, 5, 89 | syl2anr 495 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) mod 𝑁) = 0)) |
91 | 87, 90 | sylibrd 249 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (¬
((𝑀 + 1) mod 𝑁) ∈ ℕ → 𝑁 ∥ (𝑀 + 1))) |
92 | 91 | con1d 139 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (¬
𝑁 ∥ (𝑀 + 1) → ((𝑀 + 1) mod 𝑁) ∈ ℕ)) |
93 | 92 | imp 445 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → ((𝑀 + 1) mod 𝑁) ∈ ℕ) |
94 | | nnm1nn0 11334 |
. . . . . . . . 9
⊢ (((𝑀 + 1) mod 𝑁) ∈ ℕ → (((𝑀 + 1) mod 𝑁) − 1) ∈
ℕ0) |
95 | 93, 94 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → (((𝑀 + 1) mod 𝑁) − 1) ∈
ℕ0) |
96 | 95 | nn0ge0d 11354 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → 0 ≤ (((𝑀 + 1) mod 𝑁) − 1)) |
97 | 15, 16 | jca 554 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 0 <
𝑁)) |
98 | 97 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → (𝑁 ∈ ℝ ∧ 0 < 𝑁)) |
99 | | divge0 10892 |
. . . . . . 7
⊢
((((((𝑀 + 1) mod
𝑁) − 1) ∈
ℝ ∧ 0 ≤ (((𝑀 +
1) mod 𝑁) − 1)) ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → 0 ≤
((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) |
100 | 84, 96, 98, 99 | syl21anc 1325 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → 0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) |
101 | 15 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) |
102 | 81 | ltm1d 10956 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < ((𝑀 + 1) mod 𝑁)) |
103 | | nnrp 11842 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
104 | | modlt 12679 |
. . . . . . . . . . 11
⊢ (((𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ ((𝑀 + 1) mod 𝑁) < 𝑁) |
105 | 66, 103, 104 | syl2an 494 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) < 𝑁) |
106 | 83, 81, 101, 102, 105 | lttrd 10198 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < 𝑁) |
107 | 41 | mulid1d 10057 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 1) = 𝑁) |
108 | 106, 107 | breqtrrd 4681 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < (𝑁 · 1)) |
109 | 24 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 1 ∈
ℝ) |
110 | 16 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 0 <
𝑁) |
111 | | ltdivmul 10898 |
. . . . . . . . 9
⊢
(((((𝑀 + 1) mod
𝑁) − 1) ∈
ℝ ∧ 1 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1 ↔ (((𝑀 + 1) mod 𝑁) − 1) < (𝑁 · 1))) |
112 | 83, 109, 101, 110, 111 | syl112anc 1330 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1 ↔ (((𝑀 + 1) mod 𝑁) − 1) < (𝑁 · 1))) |
113 | 108, 112 | mpbird 247 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1) |
114 | 113 | adantr 481 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1) |
115 | | nndivre 11056 |
. . . . . . . . 9
⊢
(((((𝑀 + 1) mod
𝑁) − 1) ∈
ℝ ∧ 𝑁 ∈
ℕ) → ((((𝑀 + 1)
mod 𝑁) − 1) / 𝑁) ∈
ℝ) |
116 | 83, 115 | sylancom 701 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℝ) |
117 | | flbi2 12618 |
. . . . . . . 8
⊢
(((⌊‘((𝑀
+ 1) / 𝑁)) ∈ ℤ
∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℝ) →
((⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁)) ↔ (0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1))) |
118 | 69, 116, 117 | syl2anc 693 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁)) ↔ (0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1))) |
119 | 118 | adantr 481 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
((⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁)) ↔ (0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1))) |
120 | 100, 114,
119 | mpbir2and 957 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
(⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁))) |
121 | | modval 12670 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ ((𝑀 + 1) mod 𝑁) = ((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁))))) |
122 | 66, 103, 121 | syl2an 494 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) = ((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁))))) |
123 | 122 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) = (((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) − 1)) |
124 | 41, 70 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) ∈ ℂ) |
125 | 44, 40, 124 | sub32d 10424 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) − 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) = (((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) − 1)) |
126 | 123, 125 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) = (((𝑀 + 1) − 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁))))) |
127 | | pncan 10287 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 1) = 𝑀) |
128 | 38, 39, 127 | sylancl 694 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) − 1) = 𝑀) |
129 | 128 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) − 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) = (𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁))))) |
130 | 126, 129 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) = (𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁))))) |
131 | 130 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) = ((𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) / 𝑁)) |
132 | 38, 124, 41, 4 | divsubdird 10840 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) / 𝑁) = ((𝑀 / 𝑁) − ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁))) |
133 | 70, 41, 4 | divcan3d 10806 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁) = (⌊‘((𝑀 + 1) / 𝑁))) |
134 | 133 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) − ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁)) = ((𝑀 / 𝑁) − (⌊‘((𝑀 + 1) / 𝑁)))) |
135 | 131, 132,
134 | 3eqtrrd 2661 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) − (⌊‘((𝑀 + 1) / 𝑁))) = ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) |
136 | 59 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℂ) |
137 | 116 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℂ) |
138 | 136, 70, 137 | subaddd 10410 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 / 𝑁) − (⌊‘((𝑀 + 1) / 𝑁))) = ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ↔ ((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) = (𝑀 / 𝑁))) |
139 | 135, 138 | mpbid 222 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((⌊‘((𝑀 + 1) /
𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) = (𝑀 / 𝑁)) |
140 | 139 | adantr 481 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
((⌊‘((𝑀 + 1) /
𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) = (𝑀 / 𝑁)) |
141 | 140 | fveq2d 6195 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
(⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘(𝑀 / 𝑁))) |
142 | 120, 141 | eqtr3d 2658 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
(⌊‘((𝑀 + 1) /
𝑁)) = (⌊‘(𝑀 / 𝑁))) |
143 | 70, 72 | subeq0ad 10402 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(((⌊‘((𝑀 + 1) /
𝑁)) −
(⌊‘(𝑀 / 𝑁))) = 0 ↔
(⌊‘((𝑀 + 1) /
𝑁)) = (⌊‘(𝑀 / 𝑁)))) |
144 | 143 | adantr 481 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
(((⌊‘((𝑀 + 1) /
𝑁)) −
(⌊‘(𝑀 / 𝑁))) = 0 ↔
(⌊‘((𝑀 + 1) /
𝑁)) = (⌊‘(𝑀 / 𝑁)))) |
145 | 142, 144 | mpbird 247 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
((⌊‘((𝑀 + 1) /
𝑁)) −
(⌊‘(𝑀 / 𝑁))) = 0) |
146 | | iffalse 4095 |
. . . 4
⊢ (¬
𝑁 ∥ (𝑀 + 1) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 0) |
147 | 146 | adantl 482 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 0) |
148 | 145, 147 | eqtr4d 2659 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
𝑁 ∥ (𝑀 + 1)) →
((⌊‘((𝑀 + 1) /
𝑁)) −
(⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0)) |
149 | 78, 148 | pm2.61dan 832 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((⌊‘((𝑀 + 1) /
𝑁)) −
(⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0)) |