Step |
Hyp |
Ref |
Expression |
1 |
|
reflcl |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ ) |
2 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ ) |
3 |
|
simpl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ℝ ) |
4 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ ) |
5 |
4
|
zred |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ ) |
6 |
|
flle |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) |
7 |
6
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) |
8 |
2 3 5 7
|
leadd1dd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) ≤ ( 𝐴 + 𝑁 ) ) |
9 |
|
1red |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → 1 ∈ ℝ ) |
10 |
2 9
|
readdcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ ) |
11 |
|
flltp1 |
⊢ ( 𝐴 ∈ ℝ → 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) |
12 |
11
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) |
13 |
3 10 5 12
|
ltadd1dd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 + 𝑁 ) < ( ( ( ⌊ ‘ 𝐴 ) + 1 ) + 𝑁 ) ) |
14 |
2
|
recnd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ⌊ ‘ 𝐴 ) ∈ ℂ ) |
15 |
|
1cnd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → 1 ∈ ℂ ) |
16 |
5
|
recnd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℂ ) |
17 |
14 15 16
|
add32d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ( ( ⌊ ‘ 𝐴 ) + 1 ) + 𝑁 ) = ( ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) + 1 ) ) |
18 |
13 17
|
breqtrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 + 𝑁 ) < ( ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) + 1 ) ) |
19 |
3 5
|
readdcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 + 𝑁 ) ∈ ℝ ) |
20 |
3
|
flcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ ) |
21 |
20 4
|
zaddcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) ∈ ℤ ) |
22 |
|
flbi |
⊢ ( ( ( 𝐴 + 𝑁 ) ∈ ℝ ∧ ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) ∈ ℤ ) → ( ( ⌊ ‘ ( 𝐴 + 𝑁 ) ) = ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) ↔ ( ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) ≤ ( 𝐴 + 𝑁 ) ∧ ( 𝐴 + 𝑁 ) < ( ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) + 1 ) ) ) ) |
23 |
19 21 22
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ( ⌊ ‘ ( 𝐴 + 𝑁 ) ) = ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) ↔ ( ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) ≤ ( 𝐴 + 𝑁 ) ∧ ( 𝐴 + 𝑁 ) < ( ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) + 1 ) ) ) ) |
24 |
8 18 23
|
mpbir2and |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ⌊ ‘ ( 𝐴 + 𝑁 ) ) = ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) ) |