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