Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wwlkextwrd Unicode version

Theorem wwlkextwrd 30482
Description: Lemma 0 for wwlkextbij 30487. (Contributed by Alexander van der Vekens, 5-Aug-2018.)
Hypothesis
Ref Expression
wwlkextbij.d
Assertion
Ref Expression
wwlkextwrd
Distinct variable groups:   ,   ,N   ,   ,

Proof of Theorem wwlkextwrd
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 wwlkextbij.d . . 3
21a1i 11 . 2
3 3anass 969 . . . . . . 7
43anbi2i 694 . . . . . 6
5 anass 649 . . . . . 6
64, 5bitr4i 252 . . . . 5
7 wwlknprop 30442 . . . . . . . . . . 11
8 simpl 457 . . . . . . . . . . . . . . . 16
9 simpl 457 . . . . . . . . . . . . . . . . . . 19
109adantl 466 . . . . . . . . . . . . . . . . . 18
11 nn0re 10673 . . . . . . . . . . . . . . . . . . . . . 22
12 2re 10476 . . . . . . . . . . . . . . . . . . . . . . 23
1312a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
14 nn0ge0 10690 . . . . . . . . . . . . . . . . . . . . . 22
15 2pos 10498 . . . . . . . . . . . . . . . . . . . . . . 23
1615a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
1711, 13, 14, 16addgegt0d 9998 . . . . . . . . . . . . . . . . . . . . 21
1817adantr 465 . . . . . . . . . . . . . . . . . . . 20
19 breq2 4378 . . . . . . . . . . . . . . . . . . . . . 22
2019adantl 466 . . . . . . . . . . . . . . . . . . . . 21
2120adantl 466 . . . . . . . . . . . . . . . . . . . 20
2218, 21mpbird 232 . . . . . . . . . . . . . . . . . . 19
23 hashgt0n0 12218 . . . . . . . . . . . . . . . . . . 19
2410, 22, 23syl2anc 661 . . . . . . . . . . . . . . . . . 18
25 lswcl 12356 . . . . . . . . . . . . . . . . . 18
2610, 24, 25syl2anc 661 . . . . . . . . . . . . . . . . 17
2726adantrr 716 . . . . . . . . . . . . . . . 16
28 swrdcl 12401 . . . . . . . . . . . . . . . . . . . . . . 23
29 eleq1 2520 . . . . . . . . . . . . . . . . . . . . . . 23
3028, 29syl5ibr 221 . . . . . . . . . . . . . . . . . . . . . 22
3130eqcoms 2461 . . . . . . . . . . . . . . . . . . . . 21
3231adantr 465 . . . . . . . . . . . . . . . . . . . 20
3332com12 31 . . . . . . . . . . . . . . . . . . 19
3433adantr 465 . . . . . . . . . . . . . . . . . 18
3534imp 429 . . . . . . . . . . . . . . . . 17
3635adantl 466 . . . . . . . . . . . . . . . 16
37 oveq1 6181 . . . . . . . . . . . . . . . . . . . . 21
3837eqcoms 2461 . . . . . . . . . . . . . . . . . . . 20
3938adantr 465 . . . . . . . . . . . . . . . . . . 19
4039adantl 466 . . . . . . . . . . . . . . . . . 18
4140adantl 466 . . . . . . . . . . . . . . . . 17
42 oveq1 6181 . . . . . . . . . . . . . . . . . . . . . . . 24
4342adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23
44 nn0cn 10674 . . . . . . . . . . . . . . . . . . . . . . . . 25
45 2cnd 10479 . . . . . . . . . . . . . . . . . . . . . . . . 25
46 ax-1cn 9425 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4746a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
4844, 45, 47addsubassd 9824 . . . . . . . . . . . . . . . . . . . . . . . 24
49 2m1e1 10521 . . . . . . . . . . . . . . . . . . . . . . . . . 26
5049a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
5150oveq2d 6190 . . . . . . . . . . . . . . . . . . . . . . . 24
5248, 51eqtrd 2490 . . . . . . . . . . . . . . . . . . . . . . 23
5343, 52sylan9eqr 2512 . . . . . . . . . . . . . . . . . . . . . 22
5453opeq2d 4148 . . . . . . . . . . . . . . . . . . . . 21
5554oveq2d 6190 . . . . . . . . . . . . . . . . . . . 20
5655oveq1d 6189 . . . . . . . . . . . . . . . . . . 19
57 swrdccatwrd 12448 . . . . . . . . . . . . . . . . . . . 20
5810, 24, 57syl2anc 661 . . . . . . . . . . . . . . . . . . 19
5956, 58eqtr3d 2492 . . . . . . . . . . . . . . . . . 18
6059adantrr 716 . . . . . . . . . . . . . . . . 17
6141, 60eqtr2d 2491 . . . . . . . . . . . . . . . 16
62 simprrr 764 . . . . . . . . . . . . . . . 16
63 wwlknextbi 30479 . . . . . . . . . . . . . . . 16
648, 27, 36, 61, 62, 63syl23anc 1226 . . . . . . . . . . . . . . 15
6564exbiri 622 . . . . . . . . . . . . . 14
6665com23 78 . . . . . . . . . . . . 13
6766adantr 465 . . . . . . . . . . . 12
6867adantl 466 . . . . . . . . . . 11
697, 68mpcom 36 . . . . . . . . . 10
7069expcomd 438 . . . . . . . . 9
7170imp 429 . . . . . . . 8
72 wwlknimp 30443 . . . . . . . . . . . . 13
7344, 47, 47addassd 9493 . . . . . . . . . . . . . . . . . . . . 21
74 1p1e2 10520 . . . . . . . . . . . . . . . . . . . . . . 23
7574a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
7675oveq2d 6190 . . . . . . . . . . . . . . . . . . . . 21
7773, 76eqtrd 2490 . . . . . . . . . . . . . . . . . . . 20
7877eqeq2d 2463 . . . . . . . . . . . . . . . . . . 19
7978biimpd 207 . . . . . . . . . . . . . . . . . 18
8079adantr 465 . . . . . . . . . . . . . . . . 17
8180com12 31 . . . . . . . . . . . . . . . 16
8281adantl 466 . . . . . . . . . . . . . . 15
83 simpl 457 . . . . . . . . . . . . . . 15
8482, 83jctild 543 . . . . . . . . . . . . . 14
85843adant3 1008 . . . . . . . . . . . . 13
8672, 85syl 16 . . . . . . . . . . . 12
8786com12 31 . . . . . . . . . . 11
8887adantl 466 . . . . . . . . . 10
897, 88syl 16 . . . . . . . . 9
9089adantr 465 . . . . . . . 8
9171, 90impbid 191 . . . . . . 7
9291ex 434 . . . . . 6
9392pm5.32rd 640 . . . . 5
946, 93syl5bb 257 . . . 4
9594abbidv 2584 . . 3
96 df-rab 2801 . . 3
97 df-rab 2801 . . 3
9895, 96, 973eqtr4g 2515 . 2
992, 98eqtrd 2490 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  /\w3a 965  =wceq 1370  e.wcel 1757  {cab 2435  =/=wne 2641  A.wral 2792  {crab 2796   cvv 3052   c0 3719  {cpr 3961  <.cop 3965   class class class wbr 4374  rancrn 4923  `cfv 5500  (class class class)co 6174   cc 9365   cr 9366  0cc0 9367  1c1 9368   caddc 9370   clt 9503   cmin 9680  2c2 10456   cn0 10664   cfzo 11633   chash 12188  Wordcword 12307   clsw 12308   cconcat 12309  <"cs1 12310   csubstr 12311   cwwlkn 30434
This theorem is referenced by:  wwlkextsur  30485  wwlkextbij  30487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-rep 4485  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456  ax-cnex 9423  ax-resscn 9424  ax-1cn 9425  ax-icn 9426  ax-addcl 9427  ax-addrcl 9428  ax-mulcl 9429  ax-mulrcl 9430  ax-mulcom 9431  ax-addass 9432  ax-mulass 9433  ax-distr 9434  ax-i2m1 9435  ax-1ne0 9436  ax-1rid 9437  ax-rnegex 9438  ax-rrecex 9439  ax-cnre 9440  ax-pre-lttri 9441  ax-pre-lttrn 9442  ax-pre-ltadd 9443  ax-pre-mulgt0 9444
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-nel 2644  df-ral 2797  df-rex 2798  df-reu 2799  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-pss 3426  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4174  df-int 4211  df-iun 4255  df-br 4375  df-opab 4433  df-mpt 4434  df-tr 4468  df-eprel 4714  df-id 4718  df-po 4723  df-so 4724  df-fr 4761  df-we 4763  df-ord 4804  df-on 4805  df-lim 4806  df-suc 4807  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fn 5503  df-f 5504  df-f1 5505  df-fo 5506  df-f1o 5507  df-fv 5508  df-riota 6135  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-om 6561  df-1st 6661  df-2nd 6662  df-recs 6916  df-rdg 6950  df-1o 7004  df-oadd 7008  df-er 7185  df-map 7300  df-pm 7301  df-en 7395  df-dom 7396  df-sdom 7397  df-fin 7398  df-card 8194  df-pnf 9505  df-mnf 9506  df-xr 9507  df-ltxr 9508  df-le 9509  df-sub 9682  df-neg 9683  df-nn 10408  df-2 10465  df-n0 10665  df-z 10732  df-uz 10947  df-fz 11523  df-fzo 11634  df-hash 12189  df-word 12315  df-lsw 12316  df-concat 12317  df-s1 12318  df-substr 12319  df-wwlk 30435  df-wwlkn 30436
  Copyright terms: Public domain W3C validator