Theorem uzsup

Description: An upper set of integers is unbounded above. (Contributed by Mario Carneiro, 7-May-2016)

	Ref	Expression
Hypothesis	uzsup.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	uzsup	⊢ ( 𝑀 ∈ ℤ → sup ( 𝑍 , ℝ* , < ) = +∞ )

Proof

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 ( 𝑍 , ℝ* , < ) = +∞ )