Proof of Theorem clwlkclwwlklem2a1
Step | Hyp | Ref
| Expression |
1 | | lencl 13324 |
. . . . . . . . . . . 12
Word |
2 | | nn0cn 11302 |
. . . . . . . . . . . 12
|
3 | | peano2cnm 10347 |
. . . . . . . . . . . . . . 15
|
4 | 3 | subid1d 10381 |
. . . . . . . . . . . . . 14
|
5 | 4 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
6 | | sub1m1 11284 |
. . . . . . . . . . . . 13
|
7 | 5, 6 | eqtrd 2656 |
. . . . . . . . . . . 12
|
8 | 1, 2, 7 | 3syl 18 |
. . . . . . . . . . 11
Word |
9 | 8 | adantr 481 |
. . . . . . . . . 10
Word |
10 | 9 | oveq2d 6666 |
. . . . . . . . 9
Word ..^ ..^ |
11 | 10 | raleqdv 3144 |
. . . . . . . 8
Word
..^
..^ |
12 | 11 | biimpcd 239 |
. . . . . . 7
..^
Word ..^ |
13 | 12 | adantr 481 |
. . . . . 6
..^ Word
..^ |
14 | 13 | adantl 482 |
. . . . 5
lastS
..^ Word ..^ |
15 | 14 | impcom 446 |
. . . 4
Word
lastS
..^ ..^ |
16 | | lsw 13351 |
. . . . . . . . . . . . . . . 16
Word lastS |
17 | | 2m1e1 11135 |
. . . . . . . . . . . . . . . . . . . . 21
|
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
Word |
19 | 18 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . 19
Word |
20 | 19 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
Word |
21 | 1, 2 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
Word |
22 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . 19
Word |
23 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . 19
Word |
24 | 21, 22, 23 | subsubd 10420 |
. . . . . . . . . . . . . . . . . 18
Word |
25 | 20, 24 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
Word |
26 | 25 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
Word |
27 | 16, 26 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
Word lastS |
28 | 27 | adantr 481 |
. . . . . . . . . . . . . 14
Word lastS |
29 | 28 | adantr 481 |
. . . . . . . . . . . . 13
Word
lastS lastS |
30 | | eqeq1 2626 |
. . . . . . . . . . . . . 14
lastS lastS
|
31 | 30 | adantl 482 |
. . . . . . . . . . . . 13
Word
lastS lastS |
32 | 29, 31 | mpbid 222 |
. . . . . . . . . . . 12
Word
lastS |
33 | 32 | preq2d 4275 |
. . . . . . . . . . 11
Word
lastS |
34 | 33 | eleq1d 2686 |
. . . . . . . . . 10
Word
lastS
|
35 | 34 | biimpd 219 |
. . . . . . . . 9
Word
lastS |
36 | 35 | ex 450 |
. . . . . . . 8
Word lastS
|
37 | 36 | com13 88 |
. . . . . . 7
lastS Word |
38 | 37 | adantl 482 |
. . . . . 6
..^ lastS
Word |
39 | 38 | impcom 446 |
. . . . 5
lastS
..^ Word |
40 | 39 | impcom 446 |
. . . 4
Word
lastS
..^ |
41 | | ovexd 6680 |
. . . . 5
Word
lastS
..^ |
42 | | fveq2 6191 |
. . . . . . . 8
|
43 | | oveq1 6657 |
. . . . . . . . 9
|
44 | 43 | fveq2d 6195 |
. . . . . . . 8
|
45 | 42, 44 | preq12d 4276 |
. . . . . . 7
|
46 | 45 | eleq1d 2686 |
. . . . . 6
|
47 | 46 | ralunsn 4422 |
. . . . 5
..^ ..^ |
48 | 41, 47 | syl 17 |
. . . 4
Word
lastS
..^ ..^ ..^ |
49 | 15, 40, 48 | mpbir2and 957 |
. . 3
Word
lastS
..^ ..^ |
50 | | 1e2m1 11136 |
. . . . . . . . . . 11
|
51 | 50 | a1i 11 |
. . . . . . . . . 10
Word |
52 | 51 | oveq2d 6666 |
. . . . . . . . 9
Word |
53 | 52, 24 | eqtrd 2656 |
. . . . . . . 8
Word |
54 | 53 | oveq2d 6666 |
. . . . . . 7
Word ..^ ..^ |
55 | 54 | adantr 481 |
. . . . . 6
Word ..^ ..^ |
56 | | nn0re 11301 |
. . . . . . . . . . . . . 14
|
57 | | 2re 11090 |
. . . . . . . . . . . . . . 15
|
58 | 57 | a1i 11 |
. . . . . . . . . . . . . 14
|
59 | 56, 58 | subge0d 10617 |
. . . . . . . . . . . . 13
|
60 | 59 | biimprd 238 |
. . . . . . . . . . . 12
|
61 | | nn0z 11400 |
. . . . . . . . . . . . 13
|
62 | | 2z 11409 |
. . . . . . . . . . . . . 14
|
63 | 62 | a1i 11 |
. . . . . . . . . . . . 13
|
64 | 61, 63 | zsubcld 11487 |
. . . . . . . . . . . 12
|
65 | 60, 64 | jctild 566 |
. . . . . . . . . . 11
|
66 | 1, 65 | syl 17 |
. . . . . . . . . 10
Word
|
67 | 66 | imp 445 |
. . . . . . . . 9
Word |
68 | | elnn0z 11390 |
. . . . . . . . 9
|
69 | 67, 68 | sylibr 224 |
. . . . . . . 8
Word |
70 | | elnn0uz 11725 |
. . . . . . . 8
|
71 | 69, 70 | sylib 208 |
. . . . . . 7
Word |
72 | | fzosplitsn 12576 |
. . . . . . 7
..^ ..^ |
73 | 71, 72 | syl 17 |
. . . . . 6
Word ..^ ..^ |
74 | 55, 73 | eqtrd 2656 |
. . . . 5
Word ..^ ..^ |
75 | 74 | adantr 481 |
. . . 4
Word
lastS
..^ ..^ ..^ |
76 | 75 | raleqdv 3144 |
. . 3
Word
lastS
..^ ..^ ..^ |
77 | 49, 76 | mpbird 247 |
. 2
Word
lastS
..^ ..^ |
78 | 77 | ex 450 |
1
Word lastS ..^
..^ |