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 ⊢φ→A∈ℝ*
iooiinioc.2 ⊢φ→B∈ℝ
Assertion iooiinioc ⊢φ→⋂n∈ℕAB+1n=AB

Proof

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