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 
|- F/_ i B
fmul01.2 
|- F/ i ph
fmul01.3 
|- A = seq L ( x. , B )
fmul01.4 
|- ( ph -> L e. ZZ )
fmul01.5 
|- ( ph -> M e. ( ZZ>= ` L ) )
fmul01.6 
|- ( ph -> K e. ( L ... M ) )
fmul01.7 
|- ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) e. RR )
fmul01.8 
|- ( ( ph /\ i e. ( L ... M ) ) -> 0 <_ ( B ` i ) )
fmul01.9 
|- ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) <_ 1 )
Assertion fmul01 
|- ( ph -> ( 0 <_ ( A ` K ) /\ ( A ` K ) <_ 1 ) )

Proof

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