Metamath Proof Explorer

Theorem iooiinioc

Description: A left-open, right-closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses iooiinioc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
iooiinioc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion iooiinioc ( 𝜑 → ∩ 𝑛 ∈ ℕ ( 𝐴 (,) ( 𝐵 + ( 1 / 𝑛 ) ) ) = ( 𝐴 (,] 𝐵 ) )

Proof

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