Proof of Theorem swrdccat3
Step | Hyp | Ref
| Expression |
1 | | simpll 790 |
. . . 4
Word Word
Word Word |
2 | | simplrl 800 |
. . . . 5
Word Word
|
3 | | lencl 13324 |
. . . . . . . . 9
Word |
4 | | elfznn0 12433 |
. . . . . . . . . . . . . 14
|
5 | 4 | adantr 481 |
. . . . . . . . . . . . 13
|
6 | 5 | adantr 481 |
. . . . . . . . . . . 12
|
7 | | simplr 792 |
. . . . . . . . . . . 12
|
8 | | swrdccatin12.l |
. . . . . . . . . . . . . . 15
|
9 | 8 | breq2i 4661 |
. . . . . . . . . . . . . 14
|
10 | 9 | biimpi 206 |
. . . . . . . . . . . . 13
|
11 | 10 | adantl 482 |
. . . . . . . . . . . 12
|
12 | | elfz2nn0 12431 |
. . . . . . . . . . . 12
|
13 | 6, 7, 11, 12 | syl3anbrc 1246 |
. . . . . . . . . . 11
|
14 | 13 | exp31 630 |
. . . . . . . . . 10
|
15 | 14 | adantl 482 |
. . . . . . . . 9
|
16 | 3, 15 | syl5com 31 |
. . . . . . . 8
Word |
17 | 16 | adantr 481 |
. . . . . . 7
Word
Word
|
18 | 17 | imp 445 |
. . . . . 6
Word
Word
|
19 | 18 | imp 445 |
. . . . 5
Word Word
|
20 | 2, 19 | jca 554 |
. . . 4
Word Word
|
21 | | swrdccatin1 13483 |
. . . 4
Word
Word
++ substr substr |
22 | 1, 20, 21 | sylc 65 |
. . 3
Word Word
++ substr substr |
23 | | simp1l 1085 |
. . . 4
Word Word
Word Word |
24 | 8 | eleq1i 2692 |
. . . . . . . . . . 11
|
25 | | elfz2nn0 12431 |
. . . . . . . . . . . . . 14
|
26 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . 19
|
27 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
28 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | 28 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . 19
|
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
31 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . 20
|
32 | 31 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . 19
|
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
34 | 27, 30, 33 | 3jca 1242 |
. . . . . . . . . . . . . . . . 17
|
35 | 34 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
36 | | simpl3 1066 |
. . . . . . . . . . . . . . . . . 18
|
37 | 36 | anim1i 592 |
. . . . . . . . . . . . . . . . 17
|
38 | 37 | ancomd 467 |
. . . . . . . . . . . . . . . 16
|
39 | | elfz2 12333 |
. . . . . . . . . . . . . . . 16
|
40 | 35, 38, 39 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
|
41 | 40 | exp31 630 |
. . . . . . . . . . . . . 14
|
42 | 25, 41 | sylbi 207 |
. . . . . . . . . . . . 13
|
43 | 42 | adantr 481 |
. . . . . . . . . . . 12
|
44 | 43 | com12 32 |
. . . . . . . . . . 11
|
45 | 24, 44 | sylbir 225 |
. . . . . . . . . 10
|
46 | 3, 45 | syl 17 |
. . . . . . . . 9
Word |
47 | 46 | adantr 481 |
. . . . . . . 8
Word
Word
|
48 | 47 | imp 445 |
. . . . . . 7
Word
Word
|
49 | 48 | a1d 25 |
. . . . . 6
Word
Word
|
50 | 49 | 3imp 1256 |
. . . . 5
Word Word
|
51 | | elfz2nn0 12431 |
. . . . . . . . . . . 12
|
52 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . 18
|
53 | 8, 52 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . 17
|
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
55 | 54 | adantl 482 |
. . . . . . . . . . . . . . 15
|
56 | | nn0z 11400 |
. . . . . . . . . . . . . . . . 17
|
57 | 56 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . 16
|
58 | 57 | adantr 481 |
. . . . . . . . . . . . . . 15
|
59 | 28 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
|
60 | 59 | adantr 481 |
. . . . . . . . . . . . . . 15
|
61 | 55, 58, 60 | 3jca 1242 |
. . . . . . . . . . . . . 14
|
62 | 8 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . 19
|
63 | 62 | eleq1i 2692 |
. . . . . . . . . . . . . . . . . 18
|
64 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . 22
|
65 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . 22
|
66 | | ltnle 10117 |
. . . . . . . . . . . . . . . . . . . . . 22
|
67 | 64, 65, 66 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . 21
|
68 | 67 | bicomd 213 |
. . . . . . . . . . . . . . . . . . . 20
|
69 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . . . 21
|
70 | 64, 65, 69 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . 20
|
71 | 68, 70 | sylbid 230 |
. . . . . . . . . . . . . . . . . . 19
|
72 | 71 | ex 450 |
. . . . . . . . . . . . . . . . . 18
|
73 | 63, 72 | syl5bi 232 |
. . . . . . . . . . . . . . . . 17
|
74 | 73 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
|
75 | 74 | imp32 449 |
. . . . . . . . . . . . . . 15
|
76 | | simpl3 1066 |
. . . . . . . . . . . . . . 15
|
77 | 75, 76 | jca 554 |
. . . . . . . . . . . . . 14
|
78 | | elfz2 12333 |
. . . . . . . . . . . . . 14
|
79 | 61, 77, 78 | sylanbrc 698 |
. . . . . . . . . . . . 13
|
80 | 79 | exp32 631 |
. . . . . . . . . . . 12
|
81 | 51, 80 | sylbi 207 |
. . . . . . . . . . 11
|
82 | 81 | adantl 482 |
. . . . . . . . . 10
|
83 | 3, 82 | syl5com 31 |
. . . . . . . . 9
Word
|
84 | 83 | adantr 481 |
. . . . . . . 8
Word
Word
|
85 | 84 | imp 445 |
. . . . . . 7
Word
Word
|
86 | 85 | a1dd 50 |
. . . . . 6
Word
Word
|
87 | 86 | 3imp 1256 |
. . . . 5
Word Word
|
88 | 50, 87 | jca 554 |
. . . 4
Word Word
|
89 | 8 | swrdccatin2 13487 |
. . . 4
Word
Word
++ substr substr |
90 | 23, 88, 89 | sylc 65 |
. . 3
Word Word
++ substr substr
|
91 | | simp1l 1085 |
. . . 4
Word Word
Word Word |
92 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . 19
|
93 | 92 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
94 | | ltnle 10117 |
. . . . . . . . . . . . . . . . . 18
|
95 | 93, 64, 94 | syl2anr 495 |
. . . . . . . . . . . . . . . . 17
|
96 | 95 | bicomd 213 |
. . . . . . . . . . . . . . . 16
|
97 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . 20
|
99 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . . . . 22
|
100 | 92, 64, 99 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . 21
|
101 | 100 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
|
102 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . . . . . . 20
|
103 | 97, 98, 101, 102 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . . 19
|
104 | 103 | exp31 630 |
. . . . . . . . . . . . . . . . . 18
|
105 | 104 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
106 | 105 | impcom 446 |
. . . . . . . . . . . . . . . 16
|
107 | 96, 106 | sylbid 230 |
. . . . . . . . . . . . . . 15
|
108 | 107 | expcom 451 |
. . . . . . . . . . . . . 14
|
109 | 108 | 3adant3 1081 |
. . . . . . . . . . . . 13
|
110 | 25, 109 | sylbi 207 |
. . . . . . . . . . . 12
|
111 | 63, 110 | syl5bi 232 |
. . . . . . . . . . 11
|
112 | 111 | adantr 481 |
. . . . . . . . . 10
|
113 | 3, 112 | syl5com 31 |
. . . . . . . . 9
Word
|
114 | 113 | adantr 481 |
. . . . . . . 8
Word
Word
|
115 | 114 | imp 445 |
. . . . . . 7
Word
Word
|
116 | 115 | a1d 25 |
. . . . . 6
Word
Word
|
117 | 116 | 3imp 1256 |
. . . . 5
Word Word
|
118 | 65 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . 17
|
119 | 66 | bicomd 213 |
. . . . . . . . . . . . . . . . 17
|
120 | 64, 118, 119 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
121 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
122 | 57 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
123 | 59 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
124 | 121, 122,
123 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . 19
|
125 | 124 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
126 | 64, 118, 69 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
|
127 | 126 | imp 445 |
. . . . . . . . . . . . . . . . . . 19
|
128 | | simplr3 1105 |
. . . . . . . . . . . . . . . . . . 19
|
129 | 127, 128 | jca 554 |
. . . . . . . . . . . . . . . . . 18
|
130 | 125, 129,
78 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
|
131 | 130 | ex 450 |
. . . . . . . . . . . . . . . 16
|
132 | 120, 131 | sylbid 230 |
. . . . . . . . . . . . . . 15
|
133 | 132 | ex 450 |
. . . . . . . . . . . . . 14
|
134 | 63, 133 | sylbi 207 |
. . . . . . . . . . . . 13
|
135 | 3, 134 | syl 17 |
. . . . . . . . . . . 12
Word
|
136 | 135 | adantr 481 |
. . . . . . . . . . 11
Word
Word
|
137 | 136 | com12 32 |
. . . . . . . . . 10
Word
Word
|
138 | 51, 137 | sylbi 207 |
. . . . . . . . 9
Word
Word
|
139 | 138 | adantl 482 |
. . . . . . . 8
Word Word
|
140 | 139 | impcom 446 |
. . . . . . 7
Word
Word
|
141 | 140 | a1dd 50 |
. . . . . 6
Word
Word
|
142 | 141 | 3imp 1256 |
. . . . 5
Word Word
|
143 | 117, 142 | jca 554 |
. . . 4
Word Word
|
144 | 8 | swrdccatin12 13491 |
. . . 4
Word
Word
++ substr substr ++ substr |
145 | 91, 143, 144 | sylc 65 |
. . 3
Word Word
++ substr substr ++ substr |
146 | 22, 90, 145 | 2if2 4136 |
. 2
Word
Word
++ substr substr
substr
substr ++ substr |
147 | 146 | ex 450 |
1
Word
Word
++ substr substr
substr
substr ++ substr |