Step | Hyp | Ref
| Expression |
1 | | zre 11381 |
. . 3
|
2 | | chtval 24836 |
. . 3
|
3 | 1, 2 | syl 17 |
. 2
|
4 | | nnz 11399 |
. . . . . . 7
|
5 | | ppisval 24830 |
. . . . . . . . 9
|
6 | 1, 5 | syl 17 |
. . . . . . . 8
|
7 | | flid 12609 |
. . . . . . . . . 10
|
8 | 7 | oveq2d 6666 |
. . . . . . . . 9
|
9 | 8 | ineq1d 3813 |
. . . . . . . 8
|
10 | 6, 9 | eqtrd 2656 |
. . . . . . 7
|
11 | 4, 10 | syl 17 |
. . . . . 6
|
12 | | 2nn 11185 |
. . . . . . . . . . . . 13
|
13 | | nnuz 11723 |
. . . . . . . . . . . . 13
|
14 | 12, 13 | eleqtri 2699 |
. . . . . . . . . . . 12
|
15 | | fzss1 12380 |
. . . . . . . . . . . 12
|
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . 11
|
17 | | ssdif0 3942 |
. . . . . . . . . . 11
|
18 | 16, 17 | mpbi 220 |
. . . . . . . . . 10
|
19 | 18 | ineq1i 3810 |
. . . . . . . . 9
|
20 | | 0in 3969 |
. . . . . . . . 9
|
21 | 19, 20 | eqtri 2644 |
. . . . . . . 8
|
22 | 21 | a1i 11 |
. . . . . . 7
|
23 | 13 | eleq2i 2693 |
. . . . . . . . . . . . 13
|
24 | | fzpred 12389 |
. . . . . . . . . . . . 13
|
25 | 23, 24 | sylbi 207 |
. . . . . . . . . . . 12
|
26 | 25 | eqcomd 2628 |
. . . . . . . . . . 11
|
27 | | 1p1e2 11134 |
. . . . . . . . . . . . 13
|
28 | 27 | oveq1i 6660 |
. . . . . . . . . . . 12
|
29 | 28 | a1i 11 |
. . . . . . . . . . 11
|
30 | 26, 29 | difeq12d 3729 |
. . . . . . . . . 10
|
31 | | difun2 4048 |
. . . . . . . . . . 11
|
32 | | fzpreddisj 12390 |
. . . . . . . . . . . . 13
|
33 | 23, 32 | sylbi 207 |
. . . . . . . . . . . 12
|
34 | | disjdif2 4047 |
. . . . . . . . . . . 12
|
35 | 33, 34 | syl 17 |
. . . . . . . . . . 11
|
36 | 31, 35 | syl5eq 2668 |
. . . . . . . . . 10
|
37 | 30, 36 | eqtr3d 2658 |
. . . . . . . . 9
|
38 | 37 | ineq1d 3813 |
. . . . . . . 8
|
39 | | incom 3805 |
. . . . . . . . 9
|
40 | | 1nprm 15392 |
. . . . . . . . . 10
|
41 | | disjsn 4246 |
. . . . . . . . . 10
|
42 | 40, 41 | mpbir 221 |
. . . . . . . . 9
|
43 | 39, 42 | eqtr3i 2646 |
. . . . . . . 8
|
44 | 38, 43 | syl6eq 2672 |
. . . . . . 7
|
45 | | difininv 29354 |
. . . . . . 7
|
46 | 22, 44, 45 | syl2anc 693 |
. . . . . 6
|
47 | 11, 46 | eqtrd 2656 |
. . . . 5
|
48 | 47 | adantl 482 |
. . . 4
|
49 | | znnnlt1 11404 |
. . . . . 6
|
50 | 49 | biimpa 501 |
. . . . 5
|
51 | | incom 3805 |
. . . . . . 7
|
52 | | isprm3 15396 |
. . . . . . . . . . 11
|
53 | 52 | simplbi 476 |
. . . . . . . . . 10
|
54 | 53 | ssriv 3607 |
. . . . . . . . 9
|
55 | 12 | nnzi 11401 |
. . . . . . . . . 10
|
56 | | uzssico 29546 |
. . . . . . . . . 10
|
57 | 55, 56 | ax-mp 5 |
. . . . . . . . 9
|
58 | 54, 57 | sstri 3612 |
. . . . . . . 8
|
59 | | incom 3805 |
. . . . . . . . 9
|
60 | | 0xr 10086 |
. . . . . . . . . . . 12
|
61 | 60 | a1i 11 |
. . . . . . . . . . 11
|
62 | 12 | nnrei 11029 |
. . . . . . . . . . . . 13
|
63 | 62 | rexri 10097 |
. . . . . . . . . . . 12
|
64 | 63 | a1i 11 |
. . . . . . . . . . 11
|
65 | | 0le0 11110 |
. . . . . . . . . . . 12
|
66 | 65 | a1i 11 |
. . . . . . . . . . 11
|
67 | 1 | adantr 481 |
. . . . . . . . . . . 12
|
68 | | 1red 10055 |
. . . . . . . . . . . 12
|
69 | 62 | a1i 11 |
. . . . . . . . . . . 12
|
70 | | simpr 477 |
. . . . . . . . . . . 12
|
71 | | 1lt2 11194 |
. . . . . . . . . . . . 13
|
72 | 71 | a1i 11 |
. . . . . . . . . . . 12
|
73 | 67, 68, 69, 70, 72 | lttrd 10198 |
. . . . . . . . . . 11
|
74 | | iccssico 12245 |
. . . . . . . . . . 11
|
75 | 61, 64, 66, 73, 74 | syl22anc 1327 |
. . . . . . . . . 10
|
76 | | pnfxr 10092 |
. . . . . . . . . . 11
|
77 | | icodisj 12297 |
. . . . . . . . . . 11
|
78 | 60, 63, 76, 77 | mp3an 1424 |
. . . . . . . . . 10
|
79 | | ssdisj 4026 |
. . . . . . . . . 10
|
80 | 75, 78, 79 | sylancl 694 |
. . . . . . . . 9
|
81 | 59, 80 | syl5eqr 2670 |
. . . . . . . 8
|
82 | | ssdisj 4026 |
. . . . . . . 8
|
83 | 58, 81, 82 | sylancr 695 |
. . . . . . 7
|
84 | 51, 83 | syl5eq 2668 |
. . . . . 6
|
85 | | 1zzd 11408 |
. . . . . . . . 9
|
86 | | simpl 473 |
. . . . . . . . 9
|
87 | | fzn 12357 |
. . . . . . . . . 10
|
88 | 87 | biimpa 501 |
. . . . . . . . 9
|
89 | 85, 86, 70, 88 | syl21anc 1325 |
. . . . . . . 8
|
90 | 89 | ineq1d 3813 |
. . . . . . 7
|
91 | 90, 20 | syl6eq 2672 |
. . . . . 6
|
92 | 84, 91 | eqtr4d 2659 |
. . . . 5
|
93 | 50, 92 | syldan 487 |
. . . 4
|
94 | | exmidd 432 |
. . . 4
|
95 | 48, 93, 94 | mpjaodan 827 |
. . 3
|
96 | 95 | sumeq1d 14431 |
. 2
|
97 | 3, 96 | eqtrd 2656 |
1
|