Proof of Theorem clwlkclwwlklem2a4
Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . . . . 10
|
2 | | lencl 13324 |
. . . . . . . . . . 11
Word |
3 | | clwlkclwwlklem2.f |
. . . . . . . . . . . 12
..^ |
4 | 3 | clwlkclwwlklem2fv2 26897 |
. . . . . . . . . . 11
|
5 | 2, 4 | sylan 488 |
. . . . . . . . . 10
Word |
6 | 1, 5 | sylan9eqr 2678 |
. . . . . . . . 9
Word
|
7 | 6 | ex 450 |
. . . . . . . 8
Word |
8 | 7 | 3adant1 1079 |
. . . . . . 7
Word
|
9 | 8 | ad2antrr 762 |
. . . . . 6
Word lastS
..^ |
10 | 9 | impcom 446 |
. . . . 5
Word lastS
..^ |
11 | 10 | fveq2d 6195 |
. . . 4
Word lastS
..^ |
12 | | f1f1orn 6148 |
. . . . . . 7
|
13 | 12 | 3ad2ant1 1082 |
. . . . . 6
Word
|
14 | 13 | ad2antrr 762 |
. . . . 5
Word lastS
..^ |
15 | | lsw 13351 |
. . . . . . . . . . . . . . . . . 18
Word lastS |
16 | 15 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . 17
Word lastS |
17 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . 22
|
18 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
19 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
20 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
21 | 18, 19, 20 | subsubd 10420 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
22 | | 2m1e1 11135 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
24 | 23 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
25 | 21, 24 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . 22
|
26 | 2, 17, 25 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
Word |
27 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
Word |
28 | 27 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
Word |
29 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . . . 21
|
30 | 29 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . 20
|
31 | 30 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
Word
|
32 | 28, 31 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
Word |
33 | 32 | ex 450 |
. . . . . . . . . . . . . . . . 17
Word |
34 | 16, 33 | sylbid 230 |
. . . . . . . . . . . . . . . 16
Word lastS
|
35 | 34 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
Word
lastS |
36 | 35 | com12 32 |
. . . . . . . . . . . . . 14
lastS
Word |
37 | 36 | adantr 481 |
. . . . . . . . . . . . 13
lastS ..^
Word |
38 | 37 | impcom 446 |
. . . . . . . . . . . 12
Word lastS
..^ |
39 | 38 | adantr 481 |
. . . . . . . . . . 11
Word lastS
..^
|
40 | 39 | preq2d 4275 |
. . . . . . . . . 10
Word lastS
..^
|
41 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
42 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
43 | 42 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
44 | 41, 43 | preq12d 4276 |
. . . . . . . . . . . 12
|
45 | 44 | eqeq1d 2624 |
. . . . . . . . . . 11
|
46 | 45 | adantl 482 |
. . . . . . . . . 10
Word lastS
..^
|
47 | 40, 46 | mpbird 247 |
. . . . . . . . 9
Word lastS
..^
|
48 | 47 | eleq1d 2686 |
. . . . . . . 8
Word lastS
..^
|
49 | 48 | biimpd 219 |
. . . . . . 7
Word lastS
..^
|
50 | 49 | impancom 456 |
. . . . . 6
Word lastS
..^ |
51 | 50 | impcom 446 |
. . . . 5
Word lastS
..^ |
52 | | f1ocnvfv2 6533 |
. . . . 5
|
53 | 14, 51, 52 | syl2an2 875 |
. . . 4
Word lastS
..^ |
54 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . 19
|
55 | 54 | biimpi 206 |
. . . . . . . . . . . . . . . . . 18
|
56 | | 1e2m1 11136 |
. . . . . . . . . . . . . . . . . . . . . 22
|
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
Word |
58 | 57 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
Word |
59 | 2, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
Word |
60 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . . 21
Word |
61 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . 21
Word |
62 | 59, 60, 61 | subsubd 10420 |
. . . . . . . . . . . . . . . . . . . 20
Word |
63 | 58, 62 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
Word |
64 | 63 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
Word |
65 | 55, 64 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . 17
Word |
66 | 65 | ex 450 |
. . . . . . . . . . . . . . . 16
Word |
67 | 16, 66 | sylbid 230 |
. . . . . . . . . . . . . . 15
Word lastS
|
68 | 67 | imp 445 |
. . . . . . . . . . . . . 14
Word lastS |
69 | 68 | preq2d 4275 |
. . . . . . . . . . . . 13
Word lastS |
70 | 69 | adantr 481 |
. . . . . . . . . . . 12
Word
lastS
|
71 | 44 | adantl 482 |
. . . . . . . . . . . 12
Word
lastS
|
72 | 70, 71 | eqtr4d 2659 |
. . . . . . . . . . 11
Word
lastS
|
73 | 72 | exp31 630 |
. . . . . . . . . 10
Word lastS
|
74 | 73 | 3ad2ant2 1083 |
. . . . . . . . 9
Word
lastS
|
75 | 74 | com12 32 |
. . . . . . . 8
lastS
Word |
76 | 75 | adantr 481 |
. . . . . . 7
lastS ..^
Word |
77 | 76 | impcom 446 |
. . . . . 6
Word lastS
..^
|
78 | 77 | adantr 481 |
. . . . 5
Word lastS
..^
|
79 | 78 | impcom 446 |
. . . 4
Word lastS
..^ |
80 | 11, 53, 79 | 3eqtrd 2660 |
. . 3
Word lastS
..^ |
81 | | simpll 790 |
. . . . . . . . . . . . . . . . 17
..^ |
82 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
83 | 82, 22 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
84 | 83 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ ..^ |
85 | 84 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
..^ |
86 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
87 | | 2cn 11091 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
88 | 87 | subidi 10352 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
89 | 86, 88 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
90 | 89 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
91 | 90 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . 22
|
92 | 85, 91 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^ |
93 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
94 | 93 | pm2.24d 147 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
95 | | fzo01 12550 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
96 | 94, 95 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
97 | 96 | imp 445 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
98 | 92, 97 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
99 | 98 | adantld 483 |
. . . . . . . . . . . . . . . . . . 19
..^ |
100 | | df-ne 2795 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
101 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
102 | 101 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
103 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
104 | 103 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
105 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
106 | 102, 104,
105 | leltned 10190 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
107 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^
|
108 | | simp-4l 806 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
109 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
110 | | 2z 11409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
111 | 110 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
112 | 109, 111 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
113 | 112 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
114 | 101 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
115 | 114, 103 | posdifd 10614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
116 | 115 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
117 | | elnnz 11387 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
118 | 113, 116,
117 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
119 | 118 | ad5ant24 1305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
120 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
121 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
122 | 109, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
123 | | zltlem1 11430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
124 | 120, 122,
123 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
125 | 17 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
|
126 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
|
127 | 125, 126,
126 | subsub4d 10423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
128 | | 1p1e2 11134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
|
129 | 128 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
|
130 | 129 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
131 | 127, 130 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
132 | 131 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
133 | 124, 132 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
134 | | necom 2847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
135 | | df-ne 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
136 | 134, 135 | bitr2i 265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
137 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
|
138 | 137 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
|
139 | 103, 114 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
|
140 | 139 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
|
141 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
|
142 | | leltne 10127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
|
143 | 142 | bicomd 213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
|
144 | 138, 140,
141, 143 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
145 | 144 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
146 | 136, 145 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
147 | 146 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
148 | 133, 147 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
149 | 148 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
150 | 149 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
151 | 150 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
152 | 151 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
153 | 108, 119,
152 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
154 | 153 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
155 | 154 | exp41 638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
156 | 155 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
157 | 156 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
158 | 157 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
159 | 107, 158 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^
|
160 | 159 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
|
161 | 160 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^ |
162 | 161 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^ |
163 | 106, 162 | sylbird 250 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
164 | 100, 163 | syl5bir 233 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
165 | 164 | com23 86 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
166 | 165 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
167 | 166 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
..^ |
168 | 99, 167 | pm2.61i 176 |
. . . . . . . . . . . . . . . . . 18
..^ |
169 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . . 18
..^
|
170 | 168, 169 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
171 | 81, 170 | jca 554 |
. . . . . . . . . . . . . . . 16
..^
..^ |
172 | 171 | exp31 630 |
. . . . . . . . . . . . . . 15
..^
..^ |
173 | 2, 172 | syl 17 |
. . . . . . . . . . . . . 14
Word
..^
..^ |
174 | 173 | imp 445 |
. . . . . . . . . . . . 13
Word ..^
..^ |
175 | 174 | 3adant1 1079 |
. . . . . . . . . . . 12
Word
..^
..^ |
176 | 175 | expd 452 |
. . . . . . . . . . 11
Word
..^
..^ |
177 | 176 | com12 32 |
. . . . . . . . . 10
..^
Word
..^ |
178 | 177 | adantl 482 |
. . . . . . . . 9
lastS ..^
Word
..^ |
179 | 178 | impcom 446 |
. . . . . . . 8
Word lastS
..^ ..^ |
180 | 179 | adantr 481 |
. . . . . . 7
Word lastS
..^
..^ |
181 | 180 | impcom 446 |
. . . . . 6
Word
lastS ..^
..^ |
182 | 3 | clwlkclwwlklem2fv1 26896 |
. . . . . 6
..^ |
183 | 181, 182 | syl 17 |
. . . . 5
Word
lastS ..^
|
184 | 183 | fveq2d 6195 |
. . . 4
Word
lastS ..^
|
185 | | simprr 796 |
. . . . 5
Word
lastS ..^
|
186 | | f1ocnvfv2 6533 |
. . . . 5
|
187 | 14, 185, 186 | syl2an2 875 |
. . . 4
Word
lastS ..^
|
188 | 184, 187 | eqtrd 2656 |
. . 3
Word
lastS ..^
|
189 | 80, 188 | pm2.61ian 831 |
. 2
Word lastS
..^
|
190 | 189 | exp31 630 |
1
Word
lastS
..^
|