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 ⊢ Ⅎ 𝑖 𝐹
stoweidlem3.2 ⊢ Ⅎ 𝑖 𝜑
stoweidlem3.3 ⊢ 𝑋 = seq 1 ( · , 𝐹 )
stoweidlem3.4 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
stoweidlem3.5 ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑀 ) ⟶ ℝ )
stoweidlem3.6 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝐴 < ( 𝐹 ‘ 𝑖 ) )
stoweidlem3.7 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
Assertion stoweidlem3 ( 𝜑 → ( 𝐴 ↑ 𝑀 ) < ( 𝑋 ‘ 𝑀 ) )

Proof

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