# Metamath Proof Explorer

## 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 ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{B}$
fmul01lt1.2 ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{\phi }$
fmul01lt1.3 ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{A}$
fmul01lt1.4 ${⊢}{A}=seq1\left(×,{B}\right)$
fmul01lt1.5 ${⊢}{\phi }\to {M}\in ℕ$
fmul01lt1.6 ${⊢}{\phi }\to {B}:\left(1\dots {M}\right)⟶ℝ$
fmul01lt1.7 ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to 0\le {B}\left({i}\right)$
fmul01lt1.8 ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {B}\left({i}\right)\le 1$
fmul01lt1.9 ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
fmul01lt1.10 ${⊢}{\phi }\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{B}\left({j}\right)<{E}$
Assertion fmul01lt1 ${⊢}{\phi }\to {A}\left({M}\right)<{E}$

### Proof

Step Hyp Ref Expression
1 fmul01lt1.1 ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{B}$
2 fmul01lt1.2 ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{\phi }$
3 fmul01lt1.3 ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{A}$
4 fmul01lt1.4 ${⊢}{A}=seq1\left(×,{B}\right)$
5 fmul01lt1.5 ${⊢}{\phi }\to {M}\in ℕ$
6 fmul01lt1.6 ${⊢}{\phi }\to {B}:\left(1\dots {M}\right)⟶ℝ$
7 fmul01lt1.7 ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to 0\le {B}\left({i}\right)$
8 fmul01lt1.8 ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {B}\left({i}\right)\le 1$
9 fmul01lt1.9 ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
10 fmul01lt1.10 ${⊢}{\phi }\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{B}\left({j}\right)<{E}$
11 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{\phi }$
12 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{M}$
13 3 12 nffv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{A}\left({M}\right)$
14 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}<$
15 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{E}$
16 13 14 15 nfbr ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{A}\left({M}\right)<{E}$
17 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{j}\in \left(1\dots {M}\right)$
18 nfcv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{j}$
19 1 18 nffv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{B}\left({j}\right)$
20 nfcv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}<$
21 nfcv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{E}$
22 19 20 21 nfbr ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{B}\left({j}\right)<{E}$
23 2 17 22 nf3an ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {B}\left({j}\right)<{E}\right)$
24 1zzd ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {B}\left({j}\right)<{E}\right)\to 1\in ℤ$
25 elnnuz ${⊢}{M}\in ℕ↔{M}\in {ℤ}_{\ge 1}$
26 5 25 sylib ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 1}$
27 26 3ad2ant1 ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {B}\left({j}\right)<{E}\right)\to {M}\in {ℤ}_{\ge 1}$
28 6 ffvelrnda ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {B}\left({i}\right)\in ℝ$
29 28 3ad2antl1 ${⊢}\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {B}\left({j}\right)<{E}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {B}\left({i}\right)\in ℝ$
30 7 3ad2antl1 ${⊢}\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {B}\left({j}\right)<{E}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to 0\le {B}\left({i}\right)$
31 8 3ad2antl1 ${⊢}\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {B}\left({j}\right)<{E}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {B}\left({i}\right)\le 1$
32 9 3ad2ant1 ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {B}\left({j}\right)<{E}\right)\to {E}\in {ℝ}^{+}$
33 simp2 ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {B}\left({j}\right)<{E}\right)\to {j}\in \left(1\dots {M}\right)$
34 simp3 ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {B}\left({j}\right)<{E}\right)\to {B}\left({j}\right)<{E}$
35 1 23 4 24 27 29 30 31 32 33 34 fmul01lt1lem2 ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {B}\left({j}\right)<{E}\right)\to {A}\left({M}\right)<{E}$
36 35 3exp ${⊢}{\phi }\to \left({j}\in \left(1\dots {M}\right)\to \left({B}\left({j}\right)<{E}\to {A}\left({M}\right)<{E}\right)\right)$
37 11 16 36 rexlimd ${⊢}{\phi }\to \left(\exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{B}\left({j}\right)<{E}\to {A}\left({M}\right)<{E}\right)$
38 10 37 mpd ${⊢}{\phi }\to {A}\left({M}\right)<{E}$