Step |
Hyp |
Ref |
Expression |
1 |
|
uzsup.1 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
2 |
|
simpl |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → 𝑀 ∈ ℤ ) |
3 |
|
flcl |
⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ∈ ℤ ) |
4 |
3
|
peano2zd |
⊢ ( 𝑥 ∈ ℝ → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℤ ) |
5 |
|
id |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℤ ) |
6 |
|
ifcl |
⊢ ( ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ∈ ℤ ) |
7 |
4 5 6
|
syl2anr |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ∈ ℤ ) |
8 |
|
zre |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ ) |
9 |
|
reflcl |
⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ∈ ℝ ) |
10 |
|
peano2re |
⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℝ → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ ) |
11 |
9 10
|
syl |
⊢ ( 𝑥 ∈ ℝ → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ ) |
12 |
|
max1 |
⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ) |
13 |
8 11 12
|
syl2an |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ) |
14 |
|
eluz2 |
⊢ ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ∈ ℤ ∧ 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ) ) |
15 |
2 7 13 14
|
syl3anbrc |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |
16 |
15 1
|
eleqtrrdi |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ∈ 𝑍 ) |
17 |
|
simpr |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ ) |
18 |
11
|
adantl |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ ) |
19 |
7
|
zred |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ∈ ℝ ) |
20 |
|
fllep1 |
⊢ ( 𝑥 ∈ ℝ → 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) |
21 |
20
|
adantl |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) |
22 |
|
max2 |
⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ) |
23 |
8 11 22
|
syl2an |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ) |
24 |
17 18 19 21 23
|
letrd |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → 𝑥 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ) |
25 |
|
breq2 |
⊢ ( 𝑛 = if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) → ( 𝑥 ≤ 𝑛 ↔ 𝑥 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ) ) |
26 |
25
|
rspcev |
⊢ ( ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ∈ 𝑍 ∧ 𝑥 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) , ( ( ⌊ ‘ 𝑥 ) + 1 ) , 𝑀 ) ) → ∃ 𝑛 ∈ 𝑍 𝑥 ≤ 𝑛 ) |
27 |
16 24 26
|
syl2anc |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℝ ) → ∃ 𝑛 ∈ 𝑍 𝑥 ≤ 𝑛 ) |
28 |
27
|
ralrimiva |
⊢ ( 𝑀 ∈ ℤ → ∀ 𝑥 ∈ ℝ ∃ 𝑛 ∈ 𝑍 𝑥 ≤ 𝑛 ) |
29 |
|
uzssz |
⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ |
30 |
1 29
|
eqsstri |
⊢ 𝑍 ⊆ ℤ |
31 |
|
zssre |
⊢ ℤ ⊆ ℝ |
32 |
30 31
|
sstri |
⊢ 𝑍 ⊆ ℝ |
33 |
|
ressxr |
⊢ ℝ ⊆ ℝ* |
34 |
32 33
|
sstri |
⊢ 𝑍 ⊆ ℝ* |
35 |
|
supxrunb1 |
⊢ ( 𝑍 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑛 ∈ 𝑍 𝑥 ≤ 𝑛 ↔ sup ( 𝑍 , ℝ* , < ) = +∞ ) ) |
36 |
34 35
|
ax-mp |
⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑛 ∈ 𝑍 𝑥 ≤ 𝑛 ↔ sup ( 𝑍 , ℝ* , < ) = +∞ ) |
37 |
28 36
|
sylib |
⊢ ( 𝑀 ∈ ℤ → sup ( 𝑍 , ℝ* , < ) = +∞ ) |