Theorem amgm3d

Description: Arithmetic-geometric mean inequality for n = 3 . (Contributed by Stanislas Polu, 11-Sep-2020)

	Ref	Expression
Hypotheses	amgm3d.0	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	amgm3d.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	amgm3d.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
Assertion	amgm3d	⊢ ( 𝜑 → ( ( 𝐴 · ( 𝐵 · 𝐶 ) ) ↑𝑐 ( 1 / 3 ) ) ≤ ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) / 3 ) )

Proof

Step	Hyp	Ref	Expression
1		amgm3d.0	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2		amgm3d.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
3		amgm3d.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
4		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
5		fzofi	⊢ ( 0 ..^ 3 ) ∈ Fin
6	5	a1i	⊢ ( 𝜑 → ( 0 ..^ 3 ) ∈ Fin )
7		3nn	⊢ 3 ∈ ℕ
8		lbfzo0	⊢ ( 0 ∈ ( 0 ..^ 3 ) ↔ 3 ∈ ℕ )
9	7 8	mpbir	⊢ 0 ∈ ( 0 ..^ 3 )
10		ne0i	⊢ ( 0 ∈ ( 0 ..^ 3 ) → ( 0 ..^ 3 ) ≠ ∅ )
11	9 10	mp1i	⊢ ( 𝜑 → ( 0 ..^ 3 ) ≠ ∅ )
12	1 2 3	s3cld	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ℝ+ )
13		wrdf	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ℝ+ → ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) ⟶ ℝ+ )
14		s3len	⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
15		df-3	⊢ 3 = ( 2 + 1 )
16	14 15	eqtri	⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( 2 + 1 )
17	16	oveq2i	⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) = ( 0 ..^ ( 2 + 1 ) )
18	17	feq2i	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) ⟶ ℝ+ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ ( 2 + 1 ) ) ⟶ ℝ+ )
19	13 18	sylib	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ℝ+ → ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ ( 2 + 1 ) ) ⟶ ℝ+ )
20	15	oveq2i	⊢ ( 0 ..^ 3 ) = ( 0 ..^ ( 2 + 1 ) )
21	20	feq2i	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ 3 ) ⟶ ℝ+ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ ( 2 + 1 ) ) ⟶ ℝ+ )
22	19 21	sylibr	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ℝ+ → ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ 3 ) ⟶ ℝ+ )
23	12 22	syl	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ 3 ) ⟶ ℝ+ )
24	4 6 11 23	amgmlem	⊢ ( 𝜑 → ( ( ( mulGrp ‘ ℂfld ) Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ↑𝑐 ( 1 / ( ♯ ‘ ( 0 ..^ 3 ) ) ) ) ≤ ( ( ℂfld Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) / ( ♯ ‘ ( 0 ..^ 3 ) ) ) )
25		cnring	⊢ ℂfld ∈ Ring
26	4	ringmgp	⊢ ( ℂfld ∈ Ring → ( mulGrp ‘ ℂfld ) ∈ Mnd )
27	25 26	mp1i	⊢ ( 𝜑 → ( mulGrp ‘ ℂfld ) ∈ Mnd )
28	1	rpcnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
29	2	rpcnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
30	3	rpcnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
31	28 29 30	jca32	⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) )
32		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
33	4 32	mgpbas	⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
34		cnfldmul	⊢ · = ( .r ‘ ℂfld )
35	4 34	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
36	33 35	gsumws3	⊢ ( ( ( mulGrp ‘ ℂfld ) ∈ Mnd ∧ ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) ) → ( ( mulGrp ‘ ℂfld ) Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( 𝐴 · ( 𝐵 · 𝐶 ) ) )
37	27 31 36	syl2anc	⊢ ( 𝜑 → ( ( mulGrp ‘ ℂfld ) Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( 𝐴 · ( 𝐵 · 𝐶 ) ) )
38		3nn0	⊢ 3 ∈ ℕ0
39		hashfzo0	⊢ ( 3 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 )
40	38 39	mp1i	⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 )
41	40	oveq2d	⊢ ( 𝜑 → ( 1 / ( ♯ ‘ ( 0 ..^ 3 ) ) ) = ( 1 / 3 ) )
42	37 41	oveq12d	⊢ ( 𝜑 → ( ( ( mulGrp ‘ ℂfld ) Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ↑𝑐 ( 1 / ( ♯ ‘ ( 0 ..^ 3 ) ) ) ) = ( ( 𝐴 · ( 𝐵 · 𝐶 ) ) ↑𝑐 ( 1 / 3 ) ) )
43		ringmnd	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
44	25 43	mp1i	⊢ ( 𝜑 → ℂfld ∈ Mnd )
45		cnfldadd	⊢ + = ( +g ‘ ℂfld )
46	32 45	gsumws3	⊢ ( ( ℂfld ∈ Mnd ∧ ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) ) → ( ℂfld Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( 𝐴 + ( 𝐵 + 𝐶 ) ) )
47	44 31 46	syl2anc	⊢ ( 𝜑 → ( ℂfld Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( 𝐴 + ( 𝐵 + 𝐶 ) ) )
48	47 40	oveq12d	⊢ ( 𝜑 → ( ( ℂfld Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) / ( ♯ ‘ ( 0 ..^ 3 ) ) ) = ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) / 3 ) )
49	24 42 48	3brtr3d	⊢ ( 𝜑 → ( ( 𝐴 · ( 𝐵 · 𝐶 ) ) ↑𝑐 ( 1 / 3 ) ) ≤ ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) / 3 ) )