Proof of Theorem seqz
Step | Hyp | Ref
| Expression |
1 | | seqz.5 |
. . . 4
|
2 | | elfzuz 12338 |
. . . 4
|
3 | 1, 2 | syl 17 |
. . 3
|
4 | | eluzelz 11697 |
. . . . . . . . 9
|
5 | 3, 4 | syl 17 |
. . . . . . . 8
|
6 | | seq1 12814 |
. . . . . . . 8
|
7 | 5, 6 | syl 17 |
. . . . . . 7
|
8 | | seqz.7 |
. . . . . . 7
|
9 | 7, 8 | eqtrd 2656 |
. . . . . 6
|
10 | | seqeq1 12804 |
. . . . . . . 8
|
11 | 10 | fveq1d 6193 |
. . . . . . 7
|
12 | 11 | eqeq1d 2624 |
. . . . . 6
|
13 | 9, 12 | syl5ibcom 235 |
. . . . 5
|
14 | | eluzel2 11692 |
. . . . . . . . 9
|
15 | 3, 14 | syl 17 |
. . . . . . . 8
|
16 | | seqm1 12818 |
. . . . . . . 8
|
17 | 15, 16 | sylan 488 |
. . . . . . 7
|
18 | 8 | adantr 481 |
. . . . . . . . 9
|
19 | 18 | oveq2d 6666 |
. . . . . . . 8
|
20 | | eluzp1m1 11711 |
. . . . . . . . . . 11
|
21 | 15, 20 | sylan 488 |
. . . . . . . . . 10
|
22 | | fzssp1 12384 |
. . . . . . . . . . . . . . 15
|
23 | 5 | zcnd 11483 |
. . . . . . . . . . . . . . . . 17
|
24 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . 17
|
25 | | npcan 10290 |
. . . . . . . . . . . . . . . . 17
|
26 | 23, 24, 25 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
27 | 26 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
28 | 22, 27 | syl5sseq 3653 |
. . . . . . . . . . . . . 14
|
29 | | elfzuz3 12339 |
. . . . . . . . . . . . . . . 16
|
30 | 1, 29 | syl 17 |
. . . . . . . . . . . . . . 15
|
31 | | fzss2 12381 |
. . . . . . . . . . . . . . 15
|
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . 14
|
33 | 28, 32 | sstrd 3613 |
. . . . . . . . . . . . 13
|
34 | 33 | adantr 481 |
. . . . . . . . . . . 12
|
35 | 34 | sselda 3603 |
. . . . . . . . . . 11
|
36 | | seqhomo.2 |
. . . . . . . . . . . 12
|
37 | 36 | adantlr 751 |
. . . . . . . . . . 11
|
38 | 35, 37 | syldan 487 |
. . . . . . . . . 10
|
39 | | seqhomo.1 |
. . . . . . . . . . 11
|
40 | 39 | adantlr 751 |
. . . . . . . . . 10
|
41 | 21, 38, 40 | seqcl 12821 |
. . . . . . . . 9
|
42 | | seqz.4 |
. . . . . . . . . . 11
|
43 | 42 | ralrimiva 2966 |
. . . . . . . . . 10
|
44 | 43 | adantr 481 |
. . . . . . . . 9
|
45 | | oveq1 6657 |
. . . . . . . . . . 11
|
46 | 45 | eqeq1d 2624 |
. . . . . . . . . 10
|
47 | 46 | rspcv 3305 |
. . . . . . . . 9
|
48 | 41, 44, 47 | sylc 65 |
. . . . . . . 8
|
49 | 19, 48 | eqtrd 2656 |
. . . . . . 7
|
50 | 17, 49 | eqtrd 2656 |
. . . . . 6
|
51 | 50 | ex 450 |
. . . . 5
|
52 | | uzp1 11721 |
. . . . . 6
|
53 | 3, 52 | syl 17 |
. . . . 5
|
54 | 13, 51, 53 | mpjaod 396 |
. . . 4
|
55 | 54, 8 | eqtr4d 2659 |
. . 3
|
56 | | eqidd 2623 |
. . 3
|
57 | 3, 55, 30, 56 | seqfveq2 12823 |
. 2
|
58 | | fvex 6201 |
. . . . . 6
|
59 | 58 | elsn 4192 |
. . . . 5
|
60 | 8, 59 | sylibr 224 |
. . . 4
|
61 | | simprl 794 |
. . . . . . . 8
|
62 | | velsn 4193 |
. . . . . . . 8
|
63 | 61, 62 | sylib 208 |
. . . . . . 7
|
64 | 63 | oveq1d 6665 |
. . . . . 6
|
65 | | simprr 796 |
. . . . . . 7
|
66 | | seqz.3 |
. . . . . . . . 9
|
67 | 66 | ralrimiva 2966 |
. . . . . . . 8
|
68 | 67 | adantr 481 |
. . . . . . 7
|
69 | | oveq2 6658 |
. . . . . . . . 9
|
70 | 69 | eqeq1d 2624 |
. . . . . . . 8
|
71 | 70 | rspcv 3305 |
. . . . . . 7
|
72 | 65, 68, 71 | sylc 65 |
. . . . . 6
|
73 | 64, 72 | eqtrd 2656 |
. . . . 5
|
74 | | ovex 6678 |
. . . . . 6
|
75 | 74 | elsn 4192 |
. . . . 5
|
76 | 73, 75 | sylibr 224 |
. . . 4
|
77 | | peano2uz 11741 |
. . . . . . . 8
|
78 | 3, 77 | syl 17 |
. . . . . . 7
|
79 | | fzss1 12380 |
. . . . . . 7
|
80 | 78, 79 | syl 17 |
. . . . . 6
|
81 | 80 | sselda 3603 |
. . . . 5
|
82 | 81, 36 | syldan 487 |
. . . 4
|
83 | 60, 76, 30, 82 | seqcl2 12819 |
. . 3
|
84 | | elsni 4194 |
. . 3
|
85 | 83, 84 | syl 17 |
. 2
|
86 | 57, 85 | eqtrd 2656 |
1
|