Step |
Hyp |
Ref |
Expression |
1 |
|
ssrab2 |
⊢ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ⊆ ℤ |
2 |
|
zssre |
⊢ ℤ ⊆ ℝ |
3 |
1 2
|
sstri |
⊢ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ⊆ ℝ |
4 |
3
|
a1i |
⊢ ( 𝐴 ∈ ℝ → { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ⊆ ℝ ) |
5 |
|
breq1 |
⊢ ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( 𝑥 ≤ 𝐴 ↔ ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) ) |
6 |
|
flcl |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ ) |
7 |
|
flle |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) |
8 |
5 6 7
|
elrabd |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ) |
9 |
8
|
ne0d |
⊢ ( 𝐴 ∈ ℝ → { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ≠ ∅ ) |
10 |
|
reflcl |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ ) |
11 |
|
breq1 |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≤ 𝐴 ↔ 𝑧 ≤ 𝐴 ) ) |
12 |
11
|
elrab |
⊢ ( 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ↔ ( 𝑧 ∈ ℤ ∧ 𝑧 ≤ 𝐴 ) ) |
13 |
|
flge |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑧 ∈ ℤ ) → ( 𝑧 ≤ 𝐴 ↔ 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) ) |
14 |
13
|
biimpd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑧 ∈ ℤ ) → ( 𝑧 ≤ 𝐴 → 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) ) |
15 |
14
|
expimpd |
⊢ ( 𝐴 ∈ ℝ → ( ( 𝑧 ∈ ℤ ∧ 𝑧 ≤ 𝐴 ) → 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) ) |
16 |
12 15
|
syl5bi |
⊢ ( 𝐴 ∈ ℝ → ( 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } → 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) ) |
17 |
16
|
ralrimiv |
⊢ ( 𝐴 ∈ ℝ → ∀ 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) |
18 |
|
brralrspcev |
⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℝ ∧ ∀ 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } 𝑧 ≤ 𝑦 ) |
19 |
10 17 18
|
syl2anc |
⊢ ( 𝐴 ∈ ℝ → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } 𝑧 ≤ 𝑦 ) |
20 |
4 9 19 8
|
suprubd |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ) |
21 |
|
suprleub |
⊢ ( ( ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ⊆ ℝ ∧ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } 𝑧 ≤ 𝑦 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ℝ ) → ( sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ≤ ( ⌊ ‘ 𝐴 ) ↔ ∀ 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) ) |
22 |
4 9 19 10 21
|
syl31anc |
⊢ ( 𝐴 ∈ ℝ → ( sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ≤ ( ⌊ ‘ 𝐴 ) ↔ ∀ 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) ) |
23 |
17 22
|
mpbird |
⊢ ( 𝐴 ∈ ℝ → sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ≤ ( ⌊ ‘ 𝐴 ) ) |
24 |
4 9 19
|
suprcld |
⊢ ( 𝐴 ∈ ℝ → sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ∈ ℝ ) |
25 |
10 24
|
letri3d |
⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) = sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ↔ ( ( ⌊ ‘ 𝐴 ) ≤ sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ∧ sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ≤ ( ⌊ ‘ 𝐴 ) ) ) ) |
26 |
20 23 25
|
mpbir2and |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) = sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ) |