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 ⊢ A ∈ ℝ ∧ N ∈ ℕ → A N = A N

Proof

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