Metamath Proof Explorer

Theorem stoweidlem3

Description: Lemma for stoweid : if A is positive and all M terms of a finite product are larger than A , then the finite product is larger than A ^ M . (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem3.1 
|- F/_ i F
stoweidlem3.2 
|- F/ i ph
stoweidlem3.3 
|- X = seq 1 ( x. , F )
stoweidlem3.4 
|- ( ph -> M e. NN )
stoweidlem3.5 
|- ( ph -> F : ( 1 ... M ) --> RR )
stoweidlem3.6 
|- ( ( ph /\ i e. ( 1 ... M ) ) -> A < ( F ` i ) )
stoweidlem3.7 
|- ( ph -> A e. RR+ )
Assertion stoweidlem3 
|- ( ph -> ( A ^ M ) < ( X ` M ) )

Proof

Step Hyp Ref Expression
1 stoweidlem3.1 
 |-  F/_ i F
2 stoweidlem3.2 
 |-  F/ i ph
3 stoweidlem3.3 
 |-  X = seq 1 ( x. , F )
4 stoweidlem3.4 
 |-  ( ph -> M e. NN )
5 stoweidlem3.5 
 |-  ( ph -> F : ( 1 ... M ) --> RR )
6 stoweidlem3.6 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> A < ( F ` i ) )
7 stoweidlem3.7 
 |-  ( ph -> A e. RR+ )
8 elnnuz 
 |-  ( M e. NN <-> M e. ( ZZ>= ` 1 ) )
9 4 8 sylib 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
10 eluzfz2 
 |-  ( M e. ( ZZ>= ` 1 ) -> M e. ( 1 ... M ) )
11 9 10 syl 
 |-  ( ph -> M e. ( 1 ... M ) )
12 oveq2 
 |-  ( n = 1 -> ( A ^ n ) = ( A ^ 1 ) )
13 fveq2 
 |-  ( n = 1 -> ( X ` n ) = ( X ` 1 ) )
14 12 13 breq12d 
 |-  ( n = 1 -> ( ( A ^ n ) < ( X ` n ) <-> ( A ^ 1 ) < ( X ` 1 ) ) )
15 14 imbi2d 
 |-  ( n = 1 -> ( ( ph -> ( A ^ n ) < ( X ` n ) ) <-> ( ph -> ( A ^ 1 ) < ( X ` 1 ) ) ) )
16 oveq2 
 |-  ( n = m -> ( A ^ n ) = ( A ^ m ) )
17 fveq2 
 |-  ( n = m -> ( X ` n ) = ( X ` m ) )
18 16 17 breq12d 
 |-  ( n = m -> ( ( A ^ n ) < ( X ` n ) <-> ( A ^ m ) < ( X ` m ) ) )
19 18 imbi2d 
 |-  ( n = m -> ( ( ph -> ( A ^ n ) < ( X ` n ) ) <-> ( ph -> ( A ^ m ) < ( X ` m ) ) ) )
20 oveq2 
 |-  ( n = ( m + 1 ) -> ( A ^ n ) = ( A ^ ( m + 1 ) ) )
21 fveq2 
 |-  ( n = ( m + 1 ) -> ( X ` n ) = ( X ` ( m + 1 ) ) )
22 20 21 breq12d 
 |-  ( n = ( m + 1 ) -> ( ( A ^ n ) < ( X ` n ) <-> ( A ^ ( m + 1 ) ) < ( X ` ( m + 1 ) ) ) )
23 22 imbi2d 
 |-  ( n = ( m + 1 ) -> ( ( ph -> ( A ^ n ) < ( X ` n ) ) <-> ( ph -> ( A ^ ( m + 1 ) ) < ( X ` ( m + 1 ) ) ) ) )
24 oveq2 
 |-  ( n = M -> ( A ^ n ) = ( A ^ M ) )
25 fveq2 
 |-  ( n = M -> ( X ` n ) = ( X ` M ) )
26 24 25 breq12d 
 |-  ( n = M -> ( ( A ^ n ) < ( X ` n ) <-> ( A ^ M ) < ( X ` M ) ) )
27 26 imbi2d 
 |-  ( n = M -> ( ( ph -> ( A ^ n ) < ( X ` n ) ) <-> ( ph -> ( A ^ M ) < ( X ` M ) ) ) )
28 1zzd 
 |-  ( ph -> 1 e. ZZ )
29 4 nnzd 
 |-  ( ph -> M e. ZZ )
30 1le1 
 |-  1 <_ 1
31 30 a1i 
 |-  ( ph -> 1 <_ 1 )
32 4 nnge1d 
 |-  ( ph -> 1 <_ M )
33 28 29 28 31 32 elfzd 
 |-  ( ph -> 1 e. ( 1 ... M ) )
34 33 ancli 
 |-  ( ph -> ( ph /\ 1 e. ( 1 ... M ) ) )
35 nfv 
 |-  F/ i 1 e. ( 1 ... M )
36 2 35 nfan 
 |-  F/ i ( ph /\ 1 e. ( 1 ... M ) )
37 nfcv 
 |-  F/_ i A
38 nfcv 
 |-  F/_ i <
39 nfcv 
 |-  F/_ i 1
40 1 39 nffv 
 |-  F/_ i ( F ` 1 )
41 37 38 40 nfbr 
 |-  F/ i A < ( F ` 1 )
42 36 41 nfim 
 |-  F/ i ( ( ph /\ 1 e. ( 1 ... M ) ) -> A < ( F ` 1 ) )
43 eleq1 
 |-  ( i = 1 -> ( i e. ( 1 ... M ) <-> 1 e. ( 1 ... M ) ) )
44 43 anbi2d 
 |-  ( i = 1 -> ( ( ph /\ i e. ( 1 ... M ) ) <-> ( ph /\ 1 e. ( 1 ... M ) ) ) )
45 fveq2 
 |-  ( i = 1 -> ( F ` i ) = ( F ` 1 ) )
46 45 breq2d 
 |-  ( i = 1 -> ( A < ( F ` i ) <-> A < ( F ` 1 ) ) )
47 44 46 imbi12d 
 |-  ( i = 1 -> ( ( ( ph /\ i e. ( 1 ... M ) ) -> A < ( F ` i ) ) <-> ( ( ph /\ 1 e. ( 1 ... M ) ) -> A < ( F ` 1 ) ) ) )
48 42 47 6 vtoclg1f 
 |-  ( 1 e. ( 1 ... M ) -> ( ( ph /\ 1 e. ( 1 ... M ) ) -> A < ( F ` 1 ) ) )
49 33 34 48 sylc 
 |-  ( ph -> A < ( F ` 1 ) )
50 7 rpcnd 
 |-  ( ph -> A e. CC )
51 50 exp1d 
 |-  ( ph -> ( A ^ 1 ) = A )
52 3 fveq1i 
 |-  ( X ` 1 ) = ( seq 1 ( x. , F ) ` 1 )
53 1z 
 |-  1 e. ZZ
54 seq1 
 |-  ( 1 e. ZZ -> ( seq 1 ( x. , F ) ` 1 ) = ( F ` 1 ) )
55 53 54 ax-mp 
 |-  ( seq 1 ( x. , F ) ` 1 ) = ( F ` 1 )
56 52 55 eqtri 
 |-  ( X ` 1 ) = ( F ` 1 )
57 56 a1i 
 |-  ( ph -> ( X ` 1 ) = ( F ` 1 ) )
58 49 51 57 3brtr4d 
 |-  ( ph -> ( A ^ 1 ) < ( X ` 1 ) )
59 58 a1i 
 |-  ( M e. ( ZZ>= ` 1 ) -> ( ph -> ( A ^ 1 ) < ( X ` 1 ) ) )
60 7 3ad2ant3 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> A e. RR+ )
61 60 rpred 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> A e. RR )
62 elfzouz 
 |-  ( m e. ( 1 ..^ M ) -> m e. ( ZZ>= ` 1 ) )
63 elnnuz 
 |-  ( m e. NN <-> m e. ( ZZ>= ` 1 ) )
64 nnnn0 
 |-  ( m e. NN -> m e. NN0 )
65 63 64 sylbir 
 |-  ( m e. ( ZZ>= ` 1 ) -> m e. NN0 )
66 62 65 syl 
 |-  ( m e. ( 1 ..^ M ) -> m e. NN0 )
67 66 3ad2ant1 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> m e. NN0 )
68 61 67 reexpcld 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( A ^ m ) e. RR )
69 3 fveq1i 
 |-  ( X ` m ) = ( seq 1 ( x. , F ) ` m )
70 62 adantr 
 |-  ( ( m e. ( 1 ..^ M ) /\ ph ) -> m e. ( ZZ>= ` 1 ) )
71 nfv 
 |-  F/ i m e. ( 1 ..^ M )
72 71 2 nfan 
 |-  F/ i ( m e. ( 1 ..^ M ) /\ ph )
73 nfv 
 |-  F/ i a e. ( 1 ... m )
74 72 73 nfan 
 |-  F/ i ( ( m e. ( 1 ..^ M ) /\ ph ) /\ a e. ( 1 ... m ) )
75 nfcv 
 |-  F/_ i a
76 1 75 nffv 
 |-  F/_ i ( F ` a )
77 76 nfel1 
 |-  F/ i ( F ` a ) e. RR
78 74 77 nfim 
 |-  F/ i ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ a e. ( 1 ... m ) ) -> ( F ` a ) e. RR )
79 eleq1 
 |-  ( i = a -> ( i e. ( 1 ... m ) <-> a e. ( 1 ... m ) ) )
80 79 anbi2d 
 |-  ( i = a -> ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) <-> ( ( m e. ( 1 ..^ M ) /\ ph ) /\ a e. ( 1 ... m ) ) ) )
81 fveq2 
 |-  ( i = a -> ( F ` i ) = ( F ` a ) )
82 81 eleq1d 
 |-  ( i = a -> ( ( F ` i ) e. RR <-> ( F ` a ) e. RR ) )
83 80 82 imbi12d 
 |-  ( i = a -> ( ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) -> ( F ` i ) e. RR ) <-> ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ a e. ( 1 ... m ) ) -> ( F ` a ) e. RR ) ) )
84 5 ad2antlr 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) -> F : ( 1 ... M ) --> RR )
85 1zzd 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) -> 1 e. ZZ )
86 29 ad2antlr 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) -> M e. ZZ )
87 elfzelz 
 |-  ( i e. ( 1 ... m ) -> i e. ZZ )
88 87 adantl 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) -> i e. ZZ )
89 elfzle1 
 |-  ( i e. ( 1 ... m ) -> 1 <_ i )
90 89 adantl 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) -> 1 <_ i )
91 87 zred 
 |-  ( i e. ( 1 ... m ) -> i e. RR )
92 91 adantl 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) -> i e. RR )
93 elfzoelz 
 |-  ( m e. ( 1 ..^ M ) -> m e. ZZ )
94 93 zred 
 |-  ( m e. ( 1 ..^ M ) -> m e. RR )
95 94 ad2antrr 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) -> m e. RR )
96 4 nnred 
 |-  ( ph -> M e. RR )
97 96 ad2antlr 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) -> M e. RR )
98 elfzle2 
 |-  ( i e. ( 1 ... m ) -> i <_ m )
99 98 adantl 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) -> i <_ m )
100 elfzoel2 
 |-  ( m e. ( 1 ..^ M ) -> M e. ZZ )
101 100 zred 
 |-  ( m e. ( 1 ..^ M ) -> M e. RR )
102 elfzolt2 
 |-  ( m e. ( 1 ..^ M ) -> m < M )
103 94 101 102 ltled 
 |-  ( m e. ( 1 ..^ M ) -> m <_ M )
104 103 ad2antrr 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) -> m <_ M )
105 92 95 97 99 104 letrd 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) -> i <_ M )
106 85 86 88 90 105 elfzd 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) -> i e. ( 1 ... M ) )
107 84 106 ffvelcdmd 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ i e. ( 1 ... m ) ) -> ( F ` i ) e. RR )
108 78 83 107 chvarfv 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ a e. ( 1 ... m ) ) -> ( F ` a ) e. RR )
109 remulcl 
 |-  ( ( a e. RR /\ j e. RR ) -> ( a x. j ) e. RR )
110 109 adantl 
 |-  ( ( ( m e. ( 1 ..^ M ) /\ ph ) /\ ( a e. RR /\ j e. RR ) ) -> ( a x. j ) e. RR )
111 70 108 110 seqcl 
 |-  ( ( m e. ( 1 ..^ M ) /\ ph ) -> ( seq 1 ( x. , F ) ` m ) e. RR )
112 69 111 eqeltrid 
 |-  ( ( m e. ( 1 ..^ M ) /\ ph ) -> ( X ` m ) e. RR )
113 112 3adant2 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( X ` m ) e. RR )
114 5 3ad2ant3 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> F : ( 1 ... M ) --> RR )
115 fzofzp1 
 |-  ( m e. ( 1 ..^ M ) -> ( m + 1 ) e. ( 1 ... M ) )
116 115 3ad2ant1 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( m + 1 ) e. ( 1 ... M ) )
117 114 116 ffvelcdmd 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( F ` ( m + 1 ) ) e. RR )
118 7 rpge0d 
 |-  ( ph -> 0 <_ A )
119 118 3ad2ant3 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> 0 <_ A )
120 61 67 119 expge0d 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> 0 <_ ( A ^ m ) )
121 simp3 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ph )
122 simp2 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( ph -> ( A ^ m ) < ( X ` m ) ) )
123 121 122 mpd 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( A ^ m ) < ( X ` m ) )
124 115 adantr 
 |-  ( ( m e. ( 1 ..^ M ) /\ ph ) -> ( m + 1 ) e. ( 1 ... M ) )
125 simpr 
 |-  ( ( m e. ( 1 ..^ M ) /\ ph ) -> ph )
126 125 124 jca 
 |-  ( ( m e. ( 1 ..^ M ) /\ ph ) -> ( ph /\ ( m + 1 ) e. ( 1 ... M ) ) )
127 nfv 
 |-  F/ i ( m + 1 ) e. ( 1 ... M )
128 2 127 nfan 
 |-  F/ i ( ph /\ ( m + 1 ) e. ( 1 ... M ) )
129 nfcv 
 |-  F/_ i ( m + 1 )
130 1 129 nffv 
 |-  F/_ i ( F ` ( m + 1 ) )
131 37 38 130 nfbr 
 |-  F/ i A < ( F ` ( m + 1 ) )
132 128 131 nfim 
 |-  F/ i ( ( ph /\ ( m + 1 ) e. ( 1 ... M ) ) -> A < ( F ` ( m + 1 ) ) )
133 eleq1 
 |-  ( i = ( m + 1 ) -> ( i e. ( 1 ... M ) <-> ( m + 1 ) e. ( 1 ... M ) ) )
134 133 anbi2d 
 |-  ( i = ( m + 1 ) -> ( ( ph /\ i e. ( 1 ... M ) ) <-> ( ph /\ ( m + 1 ) e. ( 1 ... M ) ) ) )
135 fveq2 
 |-  ( i = ( m + 1 ) -> ( F ` i ) = ( F ` ( m + 1 ) ) )
136 135 breq2d 
 |-  ( i = ( m + 1 ) -> ( A < ( F ` i ) <-> A < ( F ` ( m + 1 ) ) ) )
137 134 136 imbi12d 
 |-  ( i = ( m + 1 ) -> ( ( ( ph /\ i e. ( 1 ... M ) ) -> A < ( F ` i ) ) <-> ( ( ph /\ ( m + 1 ) e. ( 1 ... M ) ) -> A < ( F ` ( m + 1 ) ) ) ) )
138 132 137 6 vtoclg1f 
 |-  ( ( m + 1 ) e. ( 1 ... M ) -> ( ( ph /\ ( m + 1 ) e. ( 1 ... M ) ) -> A < ( F ` ( m + 1 ) ) ) )
139 124 126 138 sylc 
 |-  ( ( m e. ( 1 ..^ M ) /\ ph ) -> A < ( F ` ( m + 1 ) ) )
140 139 3adant2 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> A < ( F ` ( m + 1 ) ) )
141 68 113 61 117 120 123 119 140 ltmul12ad 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( ( A ^ m ) x. A ) < ( ( X ` m ) x. ( F ` ( m + 1 ) ) ) )
142 50 3ad2ant3 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> A e. CC )
143 142 67 expp1d 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( A ^ ( m + 1 ) ) = ( ( A ^ m ) x. A ) )
144 3 fveq1i 
 |-  ( X ` ( m + 1 ) ) = ( seq 1 ( x. , F ) ` ( m + 1 ) )
145 144 a1i 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( X ` ( m + 1 ) ) = ( seq 1 ( x. , F ) ` ( m + 1 ) ) )
146 62 3ad2ant1 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> m e. ( ZZ>= ` 1 ) )
147 seqp1 
 |-  ( m e. ( ZZ>= ` 1 ) -> ( seq 1 ( x. , F ) ` ( m + 1 ) ) = ( ( seq 1 ( x. , F ) ` m ) x. ( F ` ( m + 1 ) ) ) )
148 146 147 syl 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( seq 1 ( x. , F ) ` ( m + 1 ) ) = ( ( seq 1 ( x. , F ) ` m ) x. ( F ` ( m + 1 ) ) ) )
149 69 a1i 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( X ` m ) = ( seq 1 ( x. , F ) ` m ) )
150 149 eqcomd 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( seq 1 ( x. , F ) ` m ) = ( X ` m ) )
151 150 oveq1d 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( ( seq 1 ( x. , F ) ` m ) x. ( F ` ( m + 1 ) ) ) = ( ( X ` m ) x. ( F ` ( m + 1 ) ) ) )
152 145 148 151 3eqtrd 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( X ` ( m + 1 ) ) = ( ( X ` m ) x. ( F ` ( m + 1 ) ) ) )
153 141 143 152 3brtr4d 
 |-  ( ( m e. ( 1 ..^ M ) /\ ( ph -> ( A ^ m ) < ( X ` m ) ) /\ ph ) -> ( A ^ ( m + 1 ) ) < ( X ` ( m + 1 ) ) )
154 153 3exp 
 |-  ( m e. ( 1 ..^ M ) -> ( ( ph -> ( A ^ m ) < ( X ` m ) ) -> ( ph -> ( A ^ ( m + 1 ) ) < ( X ` ( m + 1 ) ) ) ) )
155 15 19 23 27 59 154 fzind2 
 |-  ( M e. ( 1 ... M ) -> ( ph -> ( A ^ M ) < ( X ` M ) ) )
156 11 155 mpcom 
 |-  ( ph -> ( A ^ M ) < ( X ` M ) )