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 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < C ∧ B < C → A + B < 2 ⁢ C

Proof

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