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