Proof of Theorem iseqf1olemab
Step | Hyp | Ref
| Expression |
1 | | eqtr3 2190 |
. . . . 5
|
2 | 1 | eqcomd 2176 |
. . . 4
|
3 | 2 | adantll 473 |
. . 3
|
4 | | iseqf1olemqcl.a |
. . . . . . . 8
|
5 | | elfzelz 9968 |
. . . . . . . 8
|
6 | 4, 5 | syl 14 |
. . . . . . 7
|
7 | 6 | zred 9321 |
. . . . . 6
|
8 | 7 | ltm1d 8835 |
. . . . 5
|
9 | 8 | ad2antrr 485 |
. . . 4
|
10 | 7 | ad2antrr 485 |
. . . . 5
|
11 | | peano2rem 8173 |
. . . . . 6
|
12 | 10, 11 | syl 14 |
. . . . 5
|
13 | | iseqf1olemab.a |
. . . . . . . 8
|
14 | | elfzle2 9971 |
. . . . . . . 8
|
15 | 13, 14 | syl 14 |
. . . . . . 7
|
16 | 15 | ad2antrr 485 |
. . . . . 6
|
17 | | iseqf1olemqcl.k |
. . . . . . . . . . . 12
|
18 | | iseqf1olemqcl.j |
. . . . . . . . . . . 12
|
19 | | iseqf1olemnab.q |
. . . . . . . . . . . 12
|
20 | 17, 18, 4, 19 | iseqf1olemqval 10430 |
. . . . . . . . . . 11
|
21 | 13 | iftrued 3532 |
. . . . . . . . . . 11
|
22 | 20, 21 | eqtrd 2203 |
. . . . . . . . . 10
|
23 | 22 | ad2antrr 485 |
. . . . . . . . 9
|
24 | | iseqf1olemnab.eq |
. . . . . . . . . . 11
|
25 | 24 | ad2antrr 485 |
. . . . . . . . . 10
|
26 | | iseqf1olemnab.b |
. . . . . . . . . . . . . 14
|
27 | 17, 18, 26, 19 | iseqf1olemqval 10430 |
. . . . . . . . . . . . 13
|
28 | | iseqf1olemab.b |
. . . . . . . . . . . . . 14
|
29 | 28 | iftrued 3532 |
. . . . . . . . . . . . 13
|
30 | 27, 29 | eqtrd 2203 |
. . . . . . . . . . . 12
|
31 | 30 | ad2antrr 485 |
. . . . . . . . . . 11
|
32 | | simplr 525 |
. . . . . . . . . . . 12
|
33 | 32 | iftrued 3532 |
. . . . . . . . . . 11
|
34 | 31, 33 | eqtrd 2203 |
. . . . . . . . . 10
|
35 | 25, 34 | eqtrd 2203 |
. . . . . . . . 9
|
36 | | simpr 109 |
. . . . . . . . . 10
|
37 | 36 | iffalsed 3535 |
. . . . . . . . 9
|
38 | 23, 35, 37 | 3eqtr3d 2211 |
. . . . . . . 8
|
39 | 38 | fveq2d 5498 |
. . . . . . 7
|
40 | 18 | ad2antrr 485 |
. . . . . . . 8
|
41 | | elfzel1 9967 |
. . . . . . . . . . . . 13
|
42 | 17, 41 | syl 14 |
. . . . . . . . . . . 12
|
43 | | elfzel2 9966 |
. . . . . . . . . . . . 13
|
44 | 17, 43 | syl 14 |
. . . . . . . . . . . 12
|
45 | | peano2zm 9237 |
. . . . . . . . . . . . 13
|
46 | 6, 45 | syl 14 |
. . . . . . . . . . . 12
|
47 | 42, 44, 46 | 3jca 1172 |
. . . . . . . . . . 11
|
48 | 47 | adantr 274 |
. . . . . . . . . 10
|
49 | 42 | zred 9321 |
. . . . . . . . . . . . 13
|
50 | 49 | adantr 274 |
. . . . . . . . . . . 12
|
51 | | elfzelz 9968 |
. . . . . . . . . . . . . . 15
|
52 | 17, 51 | syl 14 |
. . . . . . . . . . . . . 14
|
53 | 52 | zred 9321 |
. . . . . . . . . . . . 13
|
54 | 53 | adantr 274 |
. . . . . . . . . . . 12
|
55 | 46 | zred 9321 |
. . . . . . . . . . . . 13
|
56 | 55 | adantr 274 |
. . . . . . . . . . . 12
|
57 | | elfzle1 9970 |
. . . . . . . . . . . . . 14
|
58 | 17, 57 | syl 14 |
. . . . . . . . . . . . 13
|
59 | 58 | adantr 274 |
. . . . . . . . . . . 12
|
60 | | simpr 109 |
. . . . . . . . . . . . . . 15
|
61 | | eqcom 2172 |
. . . . . . . . . . . . . . 15
|
62 | 60, 61 | sylnib 671 |
. . . . . . . . . . . . . 14
|
63 | | elfzle1 9970 |
. . . . . . . . . . . . . . . . 17
|
64 | 13, 63 | syl 14 |
. . . . . . . . . . . . . . . 16
|
65 | | zleloe 9246 |
. . . . . . . . . . . . . . . . 17
|
66 | 52, 6, 65 | syl2anc 409 |
. . . . . . . . . . . . . . . 16
|
67 | 64, 66 | mpbid 146 |
. . . . . . . . . . . . . . 15
|
68 | 67 | adantr 274 |
. . . . . . . . . . . . . 14
|
69 | 62, 68 | ecased 1344 |
. . . . . . . . . . . . 13
|
70 | | zltlem1 9256 |
. . . . . . . . . . . . . . 15
|
71 | 52, 6, 70 | syl2anc 409 |
. . . . . . . . . . . . . 14
|
72 | 71 | adantr 274 |
. . . . . . . . . . . . 13
|
73 | 69, 72 | mpbid 146 |
. . . . . . . . . . . 12
|
74 | 50, 54, 56, 59, 73 | letrd 8030 |
. . . . . . . . . . 11
|
75 | 7 | adantr 274 |
. . . . . . . . . . . 12
|
76 | 44 | zred 9321 |
. . . . . . . . . . . . 13
|
77 | 76 | adantr 274 |
. . . . . . . . . . . 12
|
78 | 75 | lem1d 8836 |
. . . . . . . . . . . 12
|
79 | | elfzle2 9971 |
. . . . . . . . . . . . . 14
|
80 | 4, 79 | syl 14 |
. . . . . . . . . . . . 13
|
81 | 80 | adantr 274 |
. . . . . . . . . . . 12
|
82 | 56, 75, 77, 78, 81 | letrd 8030 |
. . . . . . . . . . 11
|
83 | 74, 82 | jca 304 |
. . . . . . . . . 10
|
84 | | elfz2 9959 |
. . . . . . . . . 10
|
85 | 48, 83, 84 | sylanbrc 415 |
. . . . . . . . 9
|
86 | 85 | adantlr 474 |
. . . . . . . 8
|
87 | | f1ocnvfv1 5753 |
. . . . . . . 8
|
88 | 40, 86, 87 | syl2anc 409 |
. . . . . . 7
|
89 | 39, 88 | eqtrd 2203 |
. . . . . 6
|
90 | 16, 89 | breqtrd 4013 |
. . . . 5
|
91 | 10, 12, 90 | lensymd 8028 |
. . . 4
|
92 | 9, 91 | pm2.21dd 615 |
. . 3
|
93 | | zdceq 9274 |
. . . . . 6
DECID |
94 | 6, 52, 93 | syl2anc 409 |
. . . . 5
DECID |
95 | | exmiddc 831 |
. . . . 5
DECID
|
96 | 94, 95 | syl 14 |
. . . 4
|
97 | 96 | adantr 274 |
. . 3
|
98 | 3, 92, 97 | mpjaodan 793 |
. 2
|
99 | | elfzelz 9968 |
. . . . . . . 8
|
100 | 26, 99 | syl 14 |
. . . . . . 7
|
101 | 100 | zred 9321 |
. . . . . 6
|
102 | 101 | ltm1d 8835 |
. . . . 5
|
103 | 102 | ad2antrr 485 |
. . . 4
|
104 | 101 | ad2antrr 485 |
. . . . 5
|
105 | | peano2rem 8173 |
. . . . . 6
|
106 | 104, 105 | syl 14 |
. . . . 5
|
107 | | elfzle2 9971 |
. . . . . . . 8
|
108 | 28, 107 | syl 14 |
. . . . . . 7
|
109 | 108 | ad2antrr 485 |
. . . . . 6
|
110 | 30 | ad2antrr 485 |
. . . . . . . . 9
|
111 | 24 | eqcomd 2176 |
. . . . . . . . . . 11
|
112 | 111 | ad2antrr 485 |
. . . . . . . . . 10
|
113 | 22 | ad2antrr 485 |
. . . . . . . . . . 11
|
114 | | simpr 109 |
. . . . . . . . . . . 12
|
115 | 114 | iftrued 3532 |
. . . . . . . . . . 11
|
116 | 113, 115 | eqtrd 2203 |
. . . . . . . . . 10
|
117 | 112, 116 | eqtrd 2203 |
. . . . . . . . 9
|
118 | | simplr 525 |
. . . . . . . . . 10
|
119 | 118 | iffalsed 3535 |
. . . . . . . . 9
|
120 | 110, 117,
119 | 3eqtr3d 2211 |
. . . . . . . 8
|
121 | 120 | fveq2d 5498 |
. . . . . . 7
|
122 | 18 | ad2antrr 485 |
. . . . . . . 8
|
123 | | peano2zm 9237 |
. . . . . . . . . . . . 13
|
124 | 100, 123 | syl 14 |
. . . . . . . . . . . 12
|
125 | 42, 44, 124 | 3jca 1172 |
. . . . . . . . . . 11
|
126 | 125 | adantr 274 |
. . . . . . . . . 10
|
127 | 49 | adantr 274 |
. . . . . . . . . . . 12
|
128 | 53 | adantr 274 |
. . . . . . . . . . . 12
|
129 | 101, 105 | syl 14 |
. . . . . . . . . . . . 13
|
130 | 129 | adantr 274 |
. . . . . . . . . . . 12
|
131 | 58 | adantr 274 |
. . . . . . . . . . . 12
|
132 | | simpr 109 |
. . . . . . . . . . . . . . 15
|
133 | | eqcom 2172 |
. . . . . . . . . . . . . . 15
|
134 | 132, 133 | sylnib 671 |
. . . . . . . . . . . . . 14
|
135 | | elfzle1 9970 |
. . . . . . . . . . . . . . . . 17
|
136 | 28, 135 | syl 14 |
. . . . . . . . . . . . . . . 16
|
137 | 136 | adantr 274 |
. . . . . . . . . . . . . . 15
|
138 | | zleloe 9246 |
. . . . . . . . . . . . . . . . 17
|
139 | 52, 100, 138 | syl2anc 409 |
. . . . . . . . . . . . . . . 16
|
140 | 139 | adantr 274 |
. . . . . . . . . . . . . . 15
|
141 | 137, 140 | mpbid 146 |
. . . . . . . . . . . . . 14
|
142 | 134, 141 | ecased 1344 |
. . . . . . . . . . . . 13
|
143 | | zltlem1 9256 |
. . . . . . . . . . . . . . 15
|
144 | 52, 100, 143 | syl2anc 409 |
. . . . . . . . . . . . . 14
|
145 | 144 | adantr 274 |
. . . . . . . . . . . . 13
|
146 | 142, 145 | mpbid 146 |
. . . . . . . . . . . 12
|
147 | 127, 128,
130, 131, 146 | letrd 8030 |
. . . . . . . . . . 11
|
148 | 101 | lem1d 8836 |
. . . . . . . . . . . . 13
|
149 | | elfzle2 9971 |
. . . . . . . . . . . . . 14
|
150 | 26, 149 | syl 14 |
. . . . . . . . . . . . 13
|
151 | 129, 101,
76, 148, 150 | letrd 8030 |
. . . . . . . . . . . 12
|
152 | 151 | adantr 274 |
. . . . . . . . . . 11
|
153 | 147, 152 | jca 304 |
. . . . . . . . . 10
|
154 | | elfz2 9959 |
. . . . . . . . . 10
|
155 | 126, 153,
154 | sylanbrc 415 |
. . . . . . . . 9
|
156 | 155 | adantr 274 |
. . . . . . . 8
|
157 | | f1ocnvfv1 5753 |
. . . . . . . 8
|
158 | 122, 156,
157 | syl2anc 409 |
. . . . . . 7
|
159 | 121, 158 | eqtrd 2203 |
. . . . . 6
|
160 | 109, 159 | breqtrd 4013 |
. . . . 5
|
161 | 104, 106,
160 | lensymd 8028 |
. . . 4
|
162 | 103, 161 | pm2.21dd 615 |
. . 3
|
163 | 6 | zcnd 9322 |
. . . . 5
|
164 | 163 | ad2antrr 485 |
. . . 4
|
165 | 100 | zcnd 9322 |
. . . . 5
|
166 | 165 | ad2antrr 485 |
. . . 4
|
167 | | 1cnd 7923 |
. . . 4
|
168 | 24 | ad2antrr 485 |
. . . . . 6
|
169 | 22 | ad2antrr 485 |
. . . . . . 7
|
170 | | simpr 109 |
. . . . . . . 8
|
171 | 170 | iffalsed 3535 |
. . . . . . 7
|
172 | 169, 171 | eqtrd 2203 |
. . . . . 6
|
173 | 30 | ad2antrr 485 |
. . . . . . 7
|
174 | | simplr 525 |
. . . . . . . 8
|
175 | 174 | iffalsed 3535 |
. . . . . . 7
|
176 | 173, 175 | eqtrd 2203 |
. . . . . 6
|
177 | 168, 172,
176 | 3eqtr3d 2211 |
. . . . 5
|
178 | | f1of1 5439 |
. . . . . . . 8
|
179 | 18, 178 | syl 14 |
. . . . . . 7
|
180 | 179 | ad2antrr 485 |
. . . . . 6
|
181 | 85 | adantlr 474 |
. . . . . 6
|
182 | 155 | adantr 274 |
. . . . . 6
|
183 | | f1veqaeq 5745 |
. . . . . 6
|
184 | 180, 181,
182, 183 | syl12anc 1231 |
. . . . 5
|
185 | 177, 184 | mpd 13 |
. . . 4
|
186 | 164, 166,
167, 185 | subcan2d 8259 |
. . 3
|
187 | 96 | adantr 274 |
. . 3
|
188 | 162, 186,
187 | mpjaodan 793 |
. 2
|
189 | | zdceq 9274 |
. . . 4
DECID |
190 | 100, 52, 189 | syl2anc 409 |
. . 3
DECID |
191 | | exmiddc 831 |
. . 3
DECID
|
192 | 190, 191 | syl 14 |
. 2
|
193 | 98, 188, 192 | mpjaodan 793 |
1
|