Step Hyp Ref
Expression 1 swrdccatin12.l . . . . . . . 8
2 oveq1 6303 . . . . . . . . . 10
3 2 eleq2d 2527 . . . . . . . . 9
4 id 22 . . . . . . . . . . 11
5 oveq1 6303 . . . . . . . . . . 11
6 4 , 5 oveq12d 6314 . . . . . . . . . 10
7 6 eleq2d 2527 . . . . . . . . 9
8 3 , 7 anbi12d 710 . . . . . . . 8
9 1 , 8 ax-mp 5 . . . . . . 7
10 lencl 12562 . . . . . . . . 9
11 elnn0uz 11147 . . . . . . . . . . . . 13
12 11 biimpi 194 . . . . . . . . . . . 12
13 fzss1 11751 . . . . . . . . . . . 12
14 12 , 13 syl 16 . . . . . . . . . . 11
15 14 sseld 3502 . . . . . . . . . 10
16 fzss1 11751 . . . . . . . . . . . 12
17 12 , 16 syl 16 . . . . . . . . . . 11
18 17 sseld 3502 . . . . . . . . . 10
19 15 , 18 anim12d 563 . . . . . . . . 9
20 10 , 19 syl 16 . . . . . . . 8
21 20 adantr 465 . . . . . . 7
22 9 , 21 syl5bi 217 . . . . . 6
23 22 imp 429 . . . . 5
24 swrdccatfn 12707 . . . . 5
25 23 , 24 syldan 470 . . . 4
26 elfz2 11708 . . . . . . . . . 10
27 zcn 10894 . . . . . . . . . . . . 13
28 zcn 10894 . . . . . . . . . . . . 13
29 zcn 10894 . . . . . . . . . . . . 13
30 27 , 28 , 29 3anim123i 1181 . . . . . . . . . . . 12
31 30 3comr 1204 . . . . . . . . . . 11
32 31 adantr 465 . . . . . . . . . 10
33 26 , 32 sylbi 195 . . . . . . . . 9
34 33 adantr 465 . . . . . . . 8
35 nnncan2 9879 . . . . . . . 8
36 34 , 35 syl 16 . . . . . . 7
37 36 adantl 466 . . . . . 6
38 37 oveq2d 6312 . . . . 5
39 38 fneq2d 5677 . . . 4
40 25 , 39 mpbird 232 . . 3
41 simpr 461 . . . . 5
42 41 adantr 465 . . . 4
43 elfzmlbm 11813 . . . . 5
44 43 ad2antrl 727 . . . 4
45 lencl 12562 . . . . . . . . . 10
46 45 nn0zd 10992 . . . . . . . . 9
47 46 adantl 466 . . . . . . . 8
48 elfzmlbp 11815 . . . . . . . . 9
49 48 ex 434 . . . . . . . 8
50 47 , 49 syl 16 . . . . . . 7
51 50 com12 31 . . . . . 6
52 51 adantl 466 . . . . 5
53 52 impcom 430 . . . 4
54 swrdvalfn 12663 . . . 4
55 42 , 44 , 53 , 54 syl3anc 1228 . . 3
56 simpl 457 . . . . . . . 8
57 56 adantr 465 . . . . . . 7
58 elfzoelz 11829 . . . . . . . . 9
59 elfzelz 11717 . . . . . . . . . . 11
60 zaddcl 10929 . . . . . . . . . . . 12
61 60 expcom 435 . . . . . . . . . . 11
62 59 , 61 syl 16 . . . . . . . . . 10
63 62 ad2antrl 727 . . . . . . . . 9
64 58 , 63 syl5com 30 . . . . . . . 8
65 64 impcom 430 . . . . . . 7
66 df-3an 975 . . . . . . 7
67 57 , 65 , 66 sylanbrc 664 . . . . . 6
68 ccatsymb 12600 . . . . . 6
69 67 , 68 syl 16 . . . . 5
70 elfzonn0 11867 . . . . . . . 8
71 zre 10893 . . . . . . . . . . . . . . . . . . 19
72 zre 10893 . . . . . . . . . . . . . . . . . . 19
73 71 , 72 anim12i 566 . . . . . . . . . . . . . . . . . 18
74 elnn0z 10902 . . . . . . . . . . . . . . . . . . 19
75 zre 10893 . . . . . . . . . . . . . . . . . . . 20
76 0red 9618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77 76 anim1i 568 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
78 77 ancoms 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
79 78 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26
80 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
81 80 anim2i 569 . . . . . . . . . . . . . . . . . . . . . . . . . 26
82 le2add 10059 . . . . . . . . . . . . . . . . . . . . . . . . . 26
83 79 , 81 , 82 syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25
84 recn 9603 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
85 84 addid2d 9802 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
86 85 ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . 26
87 86 breq1d 4462 . . . . . . . . . . . . . . . . . . . . . . . . 25
88 83 , 87 sylibd 214 . . . . . . . . . . . . . . . . . . . . . . . 24
89 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . 26
90 89 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25
91 readdcl 9596 . . . . . . . . . . . . . . . . . . . . . . . . . 26
92 81 , 91 syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
93 90 , 92 lenltd 9752 . . . . . . . . . . . . . . . . . . . . . . . 24
94 88 , 93 sylibd 214 . . . . . . . . . . . . . . . . . . . . . . 23
95 94 expd 436 . . . . . . . . . . . . . . . . . . . . . 22
96 95 com12 31 . . . . . . . . . . . . . . . . . . . . 21
97 96 expd 436 . . . . . . . . . . . . . . . . . . . 20
98 75 , 97 mpan9 469 . . . . . . . . . . . . . . . . . . 19
99 74 , 98 sylbi 195 . . . . . . . . . . . . . . . . . 18
100 73 , 99 mpan9 469 . . . . . . . . . . . . . . . . 17
101 1 eqcomi 2470 . . . . . . . . . . . . . . . . . . 19
102 101 breq2i 4460 . . . . . . . . . . . . . . . . . 18
103 102 notbii 296 . . . . . . . . . . . . . . . . 17
104 100 , 103 syl6ibr 227 . . . . . . . . . . . . . . . 16
105 104 ex 434 . . . . . . . . . . . . . . 15
106 105 com23 78 . . . . . . . . . . . . . 14
107 106 3adant2 1015 . . . . . . . . . . . . 13
108 107 com12 31 . . . . . . . . . . . 12
109 108 adantr 465 . . . . . . . . . . 11
110 109 impcom 430 . . . . . . . . . 10
111 26 , 110 sylbi 195 . . . . . . . . 9
112 111 ad2antrl 727 . . . . . . . 8
113 70 , 112 syl5com 30 . . . . . . 7
114 113 impcom 430 . . . . . 6
115 114 iffalsed 3952 . . . . 5
116 zcn 10894 . . . . . . . . . . . . . . . . 17
117 116 adantl 466 . . . . . . . . . . . . . . . 16
118 28 adantl 466 . . . . . . . . . . . . . . . . 17
119 118 adantr 465 . . . . . . . . . . . . . . . 16
120 29 ad2antrr 725 . . . . . . . . . . . . . . . 16
121 117 , 119 ,
120 addsubassd 9974 . . . . . . . . . . . . . . 15
122 oveq2 6304 . . . . . . . . . . . . . . . 16
123 122 eqeq1d 2459 . . . . . . . . . . . . . . 15
124 121 , 123 syl5ib 219 . . . . . . . . . . . . . 14
125 1 , 124 ax-mp 5 . . . . . . . . . . . . 13
126 125 ex 434 . . . . . . . . . . . 12
127 126 3adant2 1015 . . . . . . . . . . 11
128 127 adantr 465 . . . . . . . . . 10
129 26 , 128 sylbi 195 . . . . . . . . 9
130 129 ad2antrl 727 . . . . . . . 8
131 58 , 130 syl5com 30 . . . . . . 7
132 131 impcom 430 . . . . . 6
133 132 fveq2d 5875 . . . . 5
134 69 , 115 , 133 3eqtrd 2502 . . . 4
135 ccatcl 12593 . . . . . 6
136 135 ad2antrr 725 . . . . 5
137 1 , 12 syl5eqel 2549 . . . . . . . . . . . 12
138 fzss1 11751 . . . . . . . . . . . 12
139 10 , 137 , 138 3syl 20 . . . . . . . . . . 11
140 139 sseld 3502 . . . . . . . . . 10
141 140 adantr 465 . . . . . . . . 9
142 141 com12 31 . . . . . . . 8
143 142 adantr 465 . . . . . . 7
144 143 impcom 430 . . . . . 6
145 144 adantr 465 . . . . 5
146 1 , 7 ax-mp 5 . . . . . . . . 9
147 10 , 12 syl 16 . . . . . . . . . . . . . . 15
148 147 adantr 465 . . . . . . . . . . . . . 14
149 148 , 16 syl 16 . . . . . . . . . . . . 13
150 149 sseld 3502 . . . . . . . . . . . 12
151 150 impcom 430 . . . . . . . . . . 11
152 ccatlen 12594 . . . . . . . . . . . . . 14
153 152 oveq2d 6312 . . . . . . . . . . . . 13
154 153 eleq2d 2527 . . . . . . . . . . . 12
155 154 adantl 466 . . . . . . . . . . 11
156 151 , 155 mpbird 232 . . . . . . . . . 10
157 156 ex 434 . . . . . . . . 9
158 146 , 157 sylbi 195 . . . . . . . 8
159 158 adantl 466 . . . . . . 7
160 159 impcom 430 . . . . . 6
161 160 adantr 465 . . . . 5
162 fzmmmeqm 11746 . . . . . . . . . 10
163 162 oveq2d 6312 . . . . . . . . 9
164 163 eleq2d 2527 . . . . . . . 8
165 164 biimpd 207 . . . . . . 7
166 165 ad2antrl 727 . . . . . 6
167 166 imp 429 . . . . 5
168 swrdfv 12651 . . . . 5
169 136 , 145 ,
161 , 167 , 168 syl31anc 1231 . . . 4
170 46 , 49 syl 16 . . . . . . . . . 10
171 170 adantl 466 . . . . . . . . 9
172 171 com12 31 . . . . . . . 8
173 172 adantl 466 . . . . . . 7
174 173 impcom 430 . . . . . 6
175 42 , 44 , 174 3jca 1176 . . . . 5
176 swrdfv 12651 . . . . 5
177 175 , 176 sylan 471 . . . 4
178 134 , 169 ,
177 3eqtr4d 2508 . . 3
179 40 , 55 , 178 eqfnfvd 5984 . 2
