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

Metamath Proof Explorer

Theorem fldiv

Description: Cancellation of the embedded floor of a real divided by an integer. (Contributed by NM, 16-Aug-2008)

Ref Expression
Assertion fldiv ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) = ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( ⌊ ‘ 𝐴 ) = ( ⌊ ‘ 𝐴 )
2 eqid ⊢ ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) = ( 𝐴 − ( ⌊ ‘ 𝐴 ) )
3 1 2 intfrac2 ⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 ∧ 𝐴 = ( ( ⌊ ‘ 𝐴 ) + ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ) ) )
4 3 simp3d ⊢ ( 𝐴 ∈ ℝ → 𝐴 = ( ( ⌊ ‘ 𝐴 ) + ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ) )
5 4 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → 𝐴 = ( ( ⌊ ‘ 𝐴 ) + ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ) )
6 5 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 / 𝑁 ) = ( ( ( ⌊ ‘ 𝐴 ) + ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ) / 𝑁 ) )
7 reflcl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
8 7 recnd ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℂ )
9 resubcl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℝ ) → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ∈ ℝ )
10 7 9 mpdan ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ∈ ℝ )
11 10 recnd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ∈ ℂ )
12 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
13 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
14 12 13 jca ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
15 divdir ⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℂ ∧ ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ∈ ℂ ∧ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ) → ( ( ( ⌊ ‘ 𝐴 ) + ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ) / 𝑁 ) = ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) )
16 8 11 14 15 syl2an3an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( ⌊ ‘ 𝐴 ) + ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ) / 𝑁 ) = ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) )
17 6 16 eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 / 𝑁 ) = ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) )
18 flcl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
19 eqid ⊢ ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) = ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) )
20 eqid ⊢ ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) = ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) )
21 19 20 intfracq ⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 0 ≤ ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ∧ ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ≤ ( ( 𝑁 − 1 ) / 𝑁 ) ∧ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) = ( ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) + ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ) ) )
22 21 simp3d ⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) = ( ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) + ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ) )
23 18 22 sylan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) = ( ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) + ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ) )
24 23 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) = ( ( ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) + ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) )
25 7 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
26 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
27 26 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
28 13 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → 𝑁 ≠ 0 )
29 25 27 28 redivcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ∈ ℝ )
30 reflcl ⊢ ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ∈ ℝ → ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ∈ ℝ )
31 29 30 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ∈ ℝ )
32 31 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ∈ ℂ )
33 29 31 resubcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ∈ ℝ )
34 33 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ∈ ℂ )
35 10 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ∈ ℝ )
36 35 27 28 redivcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ∈ ℝ )
37 36 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ∈ ℂ )
38 32 34 37 addassd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) + ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) = ( ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) + ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) ) )
39 17 24 38 3eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 / 𝑁 ) = ( ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) + ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) ) )
40 39 fveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) = ( ⌊ ‘ ( ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) + ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) ) ) )
41 21 simp1d ⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 0 ≤ ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) )
42 18 41 sylan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → 0 ≤ ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) )
43 fracge0 ⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) )
44 10 43 jca ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ) )
45 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
46 26 45 jca ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) )
47 divge0 ⊢ ( ( ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ) ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → 0 ≤ ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) )
48 44 46 47 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → 0 ≤ ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) )
49 33 36 42 48 addge0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → 0 ≤ ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) )
50 peano2rem ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )
51 26 50 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℝ )
52 51 26 13 redivcld ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) / 𝑁 ) ∈ ℝ )
53 nnrecre ⊢ ( 𝑁 ∈ ℕ → ( 1 / 𝑁 ) ∈ ℝ )
54 52 53 jca ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) / 𝑁 ) ∈ ℝ ∧ ( 1 / 𝑁 ) ∈ ℝ ) )
55 54 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 − 1 ) / 𝑁 ) ∈ ℝ ∧ ( 1 / 𝑁 ) ∈ ℝ ) )
56 33 36 55 jca31 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ∈ ℝ ∧ ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ∈ ℝ ) ∧ ( ( ( 𝑁 − 1 ) / 𝑁 ) ∈ ℝ ∧ ( 1 / 𝑁 ) ∈ ℝ ) ) )
57 21 simp2d ⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ≤ ( ( 𝑁 − 1 ) / 𝑁 ) )
58 18 57 sylan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ≤ ( ( 𝑁 − 1 ) / 𝑁 ) )
59 fraclt1 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 )
60 59 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 )
61 1re ⊢ 1 ∈ ℝ
62 ltdiv1 ⊢ ( ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 ↔ ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) < ( 1 / 𝑁 ) ) )
63 61 62 mp3an2 ⊢ ( ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 ↔ ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) < ( 1 / 𝑁 ) ) )
64 10 46 63 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 ↔ ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) < ( 1 / 𝑁 ) ) )
65 60 64 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) < ( 1 / 𝑁 ) )
66 58 65 jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ≤ ( ( 𝑁 − 1 ) / 𝑁 ) ∧ ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) < ( 1 / 𝑁 ) ) )
67 leltadd ⊢ ( ( ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ∈ ℝ ∧ ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ∈ ℝ ) ∧ ( ( ( 𝑁 − 1 ) / 𝑁 ) ∈ ℝ ∧ ( 1 / 𝑁 ) ∈ ℝ ) ) → ( ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) ≤ ( ( 𝑁 − 1 ) / 𝑁 ) ∧ ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) < ( 1 / 𝑁 ) ) → ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) < ( ( ( 𝑁 − 1 ) / 𝑁 ) + ( 1 / 𝑁 ) ) ) )
68 56 66 67 sylc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) < ( ( ( 𝑁 − 1 ) / 𝑁 ) + ( 1 / 𝑁 ) ) )
69 ax-1cn ⊢ 1 ∈ ℂ
70 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
71 12 69 70 sylancl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
72 71 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) + 1 ) / 𝑁 ) = ( 𝑁 / 𝑁 ) )
73 51 recnd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℂ )
74 divdir ⊢ ( ( ( 𝑁 − 1 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ) → ( ( ( 𝑁 − 1 ) + 1 ) / 𝑁 ) = ( ( ( 𝑁 − 1 ) / 𝑁 ) + ( 1 / 𝑁 ) ) )
75 69 74 mp3an2 ⊢ ( ( ( 𝑁 − 1 ) ∈ ℂ ∧ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ) → ( ( ( 𝑁 − 1 ) + 1 ) / 𝑁 ) = ( ( ( 𝑁 − 1 ) / 𝑁 ) + ( 1 / 𝑁 ) ) )
76 73 12 13 75 syl12anc ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) + 1 ) / 𝑁 ) = ( ( ( 𝑁 − 1 ) / 𝑁 ) + ( 1 / 𝑁 ) ) )
77 12 13 dividd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 / 𝑁 ) = 1 )
78 72 76 77 3eqtr3d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) / 𝑁 ) + ( 1 / 𝑁 ) ) = 1 )
79 78 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 − 1 ) / 𝑁 ) + ( 1 / 𝑁 ) ) = 1 )
80 68 79 breqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) < 1 )
81 29 flcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ∈ ℤ )
82 33 36 readdcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) ∈ ℝ )
83 flbi2 ⊢ ( ( ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ∈ ℤ ∧ ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) ∈ ℝ ) → ( ( ⌊ ‘ ( ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) + ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) ) ) = ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ↔ ( 0 ≤ ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) ∧ ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) < 1 ) ) )
84 81 82 83 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ⌊ ‘ ( ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) + ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) ) ) = ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ↔ ( 0 ≤ ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) ∧ ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) < 1 ) ) )
85 49 80 84 mpbir2and ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) + ( ( ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) − ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) ) + ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) / 𝑁 ) ) ) ) = ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) )
86 40 85 eqtr2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑁 ) ) = ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) )