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

Proof

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