Metamath Proof Explorer


Theorem xraddge02

Description: A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 28-Dec-2016)

Ref Expression
Assertion xraddge02 A * B * 0 B A A + 𝑒 B

Proof

Step Hyp Ref Expression
1 xrleid A * A A
2 1 adantr A * B * A A
3 simpl A * B * A *
4 0xr 0 *
5 3 4 jctir A * B * A * 0 *
6 xle2add A * 0 * A * B * A A 0 B A + 𝑒 0 A + 𝑒 B
7 5 6 mpancom A * B * A A 0 B A + 𝑒 0 A + 𝑒 B
8 2 7 mpand A * B * 0 B A + 𝑒 0 A + 𝑒 B
9 xaddid1 A * A + 𝑒 0 = A
10 9 breq1d A * A + 𝑒 0 A + 𝑒 B A A + 𝑒 B
11 10 adantr A * B * A + 𝑒 0 A + 𝑒 B A A + 𝑒 B
12 8 11 sylibd A * B * 0 B A A + 𝑒 B