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