fourierdlem31

Description: If A is finite and for any element in A there is a number m such that a property holds for all numbers larger than m , then there is a number n such that the property holds for all numbers larger than n and for all elements in A . (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 29-Sep-2020)

	Ref	Expression
Hypotheses	fourierdlem31.i	$⊢ Ⅎ i φ$
	fourierdlem31.r	$⊢ Ⅎ r φ$
	fourierdlem31.iv	$⊢ \underline{Ⅎ} i V$
	fourierdlem31.a	$⊢ φ \to A \in Fin$
	fourierdlem31.exm	$⊢ φ \to \forall i \in A \exists m \in ℕ \forall r \in (m, +∞) χ$
	fourierdlem31.m	$⊢ M = \{m \in ℕ \| \forall r \in (m, +∞) χ\}$
	fourierdlem31.v	$⊢ V = (i \in A ⟼ inf (M ℝ <))$
	fourierdlem31.n	$⊢ N = sup (ran V ℝ <)$
Assertion	fourierdlem31	$⊢ φ \to \exists n \in ℕ \forall r \in (n, +∞) \forall i \in A χ$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem31.i	$⊢ Ⅎ i φ$
2		fourierdlem31.r	$⊢ Ⅎ r φ$
3		fourierdlem31.iv	$⊢ \underline{Ⅎ} i V$
4		fourierdlem31.a	$⊢ φ \to A \in Fin$
5		fourierdlem31.exm	$⊢ φ \to \forall i \in A \exists m \in ℕ \forall r \in (m, +∞) χ$
6		fourierdlem31.m	$⊢ M = \{m \in ℕ \| \forall r \in (m, +∞) χ\}$
7		fourierdlem31.v	$⊢ V = (i \in A ⟼ inf (M ℝ <))$
8		fourierdlem31.n	$⊢ N = sup (ran V ℝ <)$
9		1nn	$⊢ 1 \in ℕ$
10		rzal	$⊢ A = \emptyset \to \forall i \in A χ$
11	10	ralrimivw	$⊢ A = \emptyset \to \forall r \in (1, +∞) \forall i \in A χ$
12		oveq1	$⊢ n = 1 \to (n, +∞) = (1, +∞)$
13	12	raleqdv	$⊢ n = 1 \to (\forall r \in (n, +∞) \forall i \in A χ \leftrightarrow \forall r \in (1, +∞) \forall i \in A χ)$
14	13	rspcev	$⊢ (1 \in ℕ \land \forall r \in (1, +∞) \forall i \in A χ) \to \exists n \in ℕ \forall r \in (n, +∞) \forall i \in A χ$
15	9 11 14	sylancr	$⊢ A = \emptyset \to \exists n \in ℕ \forall r \in (n, +∞) \forall i \in A χ$
16	15	adantl	$⊢ (φ \land A = \emptyset) \to \exists n \in ℕ \forall r \in (n, +∞) \forall i \in A χ$
17	6	a1i	$⊢ (φ \land i \in A) \to M = \{m \in ℕ \| \forall r \in (m, +∞) χ\}$
18	17	infeq1d	$⊢ (φ \land i \in A) \to inf (M ℝ <) = inf (\{m \in ℕ \| \forall r \in (m, +∞) χ\} ℝ <)$
19		ssrab2	$⊢ \{m \in ℕ \| \forall r \in (m, +∞) χ\} \subseteq ℕ$
20		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
21	19 20	sseqtri	$⊢ \{m \in ℕ \| \forall r \in (m, +∞) χ\} \subseteq ℤ_{\geq 1}$
22	5	r19.21bi	$⊢ (φ \land i \in A) \to \exists m \in ℕ \forall r \in (m, +∞) χ$
23		rabn0	$⊢ \{m \in ℕ \| \forall r \in (m, +∞) χ\} \neq \emptyset \leftrightarrow \exists m \in ℕ \forall r \in (m, +∞) χ$
24	22 23	sylibr	$⊢ (φ \land i \in A) \to \{m \in ℕ \| \forall r \in (m, +∞) χ\} \neq \emptyset$
25		infssuzcl	$⊢ (\{m \in ℕ \| \forall r \in (m, +∞) χ\} \subseteq ℤ_{\geq 1} \land \{m \in ℕ \| \forall r \in (m, +∞) χ\} \neq \emptyset) \to inf (\{m \in ℕ \| \forall r \in (m, +∞) χ\} ℝ <) \in \{m \in ℕ \| \forall r \in (m, +∞) χ\}$
26	21 24 25	sylancr	$⊢ (φ \land i \in A) \to inf (\{m \in ℕ \| \forall r \in (m, +∞) χ\} ℝ <) \in \{m \in ℕ \| \forall r \in (m, +∞) χ\}$
27	19 26	sselid	$⊢ (φ \land i \in A) \to inf (\{m \in ℕ \| \forall r \in (m, +∞) χ\} ℝ <) \in ℕ$
28	18 27	eqeltrd	$⊢ (φ \land i \in A) \to inf (M ℝ <) \in ℕ$
29	1 7 28	rnmptssd	$⊢ φ \to ran V \subseteq ℕ$
30	29	adantr	$⊢ (φ \land \neg A = \emptyset) \to ran V \subseteq ℕ$
31		ltso	$⊢ < Or ℝ$
32	31	a1i	$⊢ (φ \land \neg A = \emptyset) \to < Or ℝ$
33		mptfi	$⊢ A \in Fin \to (i \in A ⟼ inf (M ℝ <)) \in Fin$
34	4 33	syl	$⊢ φ \to (i \in A ⟼ inf (M ℝ <)) \in Fin$
35	7 34	eqeltrid	$⊢ φ \to V \in Fin$
36		rnfi	$⊢ V \in Fin \to ran V \in Fin$
37	35 36	syl	$⊢ φ \to ran V \in Fin$
38	37	adantr	$⊢ (φ \land \neg A = \emptyset) \to ran V \in Fin$
39		neqne	$⊢ \neg A = \emptyset \to A \neq \emptyset$
40		n0	$⊢ A \neq \emptyset \leftrightarrow \exists i i \in A$
41	39 40	sylib	$⊢ \neg A = \emptyset \to \exists i i \in A$
42	41	adantl	$⊢ (φ \land \neg A = \emptyset) \to \exists i i \in A$
43		nfv	$⊢ Ⅎ i \neg A = \emptyset$
44	1 43	nfan	$⊢ Ⅎ i (φ \land \neg A = \emptyset)$
45	3	nfrn	$⊢ \underline{Ⅎ} i ran V$
46		nfcv	$⊢ \underline{Ⅎ} i \emptyset$
47	45 46	nfne	$⊢ Ⅎ i ran V \neq \emptyset$
48		simpr	$⊢ (φ \land i \in A) \to i \in A$
49	7	elrnmpt1	$⊢ (i \in A \land inf (M ℝ <) \in ℕ) \to inf (M ℝ <) \in ran V$
50	48 28 49	syl2anc	$⊢ (φ \land i \in A) \to inf (M ℝ <) \in ran V$
51	50	ne0d	$⊢ (φ \land i \in A) \to ran V \neq \emptyset$
52	51	ex	$⊢ φ \to (i \in A \to ran V \neq \emptyset)$
53	52	adantr	$⊢ (φ \land \neg A = \emptyset) \to (i \in A \to ran V \neq \emptyset)$
54	44 47 53	exlimd	$⊢ (φ \land \neg A = \emptyset) \to (\exists i i \in A \to ran V \neq \emptyset)$
55	42 54	mpd	$⊢ (φ \land \neg A = \emptyset) \to ran V \neq \emptyset$
56		nnssre	$⊢ ℕ \subseteq ℝ$
57	30 56	sstrdi	$⊢ (φ \land \neg A = \emptyset) \to ran V \subseteq ℝ$
58		fisupcl	$⊢ (< Or ℝ \land (ran V \in Fin \land ran V \neq \emptyset \land ran V \subseteq ℝ)) \to sup (ran V ℝ <) \in ran V$
59	32 38 55 57 58	syl13anc	$⊢ (φ \land \neg A = \emptyset) \to sup (ran V ℝ <) \in ran V$
60	30 59	sseldd	$⊢ (φ \land \neg A = \emptyset) \to sup (ran V ℝ <) \in ℕ$
61	8 60	eqeltrid	$⊢ (φ \land \neg A = \emptyset) \to N \in ℕ$
62		nfcv	$⊢ \underline{Ⅎ} i ℝ$
63		nfcv	$⊢ \underline{Ⅎ} i <$
64	45 62 63	nfsup	$⊢ \underline{Ⅎ} i sup (ran V ℝ <)$
65	8 64	nfcxfr	$⊢ \underline{Ⅎ} i N$
66		nfcv	$⊢ \underline{Ⅎ} i (.)$
67		nfcv	$⊢ \underline{Ⅎ} i +∞$
68	65 66 67	nfov	$⊢ \underline{Ⅎ} i (N, +∞)$
69	68	nfcri	$⊢ Ⅎ i r \in (N, +∞)$
70	1 69	nfan	$⊢ Ⅎ i (φ \land r \in (N, +∞))$
71	7	fvmpt2	$⊢ (i \in A \land inf (M ℝ <) \in ℕ) \to V (i) = inf (M ℝ <)$
72	48 28 71	syl2anc	$⊢ (φ \land i \in A) \to V (i) = inf (M ℝ <)$
73	28	nnxrd	$⊢ (φ \land i \in A) \to inf (M ℝ <) \in ℝ^{*}$
74	72 73	eqeltrd	$⊢ (φ \land i \in A) \to V (i) \in ℝ^{*}$
75	74	adantr	$⊢ ((φ \land i \in A) \land r \in (N, +∞)) \to V (i) \in ℝ^{*}$
76		pnfxr	$⊢ +∞ \in ℝ^{*}$
77	76	a1i	$⊢ ((φ \land i \in A) \land r \in (N, +∞)) \to +∞ \in ℝ^{*}$
78		elioore	$⊢ r \in (N, +∞) \to r \in ℝ$
79	78	adantl	$⊢ ((φ \land i \in A) \land r \in (N, +∞)) \to r \in ℝ$
80	72 28	eqeltrd	$⊢ (φ \land i \in A) \to V (i) \in ℕ$
81	80	nnred	$⊢ (φ \land i \in A) \to V (i) \in ℝ$
82	81	adantr	$⊢ ((φ \land i \in A) \land r \in (N, +∞)) \to V (i) \in ℝ$
83		ne0i	$⊢ i \in A \to A \neq \emptyset$
84	83	adantl	$⊢ (φ \land i \in A) \to A \neq \emptyset$
85	84	neneqd	$⊢ (φ \land i \in A) \to \neg A = \emptyset$
86	85 61	syldan	$⊢ (φ \land i \in A) \to N \in ℕ$
87	86	nnred	$⊢ (φ \land i \in A) \to N \in ℝ$
88	87	adantr	$⊢ ((φ \land i \in A) \land r \in (N, +∞)) \to N \in ℝ$
89	85 57	syldan	$⊢ (φ \land i \in A) \to ran V \subseteq ℝ$
90	29 56	sstrdi	$⊢ φ \to ran V \subseteq ℝ$
91		fimaxre2	$⊢ (ran V \subseteq ℝ \land ran V \in Fin) \to \exists x \in ℝ \forall y \in ran V y \leq x$
92	90 37 91	syl2anc	$⊢ φ \to \exists x \in ℝ \forall y \in ran V y \leq x$
93	92	adantr	$⊢ (φ \land i \in A) \to \exists x \in ℝ \forall y \in ran V y \leq x$
94	72 50	eqeltrd	$⊢ (φ \land i \in A) \to V (i) \in ran V$
95		suprub	$⊢ ((ran V \subseteq ℝ \land ran V \neq \emptyset \land \exists x \in ℝ \forall y \in ran V y \leq x) \land V (i) \in ran V) \to V (i) \leq sup (ran V ℝ <)$
96	89 51 93 94 95	syl31anc	$⊢ (φ \land i \in A) \to V (i) \leq sup (ran V ℝ <)$
97	96 8	breqtrrdi	$⊢ (φ \land i \in A) \to V (i) \leq N$
98	97	adantr	$⊢ ((φ \land i \in A) \land r \in (N, +∞)) \to V (i) \leq N$
99	88	rexrd	$⊢ ((φ \land i \in A) \land r \in (N, +∞)) \to N \in ℝ^{*}$
100		simpr	$⊢ ((φ \land i \in A) \land r \in (N, +∞)) \to r \in (N, +∞)$
101		ioogtlb	$⊢ (N \in ℝ^{} \land +∞ \in ℝ^{} \land r \in (N, +∞)) \to N < r$
102	99 77 100 101	syl3anc	$⊢ ((φ \land i \in A) \land r \in (N, +∞)) \to N < r$
103	82 88 79 98 102	lelttrd	$⊢ ((φ \land i \in A) \land r \in (N, +∞)) \to V (i) < r$
104	79	ltpnfd	$⊢ ((φ \land i \in A) \land r \in (N, +∞)) \to r < +∞$
105	75 77 79 103 104	eliood	$⊢ ((φ \land i \in A) \land r \in (N, +∞)) \to r \in (V (i), +∞)$
106	18 26	eqeltrd	$⊢ (φ \land i \in A) \to inf (M ℝ <) \in \{m \in ℕ \| \forall r \in (m, +∞) χ\}$
107	72 106	eqeltrd	$⊢ (φ \land i \in A) \to V (i) \in \{m \in ℕ \| \forall r \in (m, +∞) χ\}$
108		nfcv	$⊢ \underline{Ⅎ} m A$
109		nfrab1	$⊢ \underline{Ⅎ} m \{m \in ℕ \| \forall r \in (m, +∞) χ\}$
110	6 109	nfcxfr	$⊢ \underline{Ⅎ} m M$
111		nfcv	$⊢ \underline{Ⅎ} m ℝ$
112		nfcv	$⊢ \underline{Ⅎ} m <$
113	110 111 112	nfinf	$⊢ \underline{Ⅎ} m inf (M ℝ <)$
114	108 113	nfmpt	$⊢ \underline{Ⅎ} m (i \in A ⟼ inf (M ℝ <))$
115	7 114	nfcxfr	$⊢ \underline{Ⅎ} m V$
116		nfcv	$⊢ \underline{Ⅎ} m i$
117	115 116	nffv	$⊢ \underline{Ⅎ} m V (i)$
118	117 109	nfel	$⊢ Ⅎ m V (i) \in \{m \in ℕ \| \forall r \in (m, +∞) χ\}$
119	117	nfel1	$⊢ Ⅎ m V (i) \in ℕ$
120		nfcv	$⊢ \underline{Ⅎ} m (.)$
121		nfcv	$⊢ \underline{Ⅎ} m +∞$
122	117 120 121	nfov	$⊢ \underline{Ⅎ} m (V (i), +∞)$
123		nfv	$⊢ Ⅎ m χ$
124	122 123	nfralw	$⊢ Ⅎ m \forall r \in (V (i), +∞) χ$
125	119 124	nfan	$⊢ Ⅎ m (V (i) \in ℕ \land \forall r \in (V (i), +∞) χ)$
126	118 125	nfbi	$⊢ Ⅎ m (V (i) \in \{m \in ℕ \| \forall r \in (m, +∞) χ\} \leftrightarrow (V (i) \in ℕ \land \forall r \in (V (i), +∞) χ))$
127		eleq1	$⊢ m = V (i) \to (m \in \{m \in ℕ \| \forall r \in (m, +∞) χ\} \leftrightarrow V (i) \in \{m \in ℕ \| \forall r \in (m, +∞) χ\})$
128		eleq1	$⊢ m = V (i) \to (m \in ℕ \leftrightarrow V (i) \in ℕ)$
129		oveq1	$⊢ m = V (i) \to (m, +∞) = (V (i), +∞)$
130		nfcv	$⊢ \underline{Ⅎ} r (m, +∞)$
131		nfcv	$⊢ \underline{Ⅎ} r A$
132		nfra1	$⊢ Ⅎ r \forall r \in (m, +∞) χ$
133		nfcv	$⊢ \underline{Ⅎ} r ℕ$
134	132 133	nfrabw	$⊢ \underline{Ⅎ} r \{m \in ℕ \| \forall r \in (m, +∞) χ\}$
135	6 134	nfcxfr	$⊢ \underline{Ⅎ} r M$
136		nfcv	$⊢ \underline{Ⅎ} r ℝ$
137		nfcv	$⊢ \underline{Ⅎ} r <$
138	135 136 137	nfinf	$⊢ \underline{Ⅎ} r inf (M ℝ <)$
139	131 138	nfmpt	$⊢ \underline{Ⅎ} r (i \in A ⟼ inf (M ℝ <))$
140	7 139	nfcxfr	$⊢ \underline{Ⅎ} r V$
141		nfcv	$⊢ \underline{Ⅎ} r i$
142	140 141	nffv	$⊢ \underline{Ⅎ} r V (i)$
143		nfcv	$⊢ \underline{Ⅎ} r (.)$
144		nfcv	$⊢ \underline{Ⅎ} r +∞$
145	142 143 144	nfov	$⊢ \underline{Ⅎ} r (V (i), +∞)$
146	130 145	raleqf	$⊢ (m, +∞) = (V (i), +∞) \to (\forall r \in (m, +∞) χ \leftrightarrow \forall r \in (V (i), +∞) χ)$
147	129 146	syl	$⊢ m = V (i) \to (\forall r \in (m, +∞) χ \leftrightarrow \forall r \in (V (i), +∞) χ)$
148	128 147	anbi12d	$⊢ m = V (i) \to ((m \in ℕ \land \forall r \in (m, +∞) χ) \leftrightarrow (V (i) \in ℕ \land \forall r \in (V (i), +∞) χ))$
149	127 148	bibi12d	$⊢ m = V (i) \to ((m \in \{m \in ℕ \| \forall r \in (m, +∞) χ\} \leftrightarrow (m \in ℕ \land \forall r \in (m, +∞) χ)) \leftrightarrow (V (i) \in \{m \in ℕ \| \forall r \in (m, +∞) χ\} \leftrightarrow (V (i) \in ℕ \land \forall r \in (V (i), +∞) χ)))$
150		rabid	$⊢ m \in \{m \in ℕ \| \forall r \in (m, +∞) χ\} \leftrightarrow (m \in ℕ \land \forall r \in (m, +∞) χ)$
151	117 126 149 150	vtoclgf	$⊢ V (i) \in ℕ \to (V (i) \in \{m \in ℕ \| \forall r \in (m, +∞) χ\} \leftrightarrow (V (i) \in ℕ \land \forall r \in (V (i), +∞) χ))$
152	80 151	syl	$⊢ (φ \land i \in A) \to (V (i) \in \{m \in ℕ \| \forall r \in (m, +∞) χ\} \leftrightarrow (V (i) \in ℕ \land \forall r \in (V (i), +∞) χ))$
153	107 152	mpbid	$⊢ (φ \land i \in A) \to (V (i) \in ℕ \land \forall r \in (V (i), +∞) χ)$
154	153	simprd	$⊢ (φ \land i \in A) \to \forall r \in (V (i), +∞) χ$
155	154	r19.21bi	$⊢ ((φ \land i \in A) \land r \in (V (i), +∞)) \to χ$
156	105 155	syldan	$⊢ ((φ \land i \in A) \land r \in (N, +∞)) \to χ$
157	156	an32s	$⊢ ((φ \land r \in (N, +∞)) \land i \in A) \to χ$
158	157	ex	$⊢ (φ \land r \in (N, +∞)) \to (i \in A \to χ)$
159	70 158	ralrimi	$⊢ (φ \land r \in (N, +∞)) \to \forall i \in A χ$
160	159	ex	$⊢ φ \to (r \in (N, +∞) \to \forall i \in A χ)$
161	2 160	ralrimi	$⊢ φ \to \forall r \in (N, +∞) \forall i \in A χ$
162	161	adantr	$⊢ (φ \land \neg A = \emptyset) \to \forall r \in (N, +∞) \forall i \in A χ$
163		oveq1	$⊢ n = N \to (n, +∞) = (N, +∞)$
164		nfcv	$⊢ \underline{Ⅎ} r (n, +∞)$
165	140	nfrn	$⊢ \underline{Ⅎ} r ran V$
166	165 136 137	nfsup	$⊢ \underline{Ⅎ} r sup (ran V ℝ <)$
167	8 166	nfcxfr	$⊢ \underline{Ⅎ} r N$
168	167 143 144	nfov	$⊢ \underline{Ⅎ} r (N, +∞)$
169	164 168	raleqf	$⊢ (n, +∞) = (N, +∞) \to (\forall r \in (n, +∞) \forall i \in A χ \leftrightarrow \forall r \in (N, +∞) \forall i \in A χ)$
170	163 169	syl	$⊢ n = N \to (\forall r \in (n, +∞) \forall i \in A χ \leftrightarrow \forall r \in (N, +∞) \forall i \in A χ)$
171	170	rspcev	$⊢ (N \in ℕ \land \forall r \in (N, +∞) \forall i \in A χ) \to \exists n \in ℕ \forall r \in (n, +∞) \forall i \in A χ$
172	61 162 171	syl2anc	$⊢ (φ \land \neg A = \emptyset) \to \exists n \in ℕ \forall r \in (n, +∞) \forall i \in A χ$
173	16 172	pm2.61dan	$⊢ φ \to \exists n \in ℕ \forall r \in (n, +∞) \forall i \in A χ$

Metamath Proof Explorer

Theorem fourierdlem31

Proof