Nearby theorems
|
|
Mathbox for Brendan Leahy |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > poimirlem21 | Structured version Visualization version Unicode version | ||
| Description: Lemma for poimir 31985 stating that, given a face not on a back face of the cube and a simplex in which it's opposite the final point of the walk, there exists exactly one other simplex containing it. (Contributed by Brendan Leahy, 21-Aug-2020.) |
| Ref | Expression |
|---|---|
| poimir.0 |
        |
| poimirlem22.s |
     ..^                       ![]_](_urbrack.gif "]_"){kind=small}      |
| poimirlem22.1 |
|
| poimirlem22.2 |
 |
| poimirlem22.3 |
![/\](wedge.gif "/\"){kind=small}
     |
| poimirlem21.4 |
|
| Ref | Expression |
|---|---|
| poimirlem21 |
  |
,,,,,, ,,, ,,, ,,, ,,, ,, ,,,,, ,,, ,, , ,,,, , ,
,, ,,,,,,() () ()
is distinct from all other
variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | poimir.0 |
. . 3
| |
| 2 | poimirlem22.s |
. . 3
..^ | |
| 3 | poimirlem22.1 |
. . 3
| |
| 4 | poimirlem22.2 |
. . 3
| |
| 5 | poimirlem22.3 |
. . 3
| |
| 6 | poimirlem21.4 |
. . 3
| |
| 7 | 1, 2, 3, 4, 5, 6 | poimirlem20 31972 |
. 2
|
| 8 | 6 | adantr 467 |
. . . . . . . 8
|
| 9 | 1 | nnred 10631 |
. . . . . . . . . . . . . . . 16
 |
| 10 | 9 | ltm1d 10546 |
. . . . . . . . . . . . . . 15
|
| 11 | nnm1nn0 10918 |
. . . . . . . . . . . . . . . . . 18
 | |
| 12 | 1, 11 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
| 13 | 12 | nn0red 10933 |
. . . . . . . . . . . . . . . 16
|
| 14 | 13, 9 | ltnled 9787 |
. . . . . . . . . . . . . . 15
  
|
| 15 | 10, 14 | mpbid 214 |
. . . . . . . . . . . . . 14
|
| 16 | elfzle2 11810 |
. . . . . . . . . . . . . 14
| |
| 17 | 15, 16 | nsyl 125 |
. . . . . . . . . . . . 13
|
| 18 | eleq1 2519 |
. . . . . . . . . . . . . 14
| |
| 19 | 18 | notbid 296 |
. . . . . . . . . . . . 13
|
| 20 | 17, 19 | syl5ibrcom 226 |
. . . . . . . . . . . 12
|
| 21 | 20 | necon2ad 2641 |
. . . . . . . . . . 11
|
| 22 | 21 | adantr 467 |
. . . . . . . . . 10
|
| 23 | 1 | ad2antrr 733 |
. . . . . . . . . . . . . 14
|
| 24 | fveq2 5870 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 25 | 24 | breq2d 4417 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 26 | 25 | ifbid 3905 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 27 | 26 | csbeq1d 3372 |
. . . . . . . . . . . . . . . . . . . 20
|
| 28 | fveq2 5870 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 29 | 28 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 30 | 28 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 31 | 30 | imaeq1d 5170 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 32 | 31 | xpeq1d 4860 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 33 | 30 | imaeq1d 5170 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 34 | 33 | xpeq1d 4860 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 35 | 32, 34 | uneq12d 3591 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 36 | 29, 35 | oveq12d 6313 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 37 | 36 | csbeq2dv 3783 |
. . . . . . . . . . . . . . . . . . . 20
|
| 38 | 27, 37 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . . 19
|
| 39 | 38 | mpteq2dv 4493 |
. . . . . . . . . . . . . . . . . 18
|
| 40 | 39 | eqeq2d 2463 |
. . . . . . . . . . . . . . . . 17
|
| 41 | 40, 2 | elrab2 3200 |
. . . . . . . . . . . . . . . 16
..^
|
| 42 | 41 | simprbi 466 |
. . . . . . . . . . . . . . 15
|
| 43 | 42 | ad2antlr 734 |
. . . . . . . . . . . . . 14
|
| 44 | elrabi 3195 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ | |
| 45 | 44, 2 | eleq2s 2549 |
. . . . . . . . . . . . . . . . . . 19
..^ |
| 46 | xp1st 6828 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ | |
| 47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . . 18
..^ |
| 48 | xp1st 6828 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ | |
| 49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
..^ |
| 50 | elmapi 7498 |
. . . . . . . . . . . . . . . . 17
..^ ..^ | |
| 51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
..^ |
| 52 | elfzoelz 11927 |
. . . . . . . . . . . . . . . . 17
..^
 | |
| 53 | 52 | ssriv 3438 |
. . . . . . . . . . . . . . . 16
..^  |
| 54 | fss 5742 |
. . . . . . . . . . . . . . . 16
..^ ..^
| |
| 55 | 51, 53, 54 | sylancl 669 |
. . . . . . . . . . . . . . 15
|
| 56 | 55 | ad2antlr 734 |
. . . . . . . . . . . . . 14
|
| 57 | xp2nd 6829 |
. . . . . . . . . . . . . . . . 17
..^ | |
| 58 | 47, 57 | syl 17 |
. . . . . . . . . . . . . . . 16
|
| 59 | fvex 5880 |
. . . . . . . . . . . . . . . . 17
 | |
| 60 | f1oeq1 5810 |
. . . . . . . . . . . . . . . . 17
| |
| 61 | 59, 60 | elab 3187 |
. . . . . . . . . . . . . . . 16
|
| 62 | 58, 61 | sylib 200 |
. . . . . . . . . . . . . . 15
|
| 63 | 62 | ad2antlr 734 |
. . . . . . . . . . . . . 14
|
| 64 | simpr 463 |
. . . . . . . . . . . . . 14
| |
| 65 | 23, 43, 56, 63, 64 | poimirlem1 31953 |
. . . . . . . . . . . . 13
|
| 66 | 1 | ad2antrr 733 |
. . . . . . . . . . . . . . . . 17
|
| 67 | fveq2 5870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 68 | 67 | breq2d 4417 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 69 | 68 | ifbid 3905 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 70 | 69 | csbeq1d 3372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 71 | fveq2 5870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 72 | 71 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 73 | 71 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 74 | 73 | imaeq1d 5170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 75 | 74 | xpeq1d 4860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 76 | 73 | imaeq1d 5170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 77 | 76 | xpeq1d 4860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 78 | 75, 77 | uneq12d 3591 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 79 | 72, 78 | oveq12d 6313 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 80 | 79 | csbeq2dv 3783 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 81 | 70, 80 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 82 | 81 | mpteq2dv 4493 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 83 | 82 | eqeq2d 2463 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 84 | 83, 2 | elrab2 3200 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 85 | 84 | simprbi 466 |
. . . . . . . . . . . . . . . . . . 19
|
| 86 | 4, 85 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
| 87 | 86 | ad2antrr 733 |
. . . . . . . . . . . . . . . . 17
|
| 88 | elrabi 3195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
..^ | |
| 89 | 88, 2 | eleq2s 2549 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
| 90 | 4, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
| 91 | xp1st 6828 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^ | |
| 92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
| 93 | xp1st 6828 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ | |
| 94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
| 95 | elmapi 7498 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ | |
| 96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
..^ |
| 97 | fss 5742 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
| |
| 98 | 96, 53, 97 | sylancl 669 |
. . . . . . . . . . . . . . . . . 18
|
| 99 | 98 | ad2antrr 733 |
. . . . . . . . . . . . . . . . 17
|
| 100 | xp2nd 6829 |
. . . . . . . . . . . . . . . . . . . 20
..^ | |
| 101 | 92, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
| 102 | fvex 5880 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 103 | f1oeq1 5810 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 104 | 102, 103 | elab 3187 |
. . . . . . . . . . . . . . . . . . 19
|
| 105 | 101, 104 | sylib 200 |
. . . . . . . . . . . . . . . . . 18
|
| 106 | 105 | ad2antrr 733 |
. . . . . . . . . . . . . . . . 17
|
| 107 | simplr 763 |
. . . . . . . . . . . . . . . . 17
| |
| 108 | xp2nd 6829 |
. . . . . . . . . . . . . . . . . . . 20
..^ | |
| 109 | 90, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
| 110 | 109 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
|
| 111 | eldifsn 4100 |
. . . . . . . . . . . . . . . . . . 19
![\](setminus.gif "\"){kind=small}
| |
| 112 | 111 | biimpri 210 |
. . . . . . . . . . . . . . . . . 18
|
| 113 | 110, 112 | sylan 474 |
. . . . . . . . . . . . . . . . 17
|
| 114 | 66, 87, 99, 106, 107, 113 | poimirlem2 31954 |
. . . . . . . . . . . . . . . 16
|
| 115 | 114 | ex 436 |
. . . . . . . . . . . . . . 15
|
| 116 | 115 | necon1bd 2644 |
. . . . . . . . . . . . . 14
|
| 117 | 116 | adantlr 722 |
. . . . . . . . . . . . 13
|
| 118 | 65, 117 | mpd 15 |
. . . . . . . . . . . 12
|
| 119 | 118 | neeq1d 2685 |
. . . . . . . . . . 11
|
| 120 | 119 | exbiri 628 |
. . . . . . . . . 10
|
| 121 | 22, 120 | mpdd 41 |
. . . . . . . . 9
|
| 122 | 121 | necon2bd 2642 |
. . . . . . . 8
|
| 123 | 8, 122 | mpd 15 |
. . . . . . 7
|
| 124 | xp2nd 6829 |
. . . . . . . . 9
..^ | |
| 125 | 45, 124 | syl 17 |
. . . . . . . 8
|
| 126 | nn0uz 11200 |
. . . . . . . . . . . . . . . . . 18
 | |
| 127 | 12, 126 | syl6eleq 2541 |
. . . . . . . . . . . . . . . . 17
|
| 128 | fzpred 11851 |
. . . . . . . . . . . . . . . . 17
| |
| 129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . . 16
|
| 130 | 0p1e1 10728 |
. . . . . . . . . . . . . . . . . 18
| |
| 131 | 130 | oveq1i 6305 |
. . . . . . . . . . . . . . . . 17
|
| 132 | 131 | uneq2i 3587 |
. . . . . . . . . . . . . . . 16
|
| 133 | 129, 132 | syl6eq 2503 |
. . . . . . . . . . . . . . 15
|
| 134 | 133 | eleq2d 2516 |
. . . . . . . . . . . . . 14
|
| 135 | 134 | notbid 296 |
. . . . . . . . . . . . 13
|
| 136 | ioran 493 |
. . . . . . . . . . . . . 14
 | |
| 137 | elun 3576 |
. . . . . . . . . . . . . . 15
| |
| 138 | fvex 5880 |
. . . . . . . . . . . . . . . . 17
| |
| 139 | 138 | elsnc 3994 |
. . . . . . . . . . . . . . . 16
|
| 140 | 139 | orbi1i 523 |
. . . . . . . . . . . . . . 15
|
| 141 | 137, 140 | bitri 253 |
. . . . . . . . . . . . . 14
|
| 142 | 136, 141 | xchnxbir 311 |
. . . . . . . . . . . . 13
|
| 143 | 135, 142 | syl6bb 265 |
. . . . . . . . . . . 12
|
| 144 | 143 | anbi2d 711 |
. . . . . . . . . . 11
|
| 145 | uncom 3580 |
. . . . . . . . . . . . . . . 16
| |
| 146 | 145 | difeq1i 3549 |
. . . . . . . . . . . . . . 15
|
| 147 | difun2 3849 |
. . . . . . . . . . . . . . 15
| |
| 148 | 146, 147 | eqtri 2475 |
. . . . . . . . . . . . . 14
|
| 149 | 1 | nncnd 10632 |
. . . . . . . . . . . . . . . . . . 19
 |
| 150 | npcan1 10051 |
. . . . . . . . . . . . . . . . . . 19
| |
| 151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
| 152 | 1 | nnnn0d 10932 |
. . . . . . . . . . . . . . . . . . 19
|
| 153 | 152, 126 | syl6eleq 2541 |
. . . . . . . . . . . . . . . . . 18
|
| 154 | 151, 153 | eqeltrd 2531 |
. . . . . . . . . . . . . . . . 17
|
| 155 | 12 | nn0zd 11045 |
. . . . . . . . . . . . . . . . . . 19
|
| 156 | uzid 11180 |
. . . . . . . . . . . . . . . . . . 19
| |
| 157 | peano2uz 11219 |
. . . . . . . . . . . . . . . . . . 19
| |
| 158 | 155, 156, 157 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
|
| 159 | 151, 158 | eqeltrrd 2532 |
. . . . . . . . . . . . . . . . 17
|
| 160 | fzsplit2 11831 |
. . . . . . . . . . . . . . . . 17
| |
| 161 | 154, 159, 160 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
|
| 162 | 151 | oveq1d 6310 |
. . . . . . . . . . . . . . . . . 18
|
| 163 | 1 | nnzd 11046 |
. . . . . . . . . . . . . . . . . . 19
|
| 164 | fzsn 11847 |
. . . . . . . . . . . . . . . . . . 19
| |
| 165 | 163, 164 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
| 166 | 162, 165 | eqtrd 2487 |
. . . . . . . . . . . . . . . . 17
|
| 167 | 166 | uneq2d 3590 |
. . . . . . . . . . . . . . . 16
|
| 168 | 161, 167 | eqtrd 2487 |
. . . . . . . . . . . . . . 15
|
| 169 | 168 | difeq1d 3552 |
. . . . . . . . . . . . . 14
|
| 170 | elfzle2 11810 |
. . . . . . . . . . . . . . . 16
| |
| 171 | 15, 170 | nsyl 125 |
. . . . . . . . . . . . . . 15
|
| 172 | incom 3627 |
. . . . . . . . . . . . . . . . 17
 | |
| 173 | 172 | eqeq1i 2458 |
. . . . . . . . . . . . . . . 16
 |
| 174 | disjsn 4034 |
. . . . . . . . . . . . . . . 16
| |
| 175 | disj3 3811 |
. . . . . . . . . . . . . . . 16
| |
| 176 | 173, 174, 175 | 3bitr3i 279 |
. . . . . . . . . . . . . . 15
|
| 177 | 171, 176 | sylib 200 |
. . . . . . . . . . . . . 14
|
| 178 | 148, 169, 177 | 3eqtr4a 2513 |
. . . . . . . . . . . . 13
|
| 179 | 178 | eleq2d 2516 |
. . . . . . . . . . . 12
|
| 180 | eldif 3416 |
. . . . . . . . . . . 12
| |
| 181 | 138 | elsnc 3994 |
. . . . . . . . . . . 12
|
| 182 | 179, 180, 181 | 3bitr3g 291 |
. . . . . . . . . . 11
|
| 183 | 144, 182 | bitr3d 259 |
. . . . . . . . . 10
|
| 184 | 183 | biimpd 211 |
. . . . . . . . 9
|
| 185 | 184 | expdimp 439 |
. . . . . . . 8
|
| 186 | 125, 185 | sylan2 477 |
. . . . . . 7
|
| 187 | 123, 186 | mpan2d 681 |
. . . . . 6
|
| 188 | 1, 2, 3 | poimirlem14 31966 |
. . . . . . . . . 10
|
| 189 | fveq2 5870 |
. . . . . . . . . . . 12
| |
| 190 | 189 | eqeq1d 2455 |
. . . . . . . . . . 11
|
| 191 | 190 | rmo4 3233 |
. . . . . . . . . 10
|
| 192 | 188, 191 | sylib 200 |
. . . . . . . . 9
|
| 193 | 192 | r19.21bi 2759 |
. . . . . . . 8
|
| 194 | 4 | adantr 467 |
. . . . . . . 8
|
| 195 | fveq2 5870 |
. . . . . . . . . . . 12
| |
| 196 | 195 | eqeq1d 2455 |
. . . . . . . . . . 11
|
| 197 | 196 | anbi2d 711 |
. . . . . . . . . 10
|
| 198 | eqeq2 2464 |
. . . . . . . . . 10
| |
| 199 | 197, 198 | imbi12d 322 |
. . . . . . . . 9
|
| 200 | 199 | rspccv 3149 |
. . . . . . . 8
|
| 201 | 193, 194, 200 | sylc 62 |
. . . . . . 7
|
| 202 | 8, 201 | mpan2d 681 |
. . . . . 6
|
| 203 | 187, 202 | syld 45 |
. . . . 5
|
| 204 | 203 | necon1ad 2643 |
. . . 4
|
| 205 | 204 | ralrimiva 2804 |
. . 3
|
| 206 | 1, 2, 3 | poimirlem13 31965 |
. . 3
|
| 207 | rmoim 3241 |
. . 3
| |
| 208 | 205, 206, 207 | sylc 62 |
. 2
|
| 209 | reu5 3010 |
. 2
| |
| 210 | 7, 208, 209 | sylanbrc 671 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wo 370
wa 371
wceq 1446
wcel 1889
cab 2439
wne 2624
wral 2739
wrex 2740
wreu 2741
wrmo 2742
crab 2743
csb 3365
cdif 3403
cun 3404
cin 3405
wss 3406
c0 3733
cif 3883
csn 3970
class class class wbr 4405 cmpt 4464 cxp 4835 crn 4838 cima 4840 wf 5581 wf1o 5584
cfv 5585
(class class class)co 6295 cof 6534
c1st 6796
c2nd 6797
cmap 7477
cc 9542
cc0 9544
c1 9545
caddc 9547 clt 9680 cle 9681 cmin 9865 cn 10616 cn0 10876 cz 10944 cuz 11166 cfz 11791 ..^cfzo 11922 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-rep 4518 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588 ax-cnex 9600 ax-resscn 9601 ax-1cn 9602 ax-icn 9603 ax-addcl 9604 ax-addrcl 9605 ax-mulcl 9606 ax-mulrcl 9607 ax-mulcom 9608 ax-addass 9609 ax-mulass 9610 ax-distr 9611 ax-i2m1 9612 ax-1ne0 9613 ax-1rid 9614 ax-rnegex 9615 ax-rrecex 9616 ax-cnre 9617 ax-pre-lttri 9618 ax-pre-lttrn 9619 ax-pre-ltadd 9620 ax-pre-mulgt0 9621 |
| This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-nel 2627 df-ral 2744 df-rex 2745 df-reu 2746 df-rmo 2747 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-iun 4283 df-br 4406 df-opab 4465 df-mpt 4466 df-tr 4501 df-eprel 4748 df-id 4752 df-po 4758 df-so 4759 df-fr 4796 df-we 4798 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-pred 5383 df-ord 5429 df-on 5430 df-lim 5431 df-suc 5432 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-riota 6257 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-of 6536 df-om 6698 df-1st 6798 df-2nd 6799 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-er 7368 df-map 7479 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-pnf 9682 df-mnf 9683 df-xr 9684 df-ltxr 9685 df-le 9686 df-sub 9867 df-neg 9868 df-nn 10617 df-n0 10877 df-z 10945 df-uz 11167 df-fz 11792 df-fzo 11923 |
| This theorem is referenced by: poimirlem22 31974 |
| Copyright terms: Public domain | W3C validator |