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