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

Metamath Proof Explorer

Theorem xposdif

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

Ref Expression
Assertion xposdif ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 +𝑒 -𝑒 𝐴 ) ) )

Proof

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