Theorem amgm4d

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

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

Proof

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