iooiinicc

Description: A closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	iooiinicc.a	$⊢ φ \to A \in ℝ$
	iooiinicc.b	$⊢ φ \to B \in ℝ$
Assertion	iooiinicc	$⊢ φ \to ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) = [A, B]$

Proof

Step	Hyp	Ref	Expression
1		iooiinicc.a	$⊢ φ \to A \in ℝ$
2		iooiinicc.b	$⊢ φ \to B \in ℝ$
3	1	adantr	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to A \in ℝ$
4	2	adantr	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to B \in ℝ$
5		1nn	$⊢ 1 \in ℕ$
6		ioossre	$⊢ (A - (\frac{1}{1}), B + (\frac{1}{1})) \subseteq ℝ$
7		oveq2	$⊢ n = 1 \to \frac{1}{n} = \frac{1}{1}$
8	7	oveq2d	$⊢ n = 1 \to A - (\frac{1}{n}) = A - (\frac{1}{1})$
9	7	oveq2d	$⊢ n = 1 \to B + (\frac{1}{n}) = B + (\frac{1}{1})$
10	8 9	oveq12d	$⊢ n = 1 \to (A - (\frac{1}{n}), B + (\frac{1}{n})) = (A - (\frac{1}{1}), B + (\frac{1}{1}))$
11	10	sseq1d	$⊢ n = 1 \to ((A - (\frac{1}{n}), B + (\frac{1}{n})) \subseteq ℝ \leftrightarrow (A - (\frac{1}{1}), B + (\frac{1}{1})) \subseteq ℝ)$
12	11	rspcev	$⊢ (1 \in ℕ \land (A - (\frac{1}{1}), B + (\frac{1}{1})) \subseteq ℝ) \to \exists n \in ℕ (A - (\frac{1}{n}), B + (\frac{1}{n})) \subseteq ℝ$
13	5 6 12	mp2an	$⊢ \exists n \in ℕ (A - (\frac{1}{n}), B + (\frac{1}{n})) \subseteq ℝ$
14		iinss	$⊢ \exists n \in ℕ (A - (\frac{1}{n}), B + (\frac{1}{n})) \subseteq ℝ \to ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) \subseteq ℝ$
15	13 14	ax-mp	$⊢ ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) \subseteq ℝ$
16	15	a1i	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) \subseteq ℝ$
17		simpr	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))$
18	16 17	sseldd	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to x \in ℝ$
19		nfv	$⊢ Ⅎ n φ$
20		nfcv	$⊢ \underline{Ⅎ} n x$
21		nfii1	$⊢ \underline{Ⅎ} n ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))$
22	20 21	nfel	$⊢ Ⅎ n x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))$
23	19 22	nfan	$⊢ Ⅎ n (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})))$
24		simpll	$⊢ ((φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to φ$
25		iinss2	$⊢ n \in ℕ \to ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) \subseteq (A - (\frac{1}{n}), B + (\frac{1}{n}))$
26	25	adantl	$⊢ (x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) \land n \in ℕ) \to ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) \subseteq (A - (\frac{1}{n}), B + (\frac{1}{n}))$
27		simpl	$⊢ (x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) \land n \in ℕ) \to x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))$
28	26 27	sseldd	$⊢ (x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) \land n \in ℕ) \to x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))$
29	28	adantll	$⊢ ((φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))$
30		simpr	$⊢ ((φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to n \in ℕ$
31	1	adantr	$⊢ (φ \land n \in ℕ) \to A \in ℝ$
32	31	adantlr	$⊢ ((φ \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to A \in ℝ$
33		elioore	$⊢ x \in (A - (\frac{1}{n}), B + (\frac{1}{n})) \to x \in ℝ$
34	33	adantr	$⊢ (x \in (A - (\frac{1}{n}), B + (\frac{1}{n})) \land n \in ℕ) \to x \in ℝ$
35		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
36	35	adantl	$⊢ (x \in (A - (\frac{1}{n}), B + (\frac{1}{n})) \land n \in ℕ) \to \frac{1}{n} \in ℝ$
37	34 36	readdcld	$⊢ (x \in (A - (\frac{1}{n}), B + (\frac{1}{n})) \land n \in ℕ) \to x + (\frac{1}{n}) \in ℝ$
38	37	adantll	$⊢ ((φ \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to x + (\frac{1}{n}) \in ℝ$
39	35	adantl	$⊢ (φ \land n \in ℕ) \to \frac{1}{n} \in ℝ$
40	31 39	resubcld	$⊢ (φ \land n \in ℕ) \to A - (\frac{1}{n}) \in ℝ$
41	40	rexrd	$⊢ (φ \land n \in ℕ) \to A - (\frac{1}{n}) \in ℝ^{*}$
42	41	adantlr	$⊢ ((φ \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to A - (\frac{1}{n}) \in ℝ^{*}$
43	2	adantr	$⊢ (φ \land n \in ℕ) \to B \in ℝ$
44	43 39	readdcld	$⊢ (φ \land n \in ℕ) \to B + (\frac{1}{n}) \in ℝ$
45	44	rexrd	$⊢ (φ \land n \in ℕ) \to B + (\frac{1}{n}) \in ℝ^{*}$
46	45	adantlr	$⊢ ((φ \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to B + (\frac{1}{n}) \in ℝ^{*}$
47		simplr	$⊢ ((φ \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))$
48		ioogtlb	$⊢ (A - (\frac{1}{n}) \in ℝ^{} \land B + (\frac{1}{n}) \in ℝ^{} \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to A - (\frac{1}{n}) < x$
49	42 46 47 48	syl3anc	$⊢ ((φ \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to A - (\frac{1}{n}) < x$
50	35	adantl	$⊢ ((φ \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to \frac{1}{n} \in ℝ$
51	34	adantll	$⊢ ((φ \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to x \in ℝ$
52	32 50 51	ltsubaddd	$⊢ ((φ \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to (A - (\frac{1}{n}) < x \leftrightarrow A < x + (\frac{1}{n}))$
53	49 52	mpbid	$⊢ ((φ \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to A < x + (\frac{1}{n})$
54	32 38 53	ltled	$⊢ ((φ \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to A \leq x + (\frac{1}{n})$
55	24 29 30 54	syl21anc	$⊢ ((φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to A \leq x + (\frac{1}{n})$
56	55	ex	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to (n \in ℕ \to A \leq x + (\frac{1}{n}))$
57	23 56	ralrimi	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to \forall n \in ℕ A \leq x + (\frac{1}{n})$
58	3	rexrd	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to A \in ℝ^{*}$
59	23 58 18	xrralrecnnle	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to (A \leq x \leftrightarrow \forall n \in ℕ A \leq x + (\frac{1}{n}))$
60	57 59	mpbird	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to A \leq x$
61	44	adantlr	$⊢ ((φ \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to B + (\frac{1}{n}) \in ℝ$
62		iooltub	$⊢ (A - (\frac{1}{n}) \in ℝ^{} \land B + (\frac{1}{n}) \in ℝ^{} \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to x < B + (\frac{1}{n})$
63	42 46 47 62	syl3anc	$⊢ ((φ \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to x < B + (\frac{1}{n})$
64	51 61 63	ltled	$⊢ ((φ \land x \in (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to x \leq B + (\frac{1}{n})$
65	24 29 30 64	syl21anc	$⊢ ((φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \land n \in ℕ) \to x \leq B + (\frac{1}{n})$
66	65	ex	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to (n \in ℕ \to x \leq B + (\frac{1}{n}))$
67	23 66	ralrimi	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to \forall n \in ℕ x \leq B + (\frac{1}{n})$
68	18	rexrd	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to x \in ℝ^{*}$
69	23 68 4	xrralrecnnle	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to (x \leq B \leftrightarrow \forall n \in ℕ x \leq B + (\frac{1}{n}))$
70	67 69	mpbird	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to x \leq B$
71	3 4 18 60 70	eliccd	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))) \to x \in [A, B]$
72	71	ralrimiva	$⊢ φ \to \forall x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) x \in [A, B]$
73		dfss3	$⊢ ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) \subseteq [A, B] \leftrightarrow \forall x \in ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) x \in [A, B]$
74	72 73	sylibr	$⊢ φ \to ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) \subseteq [A, B]$
75		1rp	$⊢ 1 \in ℝ^{+}$
76	75	a1i	$⊢ n \in ℕ \to 1 \in ℝ^{+}$
77		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
78	76 77	rpdivcld	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ^{+}$
79	78	adantl	$⊢ (φ \land n \in ℕ) \to \frac{1}{n} \in ℝ^{+}$
80	31 79	ltsubrpd	$⊢ (φ \land n \in ℕ) \to A - (\frac{1}{n}) < A$
81	43 79	ltaddrpd	$⊢ (φ \land n \in ℕ) \to B < B + (\frac{1}{n})$
82		iccssioo	$⊢ ((A - (\frac{1}{n}) \in ℝ^{} \land B + (\frac{1}{n}) \in ℝ^{}) \land (A - (\frac{1}{n}) < A \land B < B + (\frac{1}{n}))) \to [A, B] \subseteq (A - (\frac{1}{n}), B + (\frac{1}{n}))$
83	41 45 80 81 82	syl22anc	$⊢ (φ \land n \in ℕ) \to [A, B] \subseteq (A - (\frac{1}{n}), B + (\frac{1}{n}))$
84	83	ralrimiva	$⊢ φ \to \forall n \in ℕ [A, B] \subseteq (A - (\frac{1}{n}), B + (\frac{1}{n}))$
85		ssiin	$⊢ [A, B] \subseteq ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) \leftrightarrow \forall n \in ℕ [A, B] \subseteq (A - (\frac{1}{n}), B + (\frac{1}{n}))$
86	84 85	sylibr	$⊢ φ \to [A, B] \subseteq ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n}))$
87	74 86	eqssd	$⊢ φ \to ⋂_{n \in ℕ} (A - (\frac{1}{n}), B + (\frac{1}{n})) = [A, B]$

Metamath Proof Explorer

Theorem iooiinicc

Proof