Proof of Theorem absmax
Step | Hyp | Ref
| Expression |
1 | | recn 10819 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
2 | | 2cn 11905 |
. . . . . . 7
⊢ 2 ∈
ℂ |
3 | | 2ne0 11934 |
. . . . . . 7
⊢ 2 ≠
0 |
4 | | divcan3 11516 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → ((2 · 𝐴) / 2) = 𝐴) |
5 | 2, 3, 4 | mp3an23 1455 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → ((2
· 𝐴) / 2) = 𝐴) |
6 | 1, 5 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ → ((2
· 𝐴) / 2) = 𝐴) |
7 | 6 | ad2antlr 727 |
. . . 4
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ 𝐵 < 𝐴) → ((2 · 𝐴) / 2) = 𝐴) |
8 | | ltle 10921 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 < 𝐴 → 𝐵 ≤ 𝐴)) |
9 | 8 | imp 410 |
. . . . . . . 8
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ 𝐵 < 𝐴) → 𝐵 ≤ 𝐴) |
10 | | abssubge0 14891 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ≤ 𝐴) → (abs‘(𝐴 − 𝐵)) = (𝐴 − 𝐵)) |
11 | 10 | 3expa 1120 |
. . . . . . . 8
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → (abs‘(𝐴 − 𝐵)) = (𝐴 − 𝐵)) |
12 | 9, 11 | syldan 594 |
. . . . . . 7
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ 𝐵 < 𝐴) → (abs‘(𝐴 − 𝐵)) = (𝐴 − 𝐵)) |
13 | 12 | oveq2d 7229 |
. . . . . 6
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ 𝐵 < 𝐴) → ((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) = ((𝐴 + 𝐵) + (𝐴 − 𝐵))) |
14 | | recn 10819 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
15 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → 𝐴 ∈
ℂ) |
16 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → 𝐵 ∈
ℂ) |
17 | 15, 16, 15 | ppncand 11229 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝐴 + 𝐵) + (𝐴 − 𝐵)) = (𝐴 + 𝐴)) |
18 | | 2times 11966 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (2
· 𝐴) = (𝐴 + 𝐴)) |
19 | 18 | adantl 485 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (2
· 𝐴) = (𝐴 + 𝐴)) |
20 | 17, 19 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝐴 + 𝐵) + (𝐴 − 𝐵)) = (2 · 𝐴)) |
21 | 14, 1, 20 | syl2an 599 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝐴 + 𝐵) + (𝐴 − 𝐵)) = (2 · 𝐴)) |
22 | 21 | adantr 484 |
. . . . . 6
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ 𝐵 < 𝐴) → ((𝐴 + 𝐵) + (𝐴 − 𝐵)) = (2 · 𝐴)) |
23 | 13, 22 | eqtrd 2777 |
. . . . 5
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ 𝐵 < 𝐴) → ((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) = (2 · 𝐴)) |
24 | 23 | oveq1d 7228 |
. . . 4
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ 𝐵 < 𝐴) → (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2) = ((2 · 𝐴) / 2)) |
25 | | ltnle 10912 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 < 𝐴 ↔ ¬ 𝐴 ≤ 𝐵)) |
26 | 25 | biimpa 480 |
. . . . 5
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ 𝐵 < 𝐴) → ¬ 𝐴 ≤ 𝐵) |
27 | 26 | iffalsed 4450 |
. . . 4
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ 𝐵 < 𝐴) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = 𝐴) |
28 | 7, 24, 27 | 3eqtr4rd 2788 |
. . 3
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ 𝐵 < 𝐴) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2)) |
29 | 28 | ancom1s 653 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2)) |
30 | | divcan3 11516 |
. . . . . 6
⊢ ((𝐵 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → ((2 · 𝐵) / 2) = 𝐵) |
31 | 2, 3, 30 | mp3an23 1455 |
. . . . 5
⊢ (𝐵 ∈ ℂ → ((2
· 𝐵) / 2) = 𝐵) |
32 | 14, 31 | syl 17 |
. . . 4
⊢ (𝐵 ∈ ℝ → ((2
· 𝐵) / 2) = 𝐵) |
33 | 32 | ad2antlr 727 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((2 · 𝐵) / 2) = 𝐵) |
34 | | abssuble0 14892 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐴 − 𝐵)) = (𝐵 − 𝐴)) |
35 | 34 | 3expa 1120 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐴 − 𝐵)) = (𝐵 − 𝐴)) |
36 | 35 | oveq2d 7229 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) = ((𝐴 + 𝐵) + (𝐵 − 𝐴))) |
37 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈
ℂ) |
38 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈
ℂ) |
39 | 37, 38, 37 | ppncand 11229 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐵 + 𝐴) + (𝐵 − 𝐴)) = (𝐵 + 𝐵)) |
40 | | addcom 11018 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
41 | 40 | oveq1d 7228 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) + (𝐵 − 𝐴)) = ((𝐵 + 𝐴) + (𝐵 − 𝐴))) |
42 | | 2times 11966 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℂ → (2
· 𝐵) = (𝐵 + 𝐵)) |
43 | 42 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· 𝐵) = (𝐵 + 𝐵)) |
44 | 39, 41, 43 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) + (𝐵 − 𝐴)) = (2 · 𝐵)) |
45 | 1, 14, 44 | syl2an 599 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) + (𝐵 − 𝐴)) = (2 · 𝐵)) |
46 | 45 | adantr 484 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐴 + 𝐵) + (𝐵 − 𝐴)) = (2 · 𝐵)) |
47 | 36, 46 | eqtrd 2777 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) = (2 · 𝐵)) |
48 | 47 | oveq1d 7228 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2) = ((2 · 𝐵) / 2)) |
49 | | iftrue 4445 |
. . . 4
⊢ (𝐴 ≤ 𝐵 → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = 𝐵) |
50 | 49 | adantl 485 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = 𝐵) |
51 | 33, 48, 50 | 3eqtr4rd 2788 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2)) |
52 | | simpr 488 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈
ℝ) |
53 | | simpl 486 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈
ℝ) |
54 | 29, 51, 52, 53 | ltlecasei 10940 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2)) |