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 ⊢ M ∈ ℤ ∧ N ∈ ℕ → M − 1 N = M − 1

Proof

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