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

Metamath Proof Explorer

Theorem stoweidlem3

Proof