Proof of Theorem swrdccat3blem
Step | Hyp | Ref
| Expression |
1 | | lencl 13324 |
. . . . . . . 8
Word |
2 | | nn0le0eq0 11321 |
. . . . . . . . 9
|
3 | 2 | biimpd 219 |
. . . . . . . 8
|
4 | 1, 3 | syl 17 |
. . . . . . 7
Word |
5 | 4 | adantl 482 |
. . . . . 6
Word
Word
|
6 | | hasheq0 13154 |
. . . . . . . . . . 11
Word
|
7 | 6 | biimpd 219 |
. . . . . . . . . 10
Word |
8 | 7 | adantl 482 |
. . . . . . . . 9
Word
Word
|
9 | 8 | imp 445 |
. . . . . . . 8
Word
Word |
10 | | lencl 13324 |
. . . . . . . . . . . . . . . 16
Word |
11 | | swrdccatin12.l |
. . . . . . . . . . . . . . . . . . 19
|
12 | 11 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . 18
|
13 | 12 | eleq1i 2692 |
. . . . . . . . . . . . . . . . 17
|
14 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . 18
|
15 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . . . . . 19
|
16 | | recn 10026 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
17 | 16 | addid1d 10236 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
18 | 17 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
19 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
20 | 19 | anim1i 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
21 | 20 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
22 | | letri3 10123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
24 | 23 | biimprd 238 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
25 | 24 | exp4b 632 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
26 | 25 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
27 | 18, 26 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
28 | 27 | com3l 89 |
. . . . . . . . . . . . . . . . . . . . . 22
|
29 | 28 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . 21
|
30 | 29 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . 20
|
31 | 30 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
|
32 | 15, 31 | syl5bi 232 |
. . . . . . . . . . . . . . . . . 18
|
33 | 14, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
34 | 13, 33 | sylbi 207 |
. . . . . . . . . . . . . . . 16
|
35 | 10, 34 | syl 17 |
. . . . . . . . . . . . . . 15
Word
|
36 | 35 | imp 445 |
. . . . . . . . . . . . . 14
Word
|
37 | | elfznn0 12433 |
. . . . . . . . . . . . . . . 16
|
38 | | swrd00 13418 |
. . . . . . . . . . . . . . . . . . . . . 22
substr |
39 | | swrd00 13418 |
. . . . . . . . . . . . . . . . . . . . . 22
substr |
40 | 38, 39 | eqtr4i 2647 |
. . . . . . . . . . . . . . . . . . . . 21
substr substr |
41 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
42 | 41 | subidd 10380 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
43 | 42 | opeq1d 4408 |
. . . . . . . . . . . . . . . . . . . . . 22
|
44 | 43 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
substr substr |
45 | 41 | addid1d 10236 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
46 | 45 | opeq2d 4409 |
. . . . . . . . . . . . . . . . . . . . . 22
|
47 | 46 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
substr substr |
48 | 40, 44, 47 | 3eqtr4a 2682 |
. . . . . . . . . . . . . . . . . . . 20
substr substr |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
substr substr |
50 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . 19
|
51 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . 22
|
52 | 51 | opeq1d 4408 |
. . . . . . . . . . . . . . . . . . . . 21
|
53 | 52 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
substr substr |
54 | | opeq1 4402 |
. . . . . . . . . . . . . . . . . . . . 21
|
55 | 54 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
substr
substr |
56 | 53, 55 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . 19
substr
substr
substr
substr |
57 | 49, 50, 56 | 3imtr4d 283 |
. . . . . . . . . . . . . . . . . 18
substr substr |
58 | 57 | com12 32 |
. . . . . . . . . . . . . . . . 17
substr substr |
59 | 58 | a1d 25 |
. . . . . . . . . . . . . . . 16
Word
substr
substr |
60 | 37, 59 | syl 17 |
. . . . . . . . . . . . . . 15
Word
substr
substr |
61 | 60 | impcom 446 |
. . . . . . . . . . . . . 14
Word
substr
substr |
62 | 36, 61 | syld 47 |
. . . . . . . . . . . . 13
Word
substr
substr |
63 | 62 | imp 445 |
. . . . . . . . . . . 12
Word
substr
substr |
64 | | swrdcl 13419 |
. . . . . . . . . . . . . . . 16
Word substr Word |
65 | | ccatrid 13370 |
. . . . . . . . . . . . . . . 16
substr Word substr ++ substr |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . 15
Word substr
++ substr |
67 | 13, 41 | sylbi 207 |
. . . . . . . . . . . . . . . . . . 19
|
68 | 10, 67 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Word |
69 | | addid1 10216 |
. . . . . . . . . . . . . . . . . . 19
|
70 | 69 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
|
71 | 68, 70 | syl 17 |
. . . . . . . . . . . . . . . . 17
Word |
72 | 71 | opeq2d 4409 |
. . . . . . . . . . . . . . . 16
Word |
73 | 72 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
Word substr substr |
74 | 66, 73 | eqtrd 2656 |
. . . . . . . . . . . . . 14
Word substr
++ substr |
75 | 74 | adantr 481 |
. . . . . . . . . . . . 13
Word
substr ++
substr |
76 | 75 | adantr 481 |
. . . . . . . . . . . 12
Word
substr
++ substr |
77 | 63, 76 | ifeqda 4121 |
. . . . . . . . . . 11
Word
substr substr ++ substr |
78 | 77 | ex 450 |
. . . . . . . . . 10
Word
substr
substr ++ substr |
79 | 78 | ad3antrrr 766 |
. . . . . . . . 9
Word Word
substr substr ++ substr |
80 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
81 | 80 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
82 | 81 | eleq2d 2687 |
. . . . . . . . . . . 12
|
83 | 82 | adantr 481 |
. . . . . . . . . . 11
|
84 | | simpr 477 |
. . . . . . . . . . . . . 14
|
85 | | opeq2 4403 |
. . . . . . . . . . . . . . 15
|
86 | 85 | adantr 481 |
. . . . . . . . . . . . . 14
|
87 | 84, 86 | oveq12d 6668 |
. . . . . . . . . . . . 13
substr
substr |
88 | | oveq2 6658 |
. . . . . . . . . . . . . 14
substr ++ substr ++ |
89 | 88 | adantl 482 |
. . . . . . . . . . . . 13
substr ++ substr ++ |
90 | 87, 89 | ifeq12d 4106 |
. . . . . . . . . . . 12
substr
substr ++
substr substr ++ |
91 | 80 | opeq2d 4409 |
. . . . . . . . . . . . . 14
|
92 | 91 | oveq2d 6666 |
. . . . . . . . . . . . 13
substr substr |
93 | 92 | adantr 481 |
. . . . . . . . . . . 12
substr
substr |
94 | 90, 93 | eqeq12d 2637 |
. . . . . . . . . . 11
substr substr ++ substr
substr substr ++ substr |
95 | 83, 94 | imbi12d 334 |
. . . . . . . . . 10
substr
substr ++ substr
substr substr ++ substr |
96 | 95 | adantll 750 |
. . . . . . . . 9
Word Word
substr
substr ++ substr
substr substr ++ substr |
97 | 79, 96 | mpbird 247 |
. . . . . . . 8
Word Word
substr
substr ++ substr |
98 | 9, 97 | mpdan 702 |
. . . . . . 7
Word
Word
substr
substr ++ substr |
99 | 98 | ex 450 |
. . . . . 6
Word
Word substr
substr ++ substr |
100 | 5, 99 | syld 47 |
. . . . 5
Word
Word
substr
substr ++ substr |
101 | 100 | com23 86 |
. . . 4
Word
Word
substr
substr ++ substr |
102 | 101 | imp 445 |
. . 3
Word
Word
substr substr ++ substr |
103 | 102 | adantr 481 |
. 2
Word Word
substr
substr ++ substr |
104 | 11 | eleq1i 2692 |
. . . . . . . 8
|
105 | 104, 14 | sylbir 225 |
. . . . . . 7
|
106 | 10, 105 | syl 17 |
. . . . . 6
Word |
107 | 1 | nn0red 11352 |
. . . . . 6
Word |
108 | | leaddle0 10543 |
. . . . . 6
|
109 | 106, 107,
108 | syl2an 494 |
. . . . 5
Word
Word
|
110 | | pm2.24 121 |
. . . . 5
substr
substr ++ substr |
111 | 109, 110 | syl6bi 243 |
. . . 4
Word
Word
substr
substr ++ substr |
112 | 111 | adantr 481 |
. . 3
Word
Word
substr substr ++ substr |
113 | 112 | imp 445 |
. 2
Word Word
substr substr ++ substr |
114 | 103, 113 | pm2.61d 170 |
1
Word Word
substr substr ++ substr |