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 ⊢φ→A∈ℝ
iooiinicc.b ⊢φ→B∈ℝ
Assertion iooiinicc ⊢φ→⋂n∈ℕA−1nB+1n=AB

Proof

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