Theorem fprodge1

Description: If all of the terms of a finite product are greater than or equal to 1 , so is the product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fprodge1.ph	⊢ Ⅎ 𝑘 𝜑
	fprodge1.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprodge1.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	fprodge1.ge	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 1 ≤ 𝐵 )
Assertion	fprodge1	⊢ ( 𝜑 → 1 ≤ ∏ 𝑘 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fprodge1.ph	⊢ Ⅎ 𝑘 𝜑
2		fprodge1.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fprodge1.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4		fprodge1.ge	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 1 ≤ 𝐵 )
5		1xr	⊢ 1 ∈ ℝ*
6		pnfxr	⊢ +∞ ∈ ℝ*
7		1re	⊢ 1 ∈ ℝ
8		icossre	⊢ ( ( 1 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 1 [,) +∞ ) ⊆ ℝ )
9	7 6 8	mp2an	⊢ ( 1 [,) +∞ ) ⊆ ℝ
10		ax-resscn	⊢ ℝ ⊆ ℂ
11	9 10	sstri	⊢ ( 1 [,) +∞ ) ⊆ ℂ
12	11	a1i	⊢ ( 𝜑 → ( 1 [,) +∞ ) ⊆ ℂ )
13	5	a1i	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → 1 ∈ ℝ* )
14	6	a1i	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → +∞ ∈ ℝ* )
15	9	sseli	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 𝑥 ∈ ℝ )
16	15	adantr	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → 𝑥 ∈ ℝ )
17	9	sseli	⊢ ( 𝑦 ∈ ( 1 [,) +∞ ) → 𝑦 ∈ ℝ )
18	17	adantl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → 𝑦 ∈ ℝ )
19	16 18	remulcld	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
20	19	rexrd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ* )
21		1t1e1	⊢ ( 1 · 1 ) = 1
22	7	a1i	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → 1 ∈ ℝ )
23		0le1	⊢ 0 ≤ 1
24	23	a1i	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → 0 ≤ 1 )
25		icogelb	⊢ ( ( 1 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 1 ≤ 𝑥 )
26	5 6 25	mp3an12	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 1 ≤ 𝑥 )
27	26	adantr	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → 1 ≤ 𝑥 )
28		icogelb	⊢ ( ( 1 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → 1 ≤ 𝑦 )
29	5 6 28	mp3an12	⊢ ( 𝑦 ∈ ( 1 [,) +∞ ) → 1 ≤ 𝑦 )
30	29	adantl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → 1 ≤ 𝑦 )
31	22 16 22 18 24 24 27 30	lemul12ad	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → ( 1 · 1 ) ≤ ( 𝑥 · 𝑦 ) )
32	21 31	eqbrtrrid	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → 1 ≤ ( 𝑥 · 𝑦 ) )
33	19	ltpnfd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → ( 𝑥 · 𝑦 ) < +∞ )
34	13 14 20 32 33	elicod	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → ( 𝑥 · 𝑦 ) ∈ ( 1 [,) +∞ ) )
35	34	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ) → ( 𝑥 · 𝑦 ) ∈ ( 1 [,) +∞ ) )
36	5	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 1 ∈ ℝ* )
37	6	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → +∞ ∈ ℝ* )
38	3	rexrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
39	3	ltpnfd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 < +∞ )
40	36 37 38 4 39	elicod	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 1 [,) +∞ ) )
41		1le1	⊢ 1 ≤ 1
42		ltpnf	⊢ ( 1 ∈ ℝ → 1 < +∞ )
43	7 42	ax-mp	⊢ 1 < +∞
44		elico2	⊢ ( ( 1 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 1 ∈ ( 1 [,) +∞ ) ↔ ( 1 ∈ ℝ ∧ 1 ≤ 1 ∧ 1 < +∞ ) ) )
45	7 6 44	mp2an	⊢ ( 1 ∈ ( 1 [,) +∞ ) ↔ ( 1 ∈ ℝ ∧ 1 ≤ 1 ∧ 1 < +∞ ) )
46	7 41 43 45	mpbir3an	⊢ 1 ∈ ( 1 [,) +∞ )
47	46	a1i	⊢ ( 𝜑 → 1 ∈ ( 1 [,) +∞ ) )
48	1 12 35 2 40 47	fprodcllemf	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ∈ ( 1 [,) +∞ ) )
49		icogelb	⊢ ( ( 1 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ∏ 𝑘 ∈ 𝐴 𝐵 ∈ ( 1 [,) +∞ ) ) → 1 ≤ ∏ 𝑘 ∈ 𝐴 𝐵 )
50	5 6 48 49	mp3an12i	⊢ ( 𝜑 → 1 ≤ ∏ 𝑘 ∈ 𝐴 𝐵 )