Step | Hyp | Ref
| Expression |
1 | | uzuzle23 11729 |
. . . 4
|
2 | | 0re 10040 |
. . . . 5
|
3 | 2, 2 | axlowdimlem5 25826 |
. . . 4
|
4 | 1, 3 | syl 17 |
. . 3
|
5 | | 1re 10039 |
. . . . 5
|
6 | 5, 2 | axlowdimlem5 25826 |
. . . 4
|
7 | 1, 6 | syl 17 |
. . 3
|
8 | 2, 5 | axlowdimlem5 25826 |
. . . 4
|
9 | 1, 8 | syl 17 |
. . 3
|
10 | | eqid 2622 |
. . . 4
|
11 | 10 | axlowdimlem15 25836 |
. . 3
|
12 | | eqid 2622 |
. . . . . 6
|
13 | | eqid 2622 |
. . . . . 6
|
14 | | eqid 2622 |
. . . . . 6
|
15 | 12, 13, 14, 2, 2 | axlowdimlem17 25838 |
. . . . 5
Cgr
|
16 | | eqid 2622 |
. . . . . 6
|
17 | 12, 13, 16, 5, 2 | axlowdimlem17 25838 |
. . . . 5
Cgr
|
18 | | eqid 2622 |
. . . . . 6
|
19 | 12, 13, 18, 2, 5 | axlowdimlem17 25838 |
. . . . 5
Cgr
|
20 | | 1zzd 11408 |
. . . . . . . . . . . . . 14
|
21 | | peano2zm 11420 |
. . . . . . . . . . . . . . 15
|
22 | 21 | 3ad2ant2 1083 |
. . . . . . . . . . . . . 14
|
23 | | 2m1e1 11135 |
. . . . . . . . . . . . . . 15
|
24 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . 20
|
25 | | 3re 11094 |
. . . . . . . . . . . . . . . . . . . 20
|
26 | | 2lt3 11195 |
. . . . . . . . . . . . . . . . . . . 20
|
27 | 24, 25, 26 | ltleii 10160 |
. . . . . . . . . . . . . . . . . . 19
|
28 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | | letr 10131 |
. . . . . . . . . . . . . . . . . . . . 21
|
30 | 24, 25, 29 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . . . 20
|
31 | 28, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
32 | 27, 31 | mpani 712 |
. . . . . . . . . . . . . . . . . 18
|
33 | 32 | imp 445 |
. . . . . . . . . . . . . . . . 17
|
34 | 33 | 3adant1 1079 |
. . . . . . . . . . . . . . . 16
|
35 | 28 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . 17
|
36 | | lesub1 10522 |
. . . . . . . . . . . . . . . . . 18
|
37 | 24, 5, 36 | mp3an13 1415 |
. . . . . . . . . . . . . . . . 17
|
38 | 35, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
|
39 | 34, 38 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
40 | 23, 39 | syl5eqbrr 4689 |
. . . . . . . . . . . . . 14
|
41 | 20, 22, 40 | 3jca 1242 |
. . . . . . . . . . . . 13
|
42 | | eluz2 11693 |
. . . . . . . . . . . . 13
|
43 | | eluz2 11693 |
. . . . . . . . . . . . 13
|
44 | 41, 42, 43 | 3imtr4i 281 |
. . . . . . . . . . . 12
|
45 | | eluzfz1 12348 |
. . . . . . . . . . . 12
|
46 | 44, 45 | syl 17 |
. . . . . . . . . . 11
|
47 | 46 | adantr 481 |
. . . . . . . . . 10
|
48 | | eqeq1 2626 |
. . . . . . . . . . . 12
|
49 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
50 | 49 | opeq1d 4408 |
. . . . . . . . . . . . . 14
|
51 | 50 | sneqd 4189 |
. . . . . . . . . . . . 13
|
52 | 49 | sneqd 4189 |
. . . . . . . . . . . . . . 15
|
53 | 52 | difeq2d 3728 |
. . . . . . . . . . . . . 14
|
54 | 53 | xpeq1d 5138 |
. . . . . . . . . . . . 13
|
55 | 51, 54 | uneq12d 3768 |
. . . . . . . . . . . 12
|
56 | 48, 55 | ifbieq2d 4111 |
. . . . . . . . . . 11
|
57 | | snex 4908 |
. . . . . . . . . . . . 13
|
58 | | ovex 6678 |
. . . . . . . . . . . . . . 15
|
59 | | difexg 4808 |
. . . . . . . . . . . . . . 15
|
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
61 | | snex 4908 |
. . . . . . . . . . . . . 14
|
62 | 60, 61 | xpex 6962 |
. . . . . . . . . . . . 13
|
63 | 57, 62 | unex 6956 |
. . . . . . . . . . . 12
|
64 | | snex 4908 |
. . . . . . . . . . . . 13
|
65 | | difexg 4808 |
. . . . . . . . . . . . . . 15
|
66 | 58, 65 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
67 | 66, 61 | xpex 6962 |
. . . . . . . . . . . . 13
|
68 | 64, 67 | unex 6956 |
. . . . . . . . . . . 12
|
69 | 63, 68 | ifex 4156 |
. . . . . . . . . . 11
|
70 | 56, 10, 69 | fvmpt 6282 |
. . . . . . . . . 10
|
71 | 47, 70 | syl 17 |
. . . . . . . . 9
|
72 | | eqid 2622 |
. . . . . . . . . 10
|
73 | 72 | iftruei 4093 |
. . . . . . . . 9
|
74 | 71, 73 | syl6eq 2672 |
. . . . . . . 8
|
75 | 74 | opeq1d 4408 |
. . . . . . 7
|
76 | | 2eluzge1 11734 |
. . . . . . . . . . . . 13
|
77 | | fzss1 12380 |
. . . . . . . . . . . . 13
|
78 | 76, 77 | ax-mp 5 |
. . . . . . . . . . . 12
|
79 | 78 | sseli 3599 |
. . . . . . . . . . 11
|
80 | 79 | adantl 482 |
. . . . . . . . . 10
|
81 | | eqeq1 2626 |
. . . . . . . . . . . 12
|
82 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
83 | 82 | opeq1d 4408 |
. . . . . . . . . . . . . 14
|
84 | 83 | sneqd 4189 |
. . . . . . . . . . . . 13
|
85 | 82 | sneqd 4189 |
. . . . . . . . . . . . . . 15
|
86 | 85 | difeq2d 3728 |
. . . . . . . . . . . . . 14
|
87 | 86 | xpeq1d 5138 |
. . . . . . . . . . . . 13
|
88 | 84, 87 | uneq12d 3768 |
. . . . . . . . . . . 12
|
89 | 81, 88 | ifbieq2d 4111 |
. . . . . . . . . . 11
|
90 | | snex 4908 |
. . . . . . . . . . . . 13
|
91 | | difexg 4808 |
. . . . . . . . . . . . . . 15
|
92 | 58, 91 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
93 | 92, 61 | xpex 6962 |
. . . . . . . . . . . . 13
|
94 | 90, 93 | unex 6956 |
. . . . . . . . . . . 12
|
95 | 63, 94 | ifex 4156 |
. . . . . . . . . . 11
|
96 | 89, 10, 95 | fvmpt 6282 |
. . . . . . . . . 10
|
97 | 80, 96 | syl 17 |
. . . . . . . . 9
|
98 | | 1lt2 11194 |
. . . . . . . . . . . . . . . 16
|
99 | 5, 24 | ltnlei 10158 |
. . . . . . . . . . . . . . . 16
|
100 | 98, 99 | mpbi 220 |
. . . . . . . . . . . . . . 15
|
101 | 100 | intnanr 961 |
. . . . . . . . . . . . . 14
|
102 | | eluzelz 11697 |
. . . . . . . . . . . . . . . 16
|
103 | 102, 21 | syl 17 |
. . . . . . . . . . . . . . 15
|
104 | | 1z 11407 |
. . . . . . . . . . . . . . . 16
|
105 | | 2z 11409 |
. . . . . . . . . . . . . . . 16
|
106 | | elfz 12332 |
. . . . . . . . . . . . . . . 16
|
107 | 104, 105,
106 | mp3an12 1414 |
. . . . . . . . . . . . . . 15
|
108 | 103, 107 | syl 17 |
. . . . . . . . . . . . . 14
|
109 | 101, 108 | mtbiri 317 |
. . . . . . . . . . . . 13
|
110 | | eleq1 2689 |
. . . . . . . . . . . . . 14
|
111 | 110 | notbid 308 |
. . . . . . . . . . . . 13
|
112 | 109, 111 | syl5ibrcom 237 |
. . . . . . . . . . . 12
|
113 | 112 | con2d 129 |
. . . . . . . . . . 11
|
114 | 113 | imp 445 |
. . . . . . . . . 10
|
115 | 114 | iffalsed 4097 |
. . . . . . . . 9
|
116 | 97, 115 | eqtrd 2656 |
. . . . . . . 8
|
117 | 116 | opeq1d 4408 |
. . . . . . 7
|
118 | 75, 117 | breq12d 4666 |
. . . . . 6
Cgr
Cgr
|
119 | 74 | opeq1d 4408 |
. . . . . . 7
|
120 | 116 | opeq1d 4408 |
. . . . . . 7
|
121 | 119, 120 | breq12d 4666 |
. . . . . 6
Cgr
Cgr
|
122 | 46, 70 | syl 17 |
. . . . . . . . . 10
|
123 | 122, 73 | syl6eq 2672 |
. . . . . . . . 9
|
124 | 123 | opeq1d 4408 |
. . . . . . . 8
|
125 | 124 | adantr 481 |
. . . . . . 7
|
126 | 116 | opeq1d 4408 |
. . . . . . 7
|
127 | 125, 126 | breq12d 4666 |
. . . . . 6
Cgr
Cgr
|
128 | 118, 121,
127 | 3anbi123d 1399 |
. . . . 5
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
|
129 | 15, 17, 19, 128 | mpbir3and 1245 |
. . . 4
Cgr
Cgr
Cgr
|
130 | 129 | ralrimiva 2966 |
. . 3
Cgr
Cgr
Cgr
|
131 | 14, 16, 18 | axlowdimlem6 25827 |
. . . 4
|
132 | 1, 131 | syl 17 |
. . 3
|
133 | | opeq2 4403 |
. . . . . . . 8
|
134 | | opeq2 4403 |
. . . . . . . 8
|
135 | 133, 134 | breq12d 4666 |
. . . . . . 7
Cgr
Cgr
|
136 | 135 | 3anbi1d 1403 |
. . . . . 6
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
|
137 | 136 | ralbidv 2986 |
. . . . 5
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
|
138 | | breq1 4656 |
. . . . . . 7
|
139 | | opeq2 4403 |
. . . . . . . 8
|
140 | 139 | breq2d 4665 |
. . . . . . 7
|
141 | | opeq1 4402 |
. . . . . . . 8
|
142 | 141 | breq2d 4665 |
. . . . . . 7
|
143 | 138, 140,
142 | 3orbi123d 1398 |
. . . . . 6
|
144 | 143 | notbid 308 |
. . . . 5
|
145 | 137, 144 | 3anbi23d 1402 |
. . . 4
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
|
146 | | opeq2 4403 |
. . . . . . . 8
|
147 | | opeq2 4403 |
. . . . . . . 8
|
148 | 146, 147 | breq12d 4666 |
. . . . . . 7
Cgr
Cgr
|
149 | 148 | 3anbi2d 1404 |
. . . . . 6
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
|
150 | 149 | ralbidv 2986 |
. . . . 5
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
|
151 | | opeq1 4402 |
. . . . . . . 8
|
152 | 151 | breq2d 4665 |
. . . . . . 7
|
153 | | breq1 4656 |
. . . . . . 7
|
154 | | opeq2 4403 |
. . . . . . . 8
|
155 | 154 | breq2d 4665 |
. . . . . . 7
|
156 | 152, 153,
155 | 3orbi123d 1398 |
. . . . . 6
|
157 | 156 | notbid 308 |
. . . . 5
|
158 | 150, 157 | 3anbi23d 1402 |
. . . 4
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
|
159 | | opeq2 4403 |
. . . . . . . 8
|
160 | | opeq2 4403 |
. . . . . . . 8
|
161 | 159, 160 | breq12d 4666 |
. . . . . . 7
Cgr
Cgr
|
162 | 161 | 3anbi3d 1405 |
. . . . . 6
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
|
163 | 162 | ralbidv 2986 |
. . . . 5
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
|
164 | | opeq2 4403 |
. . . . . . . 8
|
165 | 164 | breq2d 4665 |
. . . . . . 7
|
166 | | opeq1 4402 |
. . . . . . . 8
|
167 | 166 | breq2d 4665 |
. . . . . . 7
|
168 | | breq1 4656 |
. . . . . . 7
|
169 | 165, 167,
168 | 3orbi123d 1398 |
. . . . . 6
|
170 | 169 | notbid 308 |
. . . . 5
|
171 | 163, 170 | 3anbi23d 1402 |
. . . 4
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
|
172 | 145, 158,
171 | rspc3ev 3326 |
. . 3
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
|
173 | 4, 7, 9, 11, 130, 132, 172 | syl33anc 1341 |
. 2
Cgr
Cgr
Cgr
|
174 | | ovex 6678 |
. . . 4
|
175 | 174 | mptex 6486 |
. . 3
|
176 | | f1eq1 6096 |
. . . . . 6
|
177 | | fveq1 6190 |
. . . . . . . . . 10
|
178 | 177 | opeq1d 4408 |
. . . . . . . . 9
|
179 | | fveq1 6190 |
. . . . . . . . . 10
|
180 | 179 | opeq1d 4408 |
. . . . . . . . 9
|
181 | 178, 180 | breq12d 4666 |
. . . . . . . 8
Cgr
Cgr
|
182 | 177 | opeq1d 4408 |
. . . . . . . . 9
|
183 | 179 | opeq1d 4408 |
. . . . . . . . 9
|
184 | 182, 183 | breq12d 4666 |
. . . . . . . 8
Cgr
Cgr
|
185 | 177 | opeq1d 4408 |
. . . . . . . . 9
|
186 | 179 | opeq1d 4408 |
. . . . . . . . 9
|
187 | 185, 186 | breq12d 4666 |
. . . . . . . 8
Cgr
Cgr
|
188 | 181, 184,
187 | 3anbi123d 1399 |
. . . . . . 7
Cgr Cgr Cgr
Cgr
Cgr
Cgr
|
189 | 188 | ralbidv 2986 |
. . . . . 6
Cgr Cgr Cgr
Cgr
Cgr
Cgr
|
190 | 176, 189 | 3anbi12d 1400 |
. . . . 5
Cgr Cgr Cgr
Cgr
Cgr
Cgr
|
191 | 190 | rexbidv 3052 |
. . . 4
Cgr Cgr Cgr
Cgr
Cgr
Cgr
|
192 | 191 | 2rexbidv 3057 |
. . 3
Cgr Cgr Cgr
Cgr
Cgr
Cgr
|
193 | 175, 192 | spcev 3300 |
. 2
Cgr
Cgr
Cgr
Cgr Cgr Cgr
|
194 | 173, 193 | syl 17 |
1
Cgr Cgr Cgr
|