Step | Hyp | Ref
| Expression |
1 | | iseralt.1 |
. 2
|
2 | | seqex 12803 |
. . 3
|
3 | 2 | a1i 11 |
. 2
|
4 | | iseralt.5 |
. . . 4
|
5 | | iseralt.2 |
. . . . 5
|
6 | | climrel 14223 |
. . . . . . 7
|
7 | 6 | brrelexi 5158 |
. . . . . 6
|
8 | 4, 7 | syl 17 |
. . . . 5
|
9 | | eqidd 2623 |
. . . . 5
|
10 | | iseralt.3 |
. . . . . . 7
|
11 | 10 | ffvelrnda 6359 |
. . . . . 6
|
12 | 11 | recnd 10068 |
. . . . 5
|
13 | 1, 5, 8, 9, 12 | clim0c 14238 |
. . . 4
|
14 | 4, 13 | mpbid 222 |
. . 3
|
15 | | simpr 477 |
. . . . . . . . 9
|
16 | 15, 1 | syl6eleq 2711 |
. . . . . . . 8
|
17 | | eluzelz 11697 |
. . . . . . . 8
|
18 | | uzid 11702 |
. . . . . . . 8
|
19 | 16, 17, 18 | 3syl 18 |
. . . . . . 7
|
20 | | peano2uz 11741 |
. . . . . . 7
|
21 | | fveq2 6191 |
. . . . . . . . . 10
|
22 | 21 | fveq2d 6195 |
. . . . . . . . 9
|
23 | 22 | breq1d 4663 |
. . . . . . . 8
|
24 | 23 | rspcv 3305 |
. . . . . . 7
|
25 | 19, 20, 24 | 3syl 18 |
. . . . . 6
|
26 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
27 | 26 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
28 | 27 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . 22
|
29 | 17, 1 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
30 | 29 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
31 | 30 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . 22
|
32 | 28, 31 | subcld 10392 |
. . . . . . . . . . . . . . . . . . . . 21
|
33 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . . . 22
|
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | 32, 33, 35 | divcan2d 10803 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | 36 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
38 | 31, 28 | pncan3d 10395 |
. . . . . . . . . . . . . . . . . . 19
|
39 | 37, 38 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . 18
|
40 | 39 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
41 | 40 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
42 | 41 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
43 | 42 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
44 | | simpll 790 |
. . . . . . . . . . . . . . 15
|
45 | | simpl 473 |
. . . . . . . . . . . . . . . 16
|
46 | 45 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
|
47 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
48 | 27, 30 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . . 19
|
49 | 48 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
|
50 | | eluzle 11700 |
. . . . . . . . . . . . . . . . . . . 20
|
51 | 50 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 27 | zred 11482 |
. . . . . . . . . . . . . . . . . . . 20
|
53 | 30 | zred 11482 |
. . . . . . . . . . . . . . . . . . . 20
|
54 | 52, 53 | subge0d 10617 |
. . . . . . . . . . . . . . . . . . 19
|
55 | 51, 54 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
|
56 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . 19
|
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
58 | | 2pos 11112 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
60 | | divge0 10892 |
. . . . . . . . . . . . . . . . . 18
|
61 | 49, 55, 57, 59, 60 | syl22anc 1327 |
. . . . . . . . . . . . . . . . 17
|
62 | 61 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
63 | | elnn0z 11390 |
. . . . . . . . . . . . . . . 16
|
64 | 47, 62, 63 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
|
65 | | iseralt.4 |
. . . . . . . . . . . . . . . . 17
|
66 | | iseralt.6 |
. . . . . . . . . . . . . . . . 17
|
67 | 1, 5, 10, 65, 4, 66 | iseraltlem3 14414 |
. . . . . . . . . . . . . . . 16
|
68 | 67 | simpld 475 |
. . . . . . . . . . . . . . 15
|
69 | 44, 46, 64, 68 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
70 | 43, 69 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
|
71 | | 2div2e1 11150 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
72 | 71 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
73 | | peano2cn 10208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
74 | 32, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
75 | 74, 33, 33, 35 | divsubdird 10840 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
76 | | df-2 11079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
77 | 76 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
78 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
80 | 32, 79, 79 | pnpcan2d 10430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
81 | 77, 80 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
82 | 81 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
83 | 75, 82 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
84 | 72, 83 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
85 | 84 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
86 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
87 | 32, 78, 86 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
88 | 87, 33, 35 | divcan2d 10803 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
89 | 28, 31, 79 | sub32d 10424 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
90 | 85, 88, 89 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . . . 22
|
91 | 90 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
|
92 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
93 | 28, 78, 92 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
|
94 | 31, 93 | pncan3d 10395 |
. . . . . . . . . . . . . . . . . . . . 21
|
95 | 91, 94 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
|
96 | 95 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
|
97 | | npcan 10290 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | 28, 78, 97 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
|
99 | 96, 98 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . 18
|
100 | 99 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
101 | 100 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
102 | 101 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
103 | 102 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
104 | | simpll 790 |
. . . . . . . . . . . . . . 15
|
105 | 45 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
|
106 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
107 | | uznn0sub 11719 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
108 | 107 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . 22
|
109 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . . . . . . 22
|
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
111 | 110 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . 20
|
112 | 111 | rphalfcld 11884 |
. . . . . . . . . . . . . . . . . . 19
|
113 | 112 | rpgt0d 11875 |
. . . . . . . . . . . . . . . . . 18
|
114 | 113 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
115 | | elnnz 11387 |
. . . . . . . . . . . . . . . . 17
|
116 | 106, 114,
115 | sylanbrc 698 |
. . . . . . . . . . . . . . . 16
|
117 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . 16
|
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . 15
|
119 | 1, 5, 10, 65, 4, 66 | iseraltlem3 14414 |
. . . . . . . . . . . . . . . 16
|
120 | 119 | simprd 479 |
. . . . . . . . . . . . . . 15
|
121 | 104, 105,
118, 120 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
122 | 103, 121 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
|
123 | | zeo 11463 |
. . . . . . . . . . . . . 14
|
124 | 48, 123 | syl 17 |
. . . . . . . . . . . . 13
|
125 | 70, 122, 124 | mpjaodan 827 |
. . . . . . . . . . . 12
|
126 | 1 | peano2uzs 11742 |
. . . . . . . . . . . . . . 15
|
127 | 126 | adantr 481 |
. . . . . . . . . . . . . 14
|
128 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
|
129 | 10, 127, 128 | syl2an 494 |
. . . . . . . . . . . . 13
|
130 | 1, 5, 10, 65, 4 | iseraltlem1 14412 |
. . . . . . . . . . . . . 14
|
131 | 127, 130 | sylan2 491 |
. . . . . . . . . . . . 13
|
132 | 129, 131 | absidd 14161 |
. . . . . . . . . . . 12
|
133 | 125, 132 | breqtrrd 4681 |
. . . . . . . . . . 11
|
134 | 133 | adantlr 751 |
. . . . . . . . . 10
|
135 | | neg1rr 11125 |
. . . . . . . . . . . . . . . . . . . . 21
|
136 | 135 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
137 | | neg1ne0 11126 |
. . . . . . . . . . . . . . . . . . . . 21
|
138 | 137 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
139 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . . . . . . 22
|
140 | 139, 1 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . 21
|
141 | 140 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
142 | 136, 138,
141 | reexpclzd 13034 |
. . . . . . . . . . . . . . . . . . 19
|
143 | 10 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . 19
|
144 | 142, 143 | remulcld 10070 |
. . . . . . . . . . . . . . . . . 18
|
145 | 66, 144 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
|
146 | 1, 5, 145 | serfre 12830 |
. . . . . . . . . . . . . . . 16
|
147 | 1 | uztrn2 11705 |
. . . . . . . . . . . . . . . 16
|
148 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . 16
|
149 | 146, 147,
148 | syl2an 494 |
. . . . . . . . . . . . . . 15
|
150 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . 16
|
151 | 146, 45, 150 | syl2an 494 |
. . . . . . . . . . . . . . 15
|
152 | 149, 151 | resubcld 10458 |
. . . . . . . . . . . . . 14
|
153 | 152 | recnd 10068 |
. . . . . . . . . . . . 13
|
154 | 153 | abscld 14175 |
. . . . . . . . . . . 12
|
155 | 154 | adantlr 751 |
. . . . . . . . . . 11
|
156 | 132, 129 | eqeltrd 2701 |
. . . . . . . . . . . 12
|
157 | 156 | adantlr 751 |
. . . . . . . . . . 11
|
158 | | rpre 11839 |
. . . . . . . . . . . 12
|
159 | 158 | ad2antlr 763 |
. . . . . . . . . . 11
|
160 | | lelttr 10128 |
. . . . . . . . . . 11
|
161 | 155, 157,
159, 160 | syl3anc 1326 |
. . . . . . . . . 10
|
162 | 134, 161 | mpand 711 |
. . . . . . . . 9
|
163 | 146 | adantr 481 |
. . . . . . . . . 10
|
164 | 163, 147,
148 | syl2an 494 |
. . . . . . . . 9
|
165 | 162, 164 | jctild 566 |
. . . . . . . 8
|
166 | 165 | anassrs 680 |
. . . . . . 7
|
167 | 166 | ralrimdva 2969 |
. . . . . 6
|
168 | 25, 167 | syld 47 |
. . . . 5
|
169 | 168 | reximdva 3017 |
. . . 4
|
170 | 169 | ralimdva 2962 |
. . 3
|
171 | 14, 170 | mpd 15 |
. 2
|
172 | 1, 3, 171 | caurcvg2 14408 |
1
|