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 / 𝑛 ) ) ) = ( 𝐴 [,] 𝐵 ) )