Theorem infmrp1

Description: The infimum of the positive reals is 0. (Contributed by AV, 5-Sep-2020)

	Ref	Expression
Assertion	infmrp1	⊢ inf ( ℝ+ , ℝ , < ) = 0

Proof

Step	Hyp	Ref	Expression
1		rpltrp	⊢ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ 𝑦 < 𝑥
2		ltso	⊢ < Or ℝ
3	2	a1i	⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ 𝑦 < 𝑥 → < Or ℝ )
4		0red	⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ 𝑦 < 𝑥 → 0 ∈ ℝ )
5		0red	⊢ ( 𝑧 ∈ ℝ+ → 0 ∈ ℝ )
6		rpre	⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ )
7		rpge0	⊢ ( 𝑧 ∈ ℝ+ → 0 ≤ 𝑧 )
8	5 6 7	lensymd	⊢ ( 𝑧 ∈ ℝ+ → ¬ 𝑧 < 0 )
9	8	adantl	⊢ ( ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ 𝑦 < 𝑥 ∧ 𝑧 ∈ ℝ+ ) → ¬ 𝑧 < 0 )
10		elrp	⊢ ( 𝑧 ∈ ℝ+ ↔ ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ) )
11		breq2	⊢ ( 𝑥 = 𝑧 → ( 𝑦 < 𝑥 ↔ 𝑦 < 𝑧 ) )
12	11	rexbidv	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ ℝ+ 𝑦 < 𝑥 ↔ ∃ 𝑦 ∈ ℝ+ 𝑦 < 𝑧 ) )
13	12	rspcv	⊢ ( 𝑧 ∈ ℝ+ → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ 𝑦 < 𝑥 → ∃ 𝑦 ∈ ℝ+ 𝑦 < 𝑧 ) )
14	10 13	sylbir	⊢ ( ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ 𝑦 < 𝑥 → ∃ 𝑦 ∈ ℝ+ 𝑦 < 𝑧 ) )
15	14	impcom	⊢ ( ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ 𝑦 < 𝑥 ∧ ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ) ) → ∃ 𝑦 ∈ ℝ+ 𝑦 < 𝑧 )
16	3 4 9 15	eqinfd	⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ 𝑦 < 𝑥 → inf ( ℝ+ , ℝ , < ) = 0 )
17	1 16	ax-mp	⊢ inf ( ℝ+ , ℝ , < ) = 0