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 < ( 𝐵 +𝑒 -𝑒 𝐴 ) ) )