Step | Hyp | Ref
| Expression |
1 | | 1re 10039 |
. . . . . . 7
|
2 | | elicopnf 12269 |
. . . . . . 7
|
3 | 1, 2 | mp1i 13 |
. . . . . 6
|
4 | 3 | simprbda 653 |
. . . . 5
|
5 | 4 | ex 450 |
. . . 4
|
6 | 5 | ssrdv 3609 |
. . 3
|
7 | 1 | a1i 11 |
. . 3
|
8 | | fzfid 12772 |
. . . . . . 7
|
9 | | elfznn 12370 |
. . . . . . . . . 10
|
10 | 9 | adantl 482 |
. . . . . . . . 9
|
11 | | vmacl 24844 |
. . . . . . . . 9
Λ |
12 | 10, 11 | syl 17 |
. . . . . . . 8
Λ |
13 | 10 | nnrpd 11870 |
. . . . . . . . . 10
|
14 | 13 | relogcld 24369 |
. . . . . . . . 9
|
15 | 4 | adantr 481 |
. . . . . . . . . . 11
|
16 | 15, 10 | nndivred 11069 |
. . . . . . . . . 10
|
17 | | chpcl 24850 |
. . . . . . . . . 10
ψ |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
ψ |
19 | 14, 18 | readdcld 10069 |
. . . . . . . 8
ψ |
20 | 12, 19 | remulcld 10070 |
. . . . . . 7
Λ ψ
|
21 | 8, 20 | fsumrecl 14465 |
. . . . . 6
Λ ψ |
22 | | 1rp 11836 |
. . . . . . . 8
|
23 | 22 | a1i 11 |
. . . . . . 7
|
24 | 3 | simplbda 654 |
. . . . . . 7
|
25 | 4, 23, 24 | rpgecld 11911 |
. . . . . 6
|
26 | 21, 25 | rerpdivcld 11903 |
. . . . 5
Λ ψ
|
27 | | 2re 11090 |
. . . . . . 7
|
28 | 27 | a1i 11 |
. . . . . 6
|
29 | 25 | relogcld 24369 |
. . . . . 6
|
30 | 28, 29 | remulcld 10070 |
. . . . 5
|
31 | 26, 30 | resubcld 10458 |
. . . 4
Λ ψ |
32 | 31 | recnd 10068 |
. . 3
Λ ψ |
33 | 25 | ex 450 |
. . . . 5
|
34 | 33 | ssrdv 3609 |
. . . 4
|
35 | | selberg 25237 |
. . . . 5
Λ ψ
|
36 | 35 | a1i 11 |
. . . 4
Λ ψ |
37 | 34, 36 | o1res2 14294 |
. . 3
Λ ψ |
38 | | fzfid 12772 |
. . . . 5
|
39 | | elfznn 12370 |
. . . . . . . 8
|
40 | 39 | adantl 482 |
. . . . . . 7
|
41 | 40, 11 | syl 17 |
. . . . . 6
Λ |
42 | 40 | nnrpd 11870 |
. . . . . . . 8
|
43 | 42 | relogcld 24369 |
. . . . . . 7
|
44 | | simprl 794 |
. . . . . . . . . 10
|
45 | 44 | adantr 481 |
. . . . . . . . 9
|
46 | 45, 40 | nndivred 11069 |
. . . . . . . 8
|
47 | | chpcl 24850 |
. . . . . . . 8
ψ |
48 | 46, 47 | syl 17 |
. . . . . . 7
ψ |
49 | 43, 48 | readdcld 10069 |
. . . . . 6
ψ |
50 | 41, 49 | remulcld 10070 |
. . . . 5
Λ ψ |
51 | 38, 50 | fsumrecl 14465 |
. . . 4
Λ ψ |
52 | 27 | a1i 11 |
. . . . 5
|
53 | 22 | a1i 11 |
. . . . . . 7
|
54 | | simprr 796 |
. . . . . . 7
|
55 | 44, 53, 54 | rpgecld 11911 |
. . . . . 6
|
56 | 55 | relogcld 24369 |
. . . . 5
|
57 | 52, 56 | remulcld 10070 |
. . . 4
|
58 | 51, 57 | readdcld 10069 |
. . 3
Λ ψ |
59 | 31 | adantr 481 |
. . . . . 6
Λ ψ
|
60 | 59 | recnd 10068 |
. . . . 5
Λ ψ
|
61 | 60 | abscld 14175 |
. . . 4
Λ ψ |
62 | 26 | adantr 481 |
. . . . 5
Λ ψ
|
63 | 30 | adantr 481 |
. . . . 5
|
64 | 62, 63 | readdcld 10069 |
. . . 4
Λ ψ
|
65 | | fzfid 12772 |
. . . . . 6
|
66 | 39 | adantl 482 |
. . . . . . . 8
|
67 | 66, 11 | syl 17 |
. . . . . . 7
Λ |
68 | 66 | nnrpd 11870 |
. . . . . . . . 9
|
69 | 68 | relogcld 24369 |
. . . . . . . 8
|
70 | | simprll 802 |
. . . . . . . . . . 11
|
71 | 70 | adantr 481 |
. . . . . . . . . 10
|
72 | 71, 66 | nndivred 11069 |
. . . . . . . . 9
|
73 | 72, 47 | syl 17 |
. . . . . . . 8
ψ |
74 | 69, 73 | readdcld 10069 |
. . . . . . 7
ψ |
75 | 67, 74 | remulcld 10070 |
. . . . . 6
Λ ψ |
76 | 65, 75 | fsumrecl 14465 |
. . . . 5
Λ ψ |
77 | 27 | a1i 11 |
. . . . . 6
|
78 | 25 | adantr 481 |
. . . . . . . 8
|
79 | 4 | adantr 481 |
. . . . . . . . 9
|
80 | | simprr 796 |
. . . . . . . . 9
|
81 | 79, 70, 80 | ltled 10185 |
. . . . . . . 8
|
82 | 70, 78, 81 | rpgecld 11911 |
. . . . . . 7
|
83 | 82 | relogcld 24369 |
. . . . . 6
|
84 | 77, 83 | remulcld 10070 |
. . . . 5
|
85 | 76, 84 | readdcld 10069 |
. . . 4
Λ ψ |
86 | 62 | recnd 10068 |
. . . . . 6
Λ ψ
|
87 | 63 | recnd 10068 |
. . . . . 6
|
88 | 86, 87 | abs2dif2d 14197 |
. . . . 5
Λ ψ
Λ ψ |
89 | 21 | adantr 481 |
. . . . . . . 8
Λ ψ |
90 | | vmage0 24847 |
. . . . . . . . . . . 12
Λ |
91 | 10, 90 | syl 17 |
. . . . . . . . . . 11
Λ |
92 | 10 | nnred 11035 |
. . . . . . . . . . . . 13
|
93 | 10 | nnge1d 11063 |
. . . . . . . . . . . . 13
|
94 | 92, 93 | logge0d 24376 |
. . . . . . . . . . . 12
|
95 | | chpge0 24852 |
. . . . . . . . . . . . 13
ψ |
96 | 16, 95 | syl 17 |
. . . . . . . . . . . 12
ψ |
97 | 14, 18, 94, 96 | addge0d 10603 |
. . . . . . . . . . 11
ψ
|
98 | 12, 19, 91, 97 | mulge0d 10604 |
. . . . . . . . . 10
Λ ψ
|
99 | 8, 20, 98 | fsumge0 14527 |
. . . . . . . . 9
Λ ψ
|
100 | 99 | adantr 481 |
. . . . . . . 8
Λ ψ
|
101 | 89, 78, 100 | divge0d 11912 |
. . . . . . 7
Λ ψ
|
102 | 62, 101 | absidd 14161 |
. . . . . 6
Λ ψ Λ ψ |
103 | 78 | relogcld 24369 |
. . . . . . . 8
|
104 | | 2rp 11837 |
. . . . . . . . 9
|
105 | | rpge0 11845 |
. . . . . . . . 9
|
106 | 104, 105 | mp1i 13 |
. . . . . . . 8
|
107 | 24 | adantr 481 |
. . . . . . . . 9
|
108 | 79, 107 | logge0d 24376 |
. . . . . . . 8
|
109 | 77, 103, 106, 108 | mulge0d 10604 |
. . . . . . 7
|
110 | 63, 109 | absidd 14161 |
. . . . . 6
|
111 | 102, 110 | oveq12d 6668 |
. . . . 5
Λ ψ
Λ ψ
|
112 | 88, 111 | breqtrd 4679 |
. . . 4
Λ ψ
Λ ψ
|
113 | 22 | a1i 11 |
. . . . . . 7
|
114 | 79 | adantr 481 |
. . . . . . . . . . . . 13
|
115 | 114, 66 | nndivred 11069 |
. . . . . . . . . . . 12
|
116 | 115, 17 | syl 17 |
. . . . . . . . . . 11
ψ |
117 | 69, 116 | readdcld 10069 |
. . . . . . . . . 10
ψ |
118 | 67, 117 | remulcld 10070 |
. . . . . . . . 9
Λ ψ |
119 | 65, 118 | fsumrecl 14465 |
. . . . . . . 8
Λ ψ |
120 | 66, 90 | syl 17 |
. . . . . . . . . 10
Λ |
121 | 66 | nnred 11035 |
. . . . . . . . . . . 12
|
122 | 66 | nnge1d 11063 |
. . . . . . . . . . . 12
|
123 | 121, 122 | logge0d 24376 |
. . . . . . . . . . 11
|
124 | 115, 95 | syl 17 |
. . . . . . . . . . 11
ψ |
125 | 69, 116, 123, 124 | addge0d 10603 |
. . . . . . . . . 10
ψ
|
126 | 67, 117, 120, 125 | mulge0d 10604 |
. . . . . . . . 9
Λ ψ
|
127 | | flword2 12614 |
. . . . . . . . . . 11
|
128 | 79, 70, 81, 127 | syl3anc 1326 |
. . . . . . . . . 10
|
129 | | fzss2 12381 |
. . . . . . . . . 10
|
130 | 128, 129 | syl 17 |
. . . . . . . . 9
|
131 | 65, 118, 126, 130 | fsumless 14528 |
. . . . . . . 8
Λ ψ Λ ψ
|
132 | 81 | adantr 481 |
. . . . . . . . . . . . 13
|
133 | 114, 71, 68, 132 | lediv1dd 11930 |
. . . . . . . . . . . 12
|
134 | | chpwordi 24883 |
. . . . . . . . . . . 12
ψ ψ |
135 | 115, 72, 133, 134 | syl3anc 1326 |
. . . . . . . . . . 11
ψ
ψ |
136 | 116, 73, 69, 135 | leadd2dd 10642 |
. . . . . . . . . 10
ψ ψ |
137 | 117, 74, 67, 120, 136 | lemul2ad 10964 |
. . . . . . . . 9
Λ ψ Λ ψ |
138 | 65, 118, 75, 137 | fsumle 14531 |
. . . . . . . 8
Λ ψ Λ ψ |
139 | 89, 119, 76, 131, 138 | letrd 10194 |
. . . . . . 7
Λ ψ Λ ψ |
140 | 89, 76, 113, 79, 100, 139, 107 | lediv12ad 11931 |
. . . . . 6
Λ ψ
Λ ψ |
141 | 76 | recnd 10068 |
. . . . . . 7
Λ ψ |
142 | 141 | div1d 10793 |
. . . . . 6
Λ ψ
Λ ψ |
143 | 140, 142 | breqtrd 4679 |
. . . . 5
Λ ψ
Λ ψ |
144 | 78, 82 | logled 24373 |
. . . . . . 7
|
145 | 81, 144 | mpbid 222 |
. . . . . 6
|
146 | 103, 83, 77, 106, 145 | lemul2ad 10964 |
. . . . 5
|
147 | 62, 63, 76, 84, 143, 146 | le2addd 10646 |
. . . 4
Λ ψ
Λ ψ |
148 | 61, 64, 85, 112, 147 | letrd 10194 |
. . 3
Λ ψ
Λ ψ |
149 | 6, 7, 32, 37, 58, 148 | o1bddrp 14273 |
. 2
Λ ψ
|
150 | 149 | trud 1493 |
1
Λ ψ
|