Metamath Proof Explorer

Theorem amgm2

Description: Arithmetic-geometric mean inequality for n = 2 . (Contributed by Mario Carneiro, 2-Jul-2014) (Proof shortened by AV, 9-Jul-2022)

Ref Expression
Assertion amgm2 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( √ ‘ ( 𝐴 · 𝐵 ) ) ≤ ( ( 𝐴 + 𝐵 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 2cn ⊢ 2 ∈ ℂ
2 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 𝐴 ∈ ℝ )
3 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 𝐵 ∈ ℝ )
4 remulcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
5 2 3 4 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
6 mulge0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 · 𝐵 ) )
7 resqrtcl ⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · 𝐵 ) ) → ( √ ‘ ( 𝐴 · 𝐵 ) ) ∈ ℝ )
8 5 6 7 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( √ ‘ ( 𝐴 · 𝐵 ) ) ∈ ℝ )
9 8 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( √ ‘ ( 𝐴 · 𝐵 ) ) ∈ ℂ )
10 sqmul ⊢ ( ( 2 ∈ ℂ ∧ ( √ ‘ ( 𝐴 · 𝐵 ) ) ∈ ℂ ) → ( ( 2 · ( √ ‘ ( 𝐴 · 𝐵 ) ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( ( √ ‘ ( 𝐴 · 𝐵 ) ) ↑ 2 ) ) )
11 1 9 10 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 2 · ( √ ‘ ( 𝐴 · 𝐵 ) ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( ( √ ‘ ( 𝐴 · 𝐵 ) ) ↑ 2 ) ) )
12 sq2 ⊢ ( 2 ↑ 2 ) = 4
13 12 oveq1i ⊢ ( ( 2 ↑ 2 ) · ( ( √ ‘ ( 𝐴 · 𝐵 ) ) ↑ 2 ) ) = ( 4 · ( ( √ ‘ ( 𝐴 · 𝐵 ) ) ↑ 2 ) )
14 5 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
15 sqrtth ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℂ → ( ( √ ‘ ( 𝐴 · 𝐵 ) ) ↑ 2 ) = ( 𝐴 · 𝐵 ) )
16 14 15 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( √ ‘ ( 𝐴 · 𝐵 ) ) ↑ 2 ) = ( 𝐴 · 𝐵 ) )
17 16 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 4 · ( ( √ ‘ ( 𝐴 · 𝐵 ) ) ↑ 2 ) ) = ( 4 · ( 𝐴 · 𝐵 ) ) )
18 13 17 syl5eq ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 2 ↑ 2 ) · ( ( √ ‘ ( 𝐴 · 𝐵 ) ) ↑ 2 ) ) = ( 4 · ( 𝐴 · 𝐵 ) ) )
19 11 18 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 2 · ( √ ‘ ( 𝐴 · 𝐵 ) ) ) ↑ 2 ) = ( 4 · ( 𝐴 · 𝐵 ) ) )
20 2 3 resubcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
21 20 sqge0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( ( 𝐴 − 𝐵 ) ↑ 2 ) )
22 2 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 𝐴 ∈ ℂ )
23 3 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 𝐵 ∈ ℂ )
24 binom2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )
25 22 23 24 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )
26 binom2sub ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )
27 22 23 26 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 − 𝐵 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )
28 25 27 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) − ( ( 𝐴 − 𝐵 ) ↑ 2 ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) ) )
29 2 resqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
30 2re ⊢ 2 ∈ ℝ
31 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( 𝐴 · 𝐵 ) ∈ ℝ ) → ( 2 · ( 𝐴 · 𝐵 ) ) ∈ ℝ )
32 30 5 31 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 2 · ( 𝐴 · 𝐵 ) ) ∈ ℝ )
33 29 32 readdcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) ∈ ℝ )
34 33 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) ∈ ℂ )
35 29 32 resubcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐵 ) ) ) ∈ ℝ )
36 35 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐵 ) ) ) ∈ ℂ )
37 3 resqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐵 ↑ 2 ) ∈ ℝ )
38 37 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
39 34 36 38 pnpcan2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐵 ) ) ) ) )
40 32 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 2 · ( 𝐴 · 𝐵 ) ) ∈ ℂ )
41 40 2timesd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 2 · ( 2 · ( 𝐴 · 𝐵 ) ) ) = ( ( 2 · ( 𝐴 · 𝐵 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) )
42 2t2e4 ⊢ ( 2 · 2 ) = 4
43 42 oveq1i ⊢ ( ( 2 · 2 ) · ( 𝐴 · 𝐵 ) ) = ( 4 · ( 𝐴 · 𝐵 ) )
44 2cnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 2 ∈ ℂ )
45 44 44 14 mulassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 2 · 2 ) · ( 𝐴 · 𝐵 ) ) = ( 2 · ( 2 · ( 𝐴 · 𝐵 ) ) ) )
46 43 45 syl5eqr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 4 · ( 𝐴 · 𝐵 ) ) = ( 2 · ( 2 · ( 𝐴 · 𝐵 ) ) ) )
47 29 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
48 47 40 40 pnncand ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐵 ) ) ) ) = ( ( 2 · ( 𝐴 · 𝐵 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) )
49 41 46 48 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐵 ) ) ) ) = ( 4 · ( 𝐴 · 𝐵 ) ) )
50 28 39 49 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) − ( ( 𝐴 − 𝐵 ) ↑ 2 ) ) = ( 4 · ( 𝐴 · 𝐵 ) ) )
51 2 3 readdcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
52 51 resqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) ↑ 2 ) ∈ ℝ )
53 52 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) ↑ 2 ) ∈ ℂ )
54 20 resqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 − 𝐵 ) ↑ 2 ) ∈ ℝ )
55 54 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 − 𝐵 ) ↑ 2 ) ∈ ℂ )
56 4re ⊢ 4 ∈ ℝ
57 remulcl ⊢ ( ( 4 ∈ ℝ ∧ ( 𝐴 · 𝐵 ) ∈ ℝ ) → ( 4 · ( 𝐴 · 𝐵 ) ) ∈ ℝ )
58 56 5 57 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 4 · ( 𝐴 · 𝐵 ) ) ∈ ℝ )
59 58 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 4 · ( 𝐴 · 𝐵 ) ) ∈ ℂ )
60 subsub23 ⊢ ( ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) ↑ 2 ) ∈ ℂ ∧ ( 4 · ( 𝐴 · 𝐵 ) ) ∈ ℂ ) → ( ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) − ( ( 𝐴 − 𝐵 ) ↑ 2 ) ) = ( 4 · ( 𝐴 · 𝐵 ) ) ↔ ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) − ( 4 · ( 𝐴 · 𝐵 ) ) ) = ( ( 𝐴 − 𝐵 ) ↑ 2 ) ) )
61 53 55 59 60 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) − ( ( 𝐴 − 𝐵 ) ↑ 2 ) ) = ( 4 · ( 𝐴 · 𝐵 ) ) ↔ ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) − ( 4 · ( 𝐴 · 𝐵 ) ) ) = ( ( 𝐴 − 𝐵 ) ↑ 2 ) ) )
62 50 61 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) − ( 4 · ( 𝐴 · 𝐵 ) ) ) = ( ( 𝐴 − 𝐵 ) ↑ 2 ) )
63 21 62 breqtrrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) − ( 4 · ( 𝐴 · 𝐵 ) ) ) )
64 52 58 subge0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 0 ≤ ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) − ( 4 · ( 𝐴 · 𝐵 ) ) ) ↔ ( 4 · ( 𝐴 · 𝐵 ) ) ≤ ( ( 𝐴 + 𝐵 ) ↑ 2 ) ) )
65 63 64 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 4 · ( 𝐴 · 𝐵 ) ) ≤ ( ( 𝐴 + 𝐵 ) ↑ 2 ) )
66 19 65 eqbrtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 2 · ( √ ‘ ( 𝐴 · 𝐵 ) ) ) ↑ 2 ) ≤ ( ( 𝐴 + 𝐵 ) ↑ 2 ) )
67 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( √ ‘ ( 𝐴 · 𝐵 ) ) ∈ ℝ ) → ( 2 · ( √ ‘ ( 𝐴 · 𝐵 ) ) ) ∈ ℝ )
68 30 8 67 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 2 · ( √ ‘ ( 𝐴 · 𝐵 ) ) ) ∈ ℝ )
69 sqrtge0 ⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · 𝐵 ) ) → 0 ≤ ( √ ‘ ( 𝐴 · 𝐵 ) ) )
70 5 6 69 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( √ ‘ ( 𝐴 · 𝐵 ) ) )
71 0le2 ⊢ 0 ≤ 2
72 mulge0 ⊢ ( ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) ∧ ( ( √ ‘ ( 𝐴 · 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( √ ‘ ( 𝐴 · 𝐵 ) ) ) ) → 0 ≤ ( 2 · ( √ ‘ ( 𝐴 · 𝐵 ) ) ) )
73 30 71 72 mpanl12 ⊢ ( ( ( √ ‘ ( 𝐴 · 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( √ ‘ ( 𝐴 · 𝐵 ) ) ) → 0 ≤ ( 2 · ( √ ‘ ( 𝐴 · 𝐵 ) ) ) )
74 8 70 73 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 2 · ( √ ‘ ( 𝐴 · 𝐵 ) ) ) )
75 addge0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 + 𝐵 ) )
76 75 an4s ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 + 𝐵 ) )
77 68 51 74 76 le2sqd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 2 · ( √ ‘ ( 𝐴 · 𝐵 ) ) ) ≤ ( 𝐴 + 𝐵 ) ↔ ( ( 2 · ( √ ‘ ( 𝐴 · 𝐵 ) ) ) ↑ 2 ) ≤ ( ( 𝐴 + 𝐵 ) ↑ 2 ) ) )
78 66 77 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 2 · ( √ ‘ ( 𝐴 · 𝐵 ) ) ) ≤ ( 𝐴 + 𝐵 ) )
79 2rp ⊢ 2 ∈ ℝ+
80 79 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 2 ∈ ℝ+ )
81 8 51 80 lemuldiv2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 2 · ( √ ‘ ( 𝐴 · 𝐵 ) ) ) ≤ ( 𝐴 + 𝐵 ) ↔ ( √ ‘ ( 𝐴 · 𝐵 ) ) ≤ ( ( 𝐴 + 𝐵 ) / 2 ) ) )
82 78 81 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( √ ‘ ( 𝐴 · 𝐵 ) ) ≤ ( ( 𝐴 + 𝐵 ) / 2 ) )