Proof of Theorem selberg3r
Step | Hyp | Ref
| Expression |
1 | | elioore 11691 |
. . . . . . . . . . . . 13
   
  |
2 | 1 | adantl 473 |
. . . . . . . . . . . 12
       |
3 | | 1rp 11329 |
. . . . . . . . . . . . 13
 |
4 | 3 | a1i 11 |
. . . . . . . . . . . 12
       |
5 | | 1red 9676 |
. . . . . . . . . . . . 13
       |
6 | | eliooord 11719 |
. . . . . . . . . . . . . . 15
   
    |
7 | 6 | adantl 473 |
. . . . . . . . . . . . . 14
     
   |
8 | 7 | simpld 466 |
. . . . . . . . . . . . 13
       |
9 | 5, 2, 8 | ltled 9800 |
. . . . . . . . . . . 12
       |
10 | 2, 4, 9 | rpgecld 11400 |
. . . . . . . . . . 11
       |
11 | 10 | relogcld 23651 |
. . . . . . . . . 10
           |
12 | 11 | recnd 9687 |
. . . . . . . . 9
           |
13 | 12 | 2timesd 10878 |
. . . . . . . 8
                       |
14 | 13 | oveq2d 6324 |
. . . . . . 7
         ψ                          Λ  ψ                        ψ                          Λ  ψ                          |
15 | | chpcl 24130 |
. . . . . . . . . . . . 13
 ψ    |
16 | 2, 15 | syl 17 |
. . . . . . . . . . . 12
     ψ    |
17 | 16, 11 | remulcld 9689 |
. . . . . . . . . . 11
      ψ         |
18 | | 2re 10701 |
. . . . . . . . . . . . . 14
 |
19 | 18 | a1i 11 |
. . . . . . . . . . . . 13
       |
20 | 2, 8 | rplogcld 23657 |
. . . . . . . . . . . . 13
           |
21 | 19, 20 | rerpdivcld 11392 |
. . . . . . . . . . . 12
             |
22 | | fzfid 12224 |
. . . . . . . . . . . . 13
               |
23 | | elfznn 11854 |
. . . . . . . . . . . . . . . . 17
           |
24 | 23 | adantl 473 |
. . . . . . . . . . . . . . . 16
              
  |
25 | | vmacl 24124 |
. . . . . . . . . . . . . . . 16
 Λ    |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . 15
              
Λ    |
27 | 2 | adantr 472 |
. . . . . . . . . . . . . . . . 17
              
  |
28 | 27, 24 | nndivred 10680 |
. . . . . . . . . . . . . . . 16
              
    |
29 | | chpcl 24130 |
. . . . . . . . . . . . . . . 16
   ψ      |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . 15
              
ψ      |
31 | 26, 30 | remulcld 9689 |
. . . . . . . . . . . . . 14
              
 Λ  ψ       |
32 | 24 | nnrpd 11362 |
. . . . . . . . . . . . . . 15
              
  |
33 | 32 | relogcld 23651 |
. . . . . . . . . . . . . 14
              
      |
34 | 31, 33 | remulcld 9689 |
. . . . . . . . . . . . 13
              
  Λ  ψ            |
35 | 22, 34 | fsumrecl 13877 |
. . . . . . . . . . . 12
                 Λ  ψ 
          |
36 | 21, 35 | remulcld 9689 |
. . . . . . . . . . 11
                        Λ  ψ 
           |
37 | 17, 36 | readdcld 9688 |
. . . . . . . . . 10
       ψ                          Λ  ψ              |
38 | 37, 10 | rerpdivcld 11392 |
. . . . . . . . 9
        ψ                          Λ  ψ               |
39 | 38 | recnd 9687 |
. . . . . . . 8
        ψ                          Λ  ψ               |
40 | 39, 12, 12 | subsub4d 10036 |
. . . . . . 7
          ψ                          Λ  ψ 
                         ψ                          Λ  ψ 
                        |
41 | 14, 40 | eqtr4d 2508 |
. . . . . 6
         ψ                          Λ  ψ                         ψ                          Λ  ψ                         |
42 | 41 | oveq1d 6323 |
. . . . 5
          ψ                          Λ  ψ 
                                      Λ                     ψ                          Λ  ψ                                           Λ                 |
43 | 39, 12 | subcld 10005 |
. . . . . 6
         ψ                          Λ  ψ                    |
44 | | 2cn 10702 |
. . . . . . . . 9
 |
45 | 44 | a1i 11 |
. . . . . . . 8
       |
46 | 20 | rpne0d 11369 |
. . . . . . . 8
           |
47 | 45, 12, 46 | divcld 10405 |
. . . . . . 7
             |
48 | 26, 24 | nndivred 10680 |
. . . . . . . . . 10
              
 Λ     |
49 | 48, 33 | remulcld 9689 |
. . . . . . . . 9
              
  Λ          |
50 | 22, 49 | fsumrecl 13877 |
. . . . . . . 8
                 Λ          |
51 | 50 | recnd 9687 |
. . . . . . 7
                 Λ          |
52 | 47, 51 | mulcld 9681 |
. . . . . 6
                        Λ           |
53 | 43, 52, 12 | nnncan2d 10040 |
. . . . 5
           ψ                          Λ  ψ                                           Λ                    ψ                          Λ  ψ                         
           Λ            |
54 | | pntrval.r |
. . . . . . . . . . . . 13
  ψ     |
55 | 54 | pntrf 24480 |
. . . . . . . . . . . 12
     |
56 | 55 | ffvelrni 6036 |
. . . . . . . . . . 11

      |
57 | 10, 56 | syl 17 |
. . . . . . . . . 10
           |
58 | 57 | recnd 9687 |
. . . . . . . . 9
           |
59 | 58, 12 | mulcld 9681 |
. . . . . . . 8
                 |
60 | 36 | recnd 9687 |
. . . . . . . 8
                        Λ  ψ 
           |
61 | 59, 60 | addcld 9680 |
. . . . . . 7
                                   Λ  ψ              |
62 | 2 | recnd 9687 |
. . . . . . . 8
       |
63 | 62, 52 | mulcld 9681 |
. . . . . . 7
             
           Λ            |
64 | 10 | rpne0d 11369 |
. . . . . . 7
       |
65 | 61, 63, 62, 64 | divsubdird 10444 |
. . . . . 6
                                     Λ  ψ 
                              Λ                                            Λ  ψ 
                                Λ              |
66 | 59, 60, 63 | addsubassd 10025 |
. . . . . . . 8
                                    Λ  ψ 
                              Λ                                          Λ  ψ           
                   Λ              |
67 | 35 | recnd 9687 |
. . . . . . . . . . 11
                 Λ  ψ 
          |
68 | 62, 51 | mulcld 9681 |
. . . . . . . . . . 11
                  Λ           |
69 | 47, 67, 68 | subdid 10095 |
. . . . . . . . . 10
                         Λ  ψ 
                     Λ                               Λ  ψ 
                             Λ             |
70 | 49 | recnd 9687 |
. . . . . . . . . . . . . . 15
              
  Λ          |
71 | 22, 62, 70 | fsummulc2 13922 |
. . . . . . . . . . . . . 14
                  Λ         
            Λ           |
72 | 71 | oveq2d 6324 |
. . . . . . . . . . . . 13
                  Λ  ψ 
                     Λ                       Λ  ψ 
                     Λ            |
73 | 34 | recnd 9687 |
. . . . . . . . . . . . . 14
              
  Λ  ψ            |
74 | 62 | adantr 472 |
. . . . . . . . . . . . . . 15
              
  |
75 | 74, 70 | mulcld 9681 |
. . . . . . . . . . . . . 14
              
   Λ           |
76 | 22, 73, 75 | fsumsub 13926 |
. . . . . . . . . . . . 13
                  Λ  ψ             Λ           
           Λ  ψ 
                     Λ            |
77 | 72, 76 | eqtr4d 2508 |
. . . . . . . . . . . 12
                  Λ  ψ 
                     Λ                       Λ  ψ             Λ            |
78 | 26 | recnd 9687 |
. . . . . . . . . . . . . . . . 17
              
Λ    |
79 | 30 | recnd 9687 |
. . . . . . . . . . . . . . . . 17
              
ψ      |
80 | 33 | recnd 9687 |
. . . . . . . . . . . . . . . . 17
              
      |
81 | 78, 79, 80 | mul32d 9861 |
. . . . . . . . . . . . . . . 16
              
  Λ  ψ            Λ       ψ       |
82 | 24 | nncnd 10647 |
. . . . . . . . . . . . . . . . . . 19
              
  |
83 | 24 | nnne0d 10676 |
. . . . . . . . . . . . . . . . . . 19
              
  |
84 | 78, 80, 82, 83 | div23d 10442 |
. . . . . . . . . . . . . . . . . 18
              
  Λ          Λ          |
85 | 84 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
              
   Λ            Λ           |
86 | 78, 80 | mulcld 9681 |
. . . . . . . . . . . . . . . . . 18
              
 Λ         |
87 | 74, 86, 82, 83 | div12d 10441 |
. . . . . . . . . . . . . . . . 17
              
   Λ           Λ            |
88 | 85, 87 | eqtr3d 2507 |
. . . . . . . . . . . . . . . 16
              
   Λ           Λ            |
89 | 81, 88 | oveq12d 6326 |
. . . . . . . . . . . . . . 15
              
   Λ  ψ             Λ             Λ       ψ       Λ             |
90 | 10 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
              
  |
91 | 90, 32 | rpdivcld 11381 |
. . . . . . . . . . . . . . . . . 18
              
    |
92 | 54 | pntrval 24479 |
. . . . . . . . . . . . . . . . . 18
  
       ψ         |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . 17
              
       ψ    
    |
94 | 93 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
              
  Λ                Λ        ψ 
        |
95 | 28 | recnd 9687 |
. . . . . . . . . . . . . . . . 17
              
    |
96 | 86, 79, 95 | subdid 10095 |
. . . . . . . . . . . . . . . 16
              
  Λ        ψ    
      Λ       ψ       Λ             |
97 | 94, 96 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
              
  Λ                 Λ       ψ       Λ             |
98 | 89, 97 | eqtr4d 2508 |
. . . . . . . . . . . . . 14
              
   Λ  ψ             Λ            Λ                |
99 | 55 | ffvelrni 6036 |
. . . . . . . . . . . . . . . . 17
  
        |
100 | 91, 99 | syl 17 |
. . . . . . . . . . . . . . . 16
              
        |
101 | 100 | recnd 9687 |
. . . . . . . . . . . . . . 15
              
        |
102 | 78, 101, 80 | mul32d 9861 |
. . . . . . . . . . . . . 14
              
  Λ                Λ          
     |
103 | 98, 102 | eqtr4d 2508 |
. . . . . . . . . . . . 13
              
   Λ  ψ             Λ            Λ                |
104 | 103 | sumeq2dv 13846 |
. . . . . . . . . . . 12
                  Λ  ψ             Λ                      Λ                |
105 | 77, 104 | eqtrd 2505 |
. . . . . . . . . . 11
                  Λ  ψ 
                     Λ                      Λ                |
106 | 105 | oveq2d 6324 |
. . . . . . . . . 10
                         Λ  ψ 
                     Λ                  
           Λ                 |
107 | 47, 62, 51 | mul12d 9860 |
. . . . . . . . . . 11
             
           Λ                              Λ            |
108 | 107 | oveq2d 6324 |
. . . . . . . . . 10
                         Λ  ψ                               Λ                               Λ  ψ 
         
                   Λ             |
109 | 69, 106, 108 | 3eqtr3rd 2514 |
. . . . . . . . 9
                         Λ  ψ           
                   Λ                  
           Λ                 |
110 | 109 | oveq2d 6324 |
. . . . . . . 8
                        
           Λ  ψ 
         
                   Λ                                          Λ                  |
111 | 66, 110 | eqtrd 2505 |
. . . . . . 7
                                    Λ  ψ 
                              Λ                                         Λ                  |
112 | 111 | oveq1d 6323 |
. . . . . 6
                                     Λ  ψ 
                              Λ                                           Λ                   |
113 | 54 | pntrval 24479 |
. . . . . . . . . . . . . 14

     ψ     |
114 | 10, 113 | syl 17 |
. . . . . . . . . . . . 13
          ψ     |
115 | 114 | oveq1d 6323 |
. . . . . . . . . . . 12
                 ψ          |
116 | 16 | recnd 9687 |
. . . . . . . . . . . . 13
     ψ    |
117 | 116, 62, 12 | subdird 10096 |
. . . . . . . . . . . 12
       ψ          ψ       
        |
118 | 115, 117 | eqtrd 2505 |
. . . . . . . . . . 11
                 ψ                |
119 | 118 | oveq1d 6323 |
. . . . . . . . . 10
                                   Λ  ψ               ψ                                 Λ  ψ              |
120 | 17 | recnd 9687 |
. . . . . . . . . . 11
      ψ         |
121 | 62, 12 | mulcld 9681 |
. . . . . . . . . . 11
             |
122 | 120, 60, 121 | addsubd 10026 |
. . . . . . . . . 10
        ψ                          Λ  ψ                      ψ                                 Λ  ψ              |
123 | 119, 122 | eqtr4d 2508 |
. . . . . . . . 9
                                   Λ  ψ               ψ                          Λ  ψ 
                   |
124 | 123 | oveq1d 6323 |
. . . . . . . 8
                                    Λ  ψ 
               ψ                          Λ  ψ 
                    |
125 | 37 | recnd 9687 |
. . . . . . . . . 10
       ψ                          Λ  ψ              |
126 | 125, 121,
62, 64 | divsubdird 10444 |
. . . . . . . . 9
         ψ                          Λ  ψ                        ψ                          Λ  ψ                        |
127 | 12, 62, 64 | divcan3d 10410 |
. . . . . . . . . 10
                   |
128 | 127 | oveq2d 6324 |
. . . . . . . . 9
         ψ                          Λ  ψ                          ψ                          Λ  ψ                    |
129 | 126, 128 | eqtrd 2505 |
. . . . . . . 8
         ψ                          Λ  ψ                        ψ                          Λ  ψ                    |
130 | 124, 129 | eqtrd 2505 |
. . . . . . 7
                                    Λ  ψ 
               ψ                          Λ  ψ 
                  |
131 | 52, 62, 64 | divcan3d 10410 |
. . . . . . 7
                          Λ                              Λ           |
132 | 130, 131 | oveq12d 6326 |
. . . . . 6
                                     Λ  ψ 
                                Λ                 ψ                          Λ  ψ 
                       
           Λ            |
133 | 65, 112, 132 | 3eqtr3rd 2514 |
. . . . 5
          ψ                          Λ  ψ 
                       
           Λ                                         Λ                   |
134 | 42, 53, 133 | 3eqtrrd 2510 |
. . . 4
                                    Λ                      ψ                          Λ  ψ                                        Λ                 |
135 | 134 | mpteq2dva 4482 |
. . 3
                                   Λ                           ψ                          Λ  ψ                                        Λ                  |
136 | 19, 11 | remulcld 9689 |
. . . . 5
             |
137 | 38, 136 | resubcld 10068 |
. . . 4
         ψ                          Λ  ψ                      |
138 | 21, 50 | remulcld 9689 |
. . . . 5
                        Λ           |
139 | 138, 11 | resubcld 10068 |
. . . 4
                         Λ                |
140 | | selberg3 24476 |
. . . . 5
   
    ψ                          Λ  ψ                         |
141 | 140 | a1i 11 |
. . . 4
        ψ                          Λ  ψ 
                        |
142 | 19 | recnd 9687 |
. . . . . . . 8
       |
143 | 50, 20 | rerpdivcld 11392 |
. . . . . . . . 9
                  Λ               |
144 | 143 | recnd 9687 |
. . . . . . . 8
                  Λ               |
145 | 11 | rehalfcld 10882 |
. . . . . . . . 9
             |
146 | 145 | recnd 9687 |
. . . . . . . 8
             |
147 | 142, 144,
146 | subdid 10095 |
. . . . . . 7
        
           Λ                                    Λ                         |
148 | 142, 12, 51, 46 | div32d 10428 |
. . . . . . . . 9
                        Λ                       Λ                |
149 | 148 | eqcomd 2477 |
. . . . . . . 8
                   Λ                                 Λ           |
150 | | 2ne0 10724 |
. . . . . . . . . 10
 |
151 | 150 | a1i 11 |
. . . . . . . . 9
       |
152 | 12, 142, 151 | divcan2d 10407 |
. . . . . . . 8
                   |
153 | 149, 152 | oveq12d 6326 |
. . . . . . 7
                    Λ                                           Λ                |
154 | 147, 153 | eqtrd 2505 |
. . . . . 6
        
           Λ                                         Λ                |
155 | 154 | mpteq2dva 4482 |
. . . . 5
                   Λ                                  
           Λ                 |
156 | 143, 145 | resubcld 10068 |
. . . . . 6
                   Λ                      |
157 | | ioossre 11721 |
. . . . . . . 8
    |
158 | | o1const 13760 |
. . . . . . . 8
                |
159 | 157, 44, 158 | mp2an 686 |
. . . . . . 7
   
     |
160 | 159 | a1i 11 |
. . . . . 6
          |
161 | | vmalogdivsum 24456 |
. . . . . . 7
   
  
           Λ                         |
162 | 161 | a1i 11 |
. . . . . 6
                  Λ                          |
163 | 19, 156, 160, 162 | o1mul2 13765 |
. . . . 5
                   Λ                           |
164 | 155, 163 | eqeltrrd 2550 |
. . . 4
                        Λ                    |
165 | 137, 139,
141, 164 | o1sub2 13766 |
. . 3
         ψ                          Λ  ψ                                        Λ                     |
166 | 135, 165 | eqeltrd 2549 |
. 2
                                   Λ                       |
167 | 166 | trud 1461 |
1
   
                               Λ                      |