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 ) )
27 26 3ad2ant1 
 |-  ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) -> M e. ( ZZ>= ` 1 ) )
28 6 ffvelrnda 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( B ` i ) e. RR )
29 28 3ad2antl1 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) /\ i e. ( 1 ... M ) ) -> ( B ` i ) e. RR )
30 7 3ad2antl1 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) /\ i e. ( 1 ... M ) ) -> 0 <_ ( B ` i ) )
31 8 3ad2antl1 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) /\ i e. ( 1 ... M ) ) -> ( B ` i ) <_ 1 )
32 9 3ad2ant1 
 |-  ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) -> E e. RR+ )
33 simp2 
 |-  ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) -> j e. ( 1 ... M ) )
34 simp3 
 |-  ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) -> ( B ` j ) < E )
35 1 23 4 24 27 29 30 31 32 33 34 fmul01lt1lem2 
 |-  ( ( ph /\ j e. ( 1 ... M ) /\ ( B ` j ) < E ) -> ( A ` M ) < E )
36 35 3exp 
 |-  ( ph -> ( j e. ( 1 ... M ) -> ( ( B ` j ) < E -> ( A ` M ) < E ) ) )
37 11 16 36 rexlimd 
 |-  ( ph -> ( E. j e. ( 1 ... M ) ( B ` j ) < E -> ( A ` M ) < E ) )
38 10 37 mpd 
 |-  ( ph -> ( A ` M ) < E )