Metamath Proof Explorer

Theorem fmul01

Description: Multiplying a finite number of values in [ 0 , 1 ] , gives the final product itself a number in [ 0 , 1 ]. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses fmul01.1 ⊢ Ⅎ 𝑖 𝐵
fmul01.2 ⊢ Ⅎ 𝑖 𝜑
fmul01.3 ⊢ 𝐴 = seq 𝐿 ( · , 𝐵 )
fmul01.4 ⊢ ( 𝜑 → 𝐿 ∈ ℤ )
fmul01.5 ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝐿 ) )
fmul01.6 ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐿 ... 𝑀 ) )
fmul01.7 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
fmul01.8 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝑖 ) )
fmul01.9 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ≤ 1 )
Assertion fmul01 ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝐾 ) ∧ ( 𝐴 ‘ 𝐾 ) ≤ 1 ) )

Proof

Step Hyp Ref Expression
1 fmul01.1 ⊢ Ⅎ 𝑖 𝐵
2 fmul01.2 ⊢ Ⅎ 𝑖 𝜑
3 fmul01.3 ⊢ 𝐴 = seq 𝐿 ( · , 𝐵 )
4 fmul01.4 ⊢ ( 𝜑 → 𝐿 ∈ ℤ )
5 fmul01.5 ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝐿 ) )
6 fmul01.6 ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐿 ... 𝑀 ) )
7 fmul01.7 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
8 fmul01.8 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝑖 ) )
9 fmul01.9 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ≤ 1 )
10 fveq2 ⊢ ( 𝑘 = 𝐿 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝐿 ) )
11 10 breq2d ⊢ ( 𝑘 = 𝐿 → ( 0 ≤ ( 𝐴 ‘ 𝑘 ) ↔ 0 ≤ ( 𝐴 ‘ 𝐿 ) ) )
12 10 breq1d ⊢ ( 𝑘 = 𝐿 → ( ( 𝐴 ‘ 𝑘 ) ≤ 1 ↔ ( 𝐴 ‘ 𝐿 ) ≤ 1 ) )
13 11 12 anbi12d ⊢ ( 𝑘 = 𝐿 → ( ( 0 ≤ ( 𝐴 ‘ 𝑘 ) ∧ ( 𝐴 ‘ 𝑘 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝐴 ‘ 𝐿 ) ∧ ( 𝐴 ‘ 𝐿 ) ≤ 1 ) ) )
14 13 imbi2d ⊢ ( 𝑘 = 𝐿 → ( ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑘 ) ∧ ( 𝐴 ‘ 𝑘 ) ≤ 1 ) ) ↔ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝐿 ) ∧ ( 𝐴 ‘ 𝐿 ) ≤ 1 ) ) ) )
15 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑗 ) )
16 15 breq2d ⊢ ( 𝑘 = 𝑗 → ( 0 ≤ ( 𝐴 ‘ 𝑘 ) ↔ 0 ≤ ( 𝐴 ‘ 𝑗 ) ) )
17 15 breq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐴 ‘ 𝑘 ) ≤ 1 ↔ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) )
18 16 17 anbi12d ⊢ ( 𝑘 = 𝑗 → ( ( 0 ≤ ( 𝐴 ‘ 𝑘 ) ∧ ( 𝐴 ‘ 𝑘 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) )
19 18 imbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑘 ) ∧ ( 𝐴 ‘ 𝑘 ) ≤ 1 ) ) ↔ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ) )
20 fveq2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ ( 𝑗 + 1 ) ) )
21 20 breq2d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 0 ≤ ( 𝐴 ‘ 𝑘 ) ↔ 0 ≤ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
22 20 breq1d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝐴 ‘ 𝑘 ) ≤ 1 ↔ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ≤ 1 ) )
23 21 22 anbi12d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( 0 ≤ ( 𝐴 ‘ 𝑘 ) ∧ ( 𝐴 ‘ 𝑘 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ≤ 1 ) ) )
24 23 imbi2d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑘 ) ∧ ( 𝐴 ‘ 𝑘 ) ≤ 1 ) ) ↔ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ≤ 1 ) ) ) )
25 fveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝐾 ) )
26 25 breq2d ⊢ ( 𝑘 = 𝐾 → ( 0 ≤ ( 𝐴 ‘ 𝑘 ) ↔ 0 ≤ ( 𝐴 ‘ 𝐾 ) ) )
27 25 breq1d ⊢ ( 𝑘 = 𝐾 → ( ( 𝐴 ‘ 𝑘 ) ≤ 1 ↔ ( 𝐴 ‘ 𝐾 ) ≤ 1 ) )
28 26 27 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( 0 ≤ ( 𝐴 ‘ 𝑘 ) ∧ ( 𝐴 ‘ 𝑘 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝐴 ‘ 𝐾 ) ∧ ( 𝐴 ‘ 𝐾 ) ≤ 1 ) ) )
29 28 imbi2d ⊢ ( 𝑘 = 𝐾 → ( ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑘 ) ∧ ( 𝐴 ‘ 𝑘 ) ≤ 1 ) ) ↔ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝐾 ) ∧ ( 𝐴 ‘ 𝐾 ) ≤ 1 ) ) ) )
30 4 zred ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
31 30 leidd ⊢ ( 𝜑 → 𝐿 ≤ 𝐿 )
32 eluzelz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝐿 ) → 𝑀 ∈ ℤ )
33 5 32 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
34 eluz ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 ∈ ( ℤ≥ ‘ 𝐿 ) ↔ 𝐿 ≤ 𝑀 ) )
35 4 33 34 syl2anc ⊢ ( 𝜑 → ( 𝑀 ∈ ( ℤ≥ ‘ 𝐿 ) ↔ 𝐿 ≤ 𝑀 ) )
36 5 35 mpbid ⊢ ( 𝜑 → 𝐿 ≤ 𝑀 )
37 elfz ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐿 ∈ ( 𝐿 ... 𝑀 ) ↔ ( 𝐿 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) ) )
38 4 4 33 37 syl3anc ⊢ ( 𝜑 → ( 𝐿 ∈ ( 𝐿 ... 𝑀 ) ↔ ( 𝐿 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) ) )
39 31 36 38 mpbir2and ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐿 ... 𝑀 ) )
40 39 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝐿 ∈ ( 𝐿 ... 𝑀 ) ) )
41 nfv ⊢ Ⅎ 𝑖 𝐿 ∈ ( 𝐿 ... 𝑀 )
42 2 41 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝐿 ∈ ( 𝐿 ... 𝑀 ) )
43 nfcv ⊢ Ⅎ 𝑖 0
44 nfcv ⊢ Ⅎ 𝑖 ≤
45 nfcv ⊢ Ⅎ 𝑖 𝐿
46 1 45 nffv ⊢ Ⅎ 𝑖 ( 𝐵 ‘ 𝐿 )
47 43 44 46 nfbr ⊢ Ⅎ 𝑖 0 ≤ ( 𝐵 ‘ 𝐿 )
48 42 47 nfim ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝐿 ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝐿 ) )
49 eleq1 ⊢ ( 𝑖 = 𝐿 → ( 𝑖 ∈ ( 𝐿 ... 𝑀 ) ↔ 𝐿 ∈ ( 𝐿 ... 𝑀 ) ) )
50 49 anbi2d ⊢ ( 𝑖 = 𝐿 → ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) ↔ ( 𝜑 ∧ 𝐿 ∈ ( 𝐿 ... 𝑀 ) ) ) )
51 fveq2 ⊢ ( 𝑖 = 𝐿 → ( 𝐵 ‘ 𝑖 ) = ( 𝐵 ‘ 𝐿 ) )
52 51 breq2d ⊢ ( 𝑖 = 𝐿 → ( 0 ≤ ( 𝐵 ‘ 𝑖 ) ↔ 0 ≤ ( 𝐵 ‘ 𝐿 ) ) )
53 50 52 imbi12d ⊢ ( 𝑖 = 𝐿 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝑖 ) ) ↔ ( ( 𝜑 ∧ 𝐿 ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝐿 ) ) ) )
54 48 53 8 vtoclg1f ⊢ ( 𝐿 ∈ ( 𝐿 ... 𝑀 ) → ( ( 𝜑 ∧ 𝐿 ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝐿 ) ) )
55 39 40 54 sylc ⊢ ( 𝜑 → 0 ≤ ( 𝐵 ‘ 𝐿 ) )
56 3 fveq1i ⊢ ( 𝐴 ‘ 𝐿 ) = ( seq 𝐿 ( · , 𝐵 ) ‘ 𝐿 )
57 seq1 ⊢ ( 𝐿 ∈ ℤ → ( seq 𝐿 ( · , 𝐵 ) ‘ 𝐿 ) = ( 𝐵 ‘ 𝐿 ) )
58 4 57 syl ⊢ ( 𝜑 → ( seq 𝐿 ( · , 𝐵 ) ‘ 𝐿 ) = ( 𝐵 ‘ 𝐿 ) )
59 56 58 syl5eq ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐿 ) = ( 𝐵 ‘ 𝐿 ) )
60 55 59 breqtrrd ⊢ ( 𝜑 → 0 ≤ ( 𝐴 ‘ 𝐿 ) )
61 nfcv ⊢ Ⅎ 𝑖 1
62 46 44 61 nfbr ⊢ Ⅎ 𝑖 ( 𝐵 ‘ 𝐿 ) ≤ 1
63 42 62 nfim ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝐿 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝐿 ) ≤ 1 )
64 51 breq1d ⊢ ( 𝑖 = 𝐿 → ( ( 𝐵 ‘ 𝑖 ) ≤ 1 ↔ ( 𝐵 ‘ 𝐿 ) ≤ 1 ) )
65 50 64 imbi12d ⊢ ( 𝑖 = 𝐿 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ≤ 1 ) ↔ ( ( 𝜑 ∧ 𝐿 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝐿 ) ≤ 1 ) ) )
66 63 65 9 vtoclg1f ⊢ ( 𝐿 ∈ ( 𝐿 ... 𝑀 ) → ( ( 𝜑 ∧ 𝐿 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝐿 ) ≤ 1 ) )
67 39 40 66 sylc ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐿 ) ≤ 1 )
68 59 67 eqbrtrd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐿 ) ≤ 1 )
69 60 68 jca ⊢ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝐿 ) ∧ ( 𝐴 ‘ 𝐿 ) ≤ 1 ) )
70 69 a1i ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝐿 ) → ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝐿 ) ∧ ( 𝐴 ‘ 𝐿 ) ≤ 1 ) ) )
71 elfzouz ⊢ ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝐿 ) )
72 71 3ad2ant1 ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝐿 ) )
73 simpl3 ⊢ ( ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝐿 ... 𝑗 ) ) → 𝜑 )
74 elfzouz2 ⊢ ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑗 ) )
75 fzss2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑗 ) → ( 𝐿 ... 𝑗 ) ⊆ ( 𝐿 ... 𝑀 ) )
76 74 75 syl ⊢ ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) → ( 𝐿 ... 𝑗 ) ⊆ ( 𝐿 ... 𝑀 ) )
77 76 3ad2ant1 ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( 𝐿 ... 𝑗 ) ⊆ ( 𝐿 ... 𝑀 ) )
78 77 sselda ⊢ ( ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝐿 ... 𝑗 ) ) → 𝑘 ∈ ( 𝐿 ... 𝑀 ) )
79 nfv ⊢ Ⅎ 𝑖 𝑘 ∈ ( 𝐿 ... 𝑀 )
80 2 79 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑘 ∈ ( 𝐿 ... 𝑀 ) )
81 nfcv ⊢ Ⅎ 𝑖 𝑘
82 1 81 nffv ⊢ Ⅎ 𝑖 ( 𝐵 ‘ 𝑘 )
83 82 nfel1 ⊢ Ⅎ 𝑖 ( 𝐵 ‘ 𝑘 ) ∈ ℝ
84 80 83 nfim ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
85 eleq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 ∈ ( 𝐿 ... 𝑀 ) ↔ 𝑘 ∈ ( 𝐿 ... 𝑀 ) ) )
86 85 anbi2d ⊢ ( 𝑖 = 𝑘 → ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) ↔ ( 𝜑 ∧ 𝑘 ∈ ( 𝐿 ... 𝑀 ) ) ) )
87 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝐵 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑘 ) )
88 87 eleq1d ⊢ ( 𝑖 = 𝑘 → ( ( 𝐵 ‘ 𝑖 ) ∈ ℝ ↔ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) )
89 86 88 imbi12d ⊢ ( 𝑖 = 𝑘 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ) )
90 84 89 7 chvarfv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
91 73 78 90 syl2anc ⊢ ( ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝐿 ... 𝑗 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
92 remulcl ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑙 ∈ ℝ ) → ( 𝑘 · 𝑙 ) ∈ ℝ )
93 92 adantl ⊢ ( ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) ∧ ( 𝑘 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ) → ( 𝑘 · 𝑙 ) ∈ ℝ )
94 72 91 93 seqcl ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) ∈ ℝ )
95 simp3 ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → 𝜑 )
96 fzofzp1 ⊢ ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) → ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) )
97 96 3ad2ant1 ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) )
98 nfv ⊢ Ⅎ 𝑖 ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 )
99 2 98 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) )
100 nfcv ⊢ Ⅎ 𝑖 ( 𝑗 + 1 )
101 1 100 nffv ⊢ Ⅎ 𝑖 ( 𝐵 ‘ ( 𝑗 + 1 ) )
102 101 nfel1 ⊢ Ⅎ 𝑖 ( 𝐵 ‘ ( 𝑗 + 1 ) ) ∈ ℝ
103 99 102 nfim ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
104 eleq1 ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( 𝑖 ∈ ( 𝐿 ... 𝑀 ) ↔ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) ) )
105 104 anbi2d ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) ↔ ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) ) ) )
106 fveq2 ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( 𝐵 ‘ 𝑖 ) = ( 𝐵 ‘ ( 𝑗 + 1 ) ) )
107 106 eleq1d ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( ( 𝐵 ‘ 𝑖 ) ∈ ℝ ↔ ( 𝐵 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ) )
108 105 107 imbi12d ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ) ) )
109 103 108 7 vtoclg1f ⊢ ( ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) → ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ) )
110 109 anabsi7 ⊢ ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
111 95 97 110 syl2anc ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
112 pm3.35 ⊢ ( ( 𝜑 ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ) → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) )
113 112 ancoms ⊢ ( ( ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) )
114 simpl ⊢ ( ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) → 0 ≤ ( 𝐴 ‘ 𝑗 ) )
115 113 114 syl ⊢ ( ( ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → 0 ≤ ( 𝐴 ‘ 𝑗 ) )
116 115 3adant1 ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → 0 ≤ ( 𝐴 ‘ 𝑗 ) )
117 3 fveq1i ⊢ ( 𝐴 ‘ 𝑗 ) = ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 )
118 116 117 breqtrdi ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → 0 ≤ ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) )
119 simp1 ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) )
120 96 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ) → ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) )
121 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ) → 𝜑 )
122 121 120 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ) → ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) ) )
123 43 44 101 nfbr ⊢ Ⅎ 𝑖 0 ≤ ( 𝐵 ‘ ( 𝑗 + 1 ) )
124 99 123 nfim ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ ( 𝑗 + 1 ) ) )
125 106 breq2d ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( 0 ≤ ( 𝐵 ‘ 𝑖 ) ↔ 0 ≤ ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) )
126 105 125 imbi12d ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝑖 ) ) ↔ ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) ) )
127 124 126 8 vtoclg1f ⊢ ( ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) → ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) )
128 120 122 127 sylc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ ( 𝑗 + 1 ) ) )
129 95 119 128 syl2anc ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → 0 ≤ ( 𝐵 ‘ ( 𝑗 + 1 ) ) )
130 94 111 118 129 mulge0d ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → 0 ≤ ( ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) · ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) )
131 seqp1 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝐿 ) → ( seq 𝐿 ( · , 𝐵 ) ‘ ( 𝑗 + 1 ) ) = ( ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) · ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) )
132 72 131 syl ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( seq 𝐿 ( · , 𝐵 ) ‘ ( 𝑗 + 1 ) ) = ( ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) · ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) )
133 130 132 breqtrrd ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → 0 ≤ ( seq 𝐿 ( · , 𝐵 ) ‘ ( 𝑗 + 1 ) ) )
134 3 fveq1i ⊢ ( 𝐴 ‘ ( 𝑗 + 1 ) ) = ( seq 𝐿 ( · , 𝐵 ) ‘ ( 𝑗 + 1 ) )
135 133 134 breqtrrdi ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → 0 ≤ ( 𝐴 ‘ ( 𝑗 + 1 ) ) )
136 94 111 remulcld ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) · ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
137 1red ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → 1 ∈ ℝ )
138 95 97 jca ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) ) )
139 101 44 61 nfbr ⊢ Ⅎ 𝑖 ( 𝐵 ‘ ( 𝑗 + 1 ) ) ≤ 1
140 99 139 nfim ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ≤ 1 )
141 106 breq1d ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( ( 𝐵 ‘ 𝑖 ) ≤ 1 ↔ ( 𝐵 ‘ ( 𝑗 + 1 ) ) ≤ 1 ) )
142 105 141 imbi12d ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ≤ 1 ) ↔ ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ≤ 1 ) ) )
143 140 142 9 vtoclg1f ⊢ ( ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) → ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ≤ 1 ) )
144 97 138 143 sylc ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) ≤ 1 )
145 111 137 94 118 144 lemul2ad ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) · ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) ≤ ( ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) · 1 ) )
146 94 recnd ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) ∈ ℂ )
147 146 mulid1d ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) · 1 ) = ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) )
148 145 147 breqtrd ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) · ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) ≤ ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) )
149 simp2 ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) )
150 112 simprd ⊢ ( ( 𝜑 ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ) → ( 𝐴 ‘ 𝑗 ) ≤ 1 )
151 95 149 150 syl2anc ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( 𝐴 ‘ 𝑗 ) ≤ 1 )
152 117 151 eqbrtrrid ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) ≤ 1 )
153 136 94 137 148 152 letrd ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑗 ) · ( 𝐵 ‘ ( 𝑗 + 1 ) ) ) ≤ 1 )
154 132 153 eqbrtrd ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( seq 𝐿 ( · , 𝐵 ) ‘ ( 𝑗 + 1 ) ) ≤ 1 )
155 134 154 eqbrtrid ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( 𝐴 ‘ ( 𝑗 + 1 ) ) ≤ 1 )
156 135 155 jca ⊢ ( ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) ∧ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) ∧ 𝜑 ) → ( 0 ≤ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ≤ 1 ) )
157 156 3exp ⊢ ( 𝑗 ∈ ( 𝐿 ..^ 𝑀 ) → ( ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝑗 ) ∧ ( 𝐴 ‘ 𝑗 ) ≤ 1 ) ) → ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ≤ 1 ) ) ) )
158 14 19 24 29 70 157 fzind2 ⊢ ( 𝐾 ∈ ( 𝐿 ... 𝑀 ) → ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝐾 ) ∧ ( 𝐴 ‘ 𝐾 ) ≤ 1 ) ) )
159 6 158 mpcom ⊢ ( 𝜑 → ( 0 ≤ ( 𝐴 ‘ 𝐾 ) ∧ ( 𝐴 ‘ 𝐾 ) ≤ 1 ) )