Proof of Theorem selberg4lem1
Step | Hyp | Ref
| Expression |
1 | | 2cnd 10710 |
. . . . . 6
 
      |
2 | | fzfid 12218 |
. . . . . . . . 9
 
              |
3 | | elfznn 11857 |
. . . . . . . . . . . . 13
           |
4 | 3 | adantl 472 |
. . . . . . . . . . . 12
               
  |
5 | | vmacl 24094 |
. . . . . . . . . . . 12
 Λ    |
6 | 4, 5 | syl 17 |
. . . . . . . . . . 11
               
Λ    |
7 | 6, 4 | nndivred 10686 |
. . . . . . . . . 10
               
 Λ     |
8 | | elioore 11695 |
. . . . . . . . . . . . . . 15
   
  |
9 | 8 | adantl 472 |
. . . . . . . . . . . . . 14
 
      |
10 | | 1rp 11335 |
. . . . . . . . . . . . . . 15
 |
11 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
 
      |
12 | | 1red 9684 |
. . . . . . . . . . . . . . 15
 
      |
13 | | eliooord 11723 |
. . . . . . . . . . . . . . . . 17
   
    |
14 | 13 | adantl 472 |
. . . . . . . . . . . . . . . 16
 
    
   |
15 | 14 | simpld 465 |
. . . . . . . . . . . . . . 15
 
      |
16 | 12, 9, 15 | ltled 9809 |
. . . . . . . . . . . . . 14
 
      |
17 | 9, 11, 16 | rpgecld 11406 |
. . . . . . . . . . . . 13
 
      |
18 | 17 | adantr 471 |
. . . . . . . . . . . 12
               
  |
19 | 4 | nnrpd 11368 |
. . . . . . . . . . . 12
               
  |
20 | 18, 19 | rpdivcld 11387 |
. . . . . . . . . . 11
               
    |
21 | 20 | relogcld 23621 |
. . . . . . . . . 10
               
        |
22 | 7, 21 | remulcld 9697 |
. . . . . . . . 9
               
  Λ            |
23 | 2, 22 | fsumrecl 13849 |
. . . . . . . 8
 
                Λ            |
24 | 9, 15 | rplogcld 23627 |
. . . . . . . 8
 
          |
25 | 23, 24 | rerpdivcld 11398 |
. . . . . . 7
 
                 Λ                 |
26 | 25 | recnd 9695 |
. . . . . 6
 
                 Λ                 |
27 | 17 | relogcld 23621 |
. . . . . . . 8
 
          |
28 | 27 | rehalfcld 10888 |
. . . . . . 7
 
            |
29 | 28 | recnd 9695 |
. . . . . 6
 
            |
30 | 1, 26, 29 | subdid 10102 |
. . . . 5
 
       
           Λ                                      Λ                           |
31 | 27 | recnd 9695 |
. . . . . . 7
 
          |
32 | | 2ne0 10730 |
. . . . . . . 8
 |
33 | 32 | a1i 11 |
. . . . . . 7
 
      |
34 | 31, 1, 33 | divcan2d 10413 |
. . . . . 6
 
                  |
35 | 34 | oveq2d 6331 |
. . . . 5
 
                   Λ                                        Λ                       |
36 | 30, 35 | eqtrd 2496 |
. . . 4
 
       
           Λ                                      Λ                       |
37 | 36 | mpteq2dva 4503 |
. . 3
                    Λ                                           Λ                        |
38 | | 2re 10707 |
. . . . 5
 |
39 | 38 | a1i 11 |
. . . 4
 
      |
40 | 25, 28 | resubcld 10075 |
. . . 4
 
                  Λ                        |
41 | | ioossre 11725 |
. . . . . 6
    |
42 | | 2cn 10708 |
. . . . . 6
 |
43 | | o1const 13732 |
. . . . . 6
                |
44 | 41, 42, 43 | mp2an 683 |
. . . . 5
   
     |
45 | 44 | a1i 11 |
. . . 4
           |
46 | | vmalogdivsum2 24425 |
. . . . 5
   
  
           Λ                           |
47 | 46 | a1i 11 |
. . . 4
                   Λ                            |
48 | 39, 40, 45, 47 | o1mul2 13737 |
. . 3
                    Λ                             |
49 | 37, 48 | eqeltrrd 2541 |
. 2
                    Λ                           |
50 | | fzfid 12218 |
. . . . . . . . 9
               
      
     |
51 | | elfznn 11857 |
. . . . . . . . . . . 12
             |
52 | 51 | adantl 472 |
. . . . . . . . . . 11
   
                       
  |
53 | | vmacl 24094 |
. . . . . . . . . . 11
 Λ    |
54 | 52, 53 | syl 17 |
. . . . . . . . . 10
   
                       
Λ    |
55 | 52 | nnrpd 11368 |
. . . . . . . . . . . 12
   
                       
  |
56 | 55 | relogcld 23621 |
. . . . . . . . . . 11
   
                       
      |
57 | 9 | adantr 471 |
. . . . . . . . . . . . . . 15
               
  |
58 | 57, 4 | nndivred 10686 |
. . . . . . . . . . . . . 14
               
    |
59 | 58 | adantr 471 |
. . . . . . . . . . . . 13
   
                       
    |
60 | 59, 52 | nndivred 10686 |
. . . . . . . . . . . 12
   
                       
      |
61 | | chpcl 24100 |
. . . . . . . . . . . 12
     ψ        |
62 | 60, 61 | syl 17 |
. . . . . . . . . . 11
   
                       
ψ        |
63 | 56, 62 | readdcld 9696 |
. . . . . . . . . 10
   
                       
     ψ         |
64 | 54, 63 | remulcld 9697 |
. . . . . . . . 9
   
                       
 Λ       ψ          |
65 | 50, 64 | fsumrecl 13849 |
. . . . . . . 8
               
             Λ       ψ          |
66 | 6, 65 | remulcld 9697 |
. . . . . . 7
               
 Λ               Λ       ψ           |
67 | 2, 66 | fsumrecl 13849 |
. . . . . 6
 
               Λ               Λ       ψ           |
68 | 17, 24 | rpmulcld 11386 |
. . . . . 6
 
            |
69 | 67, 68 | rerpdivcld 11398 |
. . . . 5
 
                Λ               Λ       ψ                  |
70 | 69, 27 | resubcld 10075 |
. . . 4
 
                 Λ               Λ       ψ                       |
71 | 70 | recnd 9695 |
. . 3
 
                 Λ               Λ       ψ                       |
72 | 23 | recnd 9695 |
. . . . . 6
 
                Λ            |
73 | 24 | rpne0d 11375 |
. . . . . 6
 
          |
74 | 72, 31, 73 | divcld 10411 |
. . . . 5
 
                 Λ                 |
75 | 1, 74 | mulcld 9689 |
. . . 4
 
                  Λ                  |
76 | 75, 31 | subcld 10012 |
. . 3
 
                   Λ                       |
77 | 69 | recnd 9695 |
. . . . . . 7
 
                Λ               Λ       ψ                  |
78 | 77, 75, 31 | nnncan2d 10047 |
. . . . . 6
 
                  Λ               Λ       ψ                                    Λ                                   Λ               Λ       ψ                              Λ                   |
79 | 67 | recnd 9695 |
. . . . . . . 8
 
               Λ               Λ       ψ           |
80 | 9 | recnd 9695 |
. . . . . . . 8
 
      |
81 | 17 | rpne0d 11375 |
. . . . . . . 8
 
      |
82 | 79, 80, 31, 81, 73 | divdiv1d 10442 |
. . . . . . 7
 
                 Λ               Λ       ψ                
          Λ               Λ       ψ                  |
83 | 1, 72, 31, 73 | divassd 10446 |
. . . . . . 7
 
                  Λ                              Λ                  |
84 | 82, 83 | oveq12d 6333 |
. . . . . 6
 
                  Λ               Λ       ψ                             Λ                              Λ               Λ       ψ                              Λ                   |
85 | 67, 17 | rerpdivcld 11398 |
. . . . . . . . 9
 
                Λ               Λ       ψ            |
86 | 85 | recnd 9695 |
. . . . . . . 8
 
                Λ               Λ       ψ            |
87 | 1, 72 | mulcld 9689 |
. . . . . . . 8
 
                 Λ             |
88 | 86, 87, 31, 73 | divsubdird 10450 |
. . . . . . 7
 
                  Λ               Λ       ψ                       Λ                    
          Λ               Λ       ψ                             Λ                   |
89 | 81 | adantr 471 |
. . . . . . . . . . . 12
               
  |
90 | 66, 57, 89 | redivcld 10463 |
. . . . . . . . . . 11
               
  Λ  
      
     Λ       ψ            |
91 | 90 | recnd 9695 |
. . . . . . . . . 10
               
  Λ  
      
     Λ       ψ            |
92 | 38 | a1i 11 |
. . . . . . . . . . . 12
               
  |
93 | 92, 22 | remulcld 9697 |
. . . . . . . . . . 11
               
   Λ             |
94 | 93 | recnd 9695 |
. . . . . . . . . 10
               
   Λ             |
95 | 2, 91, 94 | fsumsub 13898 |
. . . . . . . . 9
 
                 Λ               Λ       ψ             Λ                         Λ               Λ       ψ                       Λ              |
96 | 6 | recnd 9695 |
. . . . . . . . . . . 12
               
Λ    |
97 | 65, 57, 89 | redivcld 10463 |
. . . . . . . . . . . . 13
               
              Λ       ψ           |
98 | 97 | recnd 9695 |
. . . . . . . . . . . 12
               
              Λ       ψ           |
99 | | 2cnd 10710 |
. . . . . . . . . . . . 13
               
  |
100 | 21 | recnd 9695 |
. . . . . . . . . . . . . 14
               
        |
101 | 4 | nncnd 10653 |
. . . . . . . . . . . . . 14
               
  |
102 | 4 | nnne0d 10682 |
. . . . . . . . . . . . . 14
               
  |
103 | 100, 101,
102 | divcld 10411 |
. . . . . . . . . . . . 13
               
          |
104 | 99, 103 | mulcld 9689 |
. . . . . . . . . . . 12
               
            |
105 | 96, 98, 104 | subdid 10102 |
. . . . . . . . . . 11
               
 Λ                 Λ       ψ                       Λ                Λ       ψ           Λ                |
106 | 65 | recnd 9695 |
. . . . . . . . . . . . 13
               
             Λ       ψ          |
107 | 80 | adantr 471 |
. . . . . . . . . . . . 13
               
  |
108 | 96, 106, 107, 89 | divassd 10446 |
. . . . . . . . . . . 12
               
  Λ  
      
     Λ       ψ           Λ                Λ       ψ            |
109 | 96, 101, 100, 102 | div32d 10434 |
. . . . . . . . . . . . . 14
               
  Λ           Λ             |
110 | 109 | oveq2d 6331 |
. . . . . . . . . . . . 13
               
   Λ             Λ              |
111 | 99, 96, 103 | mul12d 9868 |
. . . . . . . . . . . . 13
               
  Λ             Λ               |
112 | 110, 111 | eqtrd 2496 |
. . . . . . . . . . . 12
               
   Λ            Λ               |
113 | 108, 112 | oveq12d 6333 |
. . . . . . . . . . 11
               
   Λ               Λ       ψ             Λ              Λ                Λ       ψ           Λ                |
114 | 105, 113 | eqtr4d 2499 |
. . . . . . . . . 10
               
 Λ                 Λ       ψ                        Λ               Λ       ψ             Λ              |
115 | 114 | sumeq2dv 13818 |
. . . . . . . . 9
 
               Λ    
      
     Λ       ψ                     
            Λ               Λ       ψ             Λ              |
116 | 66 | recnd 9695 |
. . . . . . . . . . 11
               
 Λ               Λ       ψ           |
117 | 2, 80, 116, 81 | fsumdivc 13896 |
. . . . . . . . . 10
 
                Λ               Λ       ψ          
           Λ               Λ       ψ            |
118 | 22 | recnd 9695 |
. . . . . . . . . . 11
               
  Λ            |
119 | 2, 1, 118 | fsummulc2 13894 |
. . . . . . . . . 10
 
                 Λ           
            Λ             |
120 | 117, 119 | oveq12d 6333 |
. . . . . . . . 9
 
                 Λ               Λ       ψ                       Λ             
           Λ               Λ       ψ                       Λ              |
121 | 95, 115, 120 | 3eqtr4rd 2507 |
. . . . . . . 8
 
                 Λ               Λ       ψ                       Λ                       Λ                 Λ       ψ                       |
122 | 121 | oveq1d 6330 |
. . . . . . 7
 
                  Λ               Λ       ψ                       Λ                             Λ    
      
     Λ       ψ                            |
123 | 88, 122 | eqtr3d 2498 |
. . . . . 6
 
                  Λ               Λ       ψ                             Λ                             Λ    
      
     Λ       ψ                            |
124 | 78, 84, 123 | 3eqtr2d 2502 |
. . . . 5
 
                  Λ               Λ       ψ                                    Λ                       
          Λ                 Λ       ψ                            |
125 | 124 | mpteq2dva 4503 |
. . . 4
                   Λ               Λ       ψ                                    Λ                                       Λ    
      
     Λ       ψ                             |
126 | | 1red 9684 |
. . . . 5
   |
127 | | selberg4lem1.1 |
. . . . . . . 8
   |
128 | 127 | adantr 471 |
. . . . . . 7
 
      |
129 | 128 | rpred 11370 |
. . . . . 6
 
      |
130 | 2, 7 | fsumrecl 13849 |
. . . . . . 7
 
               Λ     |
131 | 130, 24 | rerpdivcld 11398 |
. . . . . 6
 
                Λ          |
132 | 127 | rpcnd 11372 |
. . . . . . 7
   |
133 | | o1const 13732 |
. . . . . . 7
                |
134 | 41, 132, 133 | sylancr 674 |
. . . . . 6
           |
135 | | 1cnd 9685 |
. . . . . . . 8
   |
136 | | o1const 13732 |
. . . . . . . 8
                |
137 | 41, 135, 136 | sylancr 674 |
. . . . . . 7
           |
138 | 131 | recnd 9695 |
. . . . . . . 8
 
                Λ          |
139 | | 1cnd 9685 |
. . . . . . . 8
 
      |
140 | 130 | recnd 9695 |
. . . . . . . . . . . 12
 
               Λ     |
141 | 140, 31, 31, 73 | divsubdird 10450 |
. . . . . . . . . . 11
 
                 Λ                          Λ                     |
142 | 140, 31 | subcld 10012 |
. . . . . . . . . . . 12
 
                Λ          |
143 | 142, 31, 73 | divrecd 10414 |
. . . . . . . . . . 11
 
                 Λ                          Λ                 |
144 | 31, 73 | dividd 10409 |
. . . . . . . . . . . 12
 
                |
145 | 144 | oveq2d 6331 |
. . . . . . . . . . 11
 
                 Λ                                Λ           |
146 | 141, 143,
145 | 3eqtr3d 2504 |
. . . . . . . . . 10
 
                 Λ                            Λ           |
147 | 146 | mpteq2dva 4503 |
. . . . . . . . 9
                  Λ                   
  
          Λ            |
148 | 130, 27 | resubcld 10075 |
. . . . . . . . . 10
 
                Λ          |
149 | 12, 24 | rerpdivcld 11398 |
. . . . . . . . . 10
 
            |
150 | 17 | ex 440 |
. . . . . . . . . . . 12
        |
151 | 150 | ssrdv 3450 |
. . . . . . . . . . 11
      |
152 | | vmadivsum 24369 |
. . . . . . . . . . . 12

            Λ             |
153 | 152 | a1i 11 |
. . . . . . . . . . 11
              Λ              |
154 | 151, 153 | o1res2 13676 |
. . . . . . . . . 10
                 Λ              |
155 | | divlogrlim 23629 |
. . . . . . . . . . 11
   
         |
156 | | rlimo1 13729 |
. . . . . . . . . . 11
                             |
157 | 155, 156 | mp1i 13 |
. . . . . . . . . 10
                 |
158 | 148, 149,
154, 157 | o1mul2 13737 |
. . . . . . . . 9
                  Λ                     |
159 | 147, 158 | eqeltrrd 2541 |
. . . . . . . 8
                  Λ               |
160 | 138, 139,
159 | o1dif 13742 |
. . . . . . 7
                  Λ                       |
161 | 137, 160 | mpbird 240 |
. . . . . 6
                 Λ              |
162 | 129, 131,
134, 161 | o1mul2 13737 |
. . . . 5
                  Λ               |
163 | 129, 131 | remulcld 9697 |
. . . . 5
 
    
            Λ           |
164 | 21, 4 | nndivred 10686 |
. . . . . . . . . . 11
               
          |
165 | 92, 164 | remulcld 9697 |
. . . . . . . . . 10
               
            |
166 | 97, 165 | resubcld 10075 |
. . . . . . . . 9
               
         
     Λ       ψ                      |
167 | 6, 166 | remulcld 9697 |
. . . . . . . 8
               
 Λ                 Λ       ψ                       |
168 | 2, 167 | fsumrecl 13849 |
. . . . . . 7
 
               Λ    
      
     Λ       ψ                       |
169 | 168, 24 | rerpdivcld 11398 |
. . . . . 6
 
                Λ                 Λ       ψ                            |
170 | 169 | recnd 9695 |
. . . . 5
 
                Λ                 Λ       ψ                            |
171 | 168 | recnd 9695 |
. . . . . . . . . 10
 
               Λ    
      
     Λ       ψ                       |
172 | 171 | abscld 13547 |
. . . . . . . . 9
 
                  Λ    
      
     Λ       ψ                        |
173 | 129, 130 | remulcld 9697 |
. . . . . . . . 9
 
    
           Λ      |
174 | 98, 104 | subcld 10012 |
. . . . . . . . . . . . 13
               
         
     Λ       ψ                      |
175 | 96, 174 | mulcld 9689 |
. . . . . . . . . . . 12
               
 Λ                 Λ       ψ                       |
176 | 175 | abscld 13547 |
. . . . . . . . . . 11
               
    Λ    
      
     Λ       ψ                        |
177 | 2, 176 | fsumrecl 13849 |
. . . . . . . . . 10
 
                  Λ                 Λ       ψ                        |
178 | 167 | recnd 9695 |
. . . . . . . . . . 11
               
 Λ                 Λ       ψ                       |
179 | 2, 178 | fsumabs 13910 |
. . . . . . . . . 10
 
                  Λ    
      
     Λ       ψ                                    Λ                 Λ       ψ                        |
180 | 129 | adantr 471 |
. . . . . . . . . . . . 13
               
  |
181 | 180, 7 | remulcld 9697 |
. . . . . . . . . . . 12
               
  Λ      |
182 | 174 | abscld 13547 |
. . . . . . . . . . . . . 14
               
                  Λ       ψ                       |
183 | 180, 4 | nndivred 10686 |
. . . . . . . . . . . . . 14
               
    |
184 | | vmage0 24097 |
. . . . . . . . . . . . . . 15
 Λ    |
185 | 4, 184 | syl 17 |
. . . . . . . . . . . . . 14
               
Λ    |
186 | 106, 107,
101, 89, 102 | divdiv2d 10443 |
. . . . . . . . . . . . . . . . . . . . 21
               
              Λ       ψ                          Λ       ψ            |
187 | 106, 101,
107, 89 | div23d 10448 |
. . . . . . . . . . . . . . . . . . . . 21
               
         
     Λ       ψ                         Λ       ψ            |
188 | 186, 187 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . 20
               
              Λ       ψ                          Λ       ψ            |
189 | 99, 103, 101 | mulassd 9692 |
. . . . . . . . . . . . . . . . . . . . 21
               
                          |
190 | 100, 101,
102 | divcan1d 10412 |
. . . . . . . . . . . . . . . . . . . . . 22
               
                  |
191 | 190 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . . . 21
               
                      |
192 | 189, 191 | eqtr2d 2497 |
. . . . . . . . . . . . . . . . . . . 20
               
                      |
193 | 188, 192 | oveq12d 6333 |
. . . . . . . . . . . . . . . . . . 19
               
         
     Λ       ψ                                    Λ       ψ                         |
194 | 98, 104, 101 | subdird 10103 |
. . . . . . . . . . . . . . . . . . 19
               
                Λ       ψ                        
      
     Λ       ψ                         |
195 | 193, 194 | eqtr4d 2499 |
. . . . . . . . . . . . . . . . . 18
               
         
     Λ       ψ                                    Λ       ψ                       |
196 | 195 | fveq2d 5892 |
. . . . . . . . . . . . . . . . 17
               
                  Λ       ψ                                        Λ       ψ                        |
197 | 174, 101 | absmuld 13565 |
. . . . . . . . . . . . . . . . 17
               
                   Λ       ψ                                         Λ       ψ                            |
198 | 4 | nnred 10652 |
. . . . . . . . . . . . . . . . . . 19
               
  |
199 | 19 | rpge0d 11374 |
. . . . . . . . . . . . . . . . . . 19
               
  |
200 | 198, 199 | absidd 13533 |
. . . . . . . . . . . . . . . . . 18
               
      |
201 | 200 | oveq2d 6331 |
. . . . . . . . . . . . . . . . 17
               
                   Λ       ψ                                             Λ       ψ                        |
202 | 196, 197,
201 | 3eqtrd 2500 |
. . . . . . . . . . . . . . . 16
               
                  Λ       ψ                           
      
     Λ       ψ                        |
203 | 101 | mulid2d 9687 |
. . . . . . . . . . . . . . . . . . . 20
               
    |
204 | | fznnfl 12121 |
. . . . . . . . . . . . . . . . . . . . . 22
         
     |
205 | 9, 204 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 
            
     |
206 | 205 | simplbda 634 |
. . . . . . . . . . . . . . . . . . . 20
               
  |
207 | 203, 206 | eqbrtrd 4437 |
. . . . . . . . . . . . . . . . . . 19
               
    |
208 | | 1red 9684 |
. . . . . . . . . . . . . . . . . . . 20
               
  |
209 | 208, 57, 19 | lemuldivd 11416 |
. . . . . . . . . . . . . . . . . . 19
               
  
     |
210 | 207, 209 | mpbid 215 |
. . . . . . . . . . . . . . . . . 18
               
    |
211 | | 1re 9668 |
. . . . . . . . . . . . . . . . . . 19
 |
212 | | elicopnf 11759 |
. . . . . . . . . . . . . . . . . . 19
      
         |
213 | 211, 212 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
     
        |
214 | 58, 210, 213 | sylanbrc 675 |
. . . . . . . . . . . . . . . . 17
               
       |
215 | | selberg4lem1.2 |
. . . . . . . . . . . . . . . . . 18
                      Λ       ψ              
  |
216 | 215 | ad2antrr 737 |
. . . . . . . . . . . . . . . . 17
               
                     Λ       ψ              
  |
217 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 Λ  Λ    |
218 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
219 | | oveq2 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
220 | 219 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 ψ    ψ      |
221 | 218, 220 | oveq12d 6333 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      ψ          ψ       |
222 | 217, 221 | oveq12d 6333 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  Λ       ψ       Λ       ψ        |
223 | 222 | cbvsumv 13811 |
. . . . . . . . . . . . . . . . . . . . . . 23
           Λ       ψ      
          Λ       ψ       |
224 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
225 | 224 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       |
226 | | oveq1 6322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
227 | 226 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   ψ    ψ        |
228 | 227 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        ψ          ψ         |
229 | 228 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    Λ       ψ       Λ       ψ          |
230 | 229 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
          Λ       ψ       Λ       ψ          |
231 | 225, 230 | sumeq12dv 13821 |
. . . . . . . . . . . . . . . . . . . . . . 23
              Λ       ψ      
      
     Λ       ψ          |
232 | 223, 231 | syl5eq 2508 |
. . . . . . . . . . . . . . . . . . . . . 22
              Λ       ψ      
      
     Λ       ψ          |
233 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
234 | 232, 233 | oveq12d 6333 |
. . . . . . . . . . . . . . . . . . . . 21
               Λ       ψ                     Λ       ψ             |
235 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
236 | 235 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
237 | 234, 236 | oveq12d 6333 |
. . . . . . . . . . . . . . . . . . . 20
                Λ       ψ                             Λ       ψ                      |
238 | 237 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . . 19
        
          Λ       ψ                    
      
     Λ       ψ                       |
239 | 238 | breq1d 4426 |
. . . . . . . . . . . . . . . . . 18
                    Λ       ψ              
                  Λ       ψ                    
   |
240 | 239 | rspcv 3158 |
. . . . . . . . . . . . . . . . 17
     
 
                    Λ       ψ              
     
      
     Λ       ψ                        |
241 | 214, 216,
240 | sylc 62 |
. . . . . . . . . . . . . . . 16
               
                  Λ       ψ                    
  |
242 | 202, 241 | eqbrtrrd 4439 |
. . . . . . . . . . . . . . 15
               |