Proof of Theorem refsum2cnlem1
Step | Hyp | Ref
| Expression |
1 | | refsum2cnlem1.4 |
. . 3
   |
2 | | refsum2cnlem1.5 |
. . . . . . . . 9
           |
3 | | nfmpt1 4485 |
. . . . . . . . 9
             |
4 | 2, 3 | nfcxfr 2610 |
. . . . . . . 8
   |
5 | | nfcv 2612 |
. . . . . . . 8
   |
6 | 4, 5 | nffv 5886 |
. . . . . . 7
       |
7 | | nfcv 2612 |
. . . . . . 7
   |
8 | 6, 7 | nffv 5886 |
. . . . . 6
           |
9 | 8 | a1i 11 |
. . . . 5
 
             |
10 | | nfcv 2612 |
. . . . . . . 8
   |
11 | 4, 10 | nffv 5886 |
. . . . . . 7
       |
12 | 11, 7 | nffv 5886 |
. . . . . 6
           |
13 | 12 | a1i 11 |
. . . . 5
 
             |
14 | | 1cnd 9677 |
. . . . 5
 
   |
15 | | 2cnd 10704 |
. . . . 5
 
   |
16 | | 1ex 9656 |
. . . . . . . . . . 11
 |
17 | 16 | prid1 4071 |
. . . . . . . . . 10
    |
18 | | refsum2cnlem1.8 |
. . . . . . . . . . 11
     |
19 | | refsum2cnlem1.9 |
. . . . . . . . . . 11
     |
20 | 18, 19 | ifcld 3915 |
. . . . . . . . . 10
          |
21 | | eqeq1 2475 |
. . . . . . . . . . . 12
     |
22 | 21 | ifbid 3894 |
. . . . . . . . . . 11
             |
23 | 22, 2 | fvmptg 5961 |
. . . . . . . . . 10
                        |
24 | 17, 20, 23 | sylancr 676 |
. . . . . . . . 9
            |
25 | | eqid 2471 |
. . . . . . . . . 10
 |
26 | 25 | iftruei 3879 |
. . . . . . . . 9
      |
27 | 24, 26 | syl6eq 2521 |
. . . . . . . 8
       |
28 | 27 | adantr 472 |
. . . . . . 7
 
       |
29 | 28 | fveq1d 5881 |
. . . . . 6
 
               |
30 | | eqid 2471 |
. . . . . . . . . . 11
   |
31 | | eqid 2471 |
. . . . . . . . . . 11
   |
32 | 30, 31 | cnf 20339 |
. . . . . . . . . 10
           |
33 | 18, 32 | syl 17 |
. . . . . . . . 9
         |
34 | | refsum2cnlem1.7 |
. . . . . . . . . . . 12
 TopOn    |
35 | | toponuni 20019 |
. . . . . . . . . . . 12
 TopOn 
   |
36 | 34, 35 | syl 17 |
. . . . . . . . . . 11
    |
37 | 36 | eqcomd 2477 |
. . . . . . . . . 10
    |
38 | | refsum2cnlem1.6 |
. . . . . . . . . . . . 13
     |
39 | 38 | unieqi 4199 |
. . . . . . . . . . . 12
       |
40 | | uniretop 21861 |
. . . . . . . . . . . 12
      |
41 | 39, 40 | eqtr4i 2496 |
. . . . . . . . . . 11
  |
42 | 41 | a1i 11 |
. . . . . . . . . 10
    |
43 | 37, 42 | feq23d 5734 |
. . . . . . . . 9
       
       |
44 | 33, 43 | mpbid 215 |
. . . . . . . 8
       |
45 | 44 | anim1i 578 |
. . . . . . 7
 
     
   |
46 | | ffvelrn 6035 |
. . . . . . 7
     
       |
47 | | recn 9647 |
. . . . . . 7
           |
48 | 45, 46, 47 | 3syl 18 |
. . . . . 6
 
       |
49 | 29, 48 | eqeltrd 2549 |
. . . . 5
 
           |
50 | | 2ex 10703 |
. . . . . . . . . . 11
 |
51 | 50 | prid2 4072 |
. . . . . . . . . 10
    |
52 | 18, 19 | ifcld 3915 |
. . . . . . . . . 10
          |
53 | | eqeq1 2475 |
. . . . . . . . . . . 12
     |
54 | 53 | ifbid 3894 |
. . . . . . . . . . 11
             |
55 | 54, 2 | fvmptg 5961 |
. . . . . . . . . 10
                        |
56 | 51, 52, 55 | sylancr 676 |
. . . . . . . . 9
            |
57 | | 1ne2 10845 |
. . . . . . . . . . 11
 |
58 | 57 | nesymi 2700 |
. . . . . . . . . 10
 |
59 | 58 | iffalsei 3882 |
. . . . . . . . 9
      |
60 | 56, 59 | syl6eq 2521 |
. . . . . . . 8
       |
61 | 60 | adantr 472 |
. . . . . . 7
 
       |
62 | 61 | fveq1d 5881 |
. . . . . 6
 
               |
63 | 30, 31 | cnf 20339 |
. . . . . . . . . 10
           |
64 | 19, 63 | syl 17 |
. . . . . . . . 9
         |
65 | 37, 42 | feq23d 5734 |
. . . . . . . . 9
       
       |
66 | 64, 65 | mpbid 215 |
. . . . . . . 8
       |
67 | 66 | anim1i 578 |
. . . . . . 7
 
     
   |
68 | | ffvelrn 6035 |
. . . . . . 7
     
       |
69 | | recn 9647 |
. . . . . . 7
           |
70 | 67, 68, 69 | 3syl 18 |
. . . . . 6
 
       |
71 | 62, 70 | eqeltrd 2549 |
. . . . 5
 
           |
72 | 57 | a1i 11 |
. . . . 5
 
   |
73 | | fveq2 5879 |
. . . . . . 7
           |
74 | 73 | fveq1d 5881 |
. . . . . 6
                   |
75 | 74 | adantl 473 |
. . . . 5
                       |
76 | | fveq2 5879 |
. . . . . . 7
           |
77 | 76 | fveq1d 5881 |
. . . . . 6
                   |
78 | 77 | adantl 473 |
. . . . 5
                       |
79 | 9, 13, 14, 15, 49, 71, 72, 75, 78 | sumpair 37419 |
. . . 4
 
                                 |
80 | 29, 62 | oveq12d 6326 |
. . . 4
 
                               |
81 | 79, 80 | eqtrd 2505 |
. . 3
 
                         |
82 | 1, 81 | mpteq2da 4481 |
. 2
                             |
83 | | prfi 7864 |
. . . 4
    |
84 | 83 | a1i 11 |
. . 3
      |
85 | | eqid 2471 |
. . . . . . . . . 10
 |
86 | 85 | ax-gen 1677 |
. . . . . . . . 9

 |
87 | | refsum2cnlem1.1 |
. . . . . . . . . . . 12
   |
88 | | nfcv 2612 |
. . . . . . . . . . . 12
   |
89 | 87, 88 | nffv 5886 |
. . . . . . . . . . 11
       |
90 | | refsum2cnlem1.2 |
. . . . . . . . . . 11
   |
91 | 89, 90 | nfeq 2623 |
. . . . . . . . . 10
       |
92 | | fveq1 5878 |
. . . . . . . . . . 11
                   |
93 | 92 | a1d 25 |
. . . . . . . . . 10
                     |
94 | 91, 93 | ralrimi 2800 |
. . . . . . . . 9
     
              |
95 | | mpteq12f 4472 |
. . . . . . . . 9
   
            

                 |
96 | 86, 94, 95 | sylancr 676 |
. . . . . . . 8
                       |
97 | 96 | adantl 473 |
. . . . . . 7
 
    

                 |
98 | | retopon 21862 |
. . . . . . . . . . . . 13
    TopOn   |
99 | 38, 98 | eqeltri 2545 |
. . . . . . . . . . . 12
TopOn   |
100 | 99 | a1i 11 |
. . . . . . . . . . 11
 TopOn    |
101 | | cnf2 20342 |
. . . . . . . . . . 11
  TopOn  TopOn 
         |
102 | 34, 100, 18, 101 | syl3anc 1292 |
. . . . . . . . . 10
       |
103 | | ffn 5739 |
. . . . . . . . . 10
       |
104 | 102, 103 | syl 17 |
. . . . . . . . 9
   |
105 | 90 | dffn5f 5935 |
. . . . . . . . 9


       |
106 | 104, 105 | sylib 201 |
. . . . . . . 8
         |
107 | 106 | adantr 472 |
. . . . . . 7
 
    

       |
108 | 97, 107 | eqtr4d 2508 |
. . . . . 6
 
    

           |
109 | 18 | adantr 472 |
. . . . . 6
 
    

   |
110 | 108, 109 | eqeltrd 2549 |
. . . . 5
 
    

             |
111 | 110 | adantlr 729 |
. . . 4
                          |
112 | | refsum2cnlem1.3 |
. . . . . . . . . . 11
   |
113 | 89, 112 | nfeq 2623 |
. . . . . . . . . 10
       |
114 | | fveq1 5878 |
. . . . . . . . . . 11
                   |
115 | 114 | a1d 25 |
. . . . . . . . . 10
                     |
116 | 113, 115 | ralrimi 2800 |
. . . . . . . . 9
     
              |
117 | | mpteq12f 4472 |
. . . . . . . . 9
   
            

                 |
118 | 86, 116, 117 | sylancr 676 |
. . . . . . . 8
                       |
119 | 118 | adantl 473 |
. . . . . . 7
 
    

                 |
120 | | cnf2 20342 |
. . . . . . . . . . 11
  TopOn  TopOn 
         |
121 | 34, 100, 19, 120 | syl3anc 1292 |
. . . . . . . . . 10
       |
122 | | ffn 5739 |
. . . . . . . . . 10
       |
123 | 121, 122 | syl 17 |
. . . . . . . . 9
   |
124 | 112 | dffn5f 5935 |
. . . . . . . . 9


       |
125 | 123, 124 | sylib 201 |
. . . . . . . 8
         |
126 | 125 | adantr 472 |
. . . . . . 7
 
    

       |
127 | 119, 126 | eqtr4d 2508 |
. . . . . 6
 
    

           |
128 | 19 | adantr 472 |
. . . . . 6
 
    

   |
129 | 127, 128 | eqeltrd 2549 |
. . . . 5
 
    

             |
130 | 129 | adantlr 729 |
. . . 4
                          |
131 | | simpr 468 |
. . . . . . . 8
 
   
     |
132 | 18, 19 | ifcld 3915 |
. . . . . . . . 9
          |
133 | 132 | adantr 472 |
. . . . . . . 8
 
   
         |
134 | 2 | fvmpt2 5972 |
. . . . . . . 8
                        |
135 | 131, 133,
134 | syl2anc 673 |
. . . . . . 7
 
   
           |
136 | | iftrue 3878 |
. . . . . . 7
        |
137 | 135, 136 | sylan9eq 2525 |
. . . . . 6
              |
138 | 137 | orcd 399 |
. . . . 5
                    |
139 | 135 | adantr 472 |
. . . . . . 7
                   |
140 | | neeq2 2706 |
. . . . . . . . . . . 12
 
   |
141 | 57, 140 | mpbiri 241 |
. . . . . . . . . . 11
   |
142 | 141 | necomd 2698 |
. . . . . . . . . 10
   |
143 | 142 | neneqd 2648 |
. . . . . . . . 9

  |
144 | 143 | adantl 473 |
. . . . . . . 8
       
  |
145 | 144 | iffalsed 3883 |
. . . . . . 7
               |
146 | 139, 145 | eqtrd 2505 |
. . . . . 6
              |
147 | 146 | olcd 400 |
. . . . 5
                    |
148 | | elpri 3976 |
. . . . . 6
        |
149 | 148 | adantl 473 |
. . . . 5
 
   
    |
150 | 138, 147,
149 | mpjaodan 803 |
. . . 4
 
   
    
       |
151 | 111, 130,
150 | mpjaodan 803 |
. . 3
 
   

             |
152 | 1, 38, 34, 84, 151 | refsumcn 37414 |
. 2
                   |
153 | 82, 152 | eqeltrrd 2550 |
1
                 |