Metamath Proof Explorer


Theorem xleadd1

Description: Weakened version of xleadd1a under which the reverse implication is true. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xleadd1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( 𝐴𝐵 ↔ ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 rexr ( 𝐶 ∈ ℝ → 𝐶 ∈ ℝ* )
2 xleadd1a ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
3 2 ex ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐴𝐵 → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) ) )
4 1 3 syl3an3 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( 𝐴𝐵 → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) ) )
5 simp1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ* )
6 1 3ad2ant3 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ* )
7 xaddcl ( ( 𝐴 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐴 +𝑒 𝐶 ) ∈ ℝ* )
8 5 6 7 syl2anc ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( 𝐴 +𝑒 𝐶 ) ∈ ℝ* )
9 simp2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ* )
10 xaddcl ( ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* )
11 9 6 10 syl2anc ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* )
12 xnegcl ( 𝐶 ∈ ℝ* → -𝑒 𝐶 ∈ ℝ* )
13 6 12 syl ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → -𝑒 𝐶 ∈ ℝ* )
14 xleadd1a ( ( ( ( 𝐴 +𝑒 𝐶 ) ∈ ℝ* ∧ ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* ∧ -𝑒 𝐶 ∈ ℝ* ) ∧ ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) ) → ( ( 𝐴 +𝑒 𝐶 ) +𝑒 -𝑒 𝐶 ) ≤ ( ( 𝐵 +𝑒 𝐶 ) +𝑒 -𝑒 𝐶 ) )
15 14 ex ( ( ( 𝐴 +𝑒 𝐶 ) ∈ ℝ* ∧ ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* ∧ -𝑒 𝐶 ∈ ℝ* ) → ( ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) → ( ( 𝐴 +𝑒 𝐶 ) +𝑒 -𝑒 𝐶 ) ≤ ( ( 𝐵 +𝑒 𝐶 ) +𝑒 -𝑒 𝐶 ) ) )
16 8 11 13 15 syl3anc ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) → ( ( 𝐴 +𝑒 𝐶 ) +𝑒 -𝑒 𝐶 ) ≤ ( ( 𝐵 +𝑒 𝐶 ) +𝑒 -𝑒 𝐶 ) ) )
17 xpncan ( ( 𝐴 ∈ ℝ*𝐶 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐶 ) +𝑒 -𝑒 𝐶 ) = 𝐴 )
18 17 3adant2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐶 ) +𝑒 -𝑒 𝐶 ) = 𝐴 )
19 xpncan ( ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( ( 𝐵 +𝑒 𝐶 ) +𝑒 -𝑒 𝐶 ) = 𝐵 )
20 19 3adant1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( ( 𝐵 +𝑒 𝐶 ) +𝑒 -𝑒 𝐶 ) = 𝐵 )
21 18 20 breq12d ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( ( ( 𝐴 +𝑒 𝐶 ) +𝑒 -𝑒 𝐶 ) ≤ ( ( 𝐵 +𝑒 𝐶 ) +𝑒 -𝑒 𝐶 ) ↔ 𝐴𝐵 ) )
22 16 21 sylibd ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) → 𝐴𝐵 ) )
23 4 22 impbid ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( 𝐴𝐵 ↔ ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) ) )