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	$⊢ \underline{Ⅎ} i F$
	stoweidlem3.2	$⊢ Ⅎ i φ$
	stoweidlem3.3	$⊢ X = seq 1 (\times F)$
	stoweidlem3.4	$⊢ φ \to M \in ℕ$
	stoweidlem3.5	$⊢ φ \to F : (1 \dots M) ⟶ ℝ$
	stoweidlem3.6	$⊢ (φ \land i \in (1 \dots M)) \to A < F (i)$
	stoweidlem3.7	$⊢ φ \to A \in ℝ^{+}$
Assertion	stoweidlem3	$⊢ φ \to A^{M} < X (M)$

Proof

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

Metamath Proof Explorer

Theorem stoweidlem3

Proof