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 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) ) )