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