Metamath Proof Explorer

Theorem xltadd1

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

Ref Expression
Assertion xltadd1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ → A < B ↔ A + 𝑒 C < B + 𝑒 C

Proof

Step Hyp Ref Expression
1 xleadd1 ⊢ B ∈ ℝ * ∧ A ∈ ℝ * ∧ C ∈ ℝ → B ≤ A ↔ B + 𝑒 C ≤ A + 𝑒 C
2 1 3com12 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ → B ≤ A ↔ B + 𝑒 C ≤ A + 𝑒 C
3 2 notbid ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ → ¬ B ≤ A ↔ ¬ B + 𝑒 C ≤ A + 𝑒 C
4 xrltnle ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B ↔ ¬ B ≤ A
5 4 3adant3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ → A < B ↔ ¬ B ≤ A
6 simp1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ → A ∈ ℝ *
7 rexr ⊢ C ∈ ℝ → C ∈ ℝ *
8 7 3ad2ant3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ → C ∈ ℝ *
9 xaddcl ⊢ A ∈ ℝ * ∧ C ∈ ℝ * → A + 𝑒 C ∈ ℝ *
10 6 8 9 syl2anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ → A + 𝑒 C ∈ ℝ *
11 simp2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ → B ∈ ℝ *
12 xaddcl ⊢ B ∈ ℝ * ∧ C ∈ ℝ * → B + 𝑒 C ∈ ℝ *
13 11 8 12 syl2anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ → B + 𝑒 C ∈ ℝ *
14 xrltnle ⊢ A + 𝑒 C ∈ ℝ * ∧ B + 𝑒 C ∈ ℝ * → A + 𝑒 C < B + 𝑒 C ↔ ¬ B + 𝑒 C ≤ A + 𝑒 C
15 10 13 14 syl2anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ → A + 𝑒 C < B + 𝑒 C ↔ ¬ B + 𝑒 C ≤ A + 𝑒 C
16 3 5 15 3bitr4d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ → A < B ↔ A + 𝑒 C < B + 𝑒 C