Proof of Theorem signstfvn
Step | Hyp | Ref
| Expression |
1 | | signsv.p |
. . . . 5
|
2 | | signsv.w |
. . . . 5
|
3 | 1, 2 | signswbase 30631 |
. . . 4
|
4 | 1, 2 | signswmnd 30634 |
. . . . 5
|
5 | 4 | a1i 11 |
. . . 4
Word
|
6 | | eldifi 3732 |
. . . . . . . . 9
Word
Word |
7 | | lencl 13324 |
. . . . . . . . 9
Word
|
8 | 6, 7 | syl 17 |
. . . . . . . 8
Word |
9 | | eldifsn 4317 |
. . . . . . . . 9
Word
Word |
10 | | hasheq0 13154 |
. . . . . . . . . . 11
Word
|
11 | 10 | necon3bid 2838 |
. . . . . . . . . 10
Word
|
12 | 11 | biimpar 502 |
. . . . . . . . 9
Word |
13 | 9, 12 | sylbi 207 |
. . . . . . . 8
Word |
14 | | elnnne0 11306 |
. . . . . . . 8
|
15 | 8, 13, 14 | sylanbrc 698 |
. . . . . . 7
Word |
16 | 15 | adantr 481 |
. . . . . 6
Word
|
17 | | nnm1nn0 11334 |
. . . . . 6
|
18 | 16, 17 | syl 17 |
. . . . 5
Word
|
19 | | nn0uz 11722 |
. . . . 5
|
20 | 18, 19 | syl6eleq 2711 |
. . . 4
Word
|
21 | | s1cl 13382 |
. . . . . . . . . 10
Word
|
22 | | ccatcl 13359 |
. . . . . . . . . 10
Word Word ++
Word |
23 | 6, 21, 22 | syl2an 494 |
. . . . . . . . 9
Word
++ Word |
24 | 23 | adantr 481 |
. . . . . . . 8
Word
++
Word |
25 | | wrdf 13310 |
. . . . . . . 8
++
Word ++ ..^ ++ |
26 | 24, 25 | syl 17 |
. . . . . . 7
Word
++ ..^ ++ |
27 | 8 | adantr 481 |
. . . . . . . . . . . 12
Word
|
28 | 27 | nn0zd 11480 |
. . . . . . . . . . 11
Word
|
29 | | fzoval 12471 |
. . . . . . . . . . 11
..^ |
30 | 28, 29 | syl 17 |
. . . . . . . . . 10
Word
..^ |
31 | | fzossfz 12488 |
. . . . . . . . . 10
..^ |
32 | 30, 31 | syl6eqssr 3656 |
. . . . . . . . 9
Word
|
33 | | ccatlen 13360 |
. . . . . . . . . . . . 13
Word Word ++ |
34 | 6, 21, 33 | syl2an 494 |
. . . . . . . . . . . 12
Word
++ |
35 | | s1len 13385 |
. . . . . . . . . . . . 13
|
36 | 35 | oveq2i 6661 |
. . . . . . . . . . . 12
|
37 | 34, 36 | syl6eq 2672 |
. . . . . . . . . . 11
Word
++ |
38 | 37 | oveq2d 6666 |
. . . . . . . . . 10
Word
..^ ++ ..^ |
39 | 28 | peano2zd 11485 |
. . . . . . . . . . 11
Word
|
40 | | fzoval 12471 |
. . . . . . . . . . 11
..^ |
41 | 39, 40 | syl 17 |
. . . . . . . . . 10
Word
..^ |
42 | 27 | nn0cnd 11353 |
. . . . . . . . . . . 12
Word
|
43 | | 1cnd 10056 |
. . . . . . . . . . . 12
Word
|
44 | 42, 43 | pncand 10393 |
. . . . . . . . . . 11
Word
|
45 | 44 | oveq2d 6666 |
. . . . . . . . . 10
Word
|
46 | 38, 41, 45 | 3eqtrd 2660 |
. . . . . . . . 9
Word
..^ ++ |
47 | 32, 46 | sseqtr4d 3642 |
. . . . . . . 8
Word
..^ ++ |
48 | 47 | sselda 3603 |
. . . . . . 7
Word
..^ ++ |
49 | 26, 48 | ffvelrnd 6360 |
. . . . . 6
Word
++ |
50 | 49 | rexrd 10089 |
. . . . 5
Word
++ |
51 | | sgncl 30600 |
. . . . 5
++ sgn ++ |
52 | 50, 51 | syl 17 |
. . . 4
Word
sgn ++ |
53 | 1, 2 | signswplusg 30632 |
. . . 4
|
54 | | simpr 477 |
. . . . . 6
Word
|
55 | 54 | rexrd 10089 |
. . . . 5
Word
|
56 | | sgncl 30600 |
. . . . 5
sgn |
57 | 55, 56 | syl 17 |
. . . 4
Word
sgn |
58 | | simpr 477 |
. . . . . . . 8
Word
|
59 | 42, 43 | npcand 10396 |
. . . . . . . . 9
Word
|
60 | 59 | adantr 481 |
. . . . . . . 8
Word
|
61 | 58, 60 | eqtrd 2656 |
. . . . . . 7
Word
|
62 | 61 | fveq2d 6195 |
. . . . . 6
Word
++ ++ |
63 | 6 | adantr 481 |
. . . . . . . . 9
Word
Word |
64 | 54, 21 | syl 17 |
. . . . . . . . 9
Word
Word |
65 | | c0ex 10034 |
. . . . . . . . . . . . 13
|
66 | 65 | snid 4208 |
. . . . . . . . . . . 12
|
67 | | fzo01 12550 |
. . . . . . . . . . . 12
..^ |
68 | 66, 67 | eleqtrri 2700 |
. . . . . . . . . . 11
..^ |
69 | 35 | oveq2i 6661 |
. . . . . . . . . . 11
..^ ..^ |
70 | 68, 69 | eleqtrri 2700 |
. . . . . . . . . 10
..^ |
71 | 70 | a1i 11 |
. . . . . . . . 9
Word
..^ |
72 | | ccatval3 13363 |
. . . . . . . . 9
Word Word ..^ ++ |
73 | 63, 64, 71, 72 | syl3anc 1326 |
. . . . . . . 8
Word
++ |
74 | 42 | addid2d 10237 |
. . . . . . . . 9
Word
|
75 | 74 | fveq2d 6195 |
. . . . . . . 8
Word
++ ++ |
76 | | s1fv 13390 |
. . . . . . . . 9
|
77 | 54, 76 | syl 17 |
. . . . . . . 8
Word
|
78 | 73, 75, 77 | 3eqtr3d 2664 |
. . . . . . 7
Word
++ |
79 | 78 | adantr 481 |
. . . . . 6
Word
++ |
80 | 62, 79 | eqtrd 2656 |
. . . . 5
Word
++ |
81 | 80 | fveq2d 6195 |
. . . 4
Word
sgn ++ sgn |
82 | 3, 5, 20, 52, 53, 57, 81 | gsumnunsn 30615 |
. . 3
Word
g sgn ++ g sgn ++ sgn |
83 | 59 | oveq2d 6666 |
. . . . 5
Word
|
84 | 83 | mpteq1d 4738 |
. . . 4
Word
sgn ++ sgn ++ |
85 | 84 | oveq2d 6666 |
. . 3
Word
g sgn ++ g sgn ++ |
86 | 63 | adantr 481 |
. . . . . . . 8
Word
Word |
87 | 64 | adantr 481 |
. . . . . . . 8
Word
Word
|
88 | 30 | eleq2d 2687 |
. . . . . . . . 9
Word
..^
|
89 | 88 | biimpar 502 |
. . . . . . . 8
Word
..^ |
90 | | ccatval1 13361 |
. . . . . . . 8
Word Word ..^ ++ |
91 | 86, 87, 89, 90 | syl3anc 1326 |
. . . . . . 7
Word
++ |
92 | 91 | fveq2d 6195 |
. . . . . 6
Word
sgn ++ sgn |
93 | 92 | mpteq2dva 4744 |
. . . . 5
Word
sgn ++ sgn |
94 | 93 | oveq2d 6666 |
. . . 4
Word
g sgn ++ g sgn |
95 | 94 | oveq1d 6665 |
. . 3
Word
g sgn ++ sgn g sgn
sgn |
96 | 82, 85, 95 | 3eqtr3d 2664 |
. 2
Word
g sgn ++ g sgn sgn |
97 | | eqidd 2623 |
. . . . . 6
Word
|
98 | 97 | olcd 408 |
. . . . 5
Word
..^ |
99 | 27, 19 | syl6eleq 2711 |
. . . . . 6
Word
|
100 | | fzosplitsni 12579 |
. . . . . 6
..^ ..^ |
101 | 99, 100 | syl 17 |
. . . . 5
Word
..^ ..^ |
102 | 98, 101 | mpbird 247 |
. . . 4
Word
..^ |
103 | 102, 38 | eleqtrrd 2704 |
. . 3
Word
..^ ++ |
104 | | signsv.t |
. . . 4
Word
..^ g sgn |
105 | | signsv.v |
. . . 4
Word ..^ |
106 | 1, 2, 104, 105 | signstfval 30641 |
. . 3
++ Word ..^ ++ ++ g sgn ++ |
107 | 23, 103, 106 | syl2anc 693 |
. 2
Word
++
g sgn ++ |
108 | | fzo0end 12560 |
. . . . . 6
..^ |
109 | 15, 108 | syl 17 |
. . . . 5
Word ..^ |
110 | 1, 2, 104, 105 | signstfval 30641 |
. . . . 5
Word ..^ g sgn |
111 | 6, 109, 110 | syl2anc 693 |
. . . 4
Word g sgn |
112 | 111 | adantr 481 |
. . 3
Word
g sgn |
113 | 112 | oveq1d 6665 |
. 2
Word
sgn g sgn
sgn |
114 | 96, 107, 113 | 3eqtr4d 2666 |
1
Word
++
sgn |