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

Metamath Proof Explorer

Theorem fracge0

Description: The fractional part of a real number is nonnegative. (Contributed by NM, 17-Jul-2008)

Ref Expression
Assertion fracge0 ⊢ A ∈ ℝ → 0 ≤ A − A

Proof

Step Hyp Ref Expression
1 flle ⊢ A ∈ ℝ → A ≤ A
2 reflcl ⊢ A ∈ ℝ → A ∈ ℝ
3 subge0 ⊢ A ∈ ℝ ∧ A ∈ ℝ → 0 ≤ A − A ↔ A ≤ A
4 2 3 mpdan ⊢ A ∈ ℝ → 0 ≤ A − A ↔ A ≤ A
5 1 4 mpbird ⊢ A ∈ ℝ → 0 ≤ A − A