Theorem amgm2d

Description: Arithmetic-geometric mean inequality for n = 2 , derived from amgmlem . (Contributed by Stanislas Polu, 8-Sep-2020)

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

Proof

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