This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fldivp1

Description: The difference between the floors of adjacent fractions is either 1 or 0. (Contributed by Mario Carneiro, 8-Mar-2014)

Ref Expression
Assertion fldivp1 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) = if ( 𝑁 ∥ ( 𝑀 + 1 ) , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
2 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
3 peano2z ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 + 1 ) ∈ ℤ )
4 3 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 1 ) ∈ ℤ )
5 dvdsval2 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ ( 𝑀 + 1 ) ∈ ℤ ) → ( 𝑁 ∥ ( 𝑀 + 1 ) ↔ ( ( 𝑀 + 1 ) / 𝑁 ) ∈ ℤ ) )
6 1 2 4 5 syl2an23an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∥ ( 𝑀 + 1 ) ↔ ( ( 𝑀 + 1 ) / 𝑁 ) ∈ ℤ ) )
7 6 biimpa ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( 𝑀 + 1 ) / 𝑁 ) ∈ ℤ )
8 flid ⊢ ( ( ( 𝑀 + 1 ) / 𝑁 ) ∈ ℤ → ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) = ( ( 𝑀 + 1 ) / 𝑁 ) )
9 7 8 syl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) = ( ( 𝑀 + 1 ) / 𝑁 ) )
10 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
11 10 nn0red ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℝ )
12 10 nn0ge0d ⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( 𝑁 − 1 ) )
13 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
14 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
15 divge0 ⊢ ( ( ( ( 𝑁 − 1 ) ∈ ℝ ∧ 0 ≤ ( 𝑁 − 1 ) ) ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → 0 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) )
16 11 12 13 14 15 syl22anc ⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) )
17 16 ad2antlr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → 0 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) )
18 13 ltm1d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) < 𝑁 )
19 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
20 19 mulridd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 · 1 ) = 𝑁 )
21 18 20 breqtrrd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) < ( 𝑁 · 1 ) )
22 1re ⊢ 1 ∈ ℝ
23 22 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
24 ltdivmul ⊢ ( ( ( 𝑁 − 1 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( ( 𝑁 − 1 ) / 𝑁 ) < 1 ↔ ( 𝑁 − 1 ) < ( 𝑁 · 1 ) ) )
25 11 23 13 14 24 syl112anc ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) / 𝑁 ) < 1 ↔ ( 𝑁 − 1 ) < ( 𝑁 · 1 ) ) )
26 21 25 mpbird ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) / 𝑁 ) < 1 )
27 26 ad2antlr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( 𝑁 − 1 ) / 𝑁 ) < 1 )
28 nndivre ⊢ ( ( ( 𝑁 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) / 𝑁 ) ∈ ℝ )
29 11 28 mpancom ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) / 𝑁 ) ∈ ℝ )
30 29 ad2antlr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( 𝑁 − 1 ) / 𝑁 ) ∈ ℝ )
31 flbi2 ⊢ ( ( ( ( 𝑀 + 1 ) / 𝑁 ) ∈ ℤ ∧ ( ( 𝑁 − 1 ) / 𝑁 ) ∈ ℝ ) → ( ( ⌊ ‘ ( ( ( 𝑀 + 1 ) / 𝑁 ) + ( ( 𝑁 − 1 ) / 𝑁 ) ) ) = ( ( 𝑀 + 1 ) / 𝑁 ) ↔ ( 0 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) ∧ ( ( 𝑁 − 1 ) / 𝑁 ) < 1 ) ) )
32 7 30 31 syl2anc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( ⌊ ‘ ( ( ( 𝑀 + 1 ) / 𝑁 ) + ( ( 𝑁 − 1 ) / 𝑁 ) ) ) = ( ( 𝑀 + 1 ) / 𝑁 ) ↔ ( 0 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) ∧ ( ( 𝑁 − 1 ) / 𝑁 ) < 1 ) ) )
33 17 27 32 mpbir2and ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ⌊ ‘ ( ( ( 𝑀 + 1 ) / 𝑁 ) + ( ( 𝑁 − 1 ) / 𝑁 ) ) ) = ( ( 𝑀 + 1 ) / 𝑁 ) )
34 9 33 eqtr4d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) = ( ⌊ ‘ ( ( ( 𝑀 + 1 ) / 𝑁 ) + ( ( 𝑁 − 1 ) / 𝑁 ) ) ) )
35 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
36 35 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℂ )
37 ax-1cn ⊢ 1 ∈ ℂ
38 37 a1i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 1 ∈ ℂ )
39 19 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
40 36 38 39 ppncand ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 + 1 ) + ( 𝑁 − 1 ) ) = ( 𝑀 + 𝑁 ) )
41 40 oveq1d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) + ( 𝑁 − 1 ) ) / 𝑁 ) = ( ( 𝑀 + 𝑁 ) / 𝑁 ) )
42 4 zcnd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 1 ) ∈ ℂ )
43 subcl ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑁 − 1 ) ∈ ℂ )
44 19 37 43 sylancl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℂ )
45 44 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) ∈ ℂ )
46 2 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ≠ 0 )
47 42 45 39 46 divdird ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) + ( 𝑁 − 1 ) ) / 𝑁 ) = ( ( ( 𝑀 + 1 ) / 𝑁 ) + ( ( 𝑁 − 1 ) / 𝑁 ) ) )
48 41 47 eqtr3d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 + 𝑁 ) / 𝑁 ) = ( ( ( 𝑀 + 1 ) / 𝑁 ) + ( ( 𝑁 − 1 ) / 𝑁 ) ) )
49 36 39 39 46 divdird ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 + 𝑁 ) / 𝑁 ) = ( ( 𝑀 / 𝑁 ) + ( 𝑁 / 𝑁 ) ) )
50 48 49 eqtr3d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) / 𝑁 ) + ( ( 𝑁 − 1 ) / 𝑁 ) ) = ( ( 𝑀 / 𝑁 ) + ( 𝑁 / 𝑁 ) ) )
51 39 46 dividd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 / 𝑁 ) = 1 )
52 51 oveq2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 / 𝑁 ) + ( 𝑁 / 𝑁 ) ) = ( ( 𝑀 / 𝑁 ) + 1 ) )
53 50 52 eqtrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) / 𝑁 ) + ( ( 𝑁 − 1 ) / 𝑁 ) ) = ( ( 𝑀 / 𝑁 ) + 1 ) )
54 53 fveq2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ( 𝑀 + 1 ) / 𝑁 ) + ( ( 𝑁 − 1 ) / 𝑁 ) ) ) = ( ⌊ ‘ ( ( 𝑀 / 𝑁 ) + 1 ) ) )
55 54 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ⌊ ‘ ( ( ( 𝑀 + 1 ) / 𝑁 ) + ( ( 𝑁 − 1 ) / 𝑁 ) ) ) = ( ⌊ ‘ ( ( 𝑀 / 𝑁 ) + 1 ) ) )
56 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
57 nndivre ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 / 𝑁 ) ∈ ℝ )
58 56 57 sylan ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 / 𝑁 ) ∈ ℝ )
59 1z ⊢ 1 ∈ ℤ
60 fladdz ⊢ ( ( ( 𝑀 / 𝑁 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ⌊ ‘ ( ( 𝑀 / 𝑁 ) + 1 ) ) = ( ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) + 1 ) )
61 58 59 60 sylancl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑀 / 𝑁 ) + 1 ) ) = ( ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) + 1 ) )
62 61 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ⌊ ‘ ( ( 𝑀 / 𝑁 ) + 1 ) ) = ( ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) + 1 ) )
63 34 55 62 3eqtrrd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) + 1 ) = ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) )
64 zre ⊢ ( ( 𝑀 + 1 ) ∈ ℤ → ( 𝑀 + 1 ) ∈ ℝ )
65 3 64 syl ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 + 1 ) ∈ ℝ )
66 nndivre ⊢ ( ( ( 𝑀 + 1 ) ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 + 1 ) / 𝑁 ) ∈ ℝ )
67 65 66 sylan ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 + 1 ) / 𝑁 ) ∈ ℝ )
68 67 flcld ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ∈ ℤ )
69 68 zcnd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ∈ ℂ )
70 58 flcld ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℤ )
71 70 zcnd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℂ )
72 69 71 38 subaddd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) = 1 ↔ ( ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) + 1 ) = ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) )
73 72 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) = 1 ↔ ( ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) + 1 ) = ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) )
74 63 73 mpbird ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) = 1 )
75 iftrue ⊢ ( 𝑁 ∥ ( 𝑀 + 1 ) → if ( 𝑁 ∥ ( 𝑀 + 1 ) , 1 , 0 ) = 1 )
76 75 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → if ( 𝑁 ∥ ( 𝑀 + 1 ) , 1 , 0 ) = 1 )
77 74 76 eqtr4d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) = if ( 𝑁 ∥ ( 𝑀 + 1 ) , 1 , 0 ) )
78 zmodcl ⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 + 1 ) mod 𝑁 ) ∈ ℕ0 )
79 3 78 sylan ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 + 1 ) mod 𝑁 ) ∈ ℕ0 )
80 79 nn0red ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 + 1 ) mod 𝑁 ) ∈ ℝ )
81 resubcl ⊢ ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) ∈ ℝ )
82 80 22 81 sylancl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) ∈ ℝ )
83 82 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) ∈ ℝ )
84 elnn0 ⊢ ( ( ( 𝑀 + 1 ) mod 𝑁 ) ∈ ℕ0 ↔ ( ( ( 𝑀 + 1 ) mod 𝑁 ) ∈ ℕ ∨ ( ( 𝑀 + 1 ) mod 𝑁 ) = 0 ) )
85 79 84 sylib ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) mod 𝑁 ) ∈ ℕ ∨ ( ( 𝑀 + 1 ) mod 𝑁 ) = 0 ) )
86 85 ord ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ¬ ( ( 𝑀 + 1 ) mod 𝑁 ) ∈ ℕ → ( ( 𝑀 + 1 ) mod 𝑁 ) = 0 ) )
87 id ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
88 dvdsval3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑀 + 1 ) ∈ ℤ ) → ( 𝑁 ∥ ( 𝑀 + 1 ) ↔ ( ( 𝑀 + 1 ) mod 𝑁 ) = 0 ) )
89 87 3 88 syl2anr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∥ ( 𝑀 + 1 ) ↔ ( ( 𝑀 + 1 ) mod 𝑁 ) = 0 ) )
90 86 89 sylibrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ¬ ( ( 𝑀 + 1 ) mod 𝑁 ) ∈ ℕ → 𝑁 ∥ ( 𝑀 + 1 ) ) )
91 90 con1d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ¬ 𝑁 ∥ ( 𝑀 + 1 ) → ( ( 𝑀 + 1 ) mod 𝑁 ) ∈ ℕ ) )
92 91 imp ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( 𝑀 + 1 ) mod 𝑁 ) ∈ ℕ )
93 nnm1nn0 ⊢ ( ( ( 𝑀 + 1 ) mod 𝑁 ) ∈ ℕ → ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) ∈ ℕ0 )
94 92 93 syl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) ∈ ℕ0 )
95 94 nn0ge0d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → 0 ≤ ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) )
96 13 14 jca ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) )
97 96 ad2antlr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) )
98 divge0 ⊢ ( ( ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) ∈ ℝ ∧ 0 ≤ ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) ) ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → 0 ≤ ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) )
99 83 95 97 98 syl21anc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → 0 ≤ ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) )
100 13 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
101 80 ltm1d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) < ( ( 𝑀 + 1 ) mod 𝑁 ) )
102 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
103 modlt ⊢ ( ( ( 𝑀 + 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( 𝑀 + 1 ) mod 𝑁 ) < 𝑁 )
104 65 102 103 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 + 1 ) mod 𝑁 ) < 𝑁 )
105 82 80 100 101 104 lttrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) < 𝑁 )
106 39 mulridd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 1 ) = 𝑁 )
107 105 106 breqtrrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) < ( 𝑁 · 1 ) )
108 22 a1i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 1 ∈ ℝ )
109 14 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 0 < 𝑁 )
110 ltdivmul ⊢ ( ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) < 1 ↔ ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) < ( 𝑁 · 1 ) ) )
111 82 108 100 109 110 syl112anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) < 1 ↔ ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) < ( 𝑁 · 1 ) ) )
112 107 111 mpbird ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) < 1 )
113 112 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) < 1 )
114 nndivre ⊢ ( ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ∈ ℝ )
115 82 114 sylancom ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ∈ ℝ )
116 flbi2 ⊢ ( ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ∈ ℤ ∧ ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ∈ ℝ ) → ( ( ⌊ ‘ ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) + ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ) ) = ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ↔ ( 0 ≤ ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ∧ ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) < 1 ) ) )
117 68 115 116 syl2anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ⌊ ‘ ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) + ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ) ) = ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ↔ ( 0 ≤ ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ∧ ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) < 1 ) ) )
118 117 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( ⌊ ‘ ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) + ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ) ) = ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ↔ ( 0 ≤ ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ∧ ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) < 1 ) ) )
119 99 113 118 mpbir2and ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ⌊ ‘ ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) + ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ) ) = ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) )
120 modval ⊢ ( ( ( 𝑀 + 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( 𝑀 + 1 ) mod 𝑁 ) = ( ( 𝑀 + 1 ) − ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) ) )
121 65 102 120 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 + 1 ) mod 𝑁 ) = ( ( 𝑀 + 1 ) − ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) ) )
122 121 oveq1d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) = ( ( ( 𝑀 + 1 ) − ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) ) − 1 ) )
123 39 69 mulcld ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) ∈ ℂ )
124 42 38 123 sub32d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) − 1 ) − ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) ) = ( ( ( 𝑀 + 1 ) − ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) ) − 1 ) )
125 122 124 eqtr4d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) = ( ( ( 𝑀 + 1 ) − 1 ) − ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) ) )
126 pncan ⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
127 36 37 126 sylancl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
128 127 oveq1d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) − 1 ) − ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) ) = ( 𝑀 − ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) ) )
129 125 128 eqtrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) = ( 𝑀 − ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) ) )
130 129 oveq1d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) = ( ( 𝑀 − ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) ) / 𝑁 ) )
131 36 123 39 46 divsubdird ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 − ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) ) / 𝑁 ) = ( ( 𝑀 / 𝑁 ) − ( ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) / 𝑁 ) ) )
132 69 39 46 divcan3d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) / 𝑁 ) = ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) )
133 132 oveq2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 / 𝑁 ) − ( ( 𝑁 · ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) / 𝑁 ) ) = ( ( 𝑀 / 𝑁 ) − ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) )
134 130 131 133 3eqtrrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 / 𝑁 ) − ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) = ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) )
135 58 recnd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 / 𝑁 ) ∈ ℂ )
136 115 recnd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ∈ ℂ )
137 135 69 136 subaddd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 / 𝑁 ) − ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) ) = ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ↔ ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) + ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ) = ( 𝑀 / 𝑁 ) ) )
138 134 137 mpbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) + ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ) = ( 𝑀 / 𝑁 ) )
139 138 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) + ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ) = ( 𝑀 / 𝑁 ) )
140 139 fveq2d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ⌊ ‘ ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) + ( ( ( ( 𝑀 + 1 ) mod 𝑁 ) − 1 ) / 𝑁 ) ) ) = ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) )
141 119 140 eqtr3d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) = ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) )
142 69 71 subeq0ad ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) = 0 ↔ ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) = ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) )
143 142 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) = 0 ↔ ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) = ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) )
144 141 143 mpbird ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) = 0 )
145 iffalse ⊢ ( ¬ 𝑁 ∥ ( 𝑀 + 1 ) → if ( 𝑁 ∥ ( 𝑀 + 1 ) , 1 , 0 ) = 0 )
146 145 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → if ( 𝑁 ∥ ( 𝑀 + 1 ) , 1 , 0 ) = 0 )
147 144 146 eqtr4d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ ( 𝑀 + 1 ) ) → ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) = if ( 𝑁 ∥ ( 𝑀 + 1 ) , 1 , 0 ) )
148 77 147 pm2.61dan ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) = if ( 𝑁 ∥ ( 𝑀 + 1 ) , 1 , 0 ) )