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 
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqrt ` ( A x. B ) ) <_ ( ( A + B ) / 2 ) )

Proof

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