Metamath Proof Explorer


Theorem 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 ( 𝜑𝐴 ∈ ℝ )
iooiinicc.b ( 𝜑𝐵 ∈ ℝ )
Assertion iooiinicc ( 𝜑 𝑛 ∈ ℕ ( ( 𝐴 − ( 1 / 𝑛 ) ) (,) ( 𝐵 + ( 1 / 𝑛 ) ) ) = ( 𝐴 [,] 𝐵 ) )

Proof

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