Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  signsvtn0 Structured version   Unicode version

Theorem signsvtn0 27135
 Description: If the last letter is non zero, then this is the zero-skipping sign. (Contributed by Thierry Arnoux, 8-Oct-2018.)
Hypotheses
Ref Expression
signsv.p
signsv.w
signsv.t Word ..^ g sgn
signsv.v Word ..^
signsvtn0.1
Assertion
Ref Expression
signsvtn0 Word sgn
Distinct variable groups:   ,,   ,,,   ,,,   ,,,,,   ,   ,,,,   ,,
Allowed substitution hints:   (,,,)   (,,,)   ()   ()   (,,,,,)   (,,)

Proof of Theorem signsvtn0
StepHypRef Expression
1 eldifsn 4111 . . . . . . . . . . . 12 Word Word
21biimpi 194 . . . . . . . . . . 11 Word Word
32adantr 465 . . . . . . . . . 10 Word Word
43simpld 459 . . . . . . . . 9 Word Word
54adantr 465 . . . . . . . 8 Word Word
6 wrdf 12361 . . . . . . . 8 Word ..^
75, 6syl 16 . . . . . . 7 Word ..^
8 lennncl 12371 . . . . . . . . . 10 Word
93, 8syl 16 . . . . . . . . 9 Word
109adantr 465 . . . . . . . 8 Word
11 lbfzo0 11706 . . . . . . . 8 ..^
1210, 11sylibr 212 . . . . . . 7 Word ..^
137, 12ffvelrnd 5956 . . . . . 6 Word
14 signsv.p . . . . . . 7
15 signsv.w . . . . . . 7
16 signsv.t . . . . . . 7 Word ..^ g sgn
17 signsv.v . . . . . . 7 Word ..^
1814, 15, 16, 17signstf0 27133 . . . . . 6 sgn
1913, 18syl 16 . . . . 5 Word sgn
20 signsvtn0.1 . . . . . . . . 9
2120a1i 11 . . . . . . . 8 Word
22 simpr 461 . . . . . . . 8 Word
2321, 22eqtr3d 2497 . . . . . . 7 Word
24 eqs1 12421 . . . . . . 7 Word
255, 23, 24syl2anc 661 . . . . . 6 Word
2625fveq2d 5806 . . . . 5 Word
27 oveq1 6210 . . . . . . . . . 10
28 1m1e0 10504 . . . . . . . . . 10
2927, 28syl6eq 2511 . . . . . . . . 9
3029fveq2d 5806 . . . . . . . 8
3130fveq2d 5806 . . . . . . 7 sgn sgn
3231s1eqd 12413 . . . . . 6 sgn sgn
3322, 32syl 16 . . . . 5 Word sgn sgn
3419, 26, 333eqtr4d 2505 . . . 4 Word sgn
3522, 29syl 16 . . . 4 Word
3634, 35fveq12d 5808 . . 3 Word sgn
374, 6syl 16 . . . . . . . 8 Word ..^
3820oveq1i 6213 . . . . . . . . 9
39 fzo0end 11739 . . . . . . . . . 10 ..^
403, 8, 393syl 20 . . . . . . . . 9 Word ..^
4138, 40syl5eqel 2546 . . . . . . . 8 Word ..^
4237, 41ffvelrnd 5956 . . . . . . 7 Word
4342rexrd 9547 . . . . . 6 Word
44 sgncl 27085 . . . . . 6 sgn
4543, 44syl 16 . . . . 5 Word sgn
4645adantr 465 . . . 4 Word sgn
47 s1fv 12419 . . . 4 sgn sgn sgn
4846, 47syl 16 . . 3 Word sgn sgn
4936, 48eqtrd 2495 . 2 Word sgn
50 fzossfz 11690 . . . . . . . . . 10 ..^
5150, 40sseldi 3465 . . . . . . . . 9 Word
52 swrd0val 12438 . . . . . . . . 9 Word substr ..^
534, 51, 52syl2anc 661 . . . . . . . 8 Word substr ..^
5453oveq1d 6218 . . . . . . 7 Word substr concat ..^ concat
55 wrdeqcats1 12489 . . . . . . . 8 Word substr concat
563, 55syl 16 . . . . . . 7 Word substr concat
5738oveq2i 6214 . . . . . . . . . 10 ..^ ..^
5857a1i 11 . . . . . . . . 9 Word ..^ ..^
5958reseq2d 5221 . . . . . . . 8 Word ..^ ..^
6038a1i 11 . . . . . . . . . 10 Word
6160fveq2d 5806 . . . . . . . . 9 Word
6261s1eqd 12413 . . . . . . . 8 Word
6359, 62oveq12d 6221 . . . . . . 7 Word ..^ concat ..^ concat
6454, 56, 633eqtr4d 2505 . . . . . 6 Word ..^ concat
6564fveq2d 5806 . . . . 5 Word ..^ concat
66 ffn 5670 . . . . . . . . . . 11 ..^ ..^
6737, 66syl 16 . . . . . . . . . 10 Word ..^
6820a1i 11 . . . . . . . . . . . 12 Word
6968oveq2d 6219 . . . . . . . . . . 11 Word ..^ ..^
7069fneq2d 5613 . . . . . . . . . 10 Word ..^ ..^
7167, 70mpbird 232 . . . . . . . . 9 Word ..^
7220, 9syl5eqel 2546 . . . . . . . . . . 11 Word
7372nnnn0d 10750 . . . . . . . . . 10 Word
74 fzossrbm1 11698 . . . . . . . . . 10 ..^ ..^
7573, 74syl 16 . . . . . . . . 9 Word ..^ ..^
76 fnssres 5635 . . . . . . . . 9 ..^ ..^ ..^ ..^ ..^
7771, 75, 76syl2anc 661 . . . . . . . 8 Word ..^ ..^
78 hashfn 12259 . . . . . . . 8 ..^ ..^ ..^ ..^
7977, 78syl 16 . . . . . . 7 Word ..^ ..^
80 nnm1nn0 10735 . . . . . . . . 9
8172, 80syl 16 . . . . . . . 8 Word
82 hashfzo0 12312 . . . . . . . 8 ..^
8381, 82syl 16 . . . . . . 7 Word ..^
8479, 83eqtrd 2495 . . . . . 6 Word ..^
8584eqcomd 2462 . . . . 5 Word ..^
8665, 85fveq12d 5808 . . . 4 Word ..^ concat ..^
8786adantr 465 . . 3 Word ..^ concat ..^
8853, 59eqtr4d 2498 . . . . . . . . 9 Word substr ..^
89 swrdcl 12436 . . . . . . . . . 10 Word substr Word
904, 89syl 16 . . . . . . . . 9 Word substr Word
9188, 90eqeltrrd 2543 . . . . . . . 8 Word ..^ Word
9291adantr 465 . . . . . . 7 Word ..^ Word
9384adantr 465 . . . . . . . . 9 Word ..^
9472adantr 465 . . . . . . . . . . 11 Word
9594nncnd 10452 . . . . . . . . . 10 Word
96 ax-1cn 9454 . . . . . . . . . . 11
9796a1i 11 . . . . . . . . . 10 Word
98 simpr 461 . . . . . . . . . 10 Word
9995, 97, 98subne0d 9842 . . . . . . . . 9 Word
10093, 99eqnetrd 2745 . . . . . . . 8 Word ..^
101 fveq2 5802 . . . . . . . . . 10 ..^ ..^
102 hash0 12255 . . . . . . . . . 10
103101, 102syl6eq 2511 . . . . . . . . 9 ..^ ..^
104103necon3i 2692 . . . . . . . 8 ..^ ..^
105100, 104syl 16 . . . . . . 7 Word ..^
10692, 105jca 532 . . . . . 6 Word ..^ Word ..^
107 eldifsn 4111 . . . . . 6 ..^ Word ..^ Word ..^
108106, 107sylibr 212 . . . . 5 Word ..^ Word
10942adantr 465 . . . . 5 Word
11014, 15, 16, 17signstfvn 27134 . . . . 5 ..^ Word ..^ concat ..^ ..^ ..^ sgn
111108, 109, 110syl2anc 661 . . . 4 Word ..^ concat ..^ ..^ ..^ sgn
112106simpld 459 . . . . . 6 Word ..^ Word
113 lennncl 12371 . . . . . . 7 ..^ Word ..^ ..^
114 fzo0end 11739 . . . . . . 7 ..^ ..^ ..^ ..^
115106, 113, 1143syl 20 . . . . . 6 Word ..^ ..^ ..^
11614, 15, 16, 17signstcl 27130 . . . . . 6 ..^ Word ..^ ..^ ..^ ..^ ..^
117112, 115, 116syl2anc 661 . . . . 5 Word ..^ ..^
11845adantr 465 . . . . 5 Word sgn
119 simpr 461 . . . . . . 7 Word
120 sgn0bi 27094 . . . . . . . . 9 sgn
121120necon3bid 2710 . . . . . . . 8 sgn
122121biimpar 485 . . . . . . 7 sgn
12343, 119, 122syl2anc 661 . . . . . 6 Word sgn
124123adantr 465 . . . . 5 Word sgn
12514, 15signswlid 27124 . . . . 5 ..^ ..^ sgn sgn ..^ ..^ sgn sgn
126117, 118, 124, 125syl21anc 1218 . . . 4 Word ..^ ..^ sgn sgn
127111, 126eqtrd 2495 . . 3 Word ..^ concat ..^ sgn
12887, 127eqtrd 2495 . 2 Word sgn
129 exmidne 2658 . . 3
130129a1i 11 . 2 Word
13149, 128, 130mpjaodan 784 1 Word sgn
 Colors of variables: wff setvar class Syntax hints:   wi 4   wo 368   wa 369   wceq 1370   wcel 1758   wne 2648   cdif 3436   wss 3439  c0 3748  cif 3902  csn 3988  cpr 3990  ctp 3992  cop 3994   cmpt 4461   cres 4953   wfn 5524  wf 5525  cfv 5529  (class class class)co 6203   cmpt2 6205  cc 9394  cr 9395  cc0 9396  c1 9397  cxr 9531   cmin 9709  cneg 9710  cn 10436  cn0 10693  cfz 11557  ..^cfzo 11668  chash 12223  Word cword 12342   concat cconcat 12344  cs1 12345   substr csubstr 12346  sgncsgn 12696  csu 13284  cnx 14292  cbs 14295   cplusg 14360   g cgsu 14501 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 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4514  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485  ax-inf2 7961  ax-cnex 9452  ax-resscn 9453  ax-1cn 9454  ax-icn 9455  ax-addcl 9456  ax-addrcl 9457  ax-mulcl 9458  ax-mulrcl 9459  ax-mulcom 9460  ax-addass 9461  ax-mulass 9462  ax-distr 9463  ax-i2m1 9464  ax-1ne0 9465  ax-1rid 9466  ax-rnegex 9467  ax-rrecex 9468  ax-cnre 9469  ax-pre-lttri 9470  ax-pre-lttrn 9471  ax-pre-ltadd 9472  ax-pre-mulgt0 9473 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 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rmo 2807  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-pss 3455  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-tp 3993  df-op 3995  df-uni 4203  df-int 4240  df-iun 4284  df-br 4404  df-opab 4462  df-mpt 4463  df-tr 4497  df-eprel 4743  df-id 4747  df-po 4752  df-so 4753  df-fr 4790  df-se 4791  df-we 4792  df-ord 4833  df-on 4834  df-lim 4835  df-suc 4836  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-isom 5538  df-riota 6164  df-ov 6206  df-oprab 6207  df-mpt2 6208  df-om 6590  df-1st 6690  df-2nd 6691  df-supp 6804  df-recs 6945  df-rdg 6979  df-1o 7033  df-oadd 7037  df-er 7214  df-en 7424  df-dom 7425  df-sdom 7426  df-fin 7427  df-oi 7838  df-card 8223  df-pnf 9534  df-mnf 9535  df-xr 9536  df-ltxr 9537  df-le 9538  df-sub 9711  df-neg 9712  df-nn 10437  df-2 10494  df-n0 10694  df-z 10761  df-uz 10976  df-fz 11558  df-fzo 11669  df-seq 11927  df-hash 12224  df-word 12350  df-concat 12352  df-s1 12353  df-substr 12354  df-sgn 12697  df-struct 14297  df-ndx 14298  df-slot 14299  df-base 14300  df-plusg 14373  df-0g 14502  df-gsum 14503  df-mnd 15537  df-mulg 15670  df-cntz 15957 This theorem is referenced by:  signsvfpn  27150  signsvfnn  27151
 Copyright terms: Public domain W3C validator