Nearby theorems
|
|
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > iccpartnel | Structured version Visualization version Unicode version | ||
| Description: A point of a partition is not an element of any open interval determined by the partition. Corresponds to fourierdlem12 37981 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 11665 |
. . 3
| |
| 2 | iccpartnel.x |
. . . . . . 7
| |
| 3 | iccpartnel.p |
. . . . . . . . 9
RePart | |
| 4 | iccpartnel.m |
. . . . . . . . . . 11
| |
| 5 | iccpart 38730 |
. . . . . . . . . . 11
RePart
   ..^
| |
| 6 | 4, 5 | syl 17 |
. . . . . . . . . 10
RePart
..^
|
| 7 | elmapfn 7494 |
. . . . . . . . . . 11
 | |
| 8 | 7 | adantr 467 |
. . . . . . . . . 10
..^ |
| 9 | 6, 8 | syl6bi 232 |
. . . . . . . . 9
RePart |
| 10 | 3, 9 | mpd 15 |
. . . . . . . 8
|
| 11 | fvelrnb 5912 |
. . . . . . . 8
  | |
| 12 | 10, 11 | syl 17 |
. . . . . . 7
|
| 13 | 2, 12 | mpbid 214 |
. . . . . 6
|
| 14 | elfzelz 11800 |
. . . . . . . . . . . . 13
 | |
| 15 | 14 | zred 11040 |
. . . . . . . . . . . 12
 |
| 16 | 15 | adantl 468 |
. . . . . . . . . . 11
|
| 17 | elfzoelz 11920 |
. . . . . . . . . . . 12
..^
| |
| 18 | 17 | zred 11040 |
. . . . . . . . . . 11
..^
|
| 19 | lelttric 9741 |
. . . . . . . . . . 11
 
| |
| 20 | 16, 18, 19 | syl2an 480 |
. . . . . . . . . 10
..^
|
| 21 | breq2 4406 |
. . . . . . . . . . . . . . . . . 18
| |
| 22 | breq1 4405 |
. . . . . . . . . . . . . . . . . 18
| |
| 23 | 21, 22 | anbi12d 717 |
. . . . . . . . . . . . . . . . 17
|
| 24 | leloe 9720 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 25 | 16, 18, 24 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 26 | 4, 3 | iccpartgt 38741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 27 | 26 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 28 | 27 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
|
| 29 | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 30 | elfzofz 11935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^
| |
| 31 | breq1 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 32 | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
| |
| 33 | 32 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 34 | 31, 33 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 35 | breq2 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 36 | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
| |
| 37 | 36 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 38 | 35, 37 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 39 | 34, 38 | rspc2v 3159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 40 | 29, 30, 39 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
|
| 41 | 28, 40 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^
|
| 42 | pm3.35 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
| |
| 43 | 4 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
| 44 | 3 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
RePart |
| 45 | 43, 44, 29 | iccpartxr 38733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
| 46 | 45 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
..^
|
| 47 | simp1 1008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
| |
| 48 | xrltle 11448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
| |
| 49 | 46, 47, 48 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
..^
|
| 50 | xrlenlt 9699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
| |
| 51 | 46, 47, 50 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
..^
|
| 52 | 49, 51 | sylibd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
..^
|
| 53 | 52 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
..^
|
| 54 | 53 | com13 83 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 83 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^
|
| 63 | 41, 62 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
|
| 64 | 63 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
| 65 | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
| |
| 66 | 65 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 67 | 66 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 68 | xrltnr 11421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 69 | 68 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 26 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
| 75 | 64, 74 | jaoi 381 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
| 76 | 75 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 77 | 25, 76 | sylbid 219 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 78 | 77 | com23 81 |
. . . . . . . . . . . . . . . . . . 19
..^
|
| 79 | 78 | com14 91 |
. . . . . . . . . . . . . . . . . 18
..^
|
| 80 | 79 | adantr 467 |
. . . . . . . . . . . . . . . . 17
..^
|
| 81 | 23, 80 | syl6bir 233 |
. . . . . . . . . . . . . . . 16
..^
|
| 82 | 81 | com14 91 |
. . . . . . . . . . . . . . 15
..^
|
| 83 | 82 | com23 81 |
. . . . . . . . . . . . . 14
..^
|
| 84 | 83 | impd 433 |
. . . . . . . . . . . . 13
..^
|
| 85 | 84 | com24 90 |
. . . . . . . . . . . 12
..^
|
| 86 | 14 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 87 | zltp1le 10986 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 88 | 17, 86, 87 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 89 | 17 | peano2zd 11043 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
| 90 | 89 | zred 11040 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
| 91 | leloe 9720 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 92 | 90, 16, 91 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 93 | 88, 92 | bitrd 257 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 94 | fzofzp1 12008 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
| |
| 95 | breq1 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
| |
| 96 | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 97 | 96 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 98 | 95, 97 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 99 | breq2 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
| |
| 100 | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 101 | 100 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 102 | 99, 101 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 103 | 98, 102 | rspc2v 3159 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 104 | 94, 29, 103 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^
|
| 105 | 28, 104 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
|
| 106 | pm3.35 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 107 | simp2 1009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
| |
| 108 | xrltnsym 11436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^
|
| 116 | 106, 115 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
|
| 117 | 116 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^
|
| 118 | 117 | com13 83 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
|
| 119 | 105, 118 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
| 120 | 119 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
| 121 | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 122 | 121 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 123 | 121 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 124 | 122, 123 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 125 | xrltnr 11421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 126 | 125 | 3ad2ant2 1030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 127 | 126 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 128 | 127 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 129 | 128 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 130 | 124, 129 | syl6bir 233 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 131 | 130 | com23 81 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 132 | 131 | a1d 26 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
| 133 | 120, 132 | jaoi 381 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 134 | 133 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 135 | 93, 134 | sylbid 219 |
. . . . . . . . . . . . . . . . . . 19
..^
|
| 136 | 135 | com23 81 |
. . . . . . . . . . . . . . . . . 18
..^
|
| 137 | 136 | com14 91 |
. . . . . . . . . . . . . . . . 17
..^
|
| 138 | 23, 137 | syl6bir 233 |
. . . . . . . . . . . . . . . 16
..^
|
| 139 | 138 | com14 91 |
. . . . . . . . . . . . . . 15
..^
|
| 140 | 139 | com23 81 |
. . . . . . . . . . . . . 14
..^
|
| 141 | 140 | impd 433 |
. . . . . . . . . . . . 13
..^
|
| 142 | 141 | com24 90 |
. . . . . . . . . . . 12
..^
|
| 143 | 85, 142 | jaoi 381 |
. . . . . . . . . . 11
..^
|
| 144 | 143 | com12 32 |
. . . . . . . . . 10
..^
|
| 145 | 20, 144 | mpd 15 |
. . . . . . . . 9
..^
|
| 146 | 145 | ex 436 |
. . . . . . . 8
..^
|
| 147 | 146 | com23 81 |
. . . . . . 7
..^
|
| 148 | 147 | rexlimdva 2879 |
. . . . . 6
..^
|
| 149 | 13, 148 | mpd 15 |
. . . . 5
..^
|
| 150 | 149 | imp 431 |
. . . 4
..^
|
| 151 | 150 | com12 32 |
. . 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 985 wceq 1444 wcel 1887 wral 2737 wrex 2738 class class class wbr 4402
crn 4835
wfn 5577
cfv 5582
(class class class)co 6290 cmap 7472 cr 9538 cc0 9539 c1 9540 caddc 9542 cxr 9674 clt 9675 cle 9676 cn 10609 cz 10937 cioo 11635 cfz 11784 ..^cfzo 11915
RePartciccp 38727 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 |
| This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-er 7363 df-map 7474 df-en 7570 df-dom 7571 df-sdom 7572 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-nn 10610 df-2 10668 df-n0 10870 df-z 10938 df-uz 11160 df-ioo 11639 df-fz 11785 df-fzo 11916 df-iccp 38728 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |