Theorem fmul01lt1

Description: Given a finite multiplication of values betweeen 0 and 1, a value E larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	fmul01lt1.1	⊢ Ⅎ 𝑖 𝐵
	fmul01lt1.2	⊢ Ⅎ 𝑖 𝜑
	fmul01lt1.3	⊢ Ⅎ 𝑗 𝐴
	fmul01lt1.4	⊢ 𝐴 = seq 1 ( · , 𝐵 )
	fmul01lt1.5	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	fmul01lt1.6	⊢ ( 𝜑 → 𝐵 : ( 1 ... 𝑀 ) ⟶ ℝ )
	fmul01lt1.7	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝑖 ) )
	fmul01lt1.8	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ≤ 1 )
	fmul01lt1.9	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	fmul01lt1.10	⊢ ( 𝜑 → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝐵 ‘ 𝑗 ) < 𝐸 )
Assertion	fmul01lt1	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑀 ) < 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		fmul01lt1.1	⊢ Ⅎ 𝑖 𝐵
2		fmul01lt1.2	⊢ Ⅎ 𝑖 𝜑
3		fmul01lt1.3	⊢ Ⅎ 𝑗 𝐴
4		fmul01lt1.4	⊢ 𝐴 = seq 1 ( · , 𝐵 )
5		fmul01lt1.5	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
6		fmul01lt1.6	⊢ ( 𝜑 → 𝐵 : ( 1 ... 𝑀 ) ⟶ ℝ )
7		fmul01lt1.7	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝑖 ) )
8		fmul01lt1.8	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ≤ 1 )
9		fmul01lt1.9	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
10		fmul01lt1.10	⊢ ( 𝜑 → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝐵 ‘ 𝑗 ) < 𝐸 )
11		nfv	⊢ Ⅎ 𝑗 𝜑
12		nfcv	⊢ Ⅎ 𝑗 𝑀
13	3 12	nffv	⊢ Ⅎ 𝑗 ( 𝐴 ‘ 𝑀 )
14		nfcv	⊢ Ⅎ 𝑗 <
15		nfcv	⊢ Ⅎ 𝑗 𝐸
16	13 14 15	nfbr	⊢ Ⅎ 𝑗 ( 𝐴 ‘ 𝑀 ) < 𝐸
17		nfv	⊢ Ⅎ 𝑖 𝑗 ∈ ( 1 ... 𝑀 )
18		nfcv	⊢ Ⅎ 𝑖 𝑗
19	1 18	nffv	⊢ Ⅎ 𝑖 ( 𝐵 ‘ 𝑗 )
20		nfcv	⊢ Ⅎ 𝑖 <
21		nfcv	⊢ Ⅎ 𝑖 𝐸
22	19 20 21	nfbr	⊢ Ⅎ 𝑖 ( 𝐵 ‘ 𝑗 ) < 𝐸
23	2 17 22	nf3an	⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐵 ‘ 𝑗 ) < 𝐸 )
24		1zzd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐵 ‘ 𝑗 ) < 𝐸 ) → 1 ∈ ℤ )
25		elnnuz	⊢ ( 𝑀 ∈ ℕ ↔ 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
26	5 25	sylib	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
27	26	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐵 ‘ 𝑗 ) < 𝐸 ) → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
28	6	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
29	28	3ad2antl1	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐵 ‘ 𝑗 ) < 𝐸 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
30	7	3ad2antl1	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐵 ‘ 𝑗 ) < 𝐸 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝑖 ) )
31	8	3ad2antl1	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐵 ‘ 𝑗 ) < 𝐸 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ≤ 1 )
32	9	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐵 ‘ 𝑗 ) < 𝐸 ) → 𝐸 ∈ ℝ+ )
33		simp2	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐵 ‘ 𝑗 ) < 𝐸 ) → 𝑗 ∈ ( 1 ... 𝑀 ) )
34		simp3	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐵 ‘ 𝑗 ) < 𝐸 ) → ( 𝐵 ‘ 𝑗 ) < 𝐸 )
35	1 23 4 24 27 29 30 31 32 33 34	fmul01lt1lem2	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐵 ‘ 𝑗 ) < 𝐸 ) → ( 𝐴 ‘ 𝑀 ) < 𝐸 )
36	35	3exp	⊢ ( 𝜑 → ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( ( 𝐵 ‘ 𝑗 ) < 𝐸 → ( 𝐴 ‘ 𝑀 ) < 𝐸 ) ) )
37	11 16 36	rexlimd	⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝐵 ‘ 𝑗 ) < 𝐸 → ( 𝐴 ‘ 𝑀 ) < 𝐸 ) )
38	10 37	mpd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑀 ) < 𝐸 )