Step |
Hyp |
Ref |
Expression |
1 |
|
peano2z |
⊢ ( 𝐵 ∈ ℤ → ( 𝐵 + 1 ) ∈ ℤ ) |
2 |
1
|
ad2antrl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵 ) ) → ( 𝐵 + 1 ) ∈ ℤ ) |
3 |
|
zre |
⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ ) |
4 |
|
zre |
⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ ) |
5 |
|
lep1 |
⊢ ( 𝐵 ∈ ℝ → 𝐵 ≤ ( 𝐵 + 1 ) ) |
6 |
5
|
adantl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ≤ ( 𝐵 + 1 ) ) |
7 |
|
peano2re |
⊢ ( 𝐵 ∈ ℝ → ( 𝐵 + 1 ) ∈ ℝ ) |
8 |
7
|
ancli |
⊢ ( 𝐵 ∈ ℝ → ( 𝐵 ∈ ℝ ∧ ( 𝐵 + 1 ) ∈ ℝ ) ) |
9 |
|
letr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐵 + 1 ) ∈ ℝ ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ ( 𝐵 + 1 ) ) → 𝐴 ≤ ( 𝐵 + 1 ) ) ) |
10 |
9
|
3expb |
⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ ( 𝐵 + 1 ) ∈ ℝ ) ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ ( 𝐵 + 1 ) ) → 𝐴 ≤ ( 𝐵 + 1 ) ) ) |
11 |
8 10
|
sylan2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ ( 𝐵 + 1 ) ) → 𝐴 ≤ ( 𝐵 + 1 ) ) ) |
12 |
6 11
|
mpan2d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 → 𝐴 ≤ ( 𝐵 + 1 ) ) ) |
13 |
3 4 12
|
syl2an |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ≤ 𝐵 → 𝐴 ≤ ( 𝐵 + 1 ) ) ) |
14 |
13
|
impr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵 ) ) → 𝐴 ≤ ( 𝐵 + 1 ) ) |
15 |
2 14
|
jca |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵 ) ) → ( ( 𝐵 + 1 ) ∈ ℤ ∧ 𝐴 ≤ ( 𝐵 + 1 ) ) ) |
16 |
|
breq2 |
⊢ ( 𝑥 = 𝐵 → ( 𝐴 ≤ 𝑥 ↔ 𝐴 ≤ 𝐵 ) ) |
17 |
16
|
elrab |
⊢ ( 𝐵 ∈ { 𝑥 ∈ ℤ ∣ 𝐴 ≤ 𝑥 } ↔ ( 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵 ) ) |
18 |
17
|
anbi2i |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ { 𝑥 ∈ ℤ ∣ 𝐴 ≤ 𝑥 } ) ↔ ( 𝐴 ∈ ℤ ∧ ( 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵 ) ) ) |
19 |
|
breq2 |
⊢ ( 𝑥 = ( 𝐵 + 1 ) → ( 𝐴 ≤ 𝑥 ↔ 𝐴 ≤ ( 𝐵 + 1 ) ) ) |
20 |
19
|
elrab |
⊢ ( ( 𝐵 + 1 ) ∈ { 𝑥 ∈ ℤ ∣ 𝐴 ≤ 𝑥 } ↔ ( ( 𝐵 + 1 ) ∈ ℤ ∧ 𝐴 ≤ ( 𝐵 + 1 ) ) ) |
21 |
15 18 20
|
3imtr4i |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ { 𝑥 ∈ ℤ ∣ 𝐴 ≤ 𝑥 } ) → ( 𝐵 + 1 ) ∈ { 𝑥 ∈ ℤ ∣ 𝐴 ≤ 𝑥 } ) |