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