Step Hyp Ref
Expression 1 ssel 3497 . . . . . . . . 9
2 1 pm4.71rd 635 . . . . . . . 8
3 2 exbidv 1714 . . . . . . 7
4 df-rex 2813 . . . . . . . 8
5 renegcl 9905 . . . . . . . . 9
6 infm3lem 10526 . . . . . . . . 9
7 eleq1 2529 . . . . . . . . 9
8 5 , 6 , 7 rexxfr 4672 . . . . . . . 8
9 4 , 8 bitr3i 251 . . . . . . 7
10 3 , 9 syl6bb 261 . . . . . 6
11 n0 3794 . . . . . 6
12 rabn0 3805 . . . . . 6
13 10 , 11 , 12 3bitr4g 288 . . . . 5
14 ssel 3497 . . . . . . . . . . . 12
15 14 pm4.71rd 635 . . . . . . . . . . 11
16 15 imbi1d 317 . . . . . . . . . 10
17 impexp 446 . . . . . . . . . 10
18 16 , 17 syl6bb 261 . . . . . . . . 9
19 18 albidv 1713 . . . . . . . 8
20 df-ral 2812 . . . . . . . 8
21 renegcl 9905 . . . . . . . . . 10
22 infm3lem 10526 . . . . . . . . . 10
23 eleq1 2529 . . . . . . . . . . 11
24 breq2 4456 . . . . . . . . . . 11
25 23 , 24 imbi12d 320 . . . . . . . . . 10
26 21 , 22 , 25 ralxfr 4670 . . . . . . . . 9
27 df-ral 2812 . . . . . . . . 9
28 26 , 27 bitr3i 251 . . . . . . . 8
29 19 , 20 , 28 3bitr4g 288 . . . . . . 7
30 29 rexbidv 2968 . . . . . 6
31 renegcl 9905 . . . . . . . 8
32 infm3lem 10526 . . . . . . . 8
33 breq1 4455 . . . . . . . . . 10
34 33 imbi2d 316 . . . . . . . . 9
35 34 ralbidv 2896 . . . . . . . 8
36 31 , 32 , 35 rexxfr 4672 . . . . . . 7
37 negeq 9835 . . . . . . . . . . . . . . 15
38 37 eleq1d 2526 . . . . . . . . . . . . . 14
39 38 elrab 3257 . . . . . . . . . . . . 13
40 39 imbi1i 325 . . . . . . . . . . . 12
41 impexp 446 . . . . . . . . . . . 12
42 40 , 41 bitri 249 . . . . . . . . . . 11
43 42 albii 1640 . . . . . . . . . 10
44 df-ral 2812 . . . . . . . . . 10
45 df-ral 2812 . . . . . . . . . 10
46 43 , 44 , 45 3bitr4ri 278 . . . . . . . . 9
47 leneg 10080 . . . . . . . . . . . 12
48 47 ancoms 453 . . . . . . . . . . 11
49 48 imbi2d 316 . . . . . . . . . 10
50 49 ralbidva 2893 . . . . . . . . 9
51 46 , 50 syl5bbr 259 . . . . . . . 8
52 51 rexbiia 2958 . . . . . . 7
53 36 , 52 bitr4i 252 . . . . . 6
54 30 , 53 syl6bb 261 . . . . 5
55 13 , 54 anbi12d 710 . . . 4
56 ssrab2 3584 . . . . 5
57 sup3 10525 . . . . 5
58 56 , 57 mp3an1 1311 . . . 4
59 55 , 58 syl6bi 228 . . 3
60 15 imbi1d 317 . . . . . . . . 9
61 impexp 446 . . . . . . . . 9
62 60 , 61 syl6bb 261 . . . . . . . 8
63 62 albidv 1713 . . . . . . 7
64 df-ral 2812 . . . . . . 7
65 breq1 4455 . . . . . . . . . . 11
66 65 notbid 294 . . . . . . . . . 10
67 23 , 66 imbi12d 320 . . . . . . . . 9
68 21 , 22 , 67 ralxfr 4670 . . . . . . . 8
69 df-ral 2812 . . . . . . . 8
70 68 , 69 bitr3i 251 . . . . . . 7
71 63 , 64 , 70 3bitr4g 288 . . . . . 6
72 breq2 4456 . . . . . . . . 9
73 breq2 4456 . . . . . . . . . 10
74 73 rexbidv 2968 . . . . . . . . 9
75 72 , 74 imbi12d 320 . . . . . . . 8
76 21 , 22 , 75 ralxfr 4670 . . . . . . 7
77 ssel 3497 . . . . . . . . . . . . 13
78 77 adantrd 468 . . . . . . . . . . . 12
79 78 pm4.71rd 635 . . . . . . . . . . 11
80 79 exbidv 1714 . . . . . . . . . 10
81 df-rex 2813 . . . . . . . . . 10
82 renegcl 9905 . . . . . . . . . . . 12
83 infm3lem 10526 . . . . . . . . . . . 12
84 eleq1 2529 . . . . . . . . . . . . 13
85 breq1 4455 . . . . . . . . . . . . 13
86 84 , 85 anbi12d 710 . . . . . . . . . . . 12
87 82 , 83 , 86 rexxfr 4672 . . . . . . . . . . 11
88 df-rex 2813 . . . . . . . . . . 11
89 87 , 88 bitr3i 251 . . . . . . . . . 10
90 80 , 81 , 89 3bitr4g 288 . . . . . . . . 9
91 90 imbi2d 316 . . . . . . . 8
92 91 ralbidv 2896 . . . . . . 7
93 76 , 92 syl5bb 257 . . . . . 6
94 71 , 93 anbi12d 710 . . . . 5
95 94 rexbidv 2968 . . . 4
96 breq2 4456 . . . . . . . . . 10
97 96 notbid 294 . . . . . . . . 9
98 97 imbi2d 316 . . . . . . . 8
99 98 ralbidv 2896 . . . . . . 7
100 breq1 4455 . . . . . . . . 9
101 100 imbi1d 317 . . . . . . . 8
102 101 ralbidv 2896 . . . . . . 7
103 99 , 102 anbi12d 710 . . . . . 6
104 31 , 32 , 103 rexxfr 4672 . . . . 5
105 39 imbi1i 325 . . . . . . . . . . 11
106 impexp 446 . . . . . . . . . . 11
107 105 , 106 bitri 249 . . . . . . . . . 10
108 107 albii 1640 . . . . . . . . 9
109 df-ral 2812 . . . . . . . . 9
110 df-ral 2812 . . . . . . . . 9
111 108 , 109 ,
110 3bitr4ri 278 . . . . . . . 8
112 ltneg 10077 . . . . . . . . . . 11
113 112 notbid 294 . . . . . . . . . 10
114 113 imbi2d 316 . . . . . . . . 9
115 114 ralbidva 2893 . . . . . . . 8
116 111 , 115 syl5bbr 259 . . . . . . 7
117 ltneg 10077 . . . . . . . . . 10
118 117 ancoms 453 . . . . . . . . 9
119 negeq 9835 . . . . . . . . . . . . 13
120 119 eleq1d 2526 . . . . . . . . . . . 12
121 120 rexrab 3263 . . . . . . . . . . 11
122 ltneg 10077 . . . . . . . . . . . . 13
123 122 anbi2d 703 . . . . . . . . . . . 12
124 123 rexbidva 2965 . . . . . . . . . . 11
125 121 , 124 syl5bb 257 . . . . . . . . . 10
126 125 adantl 466 . . . . . . . . 9
127 118 , 126 imbi12d 320 . . . . . . . 8
128 127 ralbidva 2893 . . . . . . 7
129 116 , 128 anbi12d 710 . . . . . 6
130 129 rexbiia 2958 . . . . 5
131 104 , 130 bitr4i 252 . . . 4
132 95 , 131 syl6bb 261 . . 3
133 59 , 132 sylibrd 234 . 2
134 133 3impib 1194 1
