Metamath Proof Explorer


Theorem iooshift

Description: An open interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses iooshift.1 φ A
iooshift.2 φ B
iooshift.3 φ T
Assertion iooshift φ A + T B + T = w | z A B w = z + T

Proof

Step Hyp Ref Expression
1 iooshift.1 φ A
2 iooshift.2 φ B
3 iooshift.3 φ T
4 eqeq1 w = x w = z + T x = z + T
5 4 rexbidv w = x z A B w = z + T z A B x = z + T
6 5 elrab x w | z A B w = z + T x z A B x = z + T
7 simprr φ x z A B x = z + T z A B x = z + T
8 nfv z φ
9 nfv z x
10 nfre1 z z A B x = z + T
11 9 10 nfan z x z A B x = z + T
12 8 11 nfan z φ x z A B x = z + T
13 nfv z x A + T B + T
14 simp3 φ z A B x = z + T x = z + T
15 1 3 readdcld φ A + T
16 15 rexrd φ A + T *
17 16 adantr φ z A B A + T *
18 2 3 readdcld φ B + T
19 18 rexrd φ B + T *
20 19 adantr φ z A B B + T *
21 ioossre A B
22 21 a1i φ A B
23 22 sselda φ z A B z
24 3 adantr φ z A B T
25 23 24 readdcld φ z A B z + T
26 1 adantr φ z A B A
27 26 rexrd φ z A B A *
28 2 adantr φ z A B B
29 28 rexrd φ z A B B *
30 simpr φ z A B z A B
31 ioogtlb A * B * z A B A < z
32 27 29 30 31 syl3anc φ z A B A < z
33 26 23 24 32 ltadd1dd φ z A B A + T < z + T
34 iooltub A * B * z A B z < B
35 27 29 30 34 syl3anc φ z A B z < B
36 23 28 24 35 ltadd1dd φ z A B z + T < B + T
37 17 20 25 33 36 eliood φ z A B z + T A + T B + T
38 37 3adant3 φ z A B x = z + T z + T A + T B + T
39 14 38 eqeltrd φ z A B x = z + T x A + T B + T
40 39 3exp φ z A B x = z + T x A + T B + T
41 40 adantr φ x z A B x = z + T z A B x = z + T x A + T B + T
42 12 13 41 rexlimd φ x z A B x = z + T z A B x = z + T x A + T B + T
43 7 42 mpd φ x z A B x = z + T x A + T B + T
44 6 43 sylan2b φ x w | z A B w = z + T x A + T B + T
45 elioore x A + T B + T x
46 45 adantl φ x A + T B + T x
47 46 recnd φ x A + T B + T x
48 1 rexrd φ A *
49 48 adantr φ x A + T B + T A *
50 2 rexrd φ B *
51 50 adantr φ x A + T B + T B *
52 3 adantr φ x A + T B + T T
53 46 52 resubcld φ x A + T B + T x T
54 1 recnd φ A
55 3 recnd φ T
56 54 55 pncand φ A + T - T = A
57 56 eqcomd φ A = A + T - T
58 57 adantr φ x A + T B + T A = A + T - T
59 15 adantr φ x A + T B + T A + T
60 16 adantr φ x A + T B + T A + T *
61 19 adantr φ x A + T B + T B + T *
62 simpr φ x A + T B + T x A + T B + T
63 ioogtlb A + T * B + T * x A + T B + T A + T < x
64 60 61 62 63 syl3anc φ x A + T B + T A + T < x
65 59 46 52 64 ltsub1dd φ x A + T B + T A + T - T < x T
66 58 65 eqbrtrd φ x A + T B + T A < x T
67 18 adantr φ x A + T B + T B + T
68 iooltub A + T * B + T * x A + T B + T x < B + T
69 60 61 62 68 syl3anc φ x A + T B + T x < B + T
70 46 67 52 69 ltsub1dd φ x A + T B + T x T < B + T - T
71 2 recnd φ B
72 71 55 pncand φ B + T - T = B
73 72 adantr φ x A + T B + T B + T - T = B
74 70 73 breqtrd φ x A + T B + T x T < B
75 49 51 53 66 74 eliood φ x A + T B + T x T A B
76 55 adantr φ x A + T B + T T
77 47 76 npcand φ x A + T B + T x - T + T = x
78 77 eqcomd φ x A + T B + T x = x - T + T
79 oveq1 z = x T z + T = x - T + T
80 79 rspceeqv x T A B x = x - T + T z A B x = z + T
81 75 78 80 syl2anc φ x A + T B + T z A B x = z + T
82 47 81 6 sylanbrc φ x A + T B + T x w | z A B w = z + T
83 44 82 impbida φ x w | z A B w = z + T x A + T B + T
84 83 eqrdv φ w | z A B w = z + T = A + T B + T
85 84 eqcomd φ A + T B + T = w | z A B w = z + T