# 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 𝑖 𝐵
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 ( 𝜑 → ( 𝐴𝑀 ) < 𝐸 )