Step | Hyp | Ref
| Expression |
1 | | ccatvalfn 13365 |
. . . 4
Word
Word ++ ..^ |
2 | | lencl 13324 |
. . . . . . . . . . . 12
Word |
3 | 2 | adantr 481 |
. . . . . . . . . . 11
Word
Word |
4 | | nn0uz 11722 |
. . . . . . . . . . 11
|
5 | 3, 4 | syl6eleq 2711 |
. . . . . . . . . 10
Word
Word |
6 | 3 | nn0zd 11480 |
. . . . . . . . . . . 12
Word
Word |
7 | | uzid 11702 |
. . . . . . . . . . . 12
|
8 | 6, 7 | syl 17 |
. . . . . . . . . . 11
Word
Word |
9 | | lencl 13324 |
. . . . . . . . . . . 12
Word |
10 | 9 | adantl 482 |
. . . . . . . . . . 11
Word
Word |
11 | | uzaddcl 11744 |
. . . . . . . . . . 11
|
12 | 8, 10, 11 | syl2anc 693 |
. . . . . . . . . 10
Word
Word |
13 | | elfzuzb 12336 |
. . . . . . . . . 10
|
14 | 5, 12, 13 | sylanbrc 698 |
. . . . . . . . 9
Word
Word |
15 | | fzosplit 12501 |
. . . . . . . . 9
..^ ..^ ..^ |
16 | 14, 15 | syl 17 |
. . . . . . . 8
Word
Word ..^ ..^ ..^ |
17 | 16 | eleq2d 2687 |
. . . . . . 7
Word
Word ..^
..^ ..^ |
18 | | elun 3753 |
. . . . . . 7
..^ ..^ ..^ ..^ |
19 | 17, 18 | syl6bb 276 |
. . . . . 6
Word
Word ..^
..^ ..^ |
20 | | ccatval1 13361 |
. . . . . . . . . 10
Word
Word ..^ ++ |
21 | 20 | 3expa 1265 |
. . . . . . . . 9
Word
Word ..^ ++ |
22 | | ssun1 3776 |
. . . . . . . . . 10
|
23 | | simpl 473 |
. . . . . . . . . . . 12
Word
Word Word |
24 | | wrdf 13310 |
. . . . . . . . . . . 12
Word ..^ |
25 | | ffn 6045 |
. . . . . . . . . . . 12
..^ ..^ |
26 | 23, 24, 25 | 3syl 18 |
. . . . . . . . . . 11
Word
Word ..^ |
27 | | fnfvelrn 6356 |
. . . . . . . . . . 11
..^ ..^ |
28 | 26, 27 | sylan 488 |
. . . . . . . . . 10
Word
Word ..^ |
29 | 22, 28 | sseldi 3601 |
. . . . . . . . 9
Word
Word ..^ |
30 | 21, 29 | eqeltrd 2701 |
. . . . . . . 8
Word
Word ..^ ++ |
31 | | ccatval2 13362 |
. . . . . . . . . 10
Word
Word ..^ ++
|
32 | 31 | 3expa 1265 |
. . . . . . . . 9
Word
Word ..^ ++
|
33 | | ssun2 3777 |
. . . . . . . . . 10
|
34 | | simpr 477 |
. . . . . . . . . . . . 13
Word
Word Word |
35 | | wrdf 13310 |
. . . . . . . . . . . . 13
Word ..^ |
36 | | ffn 6045 |
. . . . . . . . . . . . 13
..^ ..^ |
37 | 34, 35, 36 | 3syl 18 |
. . . . . . . . . . . 12
Word
Word ..^ |
38 | 37 | adantr 481 |
. . . . . . . . . . 11
Word
Word ..^
..^ |
39 | | elfzouz 12474 |
. . . . . . . . . . . . . . 15
..^
|
40 | 39 | adantl 482 |
. . . . . . . . . . . . . 14
Word
Word ..^
|
41 | | uznn0sub 11719 |
. . . . . . . . . . . . . 14
|
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . 13
Word
Word ..^ |
43 | 42, 4 | syl6eleq 2711 |
. . . . . . . . . . . 12
Word
Word ..^ |
44 | 10 | nn0zd 11480 |
. . . . . . . . . . . . 13
Word
Word |
45 | 44 | adantr 481 |
. . . . . . . . . . . 12
Word
Word ..^ |
46 | | elfzolt2 12479 |
. . . . . . . . . . . . . 14
..^ |
47 | 46 | adantl 482 |
. . . . . . . . . . . . 13
Word
Word ..^ |
48 | | elfzoelz 12470 |
. . . . . . . . . . . . . . . 16
..^
|
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . 15
Word
Word ..^
|
50 | 49 | zred 11482 |
. . . . . . . . . . . . . 14
Word
Word ..^
|
51 | 6 | adantr 481 |
. . . . . . . . . . . . . . 15
Word
Word ..^ |
52 | 51 | zred 11482 |
. . . . . . . . . . . . . 14
Word
Word ..^ |
53 | 45 | zred 11482 |
. . . . . . . . . . . . . 14
Word
Word ..^ |
54 | 50, 52, 53 | ltsubadd2d 10625 |
. . . . . . . . . . . . 13
Word
Word ..^
|
55 | 47, 54 | mpbird 247 |
. . . . . . . . . . . 12
Word
Word ..^ |
56 | | elfzo2 12473 |
. . . . . . . . . . . 12
..^
|
57 | 43, 45, 55, 56 | syl3anbrc 1246 |
. . . . . . . . . . 11
Word
Word ..^ ..^ |
58 | | fnfvelrn 6356 |
. . . . . . . . . . 11
..^ ..^
|
59 | 38, 57, 58 | syl2anc 693 |
. . . . . . . . . 10
Word
Word ..^ |
60 | 33, 59 | sseldi 3601 |
. . . . . . . . 9
Word
Word ..^ |
61 | 32, 60 | eqeltrd 2701 |
. . . . . . . 8
Word
Word ..^ ++ |
62 | 30, 61 | jaodan 826 |
. . . . . . 7
Word
Word ..^ ..^ ++ |
63 | 62 | ex 450 |
. . . . . 6
Word
Word ..^ ..^
++ |
64 | 19, 63 | sylbid 230 |
. . . . 5
Word
Word ..^ ++ |
65 | 64 | ralrimiv 2965 |
. . . 4
Word
Word ..^ ++ |
66 | | ffnfv 6388 |
. . . 4
++ ..^ ++ ..^
..^ ++ |
67 | 1, 65, 66 | sylanbrc 698 |
. . 3
Word
Word ++ ..^ |
68 | | frn 6053 |
. . 3
++ ..^
++ |
69 | 67, 68 | syl 17 |
. 2
Word
Word ++
|
70 | 1 | adantr 481 |
. . . . . . . 8
Word
Word ..^ ++ ..^ |
71 | | fzoss2 12496 |
. . . . . . . . . 10
..^ ..^ |
72 | 12, 71 | syl 17 |
. . . . . . . . 9
Word
Word ..^ ..^ |
73 | 72 | sselda 3603 |
. . . . . . . 8
Word
Word ..^
..^ |
74 | | fnfvelrn 6356 |
. . . . . . . 8
++ ..^ ..^ ++ ++ |
75 | 70, 73, 74 | syl2anc 693 |
. . . . . . 7
Word
Word ..^ ++ ++ |
76 | 21, 75 | eqeltrrd 2702 |
. . . . . 6
Word
Word ..^ ++ |
77 | 76 | ralrimiva 2966 |
. . . . 5
Word
Word ..^ ++ |
78 | | ffnfv 6388 |
. . . . 5
..^
++
..^ ..^ ++ |
79 | 26, 77, 78 | sylanbrc 698 |
. . . 4
Word
Word ..^ ++ |
80 | | frn 6053 |
. . . 4
..^
++
++ |
81 | 79, 80 | syl 17 |
. . 3
Word
Word ++
|
82 | | ccatval3 13363 |
. . . . . . . 8
Word
Word ..^ ++ |
83 | 82 | 3expa 1265 |
. . . . . . 7
Word
Word ..^ ++ |
84 | 1 | adantr 481 |
. . . . . . . 8
Word
Word ..^ ++ ..^ |
85 | | elfzouz 12474 |
. . . . . . . . . . . . 13
..^
|
86 | 85 | adantl 482 |
. . . . . . . . . . . 12
Word
Word ..^
|
87 | 86, 4 | syl6eleqr 2712 |
. . . . . . . . . . 11
Word
Word ..^
|
88 | 3 | adantr 481 |
. . . . . . . . . . 11
Word
Word ..^ |
89 | 87, 88 | nn0addcld 11355 |
. . . . . . . . . 10
Word
Word ..^ |
90 | 89, 4 | syl6eleq 2711 |
. . . . . . . . 9
Word
Word ..^ |
91 | 3, 10 | nn0addcld 11355 |
. . . . . . . . . . 11
Word
Word |
92 | 91 | nn0zd 11480 |
. . . . . . . . . 10
Word
Word |
93 | 92 | adantr 481 |
. . . . . . . . 9
Word
Word ..^ |
94 | 87 | nn0cnd 11353 |
. . . . . . . . . . 11
Word
Word ..^
|
95 | 88 | nn0cnd 11353 |
. . . . . . . . . . 11
Word
Word ..^ |
96 | 94, 95 | addcomd 10238 |
. . . . . . . . . 10
Word
Word ..^ |
97 | 87 | nn0red 11352 |
. . . . . . . . . . 11
Word
Word ..^
|
98 | 10 | adantr 481 |
. . . . . . . . . . . 12
Word
Word ..^ |
99 | 98 | nn0red 11352 |
. . . . . . . . . . 11
Word
Word ..^ |
100 | 88 | nn0red 11352 |
. . . . . . . . . . 11
Word
Word ..^ |
101 | | elfzolt2 12479 |
. . . . . . . . . . . 12
..^
|
102 | 101 | adantl 482 |
. . . . . . . . . . 11
Word
Word ..^ |
103 | 97, 99, 100, 102 | ltadd2dd 10196 |
. . . . . . . . . 10
Word
Word ..^ |
104 | 96, 103 | eqbrtrd 4675 |
. . . . . . . . 9
Word
Word ..^
|
105 | | elfzo2 12473 |
. . . . . . . . 9
..^
|
106 | 90, 93, 104, 105 | syl3anbrc 1246 |
. . . . . . . 8
Word
Word ..^ ..^ |
107 | | fnfvelrn 6356 |
. . . . . . . 8
++ ..^ ..^
++ ++ |
108 | 84, 106, 107 | syl2anc 693 |
. . . . . . 7
Word
Word ..^ ++ ++ |
109 | 83, 108 | eqeltrrd 2702 |
. . . . . 6
Word
Word ..^ ++ |
110 | 109 | ralrimiva 2966 |
. . . . 5
Word
Word ..^ ++ |
111 | | ffnfv 6388 |
. . . . 5
..^
++
..^ ..^ ++ |
112 | 37, 110, 111 | sylanbrc 698 |
. . . 4
Word
Word ..^ ++ |
113 | | frn 6053 |
. . . 4
..^
++
++ |
114 | 112, 113 | syl 17 |
. . 3
Word
Word ++
|
115 | 81, 114 | unssd 3789 |
. 2
Word
Word ++
|
116 | 69, 115 | eqssd 3620 |
1
Word
Word ++ |