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 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ → A ≤ B ↔ A + 𝑒 C ≤ B + 𝑒 C

Proof

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