This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem alrple

Description: Show that A is less than B by showing that there is no positive bound on the difference. (Contributed by Mario Carneiro, 12-Jun-2014)

		Ref	Expression
	Assertion	alrple	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rexr	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ^* )
2		xralrple	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
3	1 2	sylan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )