Step | Hyp | Ref
| Expression |
1 | | eqeq1 2626 |
. . . . . . 7
|
2 | 1 | rexbidv 3052 |
. . . . . 6
|
3 | 2 | elrab 3363 |
. . . . 5
|
4 | | simprr 796 |
. . . . . 6
|
5 | | nfv 1843 |
. . . . . . . 8
|
6 | | nfv 1843 |
. . . . . . . . 9
|
7 | | nfre1 3005 |
. . . . . . . . 9
|
8 | 6, 7 | nfan 1828 |
. . . . . . . 8
|
9 | 5, 8 | nfan 1828 |
. . . . . . 7
|
10 | | nfv 1843 |
. . . . . . 7
|
11 | | simp3 1063 |
. . . . . . . . . 10
|
12 | | iooshift.1 |
. . . . . . . . . . . . . . 15
|
13 | | iooshift.3 |
. . . . . . . . . . . . . . 15
|
14 | 12, 13 | readdcld 10069 |
. . . . . . . . . . . . . 14
|
15 | 14 | rexrd 10089 |
. . . . . . . . . . . . 13
|
16 | 15 | adantr 481 |
. . . . . . . . . . . 12
|
17 | | iooshift.2 |
. . . . . . . . . . . . . . 15
|
18 | 17, 13 | readdcld 10069 |
. . . . . . . . . . . . . 14
|
19 | 18 | rexrd 10089 |
. . . . . . . . . . . . 13
|
20 | 19 | adantr 481 |
. . . . . . . . . . . 12
|
21 | | ioossre 12235 |
. . . . . . . . . . . . . . 15
|
22 | 21 | a1i 11 |
. . . . . . . . . . . . . 14
|
23 | 22 | sselda 3603 |
. . . . . . . . . . . . 13
|
24 | 13 | adantr 481 |
. . . . . . . . . . . . 13
|
25 | 23, 24 | readdcld 10069 |
. . . . . . . . . . . 12
|
26 | 12 | adantr 481 |
. . . . . . . . . . . . 13
|
27 | 26 | rexrd 10089 |
. . . . . . . . . . . . . 14
|
28 | 17 | adantr 481 |
. . . . . . . . . . . . . . 15
|
29 | 28 | rexrd 10089 |
. . . . . . . . . . . . . 14
|
30 | | simpr 477 |
. . . . . . . . . . . . . 14
|
31 | | ioogtlb 39717 |
. . . . . . . . . . . . . 14
|
32 | 27, 29, 30, 31 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
33 | 26, 23, 24, 32 | ltadd1dd 10638 |
. . . . . . . . . . . 12
|
34 | | iooltub 39735 |
. . . . . . . . . . . . . 14
|
35 | 27, 29, 30, 34 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
36 | 23, 28, 24, 35 | ltadd1dd 10638 |
. . . . . . . . . . . 12
|
37 | 16, 20, 25, 33, 36 | eliood 39720 |
. . . . . . . . . . 11
|
38 | 37 | 3adant3 1081 |
. . . . . . . . . 10
|
39 | 11, 38 | eqeltrd 2701 |
. . . . . . . . 9
|
40 | 39 | 3exp 1264 |
. . . . . . . 8
|
41 | 40 | adantr 481 |
. . . . . . 7
|
42 | 9, 10, 41 | rexlimd 3026 |
. . . . . 6
|
43 | 4, 42 | mpd 15 |
. . . . 5
|
44 | 3, 43 | sylan2b 492 |
. . . 4
|
45 | | elioore 12205 |
. . . . . . 7
|
46 | 45 | adantl 482 |
. . . . . 6
|
47 | 46 | recnd 10068 |
. . . . 5
|
48 | 12 | rexrd 10089 |
. . . . . . . 8
|
49 | 48 | adantr 481 |
. . . . . . 7
|
50 | 17 | rexrd 10089 |
. . . . . . . 8
|
51 | 50 | adantr 481 |
. . . . . . 7
|
52 | 13 | adantr 481 |
. . . . . . . 8
|
53 | 46, 52 | resubcld 10458 |
. . . . . . 7
|
54 | 12 | recnd 10068 |
. . . . . . . . . . 11
|
55 | 13 | recnd 10068 |
. . . . . . . . . . 11
|
56 | 54, 55 | pncand 10393 |
. . . . . . . . . 10
|
57 | 56 | eqcomd 2628 |
. . . . . . . . 9
|
58 | 57 | adantr 481 |
. . . . . . . 8
|
59 | 14 | adantr 481 |
. . . . . . . . 9
|
60 | 15 | adantr 481 |
. . . . . . . . . 10
|
61 | 19 | adantr 481 |
. . . . . . . . . 10
|
62 | | simpr 477 |
. . . . . . . . . 10
|
63 | | ioogtlb 39717 |
. . . . . . . . . 10
|
64 | 60, 61, 62, 63 | syl3anc 1326 |
. . . . . . . . 9
|
65 | 59, 46, 52, 64 | ltsub1dd 10639 |
. . . . . . . 8
|
66 | 58, 65 | eqbrtrd 4675 |
. . . . . . 7
|
67 | 18 | adantr 481 |
. . . . . . . . 9
|
68 | | iooltub 39735 |
. . . . . . . . . 10
|
69 | 60, 61, 62, 68 | syl3anc 1326 |
. . . . . . . . 9
|
70 | 46, 67, 52, 69 | ltsub1dd 10639 |
. . . . . . . 8
|
71 | 17 | recnd 10068 |
. . . . . . . . . 10
|
72 | 71, 55 | pncand 10393 |
. . . . . . . . 9
|
73 | 72 | adantr 481 |
. . . . . . . 8
|
74 | 70, 73 | breqtrd 4679 |
. . . . . . 7
|
75 | 49, 51, 53, 66, 74 | eliood 39720 |
. . . . . 6
|
76 | 55 | adantr 481 |
. . . . . . . 8
|
77 | 47, 76 | npcand 10396 |
. . . . . . 7
|
78 | 77 | eqcomd 2628 |
. . . . . 6
|
79 | | oveq1 6657 |
. . . . . . . 8
|
80 | 79 | eqeq2d 2632 |
. . . . . . 7
|
81 | 80 | rspcev 3309 |
. . . . . 6
|
82 | 75, 78, 81 | syl2anc 693 |
. . . . 5
|
83 | 47, 82, 3 | sylanbrc 698 |
. . . 4
|
84 | 44, 83 | impbida 877 |
. . 3
|
85 | 84 | eqrdv 2620 |
. 2
|
86 | 85 | eqcomd 2628 |
1
|