Step | Hyp | Ref
| Expression |
1 | | iccpartgtprec.m |
. 2
|
2 | | ral0 4076 |
. . . . 5
|
3 | | oveq2 6658 |
. . . . . . 7
..^ ..^ |
4 | | fzo0 12492 |
. . . . . . 7
..^ |
5 | 3, 4 | syl6eq 2672 |
. . . . . 6
..^ |
6 | | fveq2 6191 |
. . . . . . 7
|
7 | 6 | breq2d 4665 |
. . . . . 6
|
8 | 5, 7 | raleqbidv 3152 |
. . . . 5
..^
|
9 | 2, 8 | mpbiri 248 |
. . . 4
..^
|
10 | 9 | 2a1d 26 |
. . 3
..^
|
11 | | simpr 477 |
. . . . . . 7
|
12 | | iccpartgtprec.p |
. . . . . . . . 9
RePart |
13 | 12 | adantr 481 |
. . . . . . . 8
RePart |
14 | 13 | adantr 481 |
. . . . . . 7
RePart |
15 | | nnnn0 11299 |
. . . . . . . . 9
|
16 | | nn0fz0 12437 |
. . . . . . . . 9
|
17 | 15, 16 | sylib 208 |
. . . . . . . 8
|
18 | 17 | adantl 482 |
. . . . . . 7
|
19 | 11, 14, 18 | iccpartxr 41355 |
. . . . . 6
|
20 | | elxr 11950 |
. . . . . . 7
|
21 | | elfzoelz 12470 |
. . . . . . . . . . . . . 14
..^
|
22 | 21 | ad2antll 765 |
. . . . . . . . . . . . 13
..^ |
23 | | elfzo2 12473 |
. . . . . . . . . . . . . . 15
..^
|
24 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . . 18
|
25 | 24 | peano2zd 11485 |
. . . . . . . . . . . . . . . . 17
|
26 | 25 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
|
27 | | simp2 1062 |
. . . . . . . . . . . . . . . 16
|
28 | | zltp1le 11427 |
. . . . . . . . . . . . . . . . . 18
|
29 | 24, 28 | sylan 488 |
. . . . . . . . . . . . . . . . 17
|
30 | 29 | biimp3a 1432 |
. . . . . . . . . . . . . . . 16
|
31 | | eluz2 11693 |
. . . . . . . . . . . . . . . 16
|
32 | 26, 27, 30, 31 | syl3anbrc 1246 |
. . . . . . . . . . . . . . 15
|
33 | 23, 32 | sylbi 207 |
. . . . . . . . . . . . . 14
..^
|
34 | 33 | ad2antll 765 |
. . . . . . . . . . . . 13
..^ |
35 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
36 | 35 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 36 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
|
38 | 37 | biimpcd 239 |
. . . . . . . . . . . . . . . . 17
|
39 | 38 | adantr 481 |
. . . . . . . . . . . . . . . 16
..^ |
40 | 39 | adantr 481 |
. . . . . . . . . . . . . . 15
..^ |
41 | 40 | com12 32 |
. . . . . . . . . . . . . 14
..^ |
42 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
..^
|
43 | 42 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
..^ |
44 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . 17
..^ |
45 | 44 | adantl 482 |
. . . . . . . . . . . . . . . 16
..^
|
46 | 14 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
..^
RePart |
47 | 46 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
..^ RePart |
48 | 47 | adantr 481 |
. . . . . . . . . . . . . . . . 17
..^ RePart |
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . . 16
..^
RePart |
50 | | elfz2 12333 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
51 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
52 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
53 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
55 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
56 | 55 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
57 | | letr 10131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
58 | 52, 54, 56, 57 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
59 | 58 | expcomd 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
60 | 59 | adantrd 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
61 | 60 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
62 | 61 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
63 | 62 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
64 | 63 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
65 | 51, 64 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
66 | 65 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
67 | 23, 66 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^
|
68 | 50, 67 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
|
69 | 68 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
70 | 69 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
71 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
72 | 71, 55 | anim12ci 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
73 | 72 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
74 | | ltlen 10138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
76 | | nesym 2850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
77 | 76 | anbi2i 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
78 | 75, 77 | syl6rbb 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
79 | 78 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
80 | 79 | expd 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
81 | 80 | adantld 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
82 | 81 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
83 | 50, 82 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
84 | 83 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
85 | 84 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
86 | 70, 85 | jca 554 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
87 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
88 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
89 | | elfzel2 12340 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
90 | 87, 88, 89 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
91 | 90 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
92 | | elfzo 12472 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^
|
94 | 86, 93 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
95 | 94 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
96 | 95 | ad2antll 765 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
97 | 96 | imp 445 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
98 | 97 | impcom 446 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
99 | 45, 49, 98 | iccpartipre 41357 |
. . . . . . . . . . . . . . 15
..^ |
100 | 99 | ex 450 |
. . . . . . . . . . . . . 14
..^ |
101 | 41, 100 | pm2.61i 176 |
. . . . . . . . . . . . 13
..^ |
102 | 43 | adantr 481 |
. . . . . . . . . . . . . . 15
..^
|
103 | 47 | adantr 481 |
. . . . . . . . . . . . . . 15
..^
RePart |
104 | | 1eluzge0 11732 |
. . . . . . . . . . . . . . . . . . . 20
|
105 | | fzoss1 12495 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
106 | 104, 105 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ ..^ |
107 | | elfzoel2 12469 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
|
108 | | fzoval 12471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
|
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
..^ |
110 | 109 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
..^ |
111 | 110 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^ |
112 | | elfzouz 12474 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
113 | | fzoss1 12495 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ ..^ |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
..^ ..^ |
115 | 114 | sseld 3602 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^ ..^ |
116 | 111, 115 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
117 | 116 | imp 445 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
118 | 106, 117 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
119 | 118 | ex 450 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
120 | 119 | ad2antll 765 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
121 | 120 | imp 445 |
. . . . . . . . . . . . . . 15
..^
..^ |
122 | | iccpartimp 41353 |
. . . . . . . . . . . . . . 15
RePart
..^
|
123 | 102, 103,
121, 122 | syl3anc 1326 |
. . . . . . . . . . . . . 14
..^
|
124 | 123 | simprd 479 |
. . . . . . . . . . . . 13
..^
|
125 | 22, 34, 101, 124 | smonoord 41341 |
. . . . . . . . . . . 12
..^ |
126 | 125 | ex 450 |
. . . . . . . . . . 11
..^
|
127 | | simpr 477 |
. . . . . . . . . . . . . 14
..^
..^ |
128 | 42, 46, 127 | iccpartipre 41357 |
. . . . . . . . . . . . 13
..^
|
129 | | ltpnf 11954 |
. . . . . . . . . . . . 13
|
130 | 128, 129 | syl 17 |
. . . . . . . . . . . 12
..^
|
131 | | breq2 4657 |
. . . . . . . . . . . 12
|
132 | 130, 131 | syl5ibr 236 |
. . . . . . . . . . 11
..^
|
133 | 42 | adantl 482 |
. . . . . . . . . . . . . . 15
..^ |
134 | 46 | adantl 482 |
. . . . . . . . . . . . . . 15
..^ RePart |
135 | | elfzofz 12485 |
. . . . . . . . . . . . . . . . 17
..^
|
136 | 135 | ad2antll 765 |
. . . . . . . . . . . . . . . 16
..^ |
137 | | elfzubelfz 12353 |
. . . . . . . . . . . . . . . 16
|
138 | 136, 137 | syl 17 |
. . . . . . . . . . . . . . 15
..^ |
139 | 133, 134,
138 | iccpartgtprec 41356 |
. . . . . . . . . . . . . 14
..^ |
140 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
|
141 | 140 | eqcoms 2630 |
. . . . . . . . . . . . . . 15
|
142 | 141 | adantr 481 |
. . . . . . . . . . . . . 14
..^
|
143 | 139, 142 | mpbird 247 |
. . . . . . . . . . . . 13
..^ |
144 | 15 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
145 | 144 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
..^
|
146 | | nnne0 11053 |
. . . . . . . . . . . . . . . . . . . . . 22
|
147 | 146 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
148 | | df-ne 2795 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
149 | 148 | biimpri 218 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
150 | 149 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
151 | 150 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
152 | 144, 147,
151 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . 20
|
153 | 152 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
..^
|
154 | | nn0n0n1ge2 11358 |
. . . . . . . . . . . . . . . . . . 19
|
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . . . . . . 18
..^
|
156 | 145, 155 | jca 554 |
. . . . . . . . . . . . . . . . 17
..^
|
157 | 156 | adantl 482 |
. . . . . . . . . . . . . . . 16
..^
|
158 | | ige2m1fz 12430 |
. . . . . . . . . . . . . . . 16
|
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . . 15
..^
|
160 | 133, 134,
159 | iccpartxr 41355 |
. . . . . . . . . . . . . 14
..^ |
161 | | nltmnf 11963 |
. . . . . . . . . . . . . 14
|
162 | 160, 161 | syl 17 |
. . . . . . . . . . . . 13
..^ |
163 | 143, 162 | pm2.21dd 186 |
. . . . . . . . . . . 12
..^ |
164 | 163 | ex 450 |
. . . . . . . . . . 11
..^
|
165 | 126, 132,
164 | 3jaoi 1391 |
. . . . . . . . . 10
..^
|
166 | 165 | impl 650 |
. . . . . . . . 9
..^ |
167 | 166 | ralrimiva 2966 |
. . . . . . . 8
..^
|
168 | 167 | ex 450 |
. . . . . . 7
..^
|
169 | 20, 168 | sylbi 207 |
. . . . . 6
..^ |
170 | 19, 169 | mpcom 38 |
. . . . 5
..^ |
171 | 170 | ex 450 |
. . . 4
..^ |
172 | 171 | expcom 451 |
. . 3
..^
|
173 | 10, 172 | pm2.61i 176 |
. 2
..^ |
174 | 1, 173 | mpd 15 |
1
..^ |