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 1 n B + 1 n = A B

Proof

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