# 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
`|- F/_ i B`
fmul01lt1.2
`|- F/ i ph`
fmul01lt1.3
`|- F/_ j A`
fmul01lt1.4
`|- A = seq 1 ( x. , B )`
fmul01lt1.5
`|- ( ph -> M e. NN )`
fmul01lt1.6
`|- ( ph -> B : ( 1 ... M ) --> RR )`
fmul01lt1.7
`|- ( ( ph /\ i e. ( 1 ... M ) ) -> 0 <_ ( B ` i ) )`
fmul01lt1.8
`|- ( ( ph /\ i e. ( 1 ... M ) ) -> ( B ` i ) <_ 1 )`
fmul01lt1.9
`|- ( ph -> E e. RR+ )`
fmul01lt1.10
`|- ( ph -> E. j e. ( 1 ... M ) ( B ` j ) < E )`
Assertion fmul01lt1
`|- ( ph -> ( A ` M ) < E )`

### Proof

Step Hyp Ref Expression
1 fmul01lt1.1
` |-  F/_ i B`
2 fmul01lt1.2
` |-  F/ i ph`
3 fmul01lt1.3
` |-  F/_ j A`
4 fmul01lt1.4
` |-  A = seq 1 ( x. , B )`
5 fmul01lt1.5
` |-  ( ph -> M e. NN )`
6 fmul01lt1.6
` |-  ( ph -> B : ( 1 ... M ) --> RR )`
7 fmul01lt1.7
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> 0 <_ ( B ` i ) )`
8 fmul01lt1.8
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( B ` i ) <_ 1 )`
9 fmul01lt1.9
` |-  ( ph -> E e. RR+ )`
10 fmul01lt1.10
` |-  ( ph -> E. j e. ( 1 ... M ) ( B ` j ) < E )`
11 nfv
` |-  F/ j ph`
12 nfcv
` |-  F/_ j M`
13 3 12 nffv
` |-  F/_ j ( A ` M )`
14 nfcv
` |-  F/_ j <`
15 nfcv
` |-  F/_ j E`
16 13 14 15 nfbr
` |-  F/ j ( A ` M ) < E`
17 nfv
` |-  F/ i j e. ( 1 ... M )`
18 nfcv
` |-  F/_ i j`
19 1 18 nffv
` |-  F/_ i ( B ` j )`
20 nfcv
` |-  F/_ i <`
21 nfcv
` |-  F/_ i E`
22 19 20 21 nfbr
` |-  F/ i ( B ` j ) < E`
23 2 17 22 nf3an
` |-  F/ i ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E )`
24 1zzd
` |-  ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) -> 1 e. ZZ )`
25 elnnuz
` |-  ( M e. NN <-> M e. ( ZZ>= ` 1 ) )`
26 5 25 sylib
` |-  ( ph -> M e. ( ZZ>= ` 1 ) )`
` |-  ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) -> M e. ( ZZ>= ` 1 ) )`
28 6 ffvelrnda
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( B ` i ) e. RR )`
` |-  ( ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) /\ i e. ( 1 ... M ) ) -> ( B ` i ) e. RR )`
` |-  ( ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) /\ i e. ( 1 ... M ) ) -> 0 <_ ( B ` i ) )`
` |-  ( ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) /\ i e. ( 1 ... M ) ) -> ( B ` i ) <_ 1 )`
` |-  ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) -> E e. RR+ )`
` |-  ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) -> j e. ( 1 ... M ) )`
` |-  ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) -> ( B ` j ) < E )`
` |-  ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) -> ( A ` M ) < E )`
` |-  ( ph -> ( j e. ( 1 ... M ) -> ( ( B ` j ) < E -> ( A ` M ) < E ) ) )`
` |-  ( ph -> ( E. j e. ( 1 ... M ) ( B ` j ) < E -> ( A ` M ) < E ) )`
` |-  ( ph -> ( A ` M ) < E )`