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 A0AB0BABA+B2

Proof

Step Hyp Ref Expression
1 2cn 2
2 simpll A0AB0BA
3 simprl A0AB0BB
4 remulcl ABAB
5 2 3 4 syl2anc A0AB0BAB
6 mulge0 A0AB0B0AB
7 resqrtcl AB0ABAB
8 5 6 7 syl2anc A0AB0BAB
9 8 recnd A0AB0BAB
10 sqmul 2AB2AB2=22AB2
11 1 9 10 sylancr A0AB0B2AB2=22AB2
12 sq2 22=4
13 12 oveq1i 22AB2=4AB2
14 5 recnd A0AB0BAB
15 sqrtth ABAB2=AB
16 14 15 syl A0AB0BAB2=AB
17 16 oveq2d A0AB0B4AB2=4AB
18 13 17 eqtrid A0AB0B22AB2=4AB
19 11 18 eqtrd A0AB0B2AB2=4AB
20 2 3 resubcld A0AB0BAB
21 20 sqge0d A0AB0B0AB2
22 2 recnd A0AB0BA
23 3 recnd A0AB0BB
24 binom2 ABA+B2=A2+2AB+B2
25 22 23 24 syl2anc A0AB0BA+B2=A2+2AB+B2
26 binom2sub ABAB2=A2-2AB+B2
27 22 23 26 syl2anc A0AB0BAB2=A2-2AB+B2
28 25 27 oveq12d A0AB0BA+B2AB2=A2+2AB+B2-A2-2AB+B2
29 2 resqcld A0AB0BA2
30 2re 2
31 remulcl 2AB2AB
32 30 5 31 sylancr A0AB0B2AB
33 29 32 readdcld A0AB0BA2+2AB
34 33 recnd A0AB0BA2+2AB
35 29 32 resubcld A0AB0BA22AB
36 35 recnd A0AB0BA22AB
37 3 resqcld A0AB0BB2
38 37 recnd A0AB0BB2
39 34 36 38 pnpcan2d A0AB0BA2+2AB+B2-A2-2AB+B2=A2+2AB-A22AB
40 32 recnd A0AB0B2AB
41 40 2timesd A0AB0B22AB=2AB+2AB
42 2t2e4 22=4
43 42 oveq1i 22AB=4AB
44 2cnd A0AB0B2
45 44 44 14 mulassd A0AB0B22AB=22AB
46 43 45 eqtr3id A0AB0B4AB=22AB
47 29 recnd A0AB0BA2
48 47 40 40 pnncand A0AB0BA2+2AB-A22AB=2AB+2AB
49 41 46 48 3eqtr4rd A0AB0BA2+2AB-A22AB=4AB
50 28 39 49 3eqtrd A0AB0BA+B2AB2=4AB
51 2 3 readdcld A0AB0BA+B
52 51 resqcld A0AB0BA+B2
53 52 recnd A0AB0BA+B2
54 20 resqcld A0AB0BAB2
55 54 recnd A0AB0BAB2
56 4re 4
57 remulcl 4AB4AB
58 56 5 57 sylancr A0AB0B4AB
59 58 recnd A0AB0B4AB
60 subsub23 A+B2AB24ABA+B2AB2=4ABA+B24AB=AB2
61 53 55 59 60 syl3anc A0AB0BA+B2AB2=4ABA+B24AB=AB2
62 50 61 mpbid A0AB0BA+B24AB=AB2
63 21 62 breqtrrd A0AB0B0A+B24AB
64 52 58 subge0d A0AB0B0A+B24AB4ABA+B2
65 63 64 mpbid A0AB0B4ABA+B2
66 19 65 eqbrtrd A0AB0B2AB2A+B2
67 remulcl 2AB2AB
68 30 8 67 sylancr A0AB0B2AB
69 sqrtge0 AB0AB0AB
70 5 6 69 syl2anc A0AB0B0AB
71 0le2 02
72 mulge0 202AB0AB02AB
73 30 71 72 mpanl12 AB0AB02AB
74 8 70 73 syl2anc A0AB0B02AB
75 addge0 AB0A0B0A+B
76 75 an4s A0AB0B0A+B
77 68 51 74 76 le2sqd A0AB0B2ABA+B2AB2A+B2
78 66 77 mpbird A0AB0B2ABA+B
79 2rp 2+
80 79 a1i A0AB0B2+
81 8 51 80 lemuldiv2d A0AB0B2ABA+BABA+B2
82 78 81 mpbid A0AB0BABA+B2