Metamath Proof Explorer

Theorem xposdif

Description: Extended real version of posdif . (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion xposdif ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B ↔ 0 < B + 𝑒 − A

Proof

Step Hyp Ref Expression
1 xnegcl ⊢ B ∈ ℝ * → − B ∈ ℝ *
2 xaddcl ⊢ A ∈ ℝ * ∧ − B ∈ ℝ * → A + 𝑒 − B ∈ ℝ *
3 1 2 sylan2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A + 𝑒 − B ∈ ℝ *
4 xlt0neg1 ⊢ A + 𝑒 − B ∈ ℝ * → A + 𝑒 − B < 0 ↔ 0 < − A + 𝑒 − B
5 3 4 syl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A + 𝑒 − B < 0 ↔ 0 < − A + 𝑒 − B
6 xsubge0 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → 0 ≤ A + 𝑒 − B ↔ B ≤ A
7 6 notbid ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → ¬ 0 ≤ A + 𝑒 − B ↔ ¬ B ≤ A
8 0xr ⊢ 0 ∈ ℝ *
9 xrltnle ⊢ A + 𝑒 − B ∈ ℝ * ∧ 0 ∈ ℝ * → A + 𝑒 − B < 0 ↔ ¬ 0 ≤ A + 𝑒 − B
10 3 8 9 sylancl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A + 𝑒 − B < 0 ↔ ¬ 0 ≤ A + 𝑒 − B
11 xrltnle ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B ↔ ¬ B ≤ A
12 7 10 11 3bitr4d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A + 𝑒 − B < 0 ↔ A < B
13 xnegdi ⊢ A ∈ ℝ * ∧ − B ∈ ℝ * → − A + 𝑒 − B = − A + 𝑒 − − B
14 1 13 sylan2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − A + 𝑒 − B = − A + 𝑒 − − B
15 xnegneg ⊢ B ∈ ℝ * → − − B = B
16 15 oveq2d ⊢ B ∈ ℝ * → − A + 𝑒 − − B = − A + 𝑒 B
17 16 adantl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − A + 𝑒 − − B = − A + 𝑒 B
18 xnegcl ⊢ A ∈ ℝ * → − A ∈ ℝ *
19 xaddcom ⊢ − A ∈ ℝ * ∧ B ∈ ℝ * → − A + 𝑒 B = B + 𝑒 − A
20 18 19 sylan ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − A + 𝑒 B = B + 𝑒 − A
21 14 17 20 3eqtrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − A + 𝑒 − B = B + 𝑒 − A
22 21 breq2d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → 0 < − A + 𝑒 − B ↔ 0 < B + 𝑒 − A
23 5 12 22 3bitr3d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B ↔ 0 < B + 𝑒 − A