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	ffvelcdmd	⊢ ( ( ( 𝑚 ∈ ( 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	ffvelcdmd	⊢ ( ( 𝑚 ∈ ( 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	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑀 ) < ( 𝑋 ‘ 𝑀 ) )