Step | Hyp | Ref
| Expression |
1 | | sge0fodjrnlem.k |
. . . 4
|
2 | | sge0fodjrnlem.c |
. . . . 5
|
3 | | sge0fodjrnlem.f |
. . . . 5
|
4 | | fornex 7135 |
. . . . 5
|
5 | 2, 3, 4 | sylc 65 |
. . . 4
|
6 | | difssd 3738 |
. . . 4
|
7 | | simpl 473 |
. . . . 5
|
8 | 6 | sselda 3603 |
. . . . 5
|
9 | | sge0fodjrnlem.b |
. . . . 5
|
10 | 7, 8, 9 | syl2anc 693 |
. . . 4
|
11 | | simpl 473 |
. . . . 5
|
12 | | dfin4 3867 |
. . . . . . . . . 10
|
13 | 12 | eqcomi 2631 |
. . . . . . . . 9
|
14 | | inss2 3834 |
. . . . . . . . 9
|
15 | 13, 14 | eqsstri 3635 |
. . . . . . . 8
|
16 | | id 22 |
. . . . . . . 8
|
17 | 15, 16 | sseldi 3601 |
. . . . . . 7
|
18 | | elsni 4194 |
. . . . . . 7
|
19 | 17, 18 | syl 17 |
. . . . . 6
|
20 | 19 | adantl 482 |
. . . . 5
|
21 | | sge0fodjrnlem.b0 |
. . . . 5
|
22 | 11, 20, 21 | syl2anc 693 |
. . . 4
|
23 | 1, 5, 6, 10, 22 | sge0ss 40629 |
. . 3
Σ^ Σ^ |
24 | 23 | eqcomd 2628 |
. 2
Σ^ Σ^ |
25 | | sge0fodjrnlem.n |
. . 3
|
26 | | sge0fodjrnlem.bd |
. . 3
|
27 | | difexg 4808 |
. . . 4
|
28 | 2, 27 | syl 17 |
. . 3
|
29 | | eqid 2622 |
. . . . 5
|
30 | | fof 6115 |
. . . . . . 7
|
31 | 3, 30 | syl 17 |
. . . . . 6
|
32 | 31 | ffvelrnda 6359 |
. . . . 5
|
33 | | sge0fodjrnlem.dj |
. . . . 5
Disj
|
34 | | fveq2 6191 |
. . . . . . 7
|
35 | 34 | neeq1d 2853 |
. . . . . 6
|
36 | 35 | cbvrabv 3199 |
. . . . 5
|
37 | 34 | cbvmptv 4750 |
. . . . . . 7
|
38 | 37 | rneqi 5352 |
. . . . . 6
|
39 | 38 | difeq1i 3724 |
. . . . 5
|
40 | 25, 29, 32, 33, 36, 39 | disjf1o 39378 |
. . . 4
|
41 | 31 | feqmptd 6249 |
. . . . . 6
|
42 | | difssd 3738 |
. . . . . . . . . . . . 13
|
43 | 42 | sselda 3603 |
. . . . . . . . . . . 12
|
44 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . 19
|
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
46 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
|
47 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . 21
|
48 | 47 | elsn 4192 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | 46, 48 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
|
50 | 49 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
51 | 45, 50 | jca 554 |
. . . . . . . . . . . . . . . . 17
|
52 | 51 | adantll 750 |
. . . . . . . . . . . . . . . 16
|
53 | 31 | ffnd 6046 |
. . . . . . . . . . . . . . . . . 18
|
54 | | elpreima 6337 |
. . . . . . . . . . . . . . . . . 18
|
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
56 | 55 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
57 | 52, 56 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
58 | | sge0fodjrnlem.z |
. . . . . . . . . . . . . . 15
|
59 | 57, 58 | syl6eleqr 2712 |
. . . . . . . . . . . . . 14
|
60 | | eldifn 3733 |
. . . . . . . . . . . . . . 15
|
61 | 60 | ad2antlr 763 |
. . . . . . . . . . . . . 14
|
62 | 59, 61 | pm2.65da 600 |
. . . . . . . . . . . . 13
|
63 | 62 | neqned 2801 |
. . . . . . . . . . . 12
|
64 | 43, 63 | jca 554 |
. . . . . . . . . . 11
|
65 | 35 | elrab 3363 |
. . . . . . . . . . 11
|
66 | 64, 65 | sylibr 224 |
. . . . . . . . . 10
|
67 | 66 | ex 450 |
. . . . . . . . 9
|
68 | 65 | simplbi 476 |
. . . . . . . . . . . . . . 15
|
69 | 68 | adantl 482 |
. . . . . . . . . . . . . 14
|
70 | 58 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . 21
|
71 | 70 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 71 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
73 | 55 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
74 | 72, 73 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
|
75 | 74 | simprd 479 |
. . . . . . . . . . . . . . . . 17
|
76 | | elsni 4194 |
. . . . . . . . . . . . . . . . 17
|
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
|
78 | 77 | adantlr 751 |
. . . . . . . . . . . . . . 15
|
79 | 65 | simprbi 480 |
. . . . . . . . . . . . . . . . 17
|
80 | 79 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
|
81 | 80 | neneqd 2799 |
. . . . . . . . . . . . . . 15
|
82 | 78, 81 | pm2.65da 600 |
. . . . . . . . . . . . . 14
|
83 | 69, 82 | eldifd 3585 |
. . . . . . . . . . . . 13
|
84 | 83 | ex 450 |
. . . . . . . . . . . 12
|
85 | 25, 84 | ralrimi 2957 |
. . . . . . . . . . 11
|
86 | | dfss3 3592 |
. . . . . . . . . . 11
|
87 | 85, 86 | sylibr 224 |
. . . . . . . . . 10
|
88 | 87 | sseld 3602 |
. . . . . . . . 9
|
89 | 67, 88 | impbid 202 |
. . . . . . . 8
|
90 | 25, 89 | alrimi 2082 |
. . . . . . 7
|
91 | | dfcleq 2616 |
. . . . . . 7
|
92 | 90, 91 | sylibr 224 |
. . . . . 6
|
93 | 41, 92 | reseq12d 5397 |
. . . . 5
|
94 | 41, 37 | syl6eqr 2674 |
. . . . . . . . 9
|
95 | 94 | eqcomd 2628 |
. . . . . . . 8
|
96 | 95 | rneqd 5353 |
. . . . . . 7
|
97 | | forn 6118 |
. . . . . . . 8
|
98 | 3, 97 | syl 17 |
. . . . . . 7
|
99 | 96, 98 | eqtr2d 2657 |
. . . . . 6
|
100 | 99 | difeq1d 3727 |
. . . . 5
|
101 | 93, 92, 100 | f1oeq123d 6133 |
. . . 4
|
102 | 40, 101 | mpbird 247 |
. . 3
|
103 | | fvres 6207 |
. . . . 5
|
104 | 103 | adantl 482 |
. . . 4
|
105 | | simpl 473 |
. . . . 5
|
106 | | sge0fodjrnlem.fng |
. . . . 5
|
107 | 105, 43, 106 | syl2anc 693 |
. . . 4
|
108 | 104, 107 | eqtrd 2656 |
. . 3
|
109 | 1, 25, 26, 28, 102, 108, 10 | sge0f1o 40599 |
. 2
Σ^ Σ^ |
110 | 106 | eqcomd 2628 |
. . . . . 6
|
111 | 110, 32 | eqeltrd 2701 |
. . . . 5
|
112 | 105, 43, 111 | syl2anc 693 |
. . . 4
|
113 | 112 | ex 450 |
. . . . 5
|
114 | 113 | imdistani 726 |
. . . 4
|
115 | | nfcv 2764 |
. . . . 5
|
116 | | nfv 1843 |
. . . . . . 7
|
117 | 1, 116 | nfan 1828 |
. . . . . 6
|
118 | | nfv 1843 |
. . . . . 6
|
119 | 117, 118 | nfim 1825 |
. . . . 5
|
120 | | eleq1 2689 |
. . . . . . 7
|
121 | 120 | anbi2d 740 |
. . . . . 6
|
122 | 26 | eleq1d 2686 |
. . . . . 6
|
123 | 121, 122 | imbi12d 334 |
. . . . 5
|
124 | 115, 119,
123, 9 | vtoclgf 3264 |
. . . 4
|
125 | 112, 114,
124 | sylc 65 |
. . 3
|
126 | | simpl 473 |
. . . . 5
|
127 | | eldifi 3732 |
. . . . . 6
|
128 | 127 | adantl 482 |
. . . . 5
|
129 | 126, 128,
111 | syl2anc 693 |
. . . 4
|
130 | | dfin4 3867 |
. . . . . . . . 9
|
131 | | difss 3737 |
. . . . . . . . 9
|
132 | 130, 131 | eqsstri 3635 |
. . . . . . . 8
|
133 | | inss2 3834 |
. . . . . . . . . 10
|
134 | | id 22 |
. . . . . . . . . . 11
|
135 | | dfin4 3867 |
. . . . . . . . . . . 12
|
136 | 135 | eqcomi 2631 |
. . . . . . . . . . 11
|
137 | 134, 136 | syl6eleq 2711 |
. . . . . . . . . 10
|
138 | 133, 137 | sseldi 3601 |
. . . . . . . . 9
|
139 | 138, 127 | elind 3798 |
. . . . . . . 8
|
140 | 132, 139 | sseldi 3601 |
. . . . . . 7
|
141 | 140 | adantl 482 |
. . . . . 6
|
142 | 77 | eqcomd 2628 |
. . . . . . 7
|
143 | | simpl 473 |
. . . . . . . 8
|
144 | 74 | simpld 475 |
. . . . . . . 8
|
145 | 143, 144,
106 | syl2anc 693 |
. . . . . . 7
|
146 | 142, 145 | eqtr2d 2657 |
. . . . . 6
|
147 | 126, 141,
146 | syl2anc 693 |
. . . . 5
|
148 | 126, 147 | jca 554 |
. . . 4
|
149 | | nfv 1843 |
. . . . . . 7
|
150 | 1, 149 | nfan 1828 |
. . . . . 6
|
151 | | nfv 1843 |
. . . . . 6
|
152 | 150, 151 | nfim 1825 |
. . . . 5
|
153 | | eqeq1 2626 |
. . . . . . 7
|
154 | 153 | anbi2d 740 |
. . . . . 6
|
155 | 26 | eqeq1d 2624 |
. . . . . 6
|
156 | 154, 155 | imbi12d 334 |
. . . . 5
|
157 | 115, 152,
156, 21 | vtoclgf 3264 |
. . . 4
|
158 | 129, 148,
157 | sylc 65 |
. . 3
|
159 | 25, 2, 42, 125, 158 | sge0ss 40629 |
. 2
Σ^ Σ^ |
160 | 24, 109, 159 | 3eqtrd 2660 |
1
Σ^ Σ^ |