Step | Hyp | Ref
| Expression |
1 | | isercoll.z |
. . . . . . . . . . 11
|
2 | | uzssz 11129 |
. . . . . . . . . . 11
|
3 | 1, 2 | eqsstri 3533 |
. . . . . . . . . 10
|
4 | | zssre 10896 |
. . . . . . . . . 10
|
5 | 3, 4 | sstri 3512 |
. . . . . . . . 9
|
6 | | isercoll.g |
. . . . . . . . . . 11
|
7 | 6 | ad2antrr 725 |
. . . . . . . . . 10
|
8 | | simplrl 761 |
. . . . . . . . . 10
|
9 | 7, 8 | ffvelrnd 6032 |
. . . . . . . . 9
|
10 | 5, 9 | sseldi 3501 |
. . . . . . . 8
|
11 | | simplrr 762 |
. . . . . . . . 9
|
12 | 11 | nnred 10576 |
. . . . . . . 8
|
13 | 10, 12 | resubcld 10012 |
. . . . . . 7
|
14 | 8 | nnred 10576 |
. . . . . . . 8
|
15 | 10, 14 | resubcld 10012 |
. . . . . . 7
|
16 | 7, 11 | ffvelrnd 6032 |
. . . . . . . . 9
|
17 | 5, 16 | sseldi 3501 |
. . . . . . . 8
|
18 | 17, 12 | resubcld 10012 |
. . . . . . 7
|
19 | | simpr 461 |
. . . . . . . 8
|
20 | 14, 12, 10, 19 | ltsub2dd 10190 |
. . . . . . 7
|
21 | 8 | nnzd 10993 |
. . . . . . . . . 10
|
22 | 11 | nnzd 10993 |
. . . . . . . . . 10
|
23 | 14, 12, 19 | ltled 9754 |
. . . . . . . . . 10
|
24 | | eluz2 11116 |
. . . . . . . . . 10
|
25 | 21, 22, 23, 24 | syl3anbrc 1180 |
. . . . . . . . 9
|
26 | | elfzuz 11713 |
. . . . . . . . . 10
|
27 | | eluznn 11181 |
. . . . . . . . . . . 12
|
28 | 8, 27 | sylan 471 |
. . . . . . . . . . 11
|
29 | | fveq2 5871 |
. . . . . . . . . . . . . . 15
|
30 | | id 22 |
. . . . . . . . . . . . . . 15
|
31 | 29, 30 | oveq12d 6314 |
. . . . . . . . . . . . . 14
|
32 | | eqid 2457 |
. . . . . . . . . . . . . 14
|
33 | | ovex 6324 |
. . . . . . . . . . . . . 14
|
34 | 31, 32, 33 | fvmpt 5956 |
. . . . . . . . . . . . 13
|
35 | 34 | adantl 466 |
. . . . . . . . . . . 12
|
36 | 7 | ffvelrnda 6031 |
. . . . . . . . . . . . . 14
|
37 | 5, 36 | sseldi 3501 |
. . . . . . . . . . . . 13
|
38 | | nnre 10568 |
. . . . . . . . . . . . . 14
|
39 | 38 | adantl 466 |
. . . . . . . . . . . . 13
|
40 | 37, 39 | resubcld 10012 |
. . . . . . . . . . . 12
|
41 | 35, 40 | eqeltrd 2545 |
. . . . . . . . . . 11
|
42 | 28, 41 | syldan 470 |
. . . . . . . . . 10
|
43 | 26, 42 | sylan2 474 |
. . . . . . . . 9
|
44 | | elfzuz 11713 |
. . . . . . . . . 10
|
45 | | peano2nn 10573 |
. . . . . . . . . . . . . . . . 17
|
46 | | ffvelrn 6029 |
. . . . . . . . . . . . . . . . 17
|
47 | 7, 45, 46 | syl2an 477 |
. . . . . . . . . . . . . . . 16
|
48 | 5, 47 | sseldi 3501 |
. . . . . . . . . . . . . . 15
|
49 | | peano2rem 9909 |
. . . . . . . . . . . . . . 15
|
50 | 48, 49 | syl 16 |
. . . . . . . . . . . . . 14
|
51 | | simpll 753 |
. . . . . . . . . . . . . . . 16
|
52 | | isercoll.i |
. . . . . . . . . . . . . . . 16
|
53 | 51, 52 | sylan 471 |
. . . . . . . . . . . . . . 15
|
54 | 3, 36 | sseldi 3501 |
. . . . . . . . . . . . . . . 16
|
55 | 3, 47 | sseldi 3501 |
. . . . . . . . . . . . . . . 16
|
56 | | zltlem1 10941 |
. . . . . . . . . . . . . . . 16
|
57 | 54, 55, 56 | syl2anc 661 |
. . . . . . . . . . . . . . 15
|
58 | 53, 57 | mpbid 210 |
. . . . . . . . . . . . . 14
|
59 | 37, 50, 39, 58 | lesub1dd 10193 |
. . . . . . . . . . . . 13
|
60 | 48 | recnd 9643 |
. . . . . . . . . . . . . . 15
|
61 | | 1cnd 9633 |
. . . . . . . . . . . . . . 15
|
62 | 39 | recnd 9643 |
. . . . . . . . . . . . . . 15
|
63 | 60, 61, 62 | sub32d 9986 |
. . . . . . . . . . . . . 14
|
64 | 60, 62, 61 | subsub4d 9985 |
. . . . . . . . . . . . . 14
|
65 | 63, 64 | eqtrd 2498 |
. . . . . . . . . . . . 13
|
66 | 59, 65 | breqtrd 4476 |
. . . . . . . . . . . 12
|
67 | 45 | adantl 466 |
. . . . . . . . . . . . 13
|
68 | | fveq2 5871 |
. . . . . . . . . . . . . . 15
|
69 | | id 22 |
. . . . . . . . . . . . . . 15
|
70 | 68, 69 | oveq12d 6314 |
. . . . . . . . . . . . . 14
|
71 | | ovex 6324 |
. . . . . . . . . . . . . 14
|
72 | 70, 32, 71 | fvmpt 5956 |
. . . . . . . . . . . . 13
|
73 | 67, 72 | syl 16 |
. . . . . . . . . . . 12
|
74 | 66, 35, 73 | 3brtr4d 4482 |
. . . . . . . . . . 11
|
75 | 28, 74 | syldan 470 |
. . . . . . . . . 10
|
76 | 44, 75 | sylan2 474 |
. . . . . . . . 9
|
77 | 25, 43, 76 | monoord 12137 |
. . . . . . . 8
|
78 | | fveq2 5871 |
. . . . . . . . . . 11
|
79 | | id 22 |
. . . . . . . . . . 11
|
80 | 78, 79 | oveq12d 6314 |
. . . . . . . . . 10
|
81 | | ovex 6324 |
. . . . . . . . . 10
|
82 | 80, 32, 81 | fvmpt 5956 |
. . . . . . . . 9
|
83 | 8, 82 | syl 16 |
. . . . . . . 8
|
84 | | fveq2 5871 |
. . . . . . . . . . 11
|
85 | | id 22 |
. . . . . . . . . . 11
|
86 | 84, 85 | oveq12d 6314 |
. . . . . . . . . 10
|
87 | | ovex 6324 |
. . . . . . . . . 10
|
88 | 86, 32, 87 | fvmpt 5956 |
. . . . . . . . 9
|
89 | 11, 88 | syl 16 |
. . . . . . . 8
|
90 | 77, 83, 89 | 3brtr3d 4481 |
. . . . . . 7
|
91 | 13, 15, 18, 20, 90 | ltletrd 9763 |
. . . . . 6
|
92 | 10, 17, 12 | ltsub1d 10186 |
. . . . . 6
|
93 | 91, 92 | mpbird 232 |
. . . . 5
|
94 | 93 | ex 434 |
. . . 4
|
95 | 94 | ralrimivva 2878 |
. . 3
|
96 | | ssralv 3563 |
. . . . 5
|
97 | 96 | ralimdv 2867 |
. . . 4
|
98 | | ssralv 3563 |
. . . 4
|
99 | 97, 98 | syld 44 |
. . 3
|
100 | 95, 99 | mpan9 469 |
. 2
|
101 | | nnssre 10565 |
. . . . 5
|
102 | | ltso 9686 |
. . . . 5
|
103 | | soss 4823 |
. . . . 5
|
104 | 101, 102,
103 | mp2 9 |
. . . 4
|
105 | 104 | a1i 11 |
. . 3
|
106 | | soss 4823 |
. . . . 5
|
107 | 5, 102, 106 | mp2 9 |
. . . 4
|
108 | 107 | a1i 11 |
. . 3
|
109 | 6 | adantr 465 |
. . 3
|
110 | | simpr 461 |
. . 3
|
111 | | soisores 6223 |
. . 3
|
112 | 105, 108,
109, 110, 111 | syl22anc 1229 |
. 2
|
113 | 100, 112 | mpbird 232 |
1
|