Proof of Theorem signsvfn
Step | Hyp | Ref
| Expression |
1 | | simpl 464 |
. . . . . . 7
  Word   
 Word      |
2 | 1 | eldifad 3402 |
. . . . . 6
  Word   
 Word   |
3 | | simpr 468 |
. . . . . . 7
  Word   
   |
4 | 3 | s1cld 12795 |
. . . . . 6
  Word   
     Word   |
5 | | ccatcl 12771 |
. . . . . 6
  Word     Word   ++     
Word   |
6 | 2, 4, 5 | syl2anc 673 |
. . . . 5
  Word   
  ++      Word   |
7 | | signsv.p |
. . . . . 6
                   |
8 | | signsv.w |
. . . . . 6
      
              |
9 | | signsv.t |
. . . . . 6
 Word 
 ..^      g      sgn           |
10 | | signsv.v |
. . . . . 6
 Word   ..^                               |
11 | 7, 8, 9, 10 | signsvvfval 29539 |
. . . . 5
  ++     
Word     ++       
 ..^    ++                ++               ++
                |
12 | 6, 11 | syl 17 |
. . . 4
  Word   
     ++       
 ..^    ++                ++               ++
                |
13 | | ccatlen 12772 |
. . . . . . . 8
  Word     Word      ++                       |
14 | 2, 4, 13 | syl2anc 673 |
. . . . . . 7
  Word   
     ++                       |
15 | | s1len 12797 |
. . . . . . . 8
       
 |
16 | 15 | oveq2i 6319 |
. . . . . . 7
                     |
17 | 14, 16 | syl6eq 2521 |
. . . . . 6
  Word   
     ++               |
18 | 17 | oveq2d 6324 |
. . . . 5
  Word   
  ..^    ++         ..^         |
19 | 18 | sumeq1d 13844 |
. . . 4
  Word   
   ..^    ++                ++               ++
                ..^               ++
              ++                 |
20 | | eldifsn 4088 |
. . . . . . . 8
 Word   
 Word    |
21 | | lennncl 12738 |
. . . . . . . 8
  Word        |
22 | 20, 21 | sylbi 200 |
. . . . . . 7
 Word          |
23 | | nnuz 11218 |
. . . . . . 7
     |
24 | 22, 23 | syl6eleq 2559 |
. . . . . 6
 Word              |
25 | 24 | adantr 472 |
. . . . 5
  Word   
           |
26 | | 1cnd 9677 |
. . . . . 6
    Word                   ++               ++               |
27 | | 0cnd 9654 |
. . . . . 6
    Word                   ++               ++               |
28 | 26, 27 | ifclda 3904 |
. . . . 5
   Word
                    ++               ++                 |
29 | | fveq2 5879 |
. . . . . . 7
    
     ++               ++                |
30 | | oveq1 6315 |
. . . . . . . 8
    
          |
31 | 30 | fveq2d 5883 |
. . . . . . 7
    
     ++                 ++                  |
32 | 29, 31 | neeq12d 2704 |
. . . . . 6
    
      ++               ++                 ++                   ++                   |
33 | 32 | ifbid 3894 |
. . . . 5
    
       ++
              ++                      ++                   ++                     |
34 | 25, 28, 33 | fzosump1 13890 |
. . . 4
  Word   
   ..^               ++
              ++                  ..^             ++
              ++                      ++                   ++                      |
35 | 12, 19, 34 | 3eqtrd 2509 |
. . 3
  Word   
     ++          ..^             ++
              ++                      ++                   ++                      |
36 | 35 | adantlr 729 |
. 2
   Word
       

    ++        
 ..^             ++
              ++                      ++                   ++                      |
37 | 2 | adantr 472 |
. . . . . . . . 9
   Word
     ..^     
Word   |
38 | 3 | adantr 472 |
. . . . . . . . 9
   Word
     ..^     
  |
39 | | fzo0ss1 11975 |
. . . . . . . . . . 11
 ..^      ..^      |
40 | 39 | a1i 11 |
. . . . . . . . . 10
  Word   
  ..^      ..^       |
41 | 40 | sselda 3418 |
. . . . . . . . 9
   Word
     ..^       ..^       |
42 | 7, 8, 9, 10 | signstfvp 29532 |
. . . . . . . . 9
  Word
 ..^           ++                    |
43 | 37, 38, 41, 42 | syl3anc 1292 |
. . . . . . . 8
   Word
     ..^           ++
                   |
44 | | elfzoel2 11946 |
. . . . . . . . . . . . 13
  ..^    
      |
45 | 44 | adantl 473 |
. . . . . . . . . . . 12
   Word
     ..^            |
46 | | 1nn0 10909 |
. . . . . . . . . . . 12
 |
47 | | eluzmn 11189 |
. . . . . . . . . . . 12
     
                 |
48 | 45, 46, 47 | sylancl 675 |
. . . . . . . . . . 11
   Word
     ..^                      |
49 | | fzoss2 11973 |
. . . . . . . . . . 11
                ..^        ..^       |
50 | 48, 49 | syl 17 |
. . . . . . . . . 10
   Word
     ..^       ..^        ..^       |
51 | | simpr 468 |
. . . . . . . . . . 11
   Word
     ..^       ..^       |
52 | | elfzoelz 11947 |
. . . . . . . . . . . . 13
  ..^    
  |
53 | 52 | adantl 473 |
. . . . . . . . . . . 12
   Word
     ..^        |
54 | | elfzom1b 12039 |
. . . . . . . . . . . 12
         ..^    
   ..^          |
55 | 53, 45, 54 | syl2anc 673 |
. . . . . . . . . . 11
   Word
     ..^        ..^    
   ..^          |
56 | 51, 55 | mpbid 215 |
. . . . . . . . . 10
   Word
     ..^         ..^         |
57 | 50, 56 | sseldd 3419 |
. . . . . . . . 9
   Word
     ..^         ..^       |
58 | 7, 8, 9, 10 | signstfvp 29532 |
. . . . . . . . 9
  Word
   ..^           ++                        |
59 | 37, 38, 57, 58 | syl3anc 1292 |
. . . . . . . 8
   Word
     ..^           ++
                       |
60 | 43, 59 | neeq12d 2704 |
. . . . . . 7
   Word
     ..^            ++               ++
          
                     |
61 | 60 | ifbid 3894 |
. . . . . 6
   Word
     ..^             ++               ++
                                       |
62 | 61 | sumeq2dv 13846 |
. . . . 5
  Word   
   ..^             ++
              ++               
 ..^                               |
63 | 7, 8, 9, 10 | signsvvfval 29539 |
. . . . . 6
 Word
      ..^                               |
64 | 2, 63 | syl 17 |
. . . . 5
  Word   
       ..^                               |
65 | 62, 64 | eqtr4d 2508 |
. . . 4
  Word   
   ..^             ++
              ++                     |
66 | 65 | adantlr 729 |
. . 3
   Word
       

  ..^             ++               ++
                    |
67 | 7, 8, 9, 10 | signstfvn 29530 |
. . . . . . 7
  Word   
      ++
                            sgn     |
68 | 67 | adantlr 729 |
. . . . . 6
   Word
       

     ++                             sgn     |
69 | 2 | adantlr 729 |
. . . . . . 7
   Word
       

Word   |
70 | | simpr 468 |
. . . . . . 7
   Word
       

  |
71 | 22 | ad2antrr 740 |
. . . . . . . 8
   Word
       

      |
72 | | fzo0end 12032 |
. . . . . . . 8
    
       ..^       |
73 | 71, 72 | syl 17 |
. . . . . . 7
   Word
       

       ..^       |
74 | 7, 8, 9, 10 | signstfvp 29532 |
. . . . . . 7
  Word
       ..^           ++                                |
75 | 69, 70, 73, 74 | syl3anc 1292 |
. . . . . 6
   Word
       

     ++                                |
76 | 68, 75 | neeq12d 2704 |
. . . . 5
   Word
       

      ++                   ++               
               sgn                    |
77 | 7, 8, 9, 10 | signstfvcl 29534 |
. . . . . . 7
   Word
       
       ..^                          |
78 | 73, 77 | syldan 478 |
. . . . . 6
   Word
       

                    |
79 | 70 | rexrd 9708 |
. . . . . . 7
   Word
       

  |
80 | | sgncl 29482 |
. . . . . . 7

sgn         |
81 | 79, 80 | syl 17 |
. . . . . 6
   Word
       

sgn         |
82 | 7, 8 | signswch 29522 |
. . . . . 6
                    sgn                        sgn                                sgn      |
83 | 78, 81, 82 | syl2anc 673 |
. . . . 5
   Word
       

                sgn                
               sgn  
   |
84 | | sgnsgn 29492 |
. . . . . . . . 9

sgn sgn   sgn    |
85 | 79, 84 | syl 17 |
. . . . . . . 8
   Word
       

sgn sgn   sgn    |
86 | 85 | oveq2d 6324 |
. . . . . . 7
   Word
       

 sgn                sgn sgn     sgn                sgn     |
87 | 86 | breq1d 4405 |
. . . . . 6
   Word
       

  sgn                sgn sgn     sgn                sgn      |
88 | | neg1rr 10736 |
. . . . . . . . 9
  |
89 | | 1re 9660 |
. . . . . . . . 9
 |
90 | | prssi 4119 |
. . . . . . . . 9
          |
91 | 88, 89, 90 | mp2an 686 |
. . . . . . . 8
     |
92 | 91, 78 | sseldi 3416 |
. . . . . . 7
   Word
       

                |
93 | | sgnclre 29483 |
. . . . . . . 8
 sgn    |
94 | 93 | adantl 473 |
. . . . . . 7
   Word
       

sgn    |
95 | | sgnmulsgn 29493 |
. . . . . . 7
                sgn                   sgn  
 sgn                sgn sgn       |
96 | 92, 94, 95 | syl2anc 673 |
. . . . . 6
   Word
       

                sgn    sgn                sgn sgn       |
97 | | sgnmulsgn 29493 |
. . . . . . 7
                                 
 sgn                sgn      |
98 | 92, 70, 97 | syl2anc 673 |
. . . . . 6
   Word
       

                  sgn                sgn      |
99 | 87, 96, 98 | 3bitr4d 293 |
. . . . 5
   Word
       

                sgn                      |
100 | 76, 83, 99 | 3bitrd 287 |
. . . 4
   Word
       

      ++                   ++               
                   |
101 | 100 | ifbid 3894 |
. . 3
   Word
       

       ++
                  ++                                          |
102 | 66, 101 | oveq12d 6326 |
. 2
   Word
       

 
 ..^             ++
              ++                      ++                   ++                                                 |
103 | 36, 102 | eqtrd 2505 |
1
   Word
       

    ++                                    |