Proof of Theorem signsvtn0
Step | Hyp | Ref
| Expression |
1 | | eldifsn 4097 |
. . . . . . . . . . . 12
 Word   
 Word    |
2 | 1 | biimpi 198 |
. . . . . . . . . . 11
 Word     Word    |
3 | 2 | adantr 467 |
. . . . . . . . . 10
  Word            Word    |
4 | 3 | simpld 461 |
. . . . . . . . 9
  Word          
Word   |
5 | 4 | adantr 467 |
. . . . . . . 8
   Word
      
  
 Word   |
6 | | wrdf 12676 |
. . . . . . . 8
 Word
   ..^         |
7 | 5, 6 | syl 17 |
. . . . . . 7
   Word
      
  
    ..^         |
8 | | lennncl 12688 |
. . . . . . . . . 10
  Word        |
9 | 3, 8 | syl 17 |
. . . . . . . . 9
  Word                 |
10 | 9 | adantr 467 |
. . . . . . . 8
   Word
      
  
       |
11 | | lbfzo0 11955 |
. . . . . . . 8
  ..^           |
12 | 10, 11 | sylibr 216 |
. . . . . . 7
   Word
      
  
  ..^       |
13 | 7, 12 | ffvelrnd 6023 |
. . . . . 6
   Word
      
  
       |
14 | | signsv.p |
. . . . . . 7
                   |
15 | | signsv.w |
. . . . . . 7
      
              |
16 | | signsv.t |
. . . . . . 7
 Word 
 ..^      g      sgn           |
17 | | signsv.v |
. . . . . . 7
 Word   ..^                               |
18 | 14, 15, 16, 17 | signstf0 29457 |
. . . . . 6
                   sgn          |
19 | 13, 18 | syl 17 |
. . . . 5
   Word
      
  
               sgn          |
20 | | signsvtn0.1 |
. . . . . . . 8
     |
21 | | simpr 463 |
. . . . . . . 8
   Word
      
  
   |
22 | 20, 21 | syl5eqr 2499 |
. . . . . . 7
   Word
      
  
       |
23 | | eqs1 12750 |
. . . . . . 7
  Word     
          |
24 | 5, 22, 23 | syl2anc 667 |
. . . . . 6
   Word
      
  
           |
25 | 24 | fveq2d 5869 |
. . . . 5
   Word
      
  
                   |
26 | | oveq1 6297 |
. . . . . . . . . 10
 
     |
27 | | 1m1e0 10678 |
. . . . . . . . . 10
   |
28 | 26, 27 | syl6eq 2501 |
. . . . . . . . 9
 
   |
29 | 28 | fveq2d 5869 |
. . . . . . . 8
             |
30 | 29 | fveq2d 5869 |
. . . . . . 7
 sgn    
   sgn        |
31 | 30 | s1eqd 12740 |
. . . . . 6
   sgn    
       sgn          |
32 | 21, 31 | syl 17 |
. . . . 5
   Word
      
  
   sgn    
       sgn          |
33 | 19, 25, 32 | 3eqtr4d 2495 |
. . . 4
   Word
      
  
       sgn            |
34 | 21, 28 | syl 17 |
. . . 4
   Word
      
  
 
   |
35 | 33, 34 | fveq12d 5871 |
. . 3
   Word
      
  
              sgn    
          |
36 | 4, 6 | syl 17 |
. . . . . . . 8
  Word              ..^         |
37 | 20 | oveq1i 6300 |
. . . . . . . . 9
         |
38 | | fzo0end 12003 |
. . . . . . . . . 10
    
       ..^       |
39 | 3, 8, 38 | 3syl 18 |
. . . . . . . . 9
  Word                  ..^       |
40 | 37, 39 | syl5eqel 2533 |
. . . . . . . 8
  Word              ..^       |
41 | 36, 40 | ffvelrnd 6023 |
. . . . . . 7
  Word              
    |
42 | 41 | rexrd 9690 |
. . . . . 6
  Word              
    |
43 | | sgncl 29409 |
. . . . . 6
      
sgn               |
44 | 42, 43 | syl 17 |
. . . . 5
  Word           sgn               |
45 | 44 | adantr 467 |
. . . 4
   Word
      
  
 sgn    
          |
46 | | s1fv 12748 |
. . . 4
 sgn    
           sgn             sgn          |
47 | 45, 46 | syl 17 |
. . 3
   Word
      
  
    sgn             sgn          |
48 | 35, 47 | eqtrd 2485 |
. 2
   Word
      
  
           sgn          |
49 | | fzossfz 11938 |
. . . . . . . . . 10
 ..^              |
50 | 49, 39 | sseldi 3430 |
. . . . . . . . 9
  Word                           |
51 | | swrd0val 12777 |
. . . . . . . . 9
  Word                 substr
         
  ..^          |
52 | 4, 50, 51 | syl2anc 667 |
. . . . . . . 8
  Word            substr
         
  ..^          |
53 | 52 | oveq1d 6305 |
. . . . . . 7
  Word             substr           ++   lastS     
   ..^        ++   lastS        |
54 | | swrdccatwrd 12824 |
. . . . . . . . 9
  Word    substr
          ++
  lastS     
  |
55 | 54 | eqcomd 2457 |
. . . . . . . 8
  Word    substr           ++   lastS        |
56 | 3, 55 | syl 17 |
. . . . . . 7
  Word          
  substr           ++
  lastS        |
57 | 37 | oveq2i 6301 |
. . . . . . . . . 10
 ..^    ..^        |
58 | 57 | a1i 11 |
. . . . . . . . 9
  Word            ..^    ..^         |
59 | 58 | reseq2d 5105 |
. . . . . . . 8
  Word             ..^      ..^          |
60 | 37 | a1i 11 |
. . . . . . . . . . 11
  Word                     |
61 | 60 | fveq2d 5869 |
. . . . . . . . . 10
  Word              
              |
62 | | lsw 12711 |
. . . . . . . . . . 11
 Word    lastS               |
63 | 62 | adantr 467 |
. . . . . . . . . 10
  Word           lastS               |
64 | 61, 63 | eqtr4d 2488 |
. . . . . . . . 9
  Word              
  lastS     |
65 | 64 | s1eqd 12740 |
. . . . . . . 8
  Word                
      lastS       |
66 | 59, 65 | oveq12d 6308 |
. . . . . . 7
  Word              ..^    ++      
    
   ..^        ++   lastS        |
67 | 53, 56, 66 | 3eqtr4d 2495 |
. . . . . 6
  Word          
   ..^    ++              |
68 | 67 | fveq2d 5869 |
. . . . 5
  Word                     ..^    ++               |
69 | | ffn 5728 |
. . . . . . . . . . 11
    ..^        ..^       |
70 | 4, 6, 69 | 3syl 18 |
. . . . . . . . . 10
  Word          
 ..^       |
71 | 20 | a1i 11 |
. . . . . . . . . . . 12
  Word          
      |
72 | 71 | oveq2d 6306 |
. . . . . . . . . . 11
  Word            ..^  ..^       |
73 | 72 | fneq2d 5667 |
. . . . . . . . . 10
  Word             ..^
 ..^        |
74 | 70, 73 | mpbird 236 |
. . . . . . . . 9
  Word          
 ..^   |
75 | 20, 9 | syl5eqel 2533 |
. . . . . . . . . . 11
  Word          
  |
76 | 75 | nnnn0d 10925 |
. . . . . . . . . 10
  Word          
  |
77 | | nn0z 10960 |
. . . . . . . . . 10

  |
78 | | fzossrbm1 11947 |
. . . . . . . . . 10
  ..^    ..^   |
79 | 76, 77, 78 | 3syl 18 |
. . . . . . . . 9
  Word            ..^    ..^   |
80 | | fnssres 5689 |
. . . . . . . . 9
   ..^  ..^    ..^    ..^     ..^     |
81 | 74, 79, 80 | syl2anc 667 |
. . . . . . . 8
  Word             ..^     ..^     |
82 | | hashfn 12554 |
. . . . . . . 8
 
 ..^     ..^        ..^         ..^      |
83 | 81, 82 | syl 17 |
. . . . . . 7
  Word                ..^         ..^
     |
84 | | nnm1nn0 10911 |
. . . . . . . 8
 
   |
85 | | hashfzo0 12602 |
. . . . . . . 8
  
    ..^        |
86 | 75, 84, 85 | 3syl 18 |
. . . . . . 7
  Word               ..^        |
87 | 83, 86 | eqtrd 2485 |
. . . . . 6
  Word                ..^         |
88 | 87 | eqcomd 2457 |
. . . . 5
  Word                  ..^       |
89 | 68, 88 | fveq12d 5871 |
. . . 4
  Word                  
       
 ..^    ++      
             ..^        |
90 | 89 | adantr 467 |
. . 3
   Word
      
  
                  ..^    ++                    ..^        |
91 | 52, 59 | eqtr4d 2488 |
. . . . . . . 8
  Word            substr
         
  ..^      |
92 | | swrdcl 12775 |
. . . . . . . . 9
 Word
 substr           Word
  |
93 | 4, 92 | syl 17 |
. . . . . . . 8
  Word            substr
         
Word   |
94 | 91, 93 | eqeltrrd 2530 |
. . . . . . 7
  Word             ..^    Word   |
95 | 94 | adantr 467 |
. . . . . 6
   Word
      
  
   ..^    Word   |
96 | 87 | adantr 467 |
. . . . . . . 8
   Word
      
  
      ..^         |
97 | 75 | adantr 467 |
. . . . . . . . . 10
   Word
      
  
   |
98 | 97 | nncnd 10625 |
. . . . . . . . 9
   Word
      
  
   |
99 | | 1cnd 9659 |
. . . . . . . . 9
   Word
      
  
   |
100 | | simpr 463 |
. . . . . . . . 9
   Word
      
  
   |
101 | 98, 99, 100 | subne0d 9995 |
. . . . . . . 8
   Word
      
  
 
   |
102 | 96, 101 | eqnetrd 2691 |
. . . . . . 7
   Word
      
  
      ..^       |
103 | | fveq2 5865 |
. . . . . . . . 9
 
 ..^         ..^           |
104 | | hash0 12548 |
. . . . . . . . 9
     |
105 | 103, 104 | syl6eq 2501 |
. . . . . . . 8
 
 ..^         ..^       |
106 | 105 | necon3i 2656 |
. . . . . . 7
      ..^       ..^      |
107 | 102, 106 | syl 17 |
. . . . . 6
   Word
      
  
   ..^      |
108 | 95, 107 | jca 535 |
. . . . 5
   Word
      
  
    ..^    Word
  ..^       |
109 | | eldifsn 4097 |
. . . . 5
 
 ..^    Word   
   ..^    Word   ..^       |
110 | 108, 109 | sylibr 216 |
. . . 4
   Word
      
  
   ..^    Word
     |
111 | 41 | adantr 467 |
. . . 4
   Word
      
  
         |
112 | 14, 15, 16, 17 | signstfvn 29458 |
. . . 4
    ..^    Word                  ..^    ++      
             ..^           
 ..^             ..^      
sgn           |
113 | 110, 111,
112 | syl2anc 667 |
. . 3
   Word
      
  
        ..^    ++      
             ..^           
 ..^             ..^      
sgn           |
114 | | lennncl 12688 |
. . . . . 6
    ..^    Word
  ..^          ..^       |
115 | | fzo0end 12003 |
. . . . . 6
      ..^           ..^       ..^     ..^        |
116 | 108, 114,
115 | 3syl 18 |
. . . . 5
   Word
      
  
       ..^       ..^     ..^        |
117 | 14, 15, 16, 17 | signstcl 29454 |
. . . . 5
    ..^    Word
      ..^       ..^     ..^      
      ..^             ..^              |
118 | 95, 116, 117 | syl2anc 667 |
. . . 4
   Word
      
  
       ..^             ..^              |
119 | 44 | adantr 467 |
. . . 4
   Word
      
  
 sgn    
          |
120 | | simpr 463 |
. . . . . 6
  Word              
    |
121 | | sgn0bi 29418 |
. . . . . . . 8
      
 sgn    
      
     |
122 | 121 | necon3bid 2668 |
. . . . . . 7
      
 sgn    
      
     |
123 | 122 | biimpar 488 |
. . . . . 6
     
         sgn          |
124 | 42, 120, 123 | syl2anc 667 |
. . . . 5
  Word           sgn          |
125 | 124 | adantr 467 |
. . . 4
   Word
      
  
 sgn    
     |
126 | 14, 15 | signswlid 29448 |
. . . 4
         ..^             ..^            sgn    
         sgn    
         
 ..^             ..^      
sgn         sgn    
     |
127 | 118, 119,
125, 126 | syl21anc 1267 |
. . 3
   Word
      
  
      
 ..^             ..^      
sgn         sgn    
     |
128 | 90, 113, 127 | 3eqtrd 2489 |
. 2
   Word
      
  
           sgn          |
129 | 48, 128 | pm2.61dane 2711 |
1
  Word                  
  sgn          |