Proof of Theorem amgm2
Step | Hyp | Ref
| Expression |
1 | | 2cn 11734 |
. . . . . 6
⊢ 2 ∈
ℂ |
2 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐴 ∈ ℝ) |
3 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐵 ∈ ℝ) |
4 | | remulcl 10645 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) |
5 | 2, 3, 4 | syl2anc 588 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 · 𝐵) ∈ ℝ) |
6 | | mulge0 11181 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵)) |
7 | | resqrtcl 14646 |
. . . . . . . 8
⊢ (((𝐴 · 𝐵) ∈ ℝ ∧ 0 ≤ (𝐴 · 𝐵)) → (√‘(𝐴 · 𝐵)) ∈ ℝ) |
8 | 5, 6, 7 | syl2anc 588 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) ∈ ℝ) |
9 | 8 | recnd 10692 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) ∈ ℂ) |
10 | | sqmul 13520 |
. . . . . 6
⊢ ((2
∈ ℂ ∧ (√‘(𝐴 · 𝐵)) ∈ ℂ) → ((2 ·
(√‘(𝐴 ·
𝐵)))↑2) = ((2↑2)
· ((√‘(𝐴
· 𝐵))↑2))) |
11 | 1, 9, 10 | sylancr 591 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((2 ·
(√‘(𝐴 ·
𝐵)))↑2) = ((2↑2)
· ((√‘(𝐴
· 𝐵))↑2))) |
12 | | sq2 13595 |
. . . . . . 7
⊢
(2↑2) = 4 |
13 | 12 | oveq1i 7153 |
. . . . . 6
⊢
((2↑2) · ((√‘(𝐴 · 𝐵))↑2)) = (4 ·
((√‘(𝐴 ·
𝐵))↑2)) |
14 | 5 | recnd 10692 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 · 𝐵) ∈ ℂ) |
15 | | sqrtth 14757 |
. . . . . . . 8
⊢ ((𝐴 · 𝐵) ∈ ℂ →
((√‘(𝐴 ·
𝐵))↑2) = (𝐴 · 𝐵)) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘(𝐴 · 𝐵))↑2) = (𝐴 · 𝐵)) |
17 | 16 | oveq2d 7159 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (4 ·
((√‘(𝐴 ·
𝐵))↑2)) = (4 ·
(𝐴 · 𝐵))) |
18 | 13, 17 | syl5eq 2806 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((2↑2) ·
((√‘(𝐴 ·
𝐵))↑2)) = (4 ·
(𝐴 · 𝐵))) |
19 | 11, 18 | eqtrd 2794 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((2 ·
(√‘(𝐴 ·
𝐵)))↑2) = (4 ·
(𝐴 · 𝐵))) |
20 | 2, 3 | resubcld 11091 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 − 𝐵) ∈ ℝ) |
21 | 20 | sqge0d 13647 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ ((𝐴 − 𝐵)↑2)) |
22 | 2 | recnd 10692 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐴 ∈ ℂ) |
23 | 3 | recnd 10692 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐵 ∈ ℂ) |
24 | | binom2 13614 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2))) |
25 | 22, 23, 24 | syl2anc 588 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2))) |
26 | | binom2sub 13616 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2))) |
27 | 22, 23, 26 | syl2anc 588 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2))) |
28 | 25, 27 | oveq12d 7161 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (((𝐴 + 𝐵)↑2) − ((𝐴 − 𝐵)↑2)) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2)))) |
29 | 2 | resqcld 13646 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴↑2) ∈ ℝ) |
30 | | 2re 11733 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
31 | | remulcl 10645 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ (𝐴
· 𝐵) ∈ ℝ)
→ (2 · (𝐴
· 𝐵)) ∈
ℝ) |
32 | 30, 5, 31 | sylancr 591 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (2 · (𝐴 · 𝐵)) ∈ ℝ) |
33 | 29, 32 | readdcld 10693 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) + (2 · (𝐴 · 𝐵))) ∈ ℝ) |
34 | 33 | recnd 10692 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) + (2 · (𝐴 · 𝐵))) ∈ ℂ) |
35 | 29, 32 | resubcld 11091 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) − (2 · (𝐴 · 𝐵))) ∈ ℝ) |
36 | 35 | recnd 10692 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) − (2 · (𝐴 · 𝐵))) ∈ ℂ) |
37 | 3 | resqcld 13646 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐵↑2) ∈ ℝ) |
38 | 37 | recnd 10692 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐵↑2) ∈ ℂ) |
39 | 34, 36, 38 | pnpcan2d 11058 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2))) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) − ((𝐴↑2) − (2 · (𝐴 · 𝐵))))) |
40 | 32 | recnd 10692 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (2 · (𝐴 · 𝐵)) ∈ ℂ) |
41 | 40 | 2timesd 11902 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (2 · (2
· (𝐴 · 𝐵))) = ((2 · (𝐴 · 𝐵)) + (2 · (𝐴 · 𝐵)))) |
42 | | 2t2e4 11823 |
. . . . . . . . . . 11
⊢ (2
· 2) = 4 |
43 | 42 | oveq1i 7153 |
. . . . . . . . . 10
⊢ ((2
· 2) · (𝐴
· 𝐵)) = (4 ·
(𝐴 · 𝐵)) |
44 | | 2cnd 11737 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 2 ∈
ℂ) |
45 | 44, 44, 14 | mulassd 10687 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((2 · 2)
· (𝐴 · 𝐵)) = (2 · (2 ·
(𝐴 · 𝐵)))) |
46 | 43, 45 | syl5eqr 2808 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (4 · (𝐴 · 𝐵)) = (2 · (2 · (𝐴 · 𝐵)))) |
47 | 29 | recnd 10692 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴↑2) ∈ ℂ) |
48 | 47, 40, 40 | pnncand 11059 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (((𝐴↑2) + (2 · (𝐴 · 𝐵))) − ((𝐴↑2) − (2 · (𝐴 · 𝐵)))) = ((2 · (𝐴 · 𝐵)) + (2 · (𝐴 · 𝐵)))) |
49 | 41, 46, 48 | 3eqtr4rd 2805 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (((𝐴↑2) + (2 · (𝐴 · 𝐵))) − ((𝐴↑2) − (2 · (𝐴 · 𝐵)))) = (4 · (𝐴 · 𝐵))) |
50 | 28, 39, 49 | 3eqtrd 2798 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (((𝐴 + 𝐵)↑2) − ((𝐴 − 𝐵)↑2)) = (4 · (𝐴 · 𝐵))) |
51 | 2, 3 | readdcld 10693 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 + 𝐵) ∈ ℝ) |
52 | 51 | resqcld 13646 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 + 𝐵)↑2) ∈ ℝ) |
53 | 52 | recnd 10692 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 + 𝐵)↑2) ∈ ℂ) |
54 | 20 | resqcld 13646 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 − 𝐵)↑2) ∈ ℝ) |
55 | 54 | recnd 10692 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 − 𝐵)↑2) ∈ ℂ) |
56 | | 4re 11743 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
57 | | remulcl 10645 |
. . . . . . . . . 10
⊢ ((4
∈ ℝ ∧ (𝐴
· 𝐵) ∈ ℝ)
→ (4 · (𝐴
· 𝐵)) ∈
ℝ) |
58 | 56, 5, 57 | sylancr 591 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (4 · (𝐴 · 𝐵)) ∈ ℝ) |
59 | 58 | recnd 10692 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (4 · (𝐴 · 𝐵)) ∈ ℂ) |
60 | | subsub23 10914 |
. . . . . . . 8
⊢ ((((𝐴 + 𝐵)↑2) ∈ ℂ ∧ ((𝐴 − 𝐵)↑2) ∈ ℂ ∧ (4 ·
(𝐴 · 𝐵)) ∈ ℂ) →
((((𝐴 + 𝐵)↑2) − ((𝐴 − 𝐵)↑2)) = (4 · (𝐴 · 𝐵)) ↔ (((𝐴 + 𝐵)↑2) − (4 · (𝐴 · 𝐵))) = ((𝐴 − 𝐵)↑2))) |
61 | 53, 55, 59, 60 | syl3anc 1369 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((((𝐴 + 𝐵)↑2) − ((𝐴 − 𝐵)↑2)) = (4 · (𝐴 · 𝐵)) ↔ (((𝐴 + 𝐵)↑2) − (4 · (𝐴 · 𝐵))) = ((𝐴 − 𝐵)↑2))) |
62 | 50, 61 | mpbid 235 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (((𝐴 + 𝐵)↑2) − (4 · (𝐴 · 𝐵))) = ((𝐴 − 𝐵)↑2)) |
63 | 21, 62 | breqtrrd 5053 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (((𝐴 + 𝐵)↑2) − (4 · (𝐴 · 𝐵)))) |
64 | 52, 58 | subge0d 11253 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (0 ≤ (((𝐴 + 𝐵)↑2) − (4 · (𝐴 · 𝐵))) ↔ (4 · (𝐴 · 𝐵)) ≤ ((𝐴 + 𝐵)↑2))) |
65 | 63, 64 | mpbid 235 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (4 · (𝐴 · 𝐵)) ≤ ((𝐴 + 𝐵)↑2)) |
66 | 19, 65 | eqbrtrd 5047 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((2 ·
(√‘(𝐴 ·
𝐵)))↑2) ≤ ((𝐴 + 𝐵)↑2)) |
67 | | remulcl 10645 |
. . . . 5
⊢ ((2
∈ ℝ ∧ (√‘(𝐴 · 𝐵)) ∈ ℝ) → (2 ·
(√‘(𝐴 ·
𝐵))) ∈
ℝ) |
68 | 30, 8, 67 | sylancr 591 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (2 ·
(√‘(𝐴 ·
𝐵))) ∈
ℝ) |
69 | | sqrtge0 14650 |
. . . . . 6
⊢ (((𝐴 · 𝐵) ∈ ℝ ∧ 0 ≤ (𝐴 · 𝐵)) → 0 ≤ (√‘(𝐴 · 𝐵))) |
70 | 5, 6, 69 | syl2anc 588 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤
(√‘(𝐴 ·
𝐵))) |
71 | | 0le2 11761 |
. . . . . 6
⊢ 0 ≤
2 |
72 | | mulge0 11181 |
. . . . . 6
⊢ (((2
∈ ℝ ∧ 0 ≤ 2) ∧ ((√‘(𝐴 · 𝐵)) ∈ ℝ ∧ 0 ≤
(√‘(𝐴 ·
𝐵)))) → 0 ≤ (2
· (√‘(𝐴
· 𝐵)))) |
73 | 30, 71, 72 | mpanl12 702 |
. . . . 5
⊢
(((√‘(𝐴
· 𝐵)) ∈ ℝ
∧ 0 ≤ (√‘(𝐴 · 𝐵))) → 0 ≤ (2 ·
(√‘(𝐴 ·
𝐵)))) |
74 | 8, 70, 73 | syl2anc 588 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (2 ·
(√‘(𝐴 ·
𝐵)))) |
75 | | addge0 11152 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 + 𝐵)) |
76 | 75 | an4s 660 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 + 𝐵)) |
77 | 68, 51, 74, 76 | le2sqd 13655 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((2 ·
(√‘(𝐴 ·
𝐵))) ≤ (𝐴 + 𝐵) ↔ ((2 · (√‘(𝐴 · 𝐵)))↑2) ≤ ((𝐴 + 𝐵)↑2))) |
78 | 66, 77 | mpbird 260 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (2 ·
(√‘(𝐴 ·
𝐵))) ≤ (𝐴 + 𝐵)) |
79 | | 2rp 12420 |
. . . 4
⊢ 2 ∈
ℝ+ |
80 | 79 | a1i 11 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 2 ∈
ℝ+) |
81 | 8, 51, 80 | lemuldiv2d 12507 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((2 ·
(√‘(𝐴 ·
𝐵))) ≤ (𝐴 + 𝐵) ↔ (√‘(𝐴 · 𝐵)) ≤ ((𝐴 + 𝐵) / 2))) |
82 | 78, 81 | mpbid 235 |
1
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) ≤ ((𝐴 + 𝐵) / 2)) |