Nearby theorems
|
|
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > iccpartnel | Structured version Unicode version | |
| Description: A point of a partition is not an element of any open interval determined by the partition. Corresponds to fourierdlem12 37845 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 8-Jul-2020.) |
| Ref | Expression |
|---|---|
| iccpartnel.m |
        |
| iccpartnel.p |
 RePart |
| iccpartnel.x |
  |
| Ref | Expression |
|---|---|
| iccpartnel |
![/\](wedge.gif "/\"){kind=small}
  ..^ 
   |
are
mutually distinct and distinct from all other variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elioo3g 11667 |
. . 3
| |
| 2 | iccpartnel.x |
. . . . . . 7
| |
| 3 | iccpartnel.p |
. . . . . . . . 9
RePart | |
| 4 | iccpartnel.m |
. . . . . . . . . . 11
| |
| 5 | iccpart 38486 |
. . . . . . . . . . 11
RePart
   ..^
| |
| 6 | 4, 5 | syl 17 |
. . . . . . . . . 10
RePart
..^
|
| 7 | elmapfn 7500 |
. . . . . . . . . . 11
 | |
| 8 | 7 | adantr 467 |
. . . . . . . . . 10
..^ |
| 9 | 6, 8 | syl6bi 232 |
. . . . . . . . 9
RePart |
| 10 | 3, 9 | mpd 15 |
. . . . . . . 8
|
| 11 | fvelrnb 5926 |
. . . . . . . 8
  | |
| 12 | 10, 11 | syl 17 |
. . . . . . 7
|
| 13 | 2, 12 | mpbid 214 |
. . . . . 6
|
| 14 | elfzelz 11802 |
. . . . . . . . . . . . 13
 | |
| 15 | 14 | zred 11042 |
. . . . . . . . . . . 12
 |
| 16 | 15 | adantl 468 |
. . . . . . . . . . 11
|
| 17 | elfzoelz 11922 |
. . . . . . . . . . . 12
..^
| |
| 18 | 17 | zred 11042 |
. . . . . . . . . . 11
..^
|
| 19 | lelttric 9743 |
. . . . . . . . . . 11
 
| |
| 20 | 16, 18, 19 | syl2an 480 |
. . . . . . . . . 10
..^
|
| 21 | breq2 4425 |
. . . . . . . . . . . . . . . . . 18
| |
| 22 | breq1 4424 |
. . . . . . . . . . . . . . . . . 18
| |
| 23 | 21, 22 | anbi12d 716 |
. . . . . . . . . . . . . . . . 17
|
| 24 | leloe 9722 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 25 | 16, 18, 24 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 26 | 4, 3 | iccpartgt 38497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 27 | 26 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 28 | 27 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
|
| 29 | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 30 | elfzofz 11937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^
| |
| 31 | breq1 4424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 32 | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
| |
| 33 | 32 | breq1d 4431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 34 | 31, 33 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 35 | breq2 4425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 36 | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
| |
| 37 | 36 | breq2d 4433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 38 | 35, 37 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 39 | 34, 38 | rspc2v 3192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 40 | 29, 30, 39 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
|
| 41 | 28, 40 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^
|
| 42 | pm3.35 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
| |
| 43 | 4 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
| 44 | 3 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
RePart |
| 45 | 43, 44, 29 | iccpartxr 38489 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
| 46 | 45 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
..^
|
| 47 | simp1 1006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
| |
| 48 | xrltle 11450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
| |
| 49 | 46, 47, 48 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
..^
|
| 50 | xrlenlt 9701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
| |
| 51 | 46, 47, 50 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
..^
|
| 52 | 49, 51 | sylibd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
..^
|
| 53 | 52 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
..^
|
| 54 | 53 | com13 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
..^
|
| 55 | 54 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
..^ |
| 56 | 55 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
..^
|
| 57 | 56 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
..^
|
| 58 | 57 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^
|
| 59 | 58 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^
|
| 60 | 42, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^
|
| 61 | 60 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
|
| 62 | 61 | com13 84 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^
|
| 63 | 41, 62 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
|
| 64 | 63 | com12 33 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
| 65 | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
| |
| 66 | 65 | breq2d 4433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 67 | 66 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 68 | xrltnr 11423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 69 | 68 | 3ad2ant1 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 70 | 69 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 71 | 70 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 72 | 67, 71 | sylbid 219 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 73 | 72 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 74 | 73 | a1d 27 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
| 75 | 64, 74 | jaoi 381 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
| 76 | 75 | com12 33 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 77 | 25, 76 | sylbid 219 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 78 | 77 | com23 82 |
. . . . . . . . . . . . . . . . . . 19
..^
|
| 79 | 78 | com14 92 |
. . . . . . . . . . . . . . . . . 18
..^
|
| 80 | 79 | adantr 467 |
. . . . . . . . . . . . . . . . 17
..^
|
| 81 | 23, 80 | syl6bir 233 |
. . . . . . . . . . . . . . . 16
..^
|
| 82 | 81 | com14 92 |
. . . . . . . . . . . . . . 15
..^
|
| 83 | 82 | com23 82 |
. . . . . . . . . . . . . 14
..^
|
| 84 | 83 | impd 433 |
. . . . . . . . . . . . 13
..^
|
| 85 | 84 | com24 91 |
. . . . . . . . . . . 12
..^
|
| 86 | 14 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 87 | zltp1le 10988 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 88 | 17, 86, 87 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 89 | 17 | peano2zd 11045 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
| 90 | 89 | zred 11042 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
| 91 | leloe 9722 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 92 | 90, 16, 91 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 93 | 88, 92 | bitrd 257 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 94 | fzofzp1 12009 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
| |
| 95 | breq1 4424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
| |
| 96 | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 97 | 96 | breq1d 4431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 98 | 95, 97 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 99 | breq2 4425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
| |
| 100 | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 101 | 100 | breq2d 4433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 102 | 99, 101 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 103 | 98, 102 | rspc2v 3192 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 104 | 94, 29, 103 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^
|
| 105 | 28, 104 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
|
| 106 | pm3.35 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 107 | simp2 1007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
| |
| 108 | xrltnsym 11438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
| |
| 109 | 46, 107, 108 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
..^
|
| 110 | 109 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
..^
|
| 111 | 110 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
..^
|
| 112 | 111 | expcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
..^
|
| 113 | 112 | expd 438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^
|
| 114 | 113 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^
|
| 115 | 114 | com14 92 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^
|
| 116 | 106, 115 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
|
| 117 | 116 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^
|
| 118 | 117 | com13 84 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
|
| 119 | 105, 118 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
| 120 | 119 | com12 33 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
| 121 | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 122 | 121 | breq2d 4433 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 123 | 121 | breq1d 4431 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 124 | 122, 123 | anbi12d 716 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 125 | xrltnr 11423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 126 | 125 | 3ad2ant2 1028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 127 | 126 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 128 | 127 | com12 33 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 129 | 128 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 130 | 124, 129 | syl6bir 233 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 131 | 130 | com23 82 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 132 | 131 | a1d 27 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
| 133 | 120, 132 | jaoi 381 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 134 | 133 | com12 33 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 135 | 93, 134 | sylbid 219 |
. . . . . . . . . . . . . . . . . . 19
..^
|
| 136 | 135 | com23 82 |
. . . . . . . . . . . . . . . . . 18
..^
|
| 137 | 136 | com14 92 |
. . . . . . . . . . . . . . . . 17
..^
|
| 138 | 23, 137 | syl6bir 233 |
. . . . . . . . . . . . . . . 16
..^
|
| 139 | 138 | com14 92 |
. . . . . . . . . . . . . . 15
..^
|
| 140 | 139 | com23 82 |
. . . . . . . . . . . . . 14
..^
|
| 141 | 140 | impd 433 |
. . . . . . . . . . . . 13
..^
|
| 142 | 141 | com24 91 |
. . . . . . . . . . . 12
..^
|
| 143 | 85, 142 | jaoi 381 |
. . . . . . . . . . 11
..^
|
| 144 | 143 | com12 33 |
. . . . . . . . . 10
..^
|
| 145 | 20, 144 | mpd 15 |
. . . . . . . . 9
..^
|
| 146 | 145 | ex 436 |
. . . . . . . 8
..^
|
| 147 | 146 | com23 82 |
. . . . . . 7
..^
|
| 148 | 147 | rexlimdva 2918 |
. . . . . 6
..^
|
| 149 | 13, 148 | mpd 15 |
. . . . 5
..^
|
| 150 | 149 | imp 431 |
. . . 4
..^
|
| 151 | 150 | com12 33 |
. . 3
..^
|
| 152 | 1, 151 | sylbi 199 |
. 2
..^
|
| 153 | ax-1 6 |
. 2
..^
| |
| 154 | 152, 153 | pm2.61i 168 |
1
..^
|
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wb 188 wo 370 wa 371 w3a 983 wceq 1438 wcel 1869 wral 2776 wrex 2777 class class class wbr 4421
crn 4852
wfn 5594
cfv 5599
(class class class)co 6303 cmap 7478 cr 9540 cc0 9541 c1 9542 caddc 9544 cxr 9676 clt 9677 cle 9678 cn 10611 cz 10939 cioo 11637 cfz 11786 ..^cfzo 11917
RePartciccp 38483 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618 |
| This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-iun 4299 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-om 6705 df-1st 6805 df-2nd 6806 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-er 7369 df-map 7480 df-en 7576 df-dom 7577 df-sdom 7578 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-nn 10612 df-2 10670 df-n0 10872 df-z 10940 df-uz 11162 df-ioo 11641 df-fz 11787 df-fzo 11918 df-iccp 38484 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |