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∈ℕ→AN=AN

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∈ℕ→AN=A+A-AN
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-AN=AN+A−AN
16 8 11 14 15 syl2an3an ⊢A∈ℝ∧N∈ℕ→A+A-AN=AN+A−AN
17 6 16 eqtrd ⊢A∈ℝ∧N∈ℕ→AN=AN+A−AN
18 flcl ⊢A∈ℝ→A∈ℤ
19 eqid ⊢AN=AN
20 eqid ⊢AN−AN=AN−AN
21 19 20 intfracq ⊢A∈ℤ∧N∈ℕ→0≤AN−AN∧AN−AN≤N−1N∧AN=AN+AN-AN
22 21 simp3d ⊢A∈ℤ∧N∈ℕ→AN=AN+AN-AN
23 18 22 sylan ⊢A∈ℝ∧N∈ℕ→AN=AN+AN-AN
24 23 oveq1d ⊢A∈ℝ∧N∈ℕ→AN+A−AN=AN+AN−AN+A−AN
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∈ℕ→AN∈ℝ
30 reflcl ⊢AN∈ℝ→AN∈ℝ
31 29 30 syl ⊢A∈ℝ∧N∈ℕ→AN∈ℝ
32 31 recnd ⊢A∈ℝ∧N∈ℕ→AN∈ℂ
33 29 31 resubcld ⊢A∈ℝ∧N∈ℕ→AN−AN∈ℝ
34 33 recnd ⊢A∈ℝ∧N∈ℕ→AN−AN∈ℂ
35 10 adantr ⊢A∈ℝ∧N∈ℕ→A−A∈ℝ
36 35 27 28 redivcld ⊢A∈ℝ∧N∈ℕ→A−AN∈ℝ
37 36 recnd ⊢A∈ℝ∧N∈ℕ→A−AN∈ℂ
38 32 34 37 addassd ⊢A∈ℝ∧N∈ℕ→AN+AN−AN+A−AN=AN+AN−AN+A−AN
39 17 24 38 3eqtrd ⊢A∈ℝ∧N∈ℕ→AN=AN+AN−AN+A−AN
40 39 fveq2d ⊢A∈ℝ∧N∈ℕ→AN=AN+AN−AN+A−AN
41 21 simp1d ⊢A∈ℤ∧N∈ℕ→0≤AN−AN
42 18 41 sylan ⊢A∈ℝ∧N∈ℕ→0≤AN−AN
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−AN
48 44 46 47 syl2an ⊢A∈ℝ∧N∈ℕ→0≤A−AN
49 33 36 42 48 addge0d ⊢A∈ℝ∧N∈ℕ→0≤AN-AN+A−AN
50 peano2rem ⊢N∈ℝ→N−1∈ℝ
51 26 50 syl ⊢N∈ℕ→N−1∈ℝ
52 51 26 13 redivcld ⊢N∈ℕ→N−1N∈ℝ
53 nnrecre ⊢N∈ℕ→1N∈ℝ
54 52 53 jca ⊢N∈ℕ→N−1N∈ℝ∧1N∈ℝ
55 54 adantl ⊢A∈ℝ∧N∈ℕ→N−1N∈ℝ∧1N∈ℝ
56 33 36 55 jca31 ⊢A∈ℝ∧N∈ℕ→AN−AN∈ℝ∧A−AN∈ℝ∧N−1N∈ℝ∧1N∈ℝ
57 21 simp2d ⊢A∈ℤ∧N∈ℕ→AN−AN≤N−1N
58 18 57 sylan ⊢A∈ℝ∧N∈ℕ→AN−AN≤N−1N
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−AN<1N
63 61 62 mp3an2 ⊢A−A∈ℝ∧N∈ℝ∧0<N→A−A<1↔A−AN<1N
64 10 46 63 syl2an ⊢A∈ℝ∧N∈ℕ→A−A<1↔A−AN<1N
65 60 64 mpbid ⊢A∈ℝ∧N∈ℕ→A−AN<1N
66 58 65 jca ⊢A∈ℝ∧N∈ℕ→AN−AN≤N−1N∧A−AN<1N
67 leltadd ⊢AN−AN∈ℝ∧A−AN∈ℝ∧N−1N∈ℝ∧1N∈ℝ→AN−AN≤N−1N∧A−AN<1N→AN-AN+A−AN<N−1N+1N
68 56 66 67 sylc ⊢A∈ℝ∧N∈ℕ→AN-AN+A−AN<N−1N+1N
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+1N=NN
73 51 recnd ⊢N∈ℕ→N−1∈ℂ
74 divdir ⊢N−1∈ℂ∧1∈ℂ∧N∈ℂ∧N≠0→N-1+1N=N−1N+1N
75 69 74 mp3an2 ⊢N−1∈ℂ∧N∈ℂ∧N≠0→N-1+1N=N−1N+1N
76 73 12 13 75 syl12anc ⊢N∈ℕ→N-1+1N=N−1N+1N
77 12 13 dividd ⊢N∈ℕ→NN=1
78 72 76 77 3eqtr3d ⊢N∈ℕ→N−1N+1N=1
79 78 adantl ⊢A∈ℝ∧N∈ℕ→N−1N+1N=1
80 68 79 breqtrd ⊢A∈ℝ∧N∈ℕ→AN-AN+A−AN<1
81 29 flcld ⊢A∈ℝ∧N∈ℕ→AN∈ℤ
82 33 36 readdcld ⊢A∈ℝ∧N∈ℕ→AN-AN+A−AN∈ℝ
83 flbi2 ⊢AN∈ℤ∧AN-AN+A−AN∈ℝ→AN+AN−AN+A−AN=AN↔0≤AN-AN+A−AN∧AN-AN+A−AN<1
84 81 82 83 syl2anc ⊢A∈ℝ∧N∈ℕ→AN+AN−AN+A−AN=AN↔0≤AN-AN+A−AN∧AN-AN+A−AN<1
85 49 80 84 mpbir2and ⊢A∈ℝ∧N∈ℕ→AN+AN−AN+A−AN=AN
86 40 85 eqtr2d ⊢A∈ℝ∧N∈ℕ→AN=AN