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

Metamath Proof Explorer

Theorem fourierdlem31

Proof