Metamath Proof Explorer

Theorem flmrecm1

Description: The floor of an integer minus the reciprocal of a positive integer is the integer minus 1. (Contributed by AV, 10-Apr-2026)

Ref Expression
Assertion flmrecm1 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝑀 − ( 1 / 𝑁 ) ) ) = ( 𝑀 − 1 ) )

Proof

Step Hyp Ref Expression
1 peano2zm ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℤ )
2 1 zcnd ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℂ )
3 2 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 − 1 ) ∈ ℂ )
4 1cnd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 1 ∈ ℂ )
5 nnrecre ⊢ ( 𝑁 ∈ ℕ → ( 1 / 𝑁 ) ∈ ℝ )
6 5 recnd ⊢ ( 𝑁 ∈ ℕ → ( 1 / 𝑁 ) ∈ ℂ )
7 6 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 1 / 𝑁 ) ∈ ℂ )
8 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
9 npcan1 ⊢ ( 𝑀 ∈ ℂ → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
10 9 eqcomd ⊢ ( 𝑀 ∈ ℂ → 𝑀 = ( ( 𝑀 − 1 ) + 1 ) )
11 8 10 syl ⊢ ( 𝑀 ∈ ℤ → 𝑀 = ( ( 𝑀 − 1 ) + 1 ) )
12 11 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 = ( ( 𝑀 − 1 ) + 1 ) )
13 12 oveq1d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 − ( 1 / 𝑁 ) ) = ( ( ( 𝑀 − 1 ) + 1 ) − ( 1 / 𝑁 ) ) )
14 3 4 7 13 assraddsubd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 − ( 1 / 𝑁 ) ) = ( ( 𝑀 − 1 ) + ( 1 − ( 1 / 𝑁 ) ) ) )
15 14 fveq2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝑀 − ( 1 / 𝑁 ) ) ) = ( ⌊ ‘ ( ( 𝑀 − 1 ) + ( 1 − ( 1 / 𝑁 ) ) ) ) )
16 1red ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
17 16 5 resubcld ⊢ ( 𝑁 ∈ ℕ → ( 1 − ( 1 / 𝑁 ) ) ∈ ℝ )
18 flzadd ⊢ ( ( ( 𝑀 − 1 ) ∈ ℤ ∧ ( 1 − ( 1 / 𝑁 ) ) ∈ ℝ ) → ( ⌊ ‘ ( ( 𝑀 − 1 ) + ( 1 − ( 1 / 𝑁 ) ) ) ) = ( ( 𝑀 − 1 ) + ( ⌊ ‘ ( 1 − ( 1 / 𝑁 ) ) ) ) )
19 1 17 18 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑀 − 1 ) + ( 1 − ( 1 / 𝑁 ) ) ) ) = ( ( 𝑀 − 1 ) + ( ⌊ ‘ ( 1 − ( 1 / 𝑁 ) ) ) ) )
20 nnge1 ⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
21 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
22 divle1le ⊢ ( ( 1 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( 1 / 𝑁 ) ≤ 1 ↔ 1 ≤ 𝑁 ) )
23 16 21 22 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / 𝑁 ) ≤ 1 ↔ 1 ≤ 𝑁 ) )
24 20 23 mpbird ⊢ ( 𝑁 ∈ ℕ → ( 1 / 𝑁 ) ≤ 1 )
25 16 5 subge0d ⊢ ( 𝑁 ∈ ℕ → ( 0 ≤ ( 1 − ( 1 / 𝑁 ) ) ↔ ( 1 / 𝑁 ) ≤ 1 ) )
26 24 25 mpbird ⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( 1 − ( 1 / 𝑁 ) ) )
27 nnrecgt0 ⊢ ( 𝑁 ∈ ℕ → 0 < ( 1 / 𝑁 ) )
28 5 16 ltsubposd ⊢ ( 𝑁 ∈ ℕ → ( 0 < ( 1 / 𝑁 ) ↔ ( 1 − ( 1 / 𝑁 ) ) < 1 ) )
29 27 28 mpbid ⊢ ( 𝑁 ∈ ℕ → ( 1 − ( 1 / 𝑁 ) ) < 1 )
30 0re ⊢ 0 ∈ ℝ
31 1xr ⊢ 1 ∈ ℝ*
32 30 31 pm3.2i ⊢ ( 0 ∈ ℝ ∧ 1 ∈ ℝ* )
33 elico2 ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ* ) → ( ( 1 − ( 1 / 𝑁 ) ) ∈ ( 0 [,) 1 ) ↔ ( ( 1 − ( 1 / 𝑁 ) ) ∈ ℝ ∧ 0 ≤ ( 1 − ( 1 / 𝑁 ) ) ∧ ( 1 − ( 1 / 𝑁 ) ) < 1 ) ) )
34 32 33 mp1i ⊢ ( 𝑁 ∈ ℕ → ( ( 1 − ( 1 / 𝑁 ) ) ∈ ( 0 [,) 1 ) ↔ ( ( 1 − ( 1 / 𝑁 ) ) ∈ ℝ ∧ 0 ≤ ( 1 − ( 1 / 𝑁 ) ) ∧ ( 1 − ( 1 / 𝑁 ) ) < 1 ) ) )
35 17 26 29 34 mpbir3and ⊢ ( 𝑁 ∈ ℕ → ( 1 − ( 1 / 𝑁 ) ) ∈ ( 0 [,) 1 ) )
36 ico01fl0 ⊢ ( ( 1 − ( 1 / 𝑁 ) ) ∈ ( 0 [,) 1 ) → ( ⌊ ‘ ( 1 − ( 1 / 𝑁 ) ) ) = 0 )
37 35 36 syl ⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 1 − ( 1 / 𝑁 ) ) ) = 0 )
38 37 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 1 − ( 1 / 𝑁 ) ) ) = 0 )
39 38 oveq2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 − 1 ) + ( ⌊ ‘ ( 1 − ( 1 / 𝑁 ) ) ) ) = ( ( 𝑀 − 1 ) + 0 ) )
40 3 addridd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 − 1 ) + 0 ) = ( 𝑀 − 1 ) )
41 39 40 eqtrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 − 1 ) + ( ⌊ ‘ ( 1 − ( 1 / 𝑁 ) ) ) ) = ( 𝑀 − 1 ) )
42 15 19 41 3eqtrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝑀 − ( 1 / 𝑁 ) ) ) = ( 𝑀 − 1 ) )