Metamath Proof Explorer

Theorem 2leaddle2

Description: If two real numbers are less than a third real number, the sum of the real numbers is less than twice the third real number. (Contributed by Alexander van der Vekens, 21-May-2018)

Ref Expression
Assertion 2leaddle2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐶 ) → ( 𝐴 + 𝐵 ) < ( 2 · 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 readdcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
2 1 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
3 readdcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + 𝐶 ) ∈ ℝ )
4 3 anidms ⊢ ( 𝐶 ∈ ℝ → ( 𝐶 + 𝐶 ) ∈ ℝ )
5 4 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + 𝐶 ) ∈ ℝ )
6 2re ⊢ 2 ∈ ℝ
7 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 2 · 𝐶 ) ∈ ℝ )
8 6 7 mpan ⊢ ( 𝐶 ∈ ℝ → ( 2 · 𝐶 ) ∈ ℝ )
9 8 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 2 · 𝐶 ) ∈ ℝ )
10 2 5 9 3jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ ( 𝐶 + 𝐶 ) ∈ ℝ ∧ ( 2 · 𝐶 ) ∈ ℝ ) )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐶 ) ) → ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ ( 𝐶 + 𝐶 ) ∈ ℝ ∧ ( 2 · 𝐶 ) ∈ ℝ ) )
12 id ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
13 12 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
14 id ⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℝ )
15 14 14 jca ⊢ ( 𝐶 ∈ ℝ → ( 𝐶 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
16 15 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
17 13 16 jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) )
18 17 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐶 ) ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) )
19 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐶 ) ) → ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐶 ) )
20 lt2add ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐶 ) → ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐶 ) ) )
21 18 19 20 sylc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐶 ) ) → ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐶 ) )
22 recn ⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
23 22 2timesd ⊢ ( 𝐶 ∈ ℝ → ( 2 · 𝐶 ) = ( 𝐶 + 𝐶 ) )
24 8 leidd ⊢ ( 𝐶 ∈ ℝ → ( 2 · 𝐶 ) ≤ ( 2 · 𝐶 ) )
25 23 24 eqbrtrrd ⊢ ( 𝐶 ∈ ℝ → ( 𝐶 + 𝐶 ) ≤ ( 2 · 𝐶 ) )
26 25 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + 𝐶 ) ≤ ( 2 · 𝐶 ) )
27 26 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐶 ) ) → ( 𝐶 + 𝐶 ) ≤ ( 2 · 𝐶 ) )
28 21 27 jca ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐶 ) ) → ( ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐶 ) ∧ ( 𝐶 + 𝐶 ) ≤ ( 2 · 𝐶 ) ) )
29 ltletr ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ ( 𝐶 + 𝐶 ) ∈ ℝ ∧ ( 2 · 𝐶 ) ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐶 ) ∧ ( 𝐶 + 𝐶 ) ≤ ( 2 · 𝐶 ) ) → ( 𝐴 + 𝐵 ) < ( 2 · 𝐶 ) ) )
30 11 28 29 sylc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐶 ) ) → ( 𝐴 + 𝐵 ) < ( 2 · 𝐶 ) )
31 30 ex ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐶 ) → ( 𝐴 + 𝐵 ) < ( 2 · 𝐶 ) ) )