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 eqtrid
 |-  ( ( ( 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 ) )