Proof of Theorem amgm2
| Step | Hyp | Ref
| Expression |
| 1 | | 2cn 12341 |
. . . . . 6
⊢ 2 ∈
ℂ |
| 2 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐴 ∈ ℝ) |
| 3 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐵 ∈ ℝ) |
| 4 | | remulcl 11240 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) |
| 5 | 2, 3, 4 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 · 𝐵) ∈ ℝ) |
| 6 | | mulge0 11781 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵)) |
| 7 | | resqrtcl 15292 |
. . . . . . . 8
⊢ (((𝐴 · 𝐵) ∈ ℝ ∧ 0 ≤ (𝐴 · 𝐵)) → (√‘(𝐴 · 𝐵)) ∈ ℝ) |
| 8 | 5, 6, 7 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) ∈ ℝ) |
| 9 | 8 | recnd 11289 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) ∈ ℂ) |
| 10 | | sqmul 14159 |
. . . . . 6
⊢ ((2
∈ ℂ ∧ (√‘(𝐴 · 𝐵)) ∈ ℂ) → ((2 ·
(√‘(𝐴 ·
𝐵)))↑2) = ((2↑2)
· ((√‘(𝐴
· 𝐵))↑2))) |
| 11 | 1, 9, 10 | sylancr 587 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((2 ·
(√‘(𝐴 ·
𝐵)))↑2) = ((2↑2)
· ((√‘(𝐴
· 𝐵))↑2))) |
| 12 | | sq2 14236 |
. . . . . . 7
⊢
(2↑2) = 4 |
| 13 | 12 | oveq1i 7441 |
. . . . . 6
⊢
((2↑2) · ((√‘(𝐴 · 𝐵))↑2)) = (4 ·
((√‘(𝐴 ·
𝐵))↑2)) |
| 14 | 5 | recnd 11289 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 · 𝐵) ∈ ℂ) |
| 15 | | sqrtth 15403 |
. . . . . . . 8
⊢ ((𝐴 · 𝐵) ∈ ℂ →
((√‘(𝐴 ·
𝐵))↑2) = (𝐴 · 𝐵)) |
| 16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘(𝐴 · 𝐵))↑2) = (𝐴 · 𝐵)) |
| 17 | 16 | oveq2d 7447 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (4 ·
((√‘(𝐴 ·
𝐵))↑2)) = (4 ·
(𝐴 · 𝐵))) |
| 18 | 13, 17 | eqtrid 2789 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((2↑2) ·
((√‘(𝐴 ·
𝐵))↑2)) = (4 ·
(𝐴 · 𝐵))) |
| 19 | 11, 18 | eqtrd 2777 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((2 ·
(√‘(𝐴 ·
𝐵)))↑2) = (4 ·
(𝐴 · 𝐵))) |
| 20 | 2, 3 | resubcld 11691 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 − 𝐵) ∈ ℝ) |
| 21 | 20 | sqge0d 14177 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ ((𝐴 − 𝐵)↑2)) |
| 22 | 2 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐴 ∈ ℂ) |
| 23 | 3 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐵 ∈ ℂ) |
| 24 | | binom2 14256 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2))) |
| 25 | 22, 23, 24 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2))) |
| 26 | | binom2sub 14259 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2))) |
| 27 | 22, 23, 26 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2))) |
| 28 | 25, 27 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (((𝐴 + 𝐵)↑2) − ((𝐴 − 𝐵)↑2)) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2)))) |
| 29 | 2 | resqcld 14165 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴↑2) ∈ ℝ) |
| 30 | | 2re 12340 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
| 31 | | remulcl 11240 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ (𝐴
· 𝐵) ∈ ℝ)
→ (2 · (𝐴
· 𝐵)) ∈
ℝ) |
| 32 | 30, 5, 31 | sylancr 587 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (2 · (𝐴 · 𝐵)) ∈ ℝ) |
| 33 | 29, 32 | readdcld 11290 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) + (2 · (𝐴 · 𝐵))) ∈ ℝ) |
| 34 | 33 | recnd 11289 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) + (2 · (𝐴 · 𝐵))) ∈ ℂ) |
| 35 | 29, 32 | resubcld 11691 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) − (2 · (𝐴 · 𝐵))) ∈ ℝ) |
| 36 | 35 | recnd 11289 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) − (2 · (𝐴 · 𝐵))) ∈ ℂ) |
| 37 | 3 | resqcld 14165 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐵↑2) ∈ ℝ) |
| 38 | 37 | recnd 11289 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐵↑2) ∈ ℂ) |
| 39 | 34, 36, 38 | pnpcan2d 11658 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2))) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) − ((𝐴↑2) − (2 · (𝐴 · 𝐵))))) |
| 40 | 32 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (2 · (𝐴 · 𝐵)) ∈ ℂ) |
| 41 | 40 | 2timesd 12509 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (2 · (2
· (𝐴 · 𝐵))) = ((2 · (𝐴 · 𝐵)) + (2 · (𝐴 · 𝐵)))) |
| 42 | | 2t2e4 12430 |
. . . . . . . . . . 11
⊢ (2
· 2) = 4 |
| 43 | 42 | oveq1i 7441 |
. . . . . . . . . 10
⊢ ((2
· 2) · (𝐴
· 𝐵)) = (4 ·
(𝐴 · 𝐵)) |
| 44 | | 2cnd 12344 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 2 ∈
ℂ) |
| 45 | 44, 44, 14 | mulassd 11284 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((2 · 2)
· (𝐴 · 𝐵)) = (2 · (2 ·
(𝐴 · 𝐵)))) |
| 46 | 43, 45 | eqtr3id 2791 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (4 · (𝐴 · 𝐵)) = (2 · (2 · (𝐴 · 𝐵)))) |
| 47 | 29 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴↑2) ∈ ℂ) |
| 48 | 47, 40, 40 | pnncand 11659 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (((𝐴↑2) + (2 · (𝐴 · 𝐵))) − ((𝐴↑2) − (2 · (𝐴 · 𝐵)))) = ((2 · (𝐴 · 𝐵)) + (2 · (𝐴 · 𝐵)))) |
| 49 | 41, 46, 48 | 3eqtr4rd 2788 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (((𝐴↑2) + (2 · (𝐴 · 𝐵))) − ((𝐴↑2) − (2 · (𝐴 · 𝐵)))) = (4 · (𝐴 · 𝐵))) |
| 50 | 28, 39, 49 | 3eqtrd 2781 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (((𝐴 + 𝐵)↑2) − ((𝐴 − 𝐵)↑2)) = (4 · (𝐴 · 𝐵))) |
| 51 | 2, 3 | readdcld 11290 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 + 𝐵) ∈ ℝ) |
| 52 | 51 | resqcld 14165 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 + 𝐵)↑2) ∈ ℝ) |
| 53 | 52 | recnd 11289 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 + 𝐵)↑2) ∈ ℂ) |
| 54 | 20 | resqcld 14165 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 − 𝐵)↑2) ∈ ℝ) |
| 55 | 54 | recnd 11289 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 − 𝐵)↑2) ∈ ℂ) |
| 56 | | 4re 12350 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
| 57 | | remulcl 11240 |
. . . . . . . . . 10
⊢ ((4
∈ ℝ ∧ (𝐴
· 𝐵) ∈ ℝ)
→ (4 · (𝐴
· 𝐵)) ∈
ℝ) |
| 58 | 56, 5, 57 | sylancr 587 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (4 · (𝐴 · 𝐵)) ∈ ℝ) |
| 59 | 58 | recnd 11289 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (4 · (𝐴 · 𝐵)) ∈ ℂ) |
| 60 | | subsub23 11513 |
. . . . . . . 8
⊢ ((((𝐴 + 𝐵)↑2) ∈ ℂ ∧ ((𝐴 − 𝐵)↑2) ∈ ℂ ∧ (4 ·
(𝐴 · 𝐵)) ∈ ℂ) →
((((𝐴 + 𝐵)↑2) − ((𝐴 − 𝐵)↑2)) = (4 · (𝐴 · 𝐵)) ↔ (((𝐴 + 𝐵)↑2) − (4 · (𝐴 · 𝐵))) = ((𝐴 − 𝐵)↑2))) |
| 61 | 53, 55, 59, 60 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((((𝐴 + 𝐵)↑2) − ((𝐴 − 𝐵)↑2)) = (4 · (𝐴 · 𝐵)) ↔ (((𝐴 + 𝐵)↑2) − (4 · (𝐴 · 𝐵))) = ((𝐴 − 𝐵)↑2))) |
| 62 | 50, 61 | mpbid 232 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (((𝐴 + 𝐵)↑2) − (4 · (𝐴 · 𝐵))) = ((𝐴 − 𝐵)↑2)) |
| 63 | 21, 62 | breqtrrd 5171 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (((𝐴 + 𝐵)↑2) − (4 · (𝐴 · 𝐵)))) |
| 64 | 52, 58 | subge0d 11853 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (0 ≤ (((𝐴 + 𝐵)↑2) − (4 · (𝐴 · 𝐵))) ↔ (4 · (𝐴 · 𝐵)) ≤ ((𝐴 + 𝐵)↑2))) |
| 65 | 63, 64 | mpbid 232 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (4 · (𝐴 · 𝐵)) ≤ ((𝐴 + 𝐵)↑2)) |
| 66 | 19, 65 | eqbrtrd 5165 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((2 ·
(√‘(𝐴 ·
𝐵)))↑2) ≤ ((𝐴 + 𝐵)↑2)) |
| 67 | | remulcl 11240 |
. . . . 5
⊢ ((2
∈ ℝ ∧ (√‘(𝐴 · 𝐵)) ∈ ℝ) → (2 ·
(√‘(𝐴 ·
𝐵))) ∈
ℝ) |
| 68 | 30, 8, 67 | sylancr 587 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (2 ·
(√‘(𝐴 ·
𝐵))) ∈
ℝ) |
| 69 | | sqrtge0 15296 |
. . . . . 6
⊢ (((𝐴 · 𝐵) ∈ ℝ ∧ 0 ≤ (𝐴 · 𝐵)) → 0 ≤ (√‘(𝐴 · 𝐵))) |
| 70 | 5, 6, 69 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤
(√‘(𝐴 ·
𝐵))) |
| 71 | | 0le2 12368 |
. . . . . 6
⊢ 0 ≤
2 |
| 72 | | mulge0 11781 |
. . . . . 6
⊢ (((2
∈ ℝ ∧ 0 ≤ 2) ∧ ((√‘(𝐴 · 𝐵)) ∈ ℝ ∧ 0 ≤
(√‘(𝐴 ·
𝐵)))) → 0 ≤ (2
· (√‘(𝐴
· 𝐵)))) |
| 73 | 30, 71, 72 | mpanl12 702 |
. . . . 5
⊢
(((√‘(𝐴
· 𝐵)) ∈ ℝ
∧ 0 ≤ (√‘(𝐴 · 𝐵))) → 0 ≤ (2 ·
(√‘(𝐴 ·
𝐵)))) |
| 74 | 8, 70, 73 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (2 ·
(√‘(𝐴 ·
𝐵)))) |
| 75 | | addge0 11752 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 + 𝐵)) |
| 76 | 75 | an4s 660 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 + 𝐵)) |
| 77 | 68, 51, 74, 76 | le2sqd 14296 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((2 ·
(√‘(𝐴 ·
𝐵))) ≤ (𝐴 + 𝐵) ↔ ((2 · (√‘(𝐴 · 𝐵)))↑2) ≤ ((𝐴 + 𝐵)↑2))) |
| 78 | 66, 77 | mpbird 257 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (2 ·
(√‘(𝐴 ·
𝐵))) ≤ (𝐴 + 𝐵)) |
| 79 | | 2rp 13039 |
. . . 4
⊢ 2 ∈
ℝ+ |
| 80 | 79 | a1i 11 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 2 ∈
ℝ+) |
| 81 | 8, 51, 80 | lemuldiv2d 13127 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((2 ·
(√‘(𝐴 ·
𝐵))) ≤ (𝐴 + 𝐵) ↔ (√‘(𝐴 · 𝐵)) ≤ ((𝐴 + 𝐵) / 2))) |
| 82 | 78, 81 | mpbid 232 |
1
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) ≤ ((𝐴 + 𝐵) / 2)) |