Step | Hyp | Ref
| Expression |
1 | | sge0fodjrnlem.k |
. . . 4
   |
2 | | sge0fodjrnlem.c |
. . . . 5
   |
3 | | sge0fodjrnlem.f |
. . . . 5
       |
4 | | fornex 6781 |
. . . . 5
     
   |
5 | 2, 3, 4 | sylc 61 |
. . . 4
   |
6 | | difssd 3550 |
. . . 4
       |
7 | | simpl 464 |
. . . . 5
 

      |
8 | 6 | sselda 3418 |
. . . . 5
 

      |
9 | | sge0fodjrnlem.b |
. . . . 5
 
      |
10 | 7, 8, 9 | syl2anc 673 |
. . . 4
 

         |
11 | | simpl 464 |
. . . . 5
 

        |
12 | | dfin4 3674 |
. . . . . . . . . 10
           |
13 | 12 | eqcomi 2480 |
. . . . . . . . 9
           |
14 | | inss2 3644 |
. . . . . . . . 9
       |
15 | 13, 14 | eqsstri 3448 |
. . . . . . . 8
         |
16 | | id 22 |
. . . . . . . 8
               |
17 | 15, 16 | sseldi 3416 |
. . . . . . 7
           |
18 | | elsni 3985 |
. . . . . . 7
     |
19 | 17, 18 | syl 17 |
. . . . . 6
         |
20 | 19 | adantl 473 |
. . . . 5
 

        |
21 | | sge0fodjrnlem.b0 |
. . . . 5
 

  |
22 | 11, 20, 21 | syl2anc 673 |
. . . 4
 

        |
23 | 1, 5, 6, 10, 22 | sge0ss 38368 |
. . 3
 Σ^        Σ^      |
24 | 23 | eqcomd 2477 |
. 2
 Σ^    Σ^          |
25 | | sge0fodjrnlem.n |
. . 3
   |
26 | | sge0fodjrnlem.bd |
. . 3
   |
27 | | difexg 4545 |
. . . 4
     |
28 | 2, 27 | syl 17 |
. . 3
     |
29 | | eqid 2471 |
. . . . 5
             |
30 | | fof 5806 |
. . . . . . 7
           |
31 | 3, 30 | syl 17 |
. . . . . 6
       |
32 | 31 | ffvelrnda 6037 |
. . . . 5
 
       |
33 | | sge0fodjrnlem.dj |
. . . . 5
 Disj
      |
34 | | fveq2 5879 |
. . . . . . 7
           |
35 | 34 | neeq1d 2702 |
. . . . . 6
     
       |
36 | 35 | cbvrabv 3030 |
. . . . 5

            |
37 | 34 | cbvmptv 4488 |
. . . . . . 7
             |
38 | 37 | rneqi 5067 |
. . . . . 6
             |
39 | 38 | difeq1i 3536 |
. . . . 5
                     |
40 | 25, 29, 32, 33, 36, 39 | disjf1o 37537 |
. . . 4
        
                            |
41 | 31 | feqmptd 5932 |
. . . . . 6
         |
42 | | difssd 3550 |
. . . . . . . . . . . . 13
  
  |
43 | 42 | sselda 3418 |
. . . . . . . . . . . 12
 

 
  |
44 | | eldifi 3544 |
. . . . . . . . . . . . . . . . . . 19
     |
45 | 44 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
           |
46 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
    
      |
47 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . 21
     |
48 | | elsncg 3983 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
49 | 47, 48 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
      
      |
50 | 46, 49 | sylibr 217 |
. . . . . . . . . . . . . . . . . . 19
    
        |
51 | 50 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
                 |
52 | 45, 51 | jca 541 |
. . . . . . . . . . . . . . . . 17
                   |
53 | 52 | adantll 728 |
. . . . . . . . . . . . . . . 16
                     |
54 | 31 | ffnd 5740 |
. . . . . . . . . . . . . . . . . 18
   |
55 | | elpreima 6017 |
. . . . . . . . . . . . . . . . . 18
                    |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . 17
                    |
57 | 56 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
                              |
58 | 53, 57 | mpbird 240 |
. . . . . . . . . . . . . . 15
                    |
59 | | sge0fodjrnlem.z |
. . . . . . . . . . . . . . 15
        |
60 | 58, 59 | syl6eleqr 2560 |
. . . . . . . . . . . . . 14
             |
61 | | eldifn 3545 |
. . . . . . . . . . . . . . 15
  
  |
62 | 61 | ad2antlr 741 |
. . . . . . . . . . . . . 14
          
  |
63 | 60, 62 | pm2.65da 586 |
. . . . . . . . . . . . 13
 

 
      |
64 | 63 | neqned 2650 |
. . . . . . . . . . . 12
 

 
      |
65 | 43, 64 | jca 541 |
. . . . . . . . . . 11
 

 

       |
66 | 35 | elrab 3184 |
. . . . . . . . . . 11
               |
67 | 65, 66 | sylibr 217 |
. . . . . . . . . 10
 

 
        |
68 | 67 | ex 441 |
. . . . . . . . 9
             |
69 | 66 | simplbi 467 |
. . . . . . . . . . . . . . 15
      
  |
70 | 69 | adantl 473 |
. . . . . . . . . . . . . 14
 
         |
71 | 59 | eleq2i 2541 |
. . . . . . . . . . . . . . . . . . . . 21

         |
72 | 71 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . 20
          |
73 | 72 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
 
          |
74 | 56 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 
                    |
75 | 73, 74 | mpbid 215 |
. . . . . . . . . . . . . . . . . 18
 
           |
76 | 75 | simprd 470 |
. . . . . . . . . . . . . . . . 17
 
         |
77 | | elsni 3985 |
. . . . . . . . . . . . . . . . 17
             |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . 16
 
       |
79 | 78 | adantlr 729 |
. . . . . . . . . . . . . . 15
          
      |
80 | 66 | simprbi 471 |
. . . . . . . . . . . . . . . . 17
      
      |
81 | 80 | ad2antlr 741 |
. . . . . . . . . . . . . . . 16
          
      |
82 | 81 | neneqd 2648 |
. . . . . . . . . . . . . . 15
          
      |
83 | 79, 82 | pm2.65da 586 |
. . . . . . . . . . . . . 14
 
      
  |
84 | 70, 83 | eldifd 3401 |
. . . . . . . . . . . . 13
 
           |
85 | 84 | ex 441 |
. . . . . . . . . . . 12
             |
86 | 25, 85 | ralrimi 2800 |
. . . . . . . . . . 11
             |
87 | | dfss3 3408 |
. . . . . . . . . . 11
       
 

          |
88 | 86, 87 | sylibr 217 |
. . . . . . . . . 10
       
   |
89 | 88 | sseld 3417 |
. . . . . . . . 9
             |
90 | 68, 89 | impbid 195 |
. . . . . . . 8
    
        |
91 | 25, 90 | alrimi 1975 |
. . . . . . 7
     
         |
92 | | dfcleq 2465 |
. . . . . . 7
             
         |
93 | 91, 92 | sylibr 217 |
. . . . . 6
   
       |
94 | 41, 93 | reseq12d 5112 |
. . . . 5
                     |
95 | 41, 37 | syl6eqr 2523 |
. . . . . . . . 9
         |
96 | 95 | eqcomd 2477 |
. . . . . . . 8
         |
97 | 96 | rneqd 5068 |
. . . . . . 7
         |
98 | | forn 5809 |
. . . . . . . 8
       |
99 | 3, 98 | syl 17 |
. . . . . . 7
   |
100 | 97, 99 | eqtr2d 2506 |
. . . . . 6
         |
101 | 100 | difeq1d 3539 |
. . . . 5
                 |
102 | 94, 93, 101 | f1oeq123d 5824 |
. . . 4
   
                   
                             |
103 | 40, 102 | mpbird 240 |
. . 3
                 |
104 | | fvres 5893 |
. . . . 5
                 |
105 | 104 | adantl 473 |
. . . 4
 

 
              |
106 | | simpl 464 |
. . . . 5
 

 
  |
107 | | sge0fodjrnlem.fng |
. . . . 5
 
       |
108 | 106, 43, 107 | syl2anc 673 |
. . . 4
 

 
      |
109 | 105, 108 | eqtrd 2505 |
. . 3
 

 
          |
110 | 1, 25, 26, 28, 103, 109, 10 | sge0f1o 38338 |
. 2
 Σ^        Σ^        |
111 | 107 | eqcomd 2477 |
. . . . . 6
 
       |
112 | 111, 32 | eqeltrd 2549 |
. . . . 5
 
   |
113 | 106, 43, 112 | syl2anc 673 |
. . . 4
 

 
  |
114 | 113 | ex 441 |
. . . . 5
       |
115 | 114 | imdistani 704 |
. . . 4
 

 
    |
116 | | nfcv 2612 |
. . . . 5
   |
117 | | nfv 1769 |
. . . . . . 7
  |
118 | 1, 117 | nfan 2031 |
. . . . . 6
     |
119 | | nfv 1769 |
. . . . . 6
     |
120 | 118, 119 | nfim 2023 |
. . . . 5
   
      |
121 | | eleq1 2537 |
. . . . . . 7
 
   |
122 | 121 | anbi2d 718 |
. . . . . 6
  

     |
123 | 26 | eleq1d 2533 |
. . . . . 6
 
  
      |
124 | 122, 123 | imbi12d 327 |
. . . . 5
   
      
        |
125 | 116, 120,
124, 9 | vtoclgf 3091 |
. . . 4
  
       |
126 | 113, 115,
125 | sylc 61 |
. . 3
 

 
     |
127 | | simpl 464 |
. . . . 5
 

   
  |
128 | | eldifi 3544 |
. . . . . 6
       |
129 | 128 | adantl 473 |
. . . . 5
 

   
  |
130 | 127, 129,
112 | syl2anc 673 |
. . . 4
 

   
  |
131 | | dfin4 3674 |
. . . . . . . . 9
       |
132 | | difss 3549 |
. . . . . . . . 9
     |
133 | 131, 132 | eqsstri 3448 |
. . . . . . . 8
   |
134 | | inss2 3644 |
. . . . . . . . . 10
   |
135 | | id 22 |
. . . . . . . . . . 11
           |
136 | | dfin4 3674 |
. . . . . . . . . . . 12
       |
137 | 136 | eqcomi 2480 |
. . . . . . . . . . 11
       |
138 | 135, 137 | syl6eleq 2559 |
. . . . . . . . . 10
         |
139 | 134, 138 | sseldi 3416 |
. . . . . . . . 9
       |
140 | 139, 128 | elind 3609 |
. . . . . . . 8
         |
141 | 133, 140 | sseldi 3416 |
. . . . . . 7
       |
142 | 141 | adantl 473 |
. . . . . 6
 

   
  |
143 | 78 | eqcomd 2477 |
. . . . . . 7
 
       |
144 | | simpl 464 |
. . . . . . . 8
 
   |
145 | 75 | simpld 466 |
. . . . . . . 8
 
   |
146 | 144, 145,
107 | syl2anc 673 |
. . . . . . 7
 
       |
147 | 143, 146 | eqtr2d 2506 |
. . . . . 6
 
   |
148 | 127, 142,
147 | syl2anc 673 |
. . . . 5
 

   
  |
149 | 127, 148 | jca 541 |
. . . 4
 

   
    |
150 | | nfv 1769 |
. . . . . . 7
  |
151 | 1, 150 | nfan 2031 |
. . . . . 6
     |
152 | | nfv 1769 |
. . . . . 6
  |
153 | 151, 152 | nfim 2023 |
. . . . 5
   

  |
154 | | eqeq1 2475 |
. . . . . . 7
 
   |
155 | 154 | anbi2d 718 |
. . . . . 6
  

     |
156 | 26 | eqeq1d 2473 |
. . . . . 6
 
   |
157 | 155, 156 | imbi12d 327 |
. . . . 5
   

  

    |
158 | 116, 153,
157, 21 | vtoclgf 3091 |
. . . 4
  

   |
159 | 130, 149,
158 | sylc 61 |
. . 3
 

   
  |
160 | 25, 2, 42, 126, 159 | sge0ss 38368 |
. 2
 Σ^      Σ^      |
161 | 24, 110, 160 | 3eqtrd 2509 |
1
 Σ^    Σ^      |