Proof of Theorem selberg3r
Step | Hyp | Ref
| Expression |
1 | | elioore 12205 |
. . . . . . . . . . . . 13
|
2 | 1 | adantl 482 |
. . . . . . . . . . . 12
|
3 | | 1rp 11836 |
. . . . . . . . . . . . 13
|
4 | 3 | a1i 11 |
. . . . . . . . . . . 12
|
5 | | 1red 10055 |
. . . . . . . . . . . . 13
|
6 | | eliooord 12233 |
. . . . . . . . . . . . . . 15
|
7 | 6 | adantl 482 |
. . . . . . . . . . . . . 14
|
8 | 7 | simpld 475 |
. . . . . . . . . . . . 13
|
9 | 5, 2, 8 | ltled 10185 |
. . . . . . . . . . . 12
|
10 | 2, 4, 9 | rpgecld 11911 |
. . . . . . . . . . 11
|
11 | 10 | relogcld 24369 |
. . . . . . . . . 10
|
12 | 11 | recnd 10068 |
. . . . . . . . 9
|
13 | 12 | 2timesd 11275 |
. . . . . . . 8
|
14 | 13 | oveq2d 6666 |
. . . . . . 7
ψ Λ ψ ψ Λ ψ |
15 | | chpcl 24850 |
. . . . . . . . . . . . 13
ψ |
16 | 2, 15 | syl 17 |
. . . . . . . . . . . 12
ψ |
17 | 16, 11 | remulcld 10070 |
. . . . . . . . . . 11
ψ |
18 | | 2re 11090 |
. . . . . . . . . . . . . 14
|
19 | 18 | a1i 11 |
. . . . . . . . . . . . 13
|
20 | 2, 8 | rplogcld 24375 |
. . . . . . . . . . . . 13
|
21 | 19, 20 | rerpdivcld 11903 |
. . . . . . . . . . . 12
|
22 | | fzfid 12772 |
. . . . . . . . . . . . 13
|
23 | | elfznn 12370 |
. . . . . . . . . . . . . . . . 17
|
24 | 23 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
25 | | vmacl 24844 |
. . . . . . . . . . . . . . . 16
Λ |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . 15
Λ |
27 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
28 | 27, 24 | nndivred 11069 |
. . . . . . . . . . . . . . . 16
|
29 | | chpcl 24850 |
. . . . . . . . . . . . . . . 16
ψ |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . 15
ψ |
31 | 26, 30 | remulcld 10070 |
. . . . . . . . . . . . . 14
Λ ψ |
32 | 24 | nnrpd 11870 |
. . . . . . . . . . . . . . 15
|
33 | 32 | relogcld 24369 |
. . . . . . . . . . . . . 14
|
34 | 31, 33 | remulcld 10070 |
. . . . . . . . . . . . 13
Λ ψ |
35 | 22, 34 | fsumrecl 14465 |
. . . . . . . . . . . 12
Λ ψ
|
36 | 21, 35 | remulcld 10070 |
. . . . . . . . . . 11
Λ ψ
|
37 | 17, 36 | readdcld 10069 |
. . . . . . . . . 10
ψ Λ ψ |
38 | 37, 10 | rerpdivcld 11903 |
. . . . . . . . 9
ψ Λ ψ |
39 | 38 | recnd 10068 |
. . . . . . . 8
ψ Λ ψ |
40 | 39, 12, 12 | subsub4d 10423 |
. . . . . . 7
ψ Λ ψ
ψ Λ ψ
|
41 | 14, 40 | eqtr4d 2659 |
. . . . . 6
ψ Λ ψ ψ Λ ψ |
42 | 41 | oveq1d 6665 |
. . . . 5
ψ Λ ψ
Λ ψ Λ ψ Λ |
43 | 39, 12 | subcld 10392 |
. . . . . 6
ψ Λ ψ |
44 | | 2cn 11091 |
. . . . . . . . 9
|
45 | 44 | a1i 11 |
. . . . . . . 8
|
46 | 20 | rpne0d 11877 |
. . . . . . . 8
|
47 | 45, 12, 46 | divcld 10801 |
. . . . . . 7
|
48 | 26, 24 | nndivred 11069 |
. . . . . . . . . 10
Λ |
49 | 48, 33 | remulcld 10070 |
. . . . . . . . 9
Λ |
50 | 22, 49 | fsumrecl 14465 |
. . . . . . . 8
Λ |
51 | 50 | recnd 10068 |
. . . . . . 7
Λ |
52 | 47, 51 | mulcld 10060 |
. . . . . 6
Λ |
53 | 43, 52, 12 | nnncan2d 10427 |
. . . . 5
ψ Λ ψ Λ ψ Λ ψ
Λ |
54 | | pntrval.r |
. . . . . . . . . . . . 13
ψ |
55 | 54 | pntrf 25252 |
. . . . . . . . . . . 12
|
56 | 55 | ffvelrni 6358 |
. . . . . . . . . . 11
|
57 | 10, 56 | syl 17 |
. . . . . . . . . 10
|
58 | 57 | recnd 10068 |
. . . . . . . . 9
|
59 | 58, 12 | mulcld 10060 |
. . . . . . . 8
|
60 | 36 | recnd 10068 |
. . . . . . . 8
Λ ψ
|
61 | 59, 60 | addcld 10059 |
. . . . . . 7
Λ ψ |
62 | 2 | recnd 10068 |
. . . . . . . 8
|
63 | 62, 52 | mulcld 10060 |
. . . . . . 7
Λ |
64 | 10 | rpne0d 11877 |
. . . . . . 7
|
65 | 61, 63, 62, 64 | divsubdird 10840 |
. . . . . 6
Λ ψ
Λ Λ ψ
Λ |
66 | 59, 60, 63 | addsubassd 10412 |
. . . . . . . 8
Λ ψ
Λ Λ ψ
Λ |
67 | 35 | recnd 10068 |
. . . . . . . . . . 11
Λ ψ
|
68 | 62, 51 | mulcld 10060 |
. . . . . . . . . . 11
Λ |
69 | 47, 67, 68 | subdid 10486 |
. . . . . . . . . 10
Λ ψ
Λ Λ ψ
Λ |
70 | 49 | recnd 10068 |
. . . . . . . . . . . . . . 15
Λ |
71 | 22, 62, 70 | fsummulc2 14516 |
. . . . . . . . . . . . . 14
Λ
Λ |
72 | 71 | oveq2d 6666 |
. . . . . . . . . . . . 13
Λ ψ
Λ Λ ψ
Λ |
73 | 34 | recnd 10068 |
. . . . . . . . . . . . . 14
Λ ψ |
74 | 62 | adantr 481 |
. . . . . . . . . . . . . . 15
|
75 | 74, 70 | mulcld 10060 |
. . . . . . . . . . . . . 14
Λ |
76 | 22, 73, 75 | fsumsub 14520 |
. . . . . . . . . . . . 13
Λ ψ Λ
Λ ψ
Λ |
77 | 72, 76 | eqtr4d 2659 |
. . . . . . . . . . . 12
Λ ψ
Λ Λ ψ Λ |
78 | 26 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
Λ |
79 | 30 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
ψ |
80 | 33 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
|
81 | 78, 79, 80 | mul32d 10246 |
. . . . . . . . . . . . . . . 16
Λ ψ Λ ψ |
82 | 24 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . 19
|
83 | 24 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . 19
|
84 | 78, 80, 82, 83 | div23d 10838 |
. . . . . . . . . . . . . . . . . 18
Λ Λ |
85 | 84 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
Λ Λ |
86 | 78, 80 | mulcld 10060 |
. . . . . . . . . . . . . . . . . 18
Λ |
87 | 74, 86, 82, 83 | div12d 10837 |
. . . . . . . . . . . . . . . . 17
Λ Λ |
88 | 85, 87 | eqtr3d 2658 |
. . . . . . . . . . . . . . . 16
Λ Λ |
89 | 81, 88 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
Λ ψ Λ Λ ψ Λ |
90 | 10 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
91 | 90, 32 | rpdivcld 11889 |
. . . . . . . . . . . . . . . . . 18
|
92 | 54 | pntrval 25251 |
. . . . . . . . . . . . . . . . . 18
ψ |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . 17
ψ
|
94 | 93 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
Λ Λ ψ
|
95 | 28 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
|
96 | 86, 79, 95 | subdid 10486 |
. . . . . . . . . . . . . . . 16
Λ ψ
Λ ψ Λ |
97 | 94, 96 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
Λ Λ ψ Λ |
98 | 89, 97 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
Λ ψ Λ Λ |
99 | 55 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . 17
|
100 | 91, 99 | syl 17 |
. . . . . . . . . . . . . . . 16
|
101 | 100 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
102 | 78, 101, 80 | mul32d 10246 |
. . . . . . . . . . . . . 14
Λ Λ
|
103 | 98, 102 | eqtr4d 2659 |
. . . . . . . . . . . . 13
Λ ψ Λ Λ |
104 | 103 | sumeq2dv 14433 |
. . . . . . . . . . . 12
Λ ψ Λ Λ |
105 | 77, 104 | eqtrd 2656 |
. . . . . . . . . . 11
Λ ψ
Λ Λ |
106 | 105 | oveq2d 6666 |
. . . . . . . . . 10
Λ ψ
Λ
Λ |
107 | 47, 62, 51 | mul12d 10245 |
. . . . . . . . . . 11
Λ Λ |
108 | 107 | oveq2d 6666 |
. . . . . . . . . 10
Λ ψ Λ Λ ψ
Λ |
109 | 69, 106, 108 | 3eqtr3rd 2665 |
. . . . . . . . 9
Λ ψ
Λ
Λ |
110 | 109 | oveq2d 6666 |
. . . . . . . 8
Λ ψ
Λ Λ |
111 | 66, 110 | eqtrd 2656 |
. . . . . . 7
Λ ψ
Λ Λ |
112 | 111 | oveq1d 6665 |
. . . . . 6
Λ ψ
Λ Λ |
113 | 54 | pntrval 25251 |
. . . . . . . . . . . . . 14
ψ |
114 | 10, 113 | syl 17 |
. . . . . . . . . . . . 13
ψ |
115 | 114 | oveq1d 6665 |
. . . . . . . . . . . 12
ψ |
116 | 16 | recnd 10068 |
. . . . . . . . . . . . 13
ψ |
117 | 116, 62, 12 | subdird 10487 |
. . . . . . . . . . . 12
ψ ψ
|
118 | 115, 117 | eqtrd 2656 |
. . . . . . . . . . 11
ψ |
119 | 118 | oveq1d 6665 |
. . . . . . . . . 10
Λ ψ ψ Λ ψ |
120 | 17 | recnd 10068 |
. . . . . . . . . . 11
ψ |
121 | 62, 12 | mulcld 10060 |
. . . . . . . . . . 11
|
122 | 120, 60, 121 | addsubd 10413 |
. . . . . . . . . 10
ψ Λ ψ ψ Λ ψ |
123 | 119, 122 | eqtr4d 2659 |
. . . . . . . . 9
Λ ψ ψ Λ ψ
|
124 | 123 | oveq1d 6665 |
. . . . . . . 8
Λ ψ
ψ Λ ψ
|
125 | 37 | recnd 10068 |
. . . . . . . . . 10
ψ Λ ψ |
126 | 125, 121,
62, 64 | divsubdird 10840 |
. . . . . . . . 9
ψ Λ ψ ψ Λ ψ |
127 | 12, 62, 64 | divcan3d 10806 |
. . . . . . . . . 10
|
128 | 127 | oveq2d 6666 |
. . . . . . . . 9
ψ Λ ψ ψ Λ ψ |
129 | 126, 128 | eqtrd 2656 |
. . . . . . . 8
ψ Λ ψ ψ Λ ψ |
130 | 124, 129 | eqtrd 2656 |
. . . . . . 7
Λ ψ
ψ Λ ψ
|
131 | 52, 62, 64 | divcan3d 10806 |
. . . . . . 7
Λ Λ |
132 | 130, 131 | oveq12d 6668 |
. . . . . 6
Λ ψ
Λ ψ Λ ψ
Λ |
133 | 65, 112, 132 | 3eqtr3rd 2665 |
. . . . 5
ψ Λ ψ
Λ Λ |
134 | 42, 53, 133 | 3eqtrrd 2661 |
. . . 4
Λ ψ Λ ψ Λ |
135 | 134 | mpteq2dva 4744 |
. . 3
Λ ψ Λ ψ Λ |
136 | 19, 11 | remulcld 10070 |
. . . . 5
|
137 | 38, 136 | resubcld 10458 |
. . . 4
ψ Λ ψ |
138 | 21, 50 | remulcld 10070 |
. . . . 5
Λ |
139 | 138, 11 | resubcld 10458 |
. . . 4
Λ |
140 | | selberg3 25248 |
. . . . 5
ψ Λ ψ |
141 | 140 | a1i 11 |
. . . 4
ψ Λ ψ
|
142 | 19 | recnd 10068 |
. . . . . . . 8
|
143 | 50, 20 | rerpdivcld 11903 |
. . . . . . . . 9
Λ |
144 | 143 | recnd 10068 |
. . . . . . . 8
Λ |
145 | 11 | rehalfcld 11279 |
. . . . . . . . 9
|
146 | 145 | recnd 10068 |
. . . . . . . 8
|
147 | 142, 144,
146 | subdid 10486 |
. . . . . . 7
Λ Λ |
148 | 142, 12, 51, 46 | div32d 10824 |
. . . . . . . . 9
Λ Λ |
149 | 148 | eqcomd 2628 |
. . . . . . . 8
Λ Λ |
150 | | 2ne0 11113 |
. . . . . . . . . 10
|
151 | 150 | a1i 11 |
. . . . . . . . 9
|
152 | 12, 142, 151 | divcan2d 10803 |
. . . . . . . 8
|
153 | 149, 152 | oveq12d 6668 |
. . . . . . 7
Λ Λ |
154 | 147, 153 | eqtrd 2656 |
. . . . . 6
Λ Λ |
155 | 154 | mpteq2dva 4744 |
. . . . 5
Λ
Λ |
156 | 143, 145 | resubcld 10458 |
. . . . . 6
Λ |
157 | | ioossre 12235 |
. . . . . . . 8
|
158 | | o1const 14350 |
. . . . . . . 8
|
159 | 157, 44, 158 | mp2an 708 |
. . . . . . 7
|
160 | 159 | a1i 11 |
. . . . . 6
|
161 | | vmalogdivsum 25228 |
. . . . . . 7
Λ |
162 | 161 | a1i 11 |
. . . . . 6
Λ |
163 | 19, 156, 160, 162 | o1mul2 14355 |
. . . . 5
Λ |
164 | 155, 163 | eqeltrrd 2702 |
. . . 4
Λ |
165 | 137, 139,
141, 164 | o1sub2 14356 |
. . 3
ψ Λ ψ Λ |
166 | 135, 165 | eqeltrd 2701 |
. 2
Λ |
167 | 166 | trud 1493 |
1
Λ |