MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  swrdswrd Unicode version

Theorem swrdswrd 12685
Description: A subword of a subword. (Contributed by Alexander van der Vekens, 4-Apr-2018.)
Assertion
Ref Expression
swrdswrd

Proof of Theorem swrdswrd
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 swrdcl 12646 . . . . . 6
213ad2ant1 1017 . . . . 5
32adantr 465 . . . 4
4 elfz0ubfz0 11807 . . . . 5
54adantl 466 . . . 4
6 elfzuz 11713 . . . . . . . . 9
76adantl 466 . . . . . . . 8
8 fzss1 11751 . . . . . . . 8
97, 8syl 16 . . . . . . 7
109sseld 3502 . . . . . 6
1110impr 619 . . . . 5
12 3ancomb 982 . . . . . . . . 9
1312biimpi 194 . . . . . . . 8
1413adantr 465 . . . . . . 7
15 swrdlen 12650 . . . . . . 7
1614, 15syl 16 . . . . . 6
1716oveq2d 6312 . . . . 5
1811, 17eleqtrrd 2548 . . . 4
19 swrdval2 12647 . . . 4
203, 5, 18, 19syl3anc 1228 . . 3
21 fvex 5881 . . . . . 6
22 eqid 2457 . . . . . 6
2321, 22fnmpti 5714 . . . . 5
2423a1i 11 . . . 4
25 swrdswrdlem 12684 . . . . . 6
26 swrdvalfn 12663 . . . . . 6
2725, 26syl 16 . . . . 5
28 elfzelz 11717 . . . . . . . . . 10
29 elfzelz 11717 . . . . . . . . . . 11
30 elfzelz 11717 . . . . . . . . . . 11
31 zcn 10894 . . . . . . . . . . . . . 14
3231adantr 465 . . . . . . . . . . . . 13
33 zcn 10894 . . . . . . . . . . . . . 14
3433ad2antrl 727 . . . . . . . . . . . . 13
35 zcn 10894 . . . . . . . . . . . . . 14
3635ad2antll 728 . . . . . . . . . . . . 13
37 pnpcan 9881 . . . . . . . . . . . . . 14
3837eqcomd 2465 . . . . . . . . . . . . 13
3932, 34, 36, 38syl3anc 1228 . . . . . . . . . . . 12
4039expcom 435 . . . . . . . . . . 11
4129, 30, 40syl2anr 478 . . . . . . . . . 10
4228, 41syl5com 30 . . . . . . . . 9
43423ad2ant3 1019 . . . . . . . 8
4443imp 429 . . . . . . 7
4544oveq2d 6312 . . . . . 6
4645fneq2d 5677 . . . . 5
4727, 46mpbird 232 . . . 4
48 simpr 461 . . . . . . 7
49 fvex 5881 . . . . . . 7
50 oveq1 6303 . . . . . . . . . 10
5150oveq1d 6311 . . . . . . . . 9
5251fveq2d 5875 . . . . . . . 8
53 eqid 2457 . . . . . . . 8
5452, 53fvmptg 5954 . . . . . . 7
5548, 49, 54sylancl 662 . . . . . 6
56 elfzoelz 11829 . . . . . . . . 9
57 zcn 10894 . . . . . . . . . . . . . . . . . . 19
5857, 31, 353anim123i 1181 . . . . . . . . . . . . . . . . . 18
59583expa 1196 . . . . . . . . . . . . . . . . 17
60 add32r 9816 . . . . . . . . . . . . . . . . . 18
6160eqcomd 2465 . . . . . . . . . . . . . . . . 17
6259, 61syl 16 . . . . . . . . . . . . . . . 16
6362exp31 604 . . . . . . . . . . . . . . 15
6463com13 80 . . . . . . . . . . . . . 14
6530, 64syl 16 . . . . . . . . . . . . 13
6665adantr 465 . . . . . . . . . . . 12
6728, 66syl5com 30 . . . . . . . . . . 11
68673ad2ant3 1019 . . . . . . . . . 10
6968imp 429 . . . . . . . . 9
7056, 69syl5com 30 . . . . . . . 8
7170impcom 430 . . . . . . 7
7271fveq2d 5875 . . . . . 6
7355, 72eqtrd 2498 . . . . 5
7413ad3antrrr 729 . . . . . . . 8
75 elfz2nn0 11798 . . . . . . . . . . . . 13
76 elfz2 11708 . . . . . . . . . . . . . . . 16
77 elfzo0 11863 . . . . . . . . . . . . . . . . . . . . . 22
78 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7978ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
80 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8180adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
82 zre 10893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8382ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
84 ltaddsub 10051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8584bicomd 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8679, 81, 83, 85syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
87 nn0addcl 10856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
8887ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
8988adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9089impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9190ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
92 elnn0z 10902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
93 0red 9618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
94 zre 10893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
9594adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
9682adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
97 lelttr 9696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
9893, 95, 96, 97syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
99 0red 9618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
10082adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
101 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
102101adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
103 ltletr 9697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
10499, 100, 102, 103syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
105 elnnnn0b 10865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
106105simplbi2 625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
107106adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
108104, 107syld 44 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
109108exp4b 607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
110109com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
111110adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
11298, 111syld 44 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
113112expd 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
114113a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
115114ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
116115com24 87 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
117116imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
11892, 117sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
11987, 118mpcom 36 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
120119impancom 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
121120impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
122121imp41 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
123 nn0readdcl 10883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
124123ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
125124adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
126125impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
127126adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
12883adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
129101adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
130 ltletr 9697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
131127, 128, 129, 130syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
132131exp4b 607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
133132com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
134133imp41 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
135 elfzo0 11863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
13691, 122, 134, 135syl3anbrc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
137136exp41 610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
13886, 137sylbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
139138ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
140139com24 87 . . . . . . . . . . . . . . . . . . . . . . . . . 26
141140imp 429 . . . . . . . . . . . . . . . . . . . . . . . . 25
142141com13 80 . . . . . . . . . . . . . . . . . . . . . . . 24
143142impancom 440 . . . . . . . . . . . . . . . . . . . . . . 23
1441433adant2 1015 . . . . . . . . . . . . . . . . . . . . . 22
14577, 144sylbi 195 . . . . . . . . . . . . . . . . . . . . 21
146145com14 88 . . . . . . . . . . . . . . . . . . . 20
147146adantl 466 . . . . . . . . . . . . . . . . . . 19
148147com12 31 . . . . . . . . . . . . . . . . . 18
1491483ad2ant3 1019 . . . . . . . . . . . . . . . . 17
150149imp 429 . . . . . . . . . . . . . . . 16
15176, 150sylbi 195 . . . . . . . . . . . . . . 15
152151com12 31 . . . . . . . . . . . . . 14
1531523adant3 1016 . . . . . . . . . . . . 13