Proof of Theorem swrdccat
Step | Hyp | Ref
| Expression |
1 | | swrdccatin12.l |
. . . . 5
|
2 | 1 | swrdccat3 13492 |
. . . 4
Word
Word
++ substr substr
substr
substr ++ substr |
3 | 2 | imp 445 |
. . 3
Word
Word
++ substr substr
substr
substr ++ substr |
4 | | lencl 13324 |
. . . . . 6
Word |
5 | 4 | adantr 481 |
. . . . 5
Word
Word |
6 | 1 | eqcomi 2631 |
. . . . . . 7
|
7 | 6 | eleq1i 2692 |
. . . . . 6
|
8 | | elfz2nn0 12431 |
. . . . . . . . 9
|
9 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . 18
|
10 | 9 | adantl 482 |
. . . . . . . . . . . . . . . . 17
Word Word
|
11 | 10 | opeq2d 4409 |
. . . . . . . . . . . . . . . 16
Word Word
|
12 | 11 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
Word Word
substr
substr |
13 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . 20
|
14 | 13 | opeq1d 4408 |
. . . . . . . . . . . . . . . . . . 19
|
15 | 14 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
substr substr |
16 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word Word
substr
substr |
17 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
Word
Word Word |
18 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . 22
|
19 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
21 | | zsubcl 11419 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
22 | 20, 21 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
23 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
24 | 23 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
25 | | zsubcl 11419 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
26 | 24, 25 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
27 | 22, 26 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . 22
|
28 | 18, 27 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . 21
|
29 | 17, 28 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . 20
Word
Word
Word |
30 | | 3anass 1042 |
. . . . . . . . . . . . . . . . . . . 20
Word
Word |
31 | 29, 30 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
Word
Word
Word
|
32 | 31 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . 18
Word Word
Word |
33 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
34 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
35 | 33, 34 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
36 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
37 | | subge0 10541 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
38 | 37 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
39 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
40 | 39 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
41 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
42 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
43 | 42 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
44 | 40, 41, 43 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
45 | | letr 10131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
47 | 46 | expcomd 454 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
48 | 38, 47 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
49 | 48 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
50 | 35, 36, 49 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . 22
|
51 | 50 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
Word
Word
|
52 | 51 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
Word Word
|
53 | 52 | impcom 446 |
. . . . . . . . . . . . . . . . . . 19
Word Word
|
54 | 34 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
55 | 54 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
56 | 33 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
58 | 36 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
59 | 55, 57, 58 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . 22
|
60 | 59 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
Word
Word
|
61 | 60 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . 20
Word Word
|
62 | | lesub1 10522 |
. . . . . . . . . . . . . . . . . . . 20
|
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
Word Word
|
64 | 53, 63 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
Word Word
|
65 | | swrdlend 13431 |
. . . . . . . . . . . . . . . . . 18
Word
substr |
66 | 32, 64, 65 | sylc 65 |
. . . . . . . . . . . . . . . . 17
Word Word
substr
|
67 | 16, 66 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
Word Word
substr
|
68 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . 19
|
69 | 68 | opeq1d 4408 |
. . . . . . . . . . . . . . . . . 18
|
70 | 69 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
substr substr |
71 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
Word
Word
Word |
72 | 71 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
Word Word
Word |
73 | | 0zd 11389 |
. . . . . . . . . . . . . . . . . . 19
Word Word
|
74 | 24, 18, 25 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . 21
|
75 | 74 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
Word
Word
|
76 | 75 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
Word Word
|
77 | 72, 73, 76 | 3jca 1242 |
. . . . . . . . . . . . . . . . . 18
Word Word
Word
|
78 | 54, 36 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . 21
|
79 | 78 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
Word
Word
|
80 | | suble0 10542 |
. . . . . . . . . . . . . . . . . . . 20
|
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
Word
Word
|
82 | 81 | biimpar 502 |
. . . . . . . . . . . . . . . . . 18
Word Word
|
83 | | swrdlend 13431 |
. . . . . . . . . . . . . . . . . 18
Word
substr
|
84 | 77, 82, 83 | sylc 65 |
. . . . . . . . . . . . . . . . 17
Word Word
substr
|
85 | 70, 84 | sylan9eq 2676 |
. . . . . . . . . . . . . . . 16
Word Word
substr
|
86 | 67, 85 | pm2.61ian 831 |
. . . . . . . . . . . . . . 15
Word Word
substr
|
87 | 12, 86 | oveq12d 6668 |
. . . . . . . . . . . . . 14
Word Word
substr ++
substr
substr ++ |
88 | | swrdcl 13419 |
. . . . . . . . . . . . . . . . . 18
Word substr Word |
89 | | ccatrid 13370 |
. . . . . . . . . . . . . . . . . 18
substr Word substr ++ substr |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . . . 17
Word substr
++ substr |
91 | 90 | adantr 481 |
. . . . . . . . . . . . . . . 16
Word
Word substr ++ substr |
92 | 91 | adantr 481 |
. . . . . . . . . . . . . . 15
Word
Word
substr ++ substr |
93 | 92 | adantr 481 |
. . . . . . . . . . . . . 14
Word Word
substr ++ substr |
94 | 87, 93 | eqtrd 2656 |
. . . . . . . . . . . . 13
Word Word
substr ++
substr
substr |
95 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . 19
|
96 | 95 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . 18
Word Word
|
97 | 96 | opeq2d 4409 |
. . . . . . . . . . . . . . . . 17
Word Word
|
98 | 97 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
Word Word
substr
substr |
99 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . 21
Word
Word Word |
100 | 99, 20, 18 | 3anim123i 1247 |
. . . . . . . . . . . . . . . . . . . 20
Word
Word
Word |
101 | 100 | 3expb 1266 |
. . . . . . . . . . . . . . . . . . 19
Word
Word
Word
|
102 | | swrdlend 13431 |
. . . . . . . . . . . . . . . . . . 19
Word
substr |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Word
Word
substr |
104 | 103 | imp 445 |
. . . . . . . . . . . . . . . . 17
Word Word
substr
|
105 | 104 | 3adant2 1080 |
. . . . . . . . . . . . . . . 16
Word Word
substr
|
106 | 98, 105 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
Word Word
substr
|
107 | 56, 36, 37 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . 21
|
108 | 107 | biimprd 238 |
. . . . . . . . . . . . . . . . . . . 20
|
109 | 108 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
Word
Word
|
110 | 109 | imp 445 |
. . . . . . . . . . . . . . . . . 18
Word Word
|
111 | 110 | 3adant2 1080 |
. . . . . . . . . . . . . . . . 17
Word Word
|
112 | 111, 14 | syl 17 |
. . . . . . . . . . . . . . . 16
Word Word
|
113 | 112 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
Word Word
substr
substr |
114 | 106, 113 | oveq12d 6668 |
. . . . . . . . . . . . . 14
Word Word
substr ++
substr
++ substr
|
115 | | swrdcl 13419 |
. . . . . . . . . . . . . . . . . 18
Word substr
Word |
116 | 115 | adantl 482 |
. . . . . . . . . . . . . . . . 17
Word
Word substr
Word |
117 | | ccatlid 13369 |
. . . . . . . . . . . . . . . . 17
substr
Word ++ substr
substr |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . 16
Word
Word
++ substr substr |
119 | 118 | adantr 481 |
. . . . . . . . . . . . . . 15
Word
Word
++ substr
substr |
120 | 119 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
Word Word
++ substr
substr |
121 | 114, 120 | eqtrd 2656 |
. . . . . . . . . . . . 13
Word Word
substr ++
substr
substr |
122 | 95 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . 16
Word Word
|
123 | 122 | opeq2d 4409 |
. . . . . . . . . . . . . . 15
Word Word
|
124 | 123 | oveq2d 6666 |
. . . . . . . . . . . . . 14
Word Word
substr
substr |
125 | 33, 36, 37 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . 22
|
126 | 125 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . 21
|
127 | 126 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
Word
Word
|
128 | 127 | biimpd 219 |
. . . . . . . . . . . . . . . . . . 19
Word
Word
|
129 | 128 | con3dimp 457 |
. . . . . . . . . . . . . . . . . 18
Word Word
|
130 | 129 | 3adant2 1080 |
. . . . . . . . . . . . . . . . 17
Word Word
|
131 | 130, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
Word Word
|
132 | 131 | opeq1d 4408 |
. . . . . . . . . . . . . . 15
Word Word
|
133 | 132 | oveq2d 6666 |
. . . . . . . . . . . . . 14
Word Word
substr
substr |
134 | 124, 133 | oveq12d 6668 |
. . . . . . . . . . . . 13
Word Word
substr
++ substr
substr ++ substr |
135 | 94, 121, 134 | 2if2 4136 |
. . . . . . . . . . . 12
Word
Word
substr ++
substr
substr
substr
substr ++ substr |
136 | 135 | exp32 631 |
. . . . . . . . . . 11
Word
Word
substr
++ substr
substr
substr substr ++ substr |
137 | 136 | com12 32 |
. . . . . . . . . 10
Word Word
substr
++ substr
substr
substr substr ++ substr |
138 | 137 | 3adant3 1081 |
. . . . . . . . 9
Word
Word substr
++ substr
substr
substr substr ++ substr |
139 | 8, 138 | sylbi 207 |
. . . . . . . 8
Word
Word substr
++ substr
substr
substr substr ++ substr |
140 | 139 | adantr 481 |
. . . . . . 7
Word Word
substr
++ substr
substr
substr substr ++ substr |
141 | 140 | com13 88 |
. . . . . 6
Word
Word
substr
++ substr
substr
substr substr ++ substr |
142 | 7, 141 | sylbi 207 |
. . . . 5
Word Word substr
++ substr
substr
substr substr ++ substr |
143 | 5, 142 | mpcom 38 |
. . . 4
Word
Word
substr
++ substr
substr
substr substr ++ substr |
144 | 143 | imp 445 |
. . 3
Word
Word
substr
++ substr
substr
substr substr ++ substr |
145 | 3, 144 | eqtr4d 2659 |
. 2
Word
Word
++ substr substr ++
substr
|
146 | 145 | ex 450 |
1
Word
Word
++ substr substr ++
substr
|