Proof of Theorem maxltsup
Step | Hyp | Ref
| Expression |
1 | | simpl1 995 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧
sup({𝐴, 𝐵}, ℝ, < ) < 𝐶) → 𝐴 ∈ ℝ) |
2 | | simpl2 996 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧
sup({𝐴, 𝐵}, ℝ, < ) < 𝐶) → 𝐵 ∈ ℝ) |
3 | | maxcl 11174 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
sup({𝐴, 𝐵}, ℝ, < ) ∈
ℝ) |
4 | 1, 2, 3 | syl2anc 409 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧
sup({𝐴, 𝐵}, ℝ, < ) < 𝐶) → sup({𝐴, 𝐵}, ℝ, < ) ∈
ℝ) |
5 | | simpl3 997 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧
sup({𝐴, 𝐵}, ℝ, < ) < 𝐶) → 𝐶 ∈ ℝ) |
6 | | maxle1 11175 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ sup({𝐴, 𝐵}, ℝ, < )) |
7 | 6 | 3adant3 1012 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ≤ sup({𝐴, 𝐵}, ℝ, < )) |
8 | 7 | adantr 274 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧
sup({𝐴, 𝐵}, ℝ, < ) < 𝐶) → 𝐴 ≤ sup({𝐴, 𝐵}, ℝ, < )) |
9 | | simpr 109 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧
sup({𝐴, 𝐵}, ℝ, < ) < 𝐶) → sup({𝐴, 𝐵}, ℝ, < ) < 𝐶) |
10 | 1, 4, 5, 8, 9 | lelttrd 8044 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧
sup({𝐴, 𝐵}, ℝ, < ) < 𝐶) → 𝐴 < 𝐶) |
11 | | maxle2 11176 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ sup({𝐴, 𝐵}, ℝ, < )) |
12 | 1, 2, 11 | syl2anc 409 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧
sup({𝐴, 𝐵}, ℝ, < ) < 𝐶) → 𝐵 ≤ sup({𝐴, 𝐵}, ℝ, < )) |
13 | 2, 4, 5, 12, 9 | lelttrd 8044 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧
sup({𝐴, 𝐵}, ℝ, < ) < 𝐶) → 𝐵 < 𝐶) |
14 | 10, 13 | jca 304 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧
sup({𝐴, 𝐵}, ℝ, < ) < 𝐶) → (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) |
15 | | maxabs 11173 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
sup({𝐴, 𝐵}, ℝ, < ) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2)) |
16 | 15 | 3adant3 1012 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) →
sup({𝐴, 𝐵}, ℝ, < ) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2)) |
17 | 16 | adantr 274 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → sup({𝐴, 𝐵}, ℝ, < ) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2)) |
18 | | 2re 8948 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
19 | 18 | a1i 9 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → 2 ∈ ℝ) |
20 | | simpl3 997 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → 𝐶 ∈ ℝ) |
21 | 19, 20 | remulcld 7950 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (2 · 𝐶) ∈ ℝ) |
22 | 21 | recnd 7948 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (2 · 𝐶) ∈ ℂ) |
23 | | simpl1 995 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → 𝐴 ∈ ℝ) |
24 | 23 | recnd 7948 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → 𝐴 ∈ ℂ) |
25 | | simpl2 996 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℝ) |
26 | 25 | recnd 7948 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℂ) |
27 | 24, 26 | addcld 7939 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (𝐴 + 𝐵) ∈ ℂ) |
28 | 22, 27 | negsubdi2d 8246 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → -((2 · 𝐶) − (𝐴 + 𝐵)) = ((𝐴 + 𝐵) − (2 · 𝐶))) |
29 | 23, 25 | readdcld 7949 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (𝐴 + 𝐵) ∈ ℝ) |
30 | 23, 25 | resubcld 8300 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (𝐴 − 𝐵) ∈ ℝ) |
31 | 26 | 2timesd 9120 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (2 · 𝐵) = (𝐵 + 𝐵)) |
32 | 24, 26, 26 | pnncand 8269 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → ((𝐴 + 𝐵) − (𝐴 − 𝐵)) = (𝐵 + 𝐵)) |
33 | 31, 32 | eqtr4d 2206 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (2 · 𝐵) = ((𝐴 + 𝐵) − (𝐴 − 𝐵))) |
34 | | 2rp 9615 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ+ |
35 | 34 | a1i 9 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → 2 ∈
ℝ+) |
36 | | simprr 527 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → 𝐵 < 𝐶) |
37 | 25, 20, 35, 36 | ltmul2dd 9710 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (2 · 𝐵) < (2 · 𝐶)) |
38 | 33, 37 | eqbrtrrd 4013 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → ((𝐴 + 𝐵) − (𝐴 − 𝐵)) < (2 · 𝐶)) |
39 | 29, 30, 21, 38 | ltsub23d 8469 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → ((𝐴 + 𝐵) − (2 · 𝐶)) < (𝐴 − 𝐵)) |
40 | 28, 39 | eqbrtrd 4011 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → -((2 · 𝐶) − (𝐴 + 𝐵)) < (𝐴 − 𝐵)) |
41 | 24, 26, 24 | nppcan3d 8257 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → ((𝐴 − 𝐵) + (𝐴 + 𝐵)) = (𝐴 + 𝐴)) |
42 | 24 | 2timesd 9120 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (2 · 𝐴) = (𝐴 + 𝐴)) |
43 | 41, 42 | eqtr4d 2206 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → ((𝐴 − 𝐵) + (𝐴 + 𝐵)) = (2 · 𝐴)) |
44 | | simprl 526 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → 𝐴 < 𝐶) |
45 | 23, 20, 35, 44 | ltmul2dd 9710 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (2 · 𝐴) < (2 · 𝐶)) |
46 | 43, 45 | eqbrtrd 4011 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → ((𝐴 − 𝐵) + (𝐴 + 𝐵)) < (2 · 𝐶)) |
47 | 30, 29, 21 | ltaddsubd 8464 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (((𝐴 − 𝐵) + (𝐴 + 𝐵)) < (2 · 𝐶) ↔ (𝐴 − 𝐵) < ((2 · 𝐶) − (𝐴 + 𝐵)))) |
48 | 46, 47 | mpbid 146 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (𝐴 − 𝐵) < ((2 · 𝐶) − (𝐴 + 𝐵))) |
49 | 40, 48 | jca 304 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (-((2 · 𝐶) − (𝐴 + 𝐵)) < (𝐴 − 𝐵) ∧ (𝐴 − 𝐵) < ((2 · 𝐶) − (𝐴 + 𝐵)))) |
50 | 21, 29 | resubcld 8300 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → ((2 · 𝐶) − (𝐴 + 𝐵)) ∈ ℝ) |
51 | 30, 50 | absltd 11138 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → ((abs‘(𝐴 − 𝐵)) < ((2 · 𝐶) − (𝐴 + 𝐵)) ↔ (-((2 · 𝐶) − (𝐴 + 𝐵)) < (𝐴 − 𝐵) ∧ (𝐴 − 𝐵) < ((2 · 𝐶) − (𝐴 + 𝐵))))) |
52 | 49, 51 | mpbird 166 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (abs‘(𝐴 − 𝐵)) < ((2 · 𝐶) − (𝐴 + 𝐵))) |
53 | 30 | recnd 7948 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (𝐴 − 𝐵) ∈ ℂ) |
54 | 53 | abscld 11145 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (abs‘(𝐴 − 𝐵)) ∈ ℝ) |
55 | 29, 54, 21 | ltaddsub2d 8465 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) < (2 · 𝐶) ↔ (abs‘(𝐴 − 𝐵)) < ((2 · 𝐶) − (𝐴 + 𝐵)))) |
56 | 52, 55 | mpbird 166 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → ((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) < (2 · 𝐶)) |
57 | 29, 54 | readdcld 7949 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → ((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) ∈ ℝ) |
58 | 57, 20, 35 | ltdivmuld 9705 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → ((((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2) < 𝐶 ↔ ((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) < (2 · 𝐶))) |
59 | 56, 58 | mpbird 166 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2) < 𝐶) |
60 | 17, 59 | eqbrtrd 4011 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → sup({𝐴, 𝐵}, ℝ, < ) < 𝐶) |
61 | 14, 60 | impbida 591 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) →
(sup({𝐴, 𝐵}, ℝ, < ) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶))) |