Step | Hyp | Ref
| Expression |
1 | | elqsi 6577 |
. . . . . . . 8
|
2 | | eropr.1 |
. . . . . . . 8
|
3 | 1, 2 | eleq2s 2270 |
. . . . . . 7
|
4 | | elqsi 6577 |
. . . . . . . 8
|
5 | | eropr.2 |
. . . . . . . 8
|
6 | 4, 5 | eleq2s 2270 |
. . . . . . 7
|
7 | 3, 6 | anim12i 338 |
. . . . . 6
|
8 | 7 | adantl 277 |
. . . . 5
|
9 | | reeanv 2644 |
. . . . 5
|
10 | 8, 9 | sylibr 134 |
. . . 4
|
11 | | eropr.3 |
. . . . . . . 8
|
12 | 11 | adantr 276 |
. . . . . . 7
|
13 | | ecexg 6529 |
. . . . . . 7
|
14 | | elisset 2749 |
. . . . . . 7
|
15 | 12, 13, 14 | 3syl 17 |
. . . . . 6
|
16 | 15 | biantrud 304 |
. . . . 5
|
17 | 16 | 2rexbidv 2500 |
. . . 4
|
18 | 10, 17 | mpbid 147 |
. . 3
|
19 | | 19.42v 1904 |
. . . . . . . 8
|
20 | 19 | bicomi 132 |
. . . . . . 7
|
21 | 20 | rexbii 2482 |
. . . . . 6
|
22 | | rexcom4 2758 |
. . . . . 6
|
23 | 21, 22 | bitri 184 |
. . . . 5
|
24 | 23 | rexbii 2482 |
. . . 4
|
25 | | rexcom4 2758 |
. . . 4
|
26 | 24, 25 | bitri 184 |
. . 3
|
27 | 18, 26 | sylib 122 |
. 2
|
28 | | reeanv 2644 |
. . . . . 6
|
29 | | eceq1 6560 |
. . . . . . . . . . 11
|
30 | 29 | eqeq2d 2187 |
. . . . . . . . . 10
|
31 | 30 | anbi1d 465 |
. . . . . . . . 9
|
32 | | oveq1 5872 |
. . . . . . . . . . 11
|
33 | 32 | eceq1d 6561 |
. . . . . . . . . 10
|
34 | 33 | eqeq2d 2187 |
. . . . . . . . 9
|
35 | 31, 34 | anbi12d 473 |
. . . . . . . 8
|
36 | | eceq1 6560 |
. . . . . . . . . . 11
|
37 | 36 | eqeq2d 2187 |
. . . . . . . . . 10
|
38 | 37 | anbi2d 464 |
. . . . . . . . 9
|
39 | | oveq2 5873 |
. . . . . . . . . . 11
|
40 | 39 | eceq1d 6561 |
. . . . . . . . . 10
|
41 | 40 | eqeq2d 2187 |
. . . . . . . . 9
|
42 | 38, 41 | anbi12d 473 |
. . . . . . . 8
|
43 | 35, 42 | cbvrex2v 2715 |
. . . . . . 7
|
44 | | eceq1 6560 |
. . . . . . . . . . 11
|
45 | 44 | eqeq2d 2187 |
. . . . . . . . . 10
|
46 | 45 | anbi1d 465 |
. . . . . . . . 9
|
47 | | oveq1 5872 |
. . . . . . . . . . 11
|
48 | 47 | eceq1d 6561 |
. . . . . . . . . 10
|
49 | 48 | eqeq2d 2187 |
. . . . . . . . 9
|
50 | 46, 49 | anbi12d 473 |
. . . . . . . 8
|
51 | | eceq1 6560 |
. . . . . . . . . . 11
|
52 | 51 | eqeq2d 2187 |
. . . . . . . . . 10
|
53 | 52 | anbi2d 464 |
. . . . . . . . 9
|
54 | | oveq2 5873 |
. . . . . . . . . . 11
|
55 | 54 | eceq1d 6561 |
. . . . . . . . . 10
|
56 | 55 | eqeq2d 2187 |
. . . . . . . . 9
|
57 | 53, 56 | anbi12d 473 |
. . . . . . . 8
|
58 | 50, 57 | cbvrex2v 2715 |
. . . . . . 7
|
59 | 43, 58 | anbi12i 460 |
. . . . . 6
|
60 | 28, 59 | bitr4i 187 |
. . . . 5
|
61 | | reeanv 2644 |
. . . . . . 7
|
62 | | eropr.11 |
. . . . . . . . . . . . . 14
|
63 | | eropr.4 |
. . . . . . . . . . . . . . . . 17
|
64 | 63 | adantr 276 |
. . . . . . . . . . . . . . . 16
|
65 | | eropr.7 |
. . . . . . . . . . . . . . . . . 18
|
66 | 65 | adantr 276 |
. . . . . . . . . . . . . . . . 17
|
67 | | simprll 537 |
. . . . . . . . . . . . . . . . 17
|
68 | 66, 67 | sseldd 3154 |
. . . . . . . . . . . . . . . 16
|
69 | 64, 68 | erth 6569 |
. . . . . . . . . . . . . . 15
|
70 | | eropr.5 |
. . . . . . . . . . . . . . . . 17
|
71 | 70 | adantr 276 |
. . . . . . . . . . . . . . . 16
|
72 | | eropr.8 |
. . . . . . . . . . . . . . . . . 18
|
73 | 72 | adantr 276 |
. . . . . . . . . . . . . . . . 17
|
74 | | simprrl 539 |
. . . . . . . . . . . . . . . . 17
|
75 | 73, 74 | sseldd 3154 |
. . . . . . . . . . . . . . . 16
|
76 | 71, 75 | erth 6569 |
. . . . . . . . . . . . . . 15
|
77 | 69, 76 | anbi12d 473 |
. . . . . . . . . . . . . 14
|
78 | | eropr.6 |
. . . . . . . . . . . . . . . 16
|
79 | 78 | adantr 276 |
. . . . . . . . . . . . . . 15
|
80 | | eropr.9 |
. . . . . . . . . . . . . . . . 17
|
81 | 80 | adantr 276 |
. . . . . . . . . . . . . . . 16
|
82 | | eropr.10 |
. . . . . . . . . . . . . . . . . 18
|
83 | 82 | adantr 276 |
. . . . . . . . . . . . . . . . 17
|
84 | 83, 67, 74 | fovrnd 6009 |
. . . . . . . . . . . . . . . 16
|
85 | 81, 84 | sseldd 3154 |
. . . . . . . . . . . . . . 15
|
86 | 79, 85 | erth 6569 |
. . . . . . . . . . . . . 14
|
87 | 62, 77, 86 | 3imtr3d 202 |
. . . . . . . . . . . . 13
|
88 | | eqeq2 2185 |
. . . . . . . . . . . . . 14
|
89 | 88 | biimprcd 160 |
. . . . . . . . . . . . 13
|
90 | 87, 89 | syl6 33 |
. . . . . . . . . . . 12
|
91 | 90 | impd 254 |
. . . . . . . . . . 11
|
92 | | eqeq1 2182 |
. . . . . . . . . . . . . . 15
|
93 | | eqeq1 2182 |
. . . . . . . . . . . . . . 15
|
94 | 92, 93 | bi2anan9 606 |
. . . . . . . . . . . . . 14
|
95 | 94 | anbi1d 465 |
. . . . . . . . . . . . 13
|
96 | 95 | adantr 276 |
. . . . . . . . . . . 12
|
97 | | eqeq1 2182 |
. . . . . . . . . . . . 13
|
98 | 97 | adantl 277 |
. . . . . . . . . . . 12
|
99 | 96, 98 | imbi12d 234 |
. . . . . . . . . . 11
|
100 | 91, 99 | syl5ibrcom 157 |
. . . . . . . . . 10
|
101 | 100 | impd 254 |
. . . . . . . . 9
|
102 | 101 | anassrs 400 |
. . . . . . . 8
|
103 | 102 | rexlimdvva 2600 |
. . . . . . 7
|
104 | 61, 103 | syl5bir 153 |
. . . . . 6
|
105 | 104 | rexlimdvva 2600 |
. . . . 5
|
106 | 60, 105 | syl5bir 153 |
. . . 4
|
107 | 106 | adantr 276 |
. . 3
|
108 | 107 | alrimivv 1873 |
. 2
|
109 | | eqeq1 2182 |
. . . . 5
|
110 | 109 | anbi2d 464 |
. . . 4
|
111 | 110 | 2rexbidv 2500 |
. . 3
|
112 | 111 | eu4 2086 |
. 2
|
113 | 27, 108, 112 | sylanbrc 417 |
1
|