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 
|- ( ph -> A e. RR* )
iooiinioc.2 
|- ( ph -> B e. RR )
Assertion iooiinioc 
|- ( ph -> |^|_ n e. NN ( A (,) ( B + ( 1 / n ) ) ) = ( A (,] B ) )

Proof

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