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 \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to \sqrt{A B} \leq \frac{A + B}{2}$

Proof

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

Metamath Proof Explorer

Theorem amgm2

Proof