Nearby theorems
|
|
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > ILE Home > Th. List > modfzo0difsn | Unicode version | ||
| Description: For a number within a half-open range of nonnegative integers with one excluded integer there is a positive integer so that the number is equal to the sum of the positive integer and the excluded integer modulo the upper bound of the range. (Contributed by AV, 19-Mar-2021.) |
| Ref | Expression |
|---|---|
| modfzo0difsn |
     ..^  ![/\](wedge.gif "/\"){kind=small}  ..^ ![\](setminus.gif "\"){kind=small}     
 ..^    |
, , ,| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eldifi 3276 |
. . . 4
..^ ..^ | |
| 2 | elfzoelz 10189 |
. . . 4
..^
 | |
| 3 | 1, 2 | syl 14 |
. . 3
..^ |
| 4 | elfzoelz 10189 |
. . 3
..^
| |
| 5 | zdcle 9370 |
. . . 4
DECID  | |
| 6 | exmiddc 837 |
. . . 4
DECID 
 | |
| 7 | 5, 6 | syl 14 |
. . 3
|
| 8 | 3, 4, 7 | syl2anr 290 |
. 2
..^ ..^ |
| 9 | zleloe 9341 |
. . . . . 6
 
| |
| 10 | 3, 4, 9 | syl2anr 290 |
. . . . 5
..^ ..^
|
| 11 | elfzo0 10224 |
. . . . . . . . . . . . 13
..^ 
 | |
| 12 | elfzo0 10224 |
. . . . . . . . . . . . . . . 16
..^
| |
| 13 | nn0cn 9227 |
. . . . . . . . . . . . . . . . . . . . . . 23
 | |
| 14 | 13 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 15 | 14 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 16 | nn0cn 9227 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 17 | 16 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 18 | 17 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 19 | nncn 8968 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 20 | 19 | 3ad2ant2 1021 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 21 | 20 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 22 | 15, 18, 21 | subadd23d 8331 |
. . . . . . . . . . . . . . . . . . . 20
|
| 23 | simpl 109 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 24 | nn0z 9314 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 25 | nnz 9313 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 26 | znnsub 9345 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 27 | 24, 25, 26 | syl2an 289 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 28 | 27 | biimp3a 1356 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 29 | nn0nnaddcl 9248 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 30 | 23, 28, 29 | syl2anr 290 |
. . . . . . . . . . . . . . . . . . . 20
|
| 31 | 22, 30 | eqeltrd 2266 |
. . . . . . . . . . . . . . . . . . 19
|
| 32 | 31 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
|
| 33 | simp2 1000 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 34 | 33 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
|
| 35 | 34 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
|
| 36 | nn0re 9226 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 | |
| 37 | 36 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 38 | 37 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 39 | nn0re 9226 |
. . . . . . . . . . . . . . . . . . . . . . . 24
| |
| 40 | 39 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 41 | 40 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 42 | 38, 41 | sublt0d 8568 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 43 | 42 | bicomd 141 |
. . . . . . . . . . . . . . . . . . . 20
|
| 44 | 43 | biimpa 296 |
. . . . . . . . . . . . . . . . . . 19
|
| 45 | resubcl 8262 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 46 | 37, 40, 45 | syl2anr 290 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 47 | nnre 8967 |
. . . . . . . . . . . . . . . . . . . . . . . 24
| |
| 48 | 47 | 3ad2ant2 1021 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 49 | 48 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 50 | 46, 49 | jca 306 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 51 | 50 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
|
| 52 | ltaddnegr 8423 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 53 | 51, 52 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
|
| 54 | 44, 53 | mpbid 147 |
. . . . . . . . . . . . . . . . . 18
|
| 55 | elfzo1 10232 |
. . . . . . . . . . . . . . . . . 18
..^ | |
| 56 | 32, 35, 54, 55 | syl3anbrc 1183 |
. . . . . . . . . . . . . . . . 17
..^ |
| 57 | 56 | exp31 364 |
. . . . . . . . . . . . . . . 16
..^ |
| 58 | 12, 57 | sylbi 121 |
. . . . . . . . . . . . . . 15
..^
..^ |
| 59 | 58 | com12 30 |
. . . . . . . . . . . . . 14
..^ ..^ |
| 60 | 59 | 3adant2 1018 |
. . . . . . . . . . . . 13
..^ ..^ |
| 61 | 11, 60 | sylbi 121 |
. . . . . . . . . . . 12
..^
..^
..^ |
| 62 | 1, 61 | syl 14 |
. . . . . . . . . . 11
..^
..^ ..^ |
| 63 | 62 | impcom 125 |
. . . . . . . . . 10
..^ ..^ ..^ |
| 64 | 63 | impcom 125 |
. . . . . . . . 9
..^
..^
..^ |
| 65 | oveq1 5911 |
. . . . . . . . . . . 12
| |
| 66 | 2 | zcnd 9417 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
| 67 | 66 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 68 | 16 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 69 | 68 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 70 | 19 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 71 | 70 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 72 | 67, 69, 71 | 3jca 1179 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 73 | 72 | ex 115 |
. . . . . . . . . . . . . . . . . . 19
..^
|
| 74 | 1, 73 | syl 14 |
. . . . . . . . . . . . . . . . . 18
..^ |
| 75 | 74 | com12 30 |
. . . . . . . . . . . . . . . . 17
..^
|
| 76 | 75 | 3adant3 1019 |
. . . . . . . . . . . . . . . 16
..^
|
| 77 | 12, 76 | sylbi 121 |
. . . . . . . . . . . . . . 15
..^
..^
|
| 78 | 77 | imp 124 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 79 | 78 | adantl 277 |
. . . . . . . . . . . . 13
..^
..^
|
| 80 | nppcan 8220 |
. . . . . . . . . . . . 13
| |
| 81 | 79, 80 | syl 14 |
. . . . . . . . . . . 12
..^
..^
|
| 82 | 65, 81 | sylan9eqr 2244 |
. . . . . . . . . . 11
..^
..^ |
| 83 | 82 | oveq1d 5919 |
. . . . . . . . . 10
..^
..^
|
| 84 | 83 | eqeq2d 2201 |
. . . . . . . . 9
..^
..^
|
| 85 | 11 | biimpi 120 |
. . . . . . . . . . . . . 14
..^
|
| 86 | 85 | a1d 22 |
. . . . . . . . . . . . 13
..^
..^
|
| 87 | 1, 86 | syl 14 |
. . . . . . . . . . . 12
..^
..^
|
| 88 | 87 | impcom 125 |
. . . . . . . . . . 11
..^ ..^ |
| 89 | 88 | adantl 277 |
. . . . . . . . . 10
..^
..^
|
| 90 | addmodidr 10416 |
. . . . . . . . . . 11
| |
| 91 | 90 | eqcomd 2195 |
. . . . . . . . . 10
|
| 92 | 89, 91 | syl 14 |
. . . . . . . . 9
..^
..^
|
| 93 | 64, 84, 92 | rspcedvd 2866 |
. . . . . . . 8
..^
..^
..^ |
| 94 | 93 | ex 115 |
. . . . . . 7
..^
..^ ..^ |
| 95 | eldifsn 3741 |
. . . . . . . . . 10
..^
..^  | |
| 96 | eqneqall 2370 |
. . . . . . . . . . . 12
..^ | |
| 97 | 96 | com12 30 |
. . . . . . . . . . 11
..^ |
| 98 | 97 | adantl 277 |
. . . . . . . . . 10
..^
..^ |
| 99 | 95, 98 | sylbi 121 |
. . . . . . . . 9
..^
..^ |
| 100 | 99 | adantl 277 |
. . . . . . . 8
..^ ..^ ..^ |
| 101 | 100 | com12 30 |
. . . . . . 7
..^
..^ ..^ |
| 102 | 94, 101 | jaoi 717 |
. . . . . 6
..^ ..^ ..^ |
| 103 | 102 | com12 30 |
. . . . 5
..^ ..^ ..^ |
| 104 | 10, 103 | sylbid 150 |
. . . 4
..^ ..^ ..^ |
| 105 | 104 | com12 30 |
. . 3
..^
..^ ..^ |
| 106 | zltnle 9340 |
. . . . . . . . . 10
| |
| 107 | 4, 3, 106 | syl2an 289 |
. . . . . . . . 9
..^ ..^
|
| 108 | 107 | bicomd 141 |
. . . . . . . 8
..^ ..^ |
| 109 | 24 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . . . . 18
|
| 110 | nn0z 9314 |
. . . . . . . . . . . . . . . . . . 19
| |
| 111 | 110 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
|
| 112 | znnsub 9345 |
. . . . . . . . . . . . . . . . . 18
| |
| 113 | 109, 111, 112 | syl2anr 290 |
. . . . . . . . . . . . . . . . 17
|
| 114 | 113 | biimpa 296 |
. . . . . . . . . . . . . . . 16
|
| 115 | 33 | adantl 277 |
. . . . . . . . . . . . . . . . 17
|
| 116 | 115 | adantr 276 |
. . . . . . . . . . . . . . . 16
|
| 117 | nn0ge0 9242 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 118 | 117 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 119 | 118 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 120 | subge02 8476 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 121 | 36, 40, 120 | syl2an 289 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 122 | 119, 121 | mpbid 147 |
. . . . . . . . . . . . . . . . . . . 20
|
| 123 | 40 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 124 | 36 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 125 | 48 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 126 | 123, 124, 125 | 3jca 1179 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 127 | 45 | ancoms 268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 128 | 127 | 3adant3 1019 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 129 | simp2 1000 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 130 | simp3 1001 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 131 | 128, 129, 130 | 3jca 1179 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 132 | 126, 131 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 133 | lelttr 8087 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 134 | 132, 133 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
|
| 135 | 122, 134 | mpand 429 |
. . . . . . . . . . . . . . . . . . 19
|
| 136 | 135 | impancom 260 |
. . . . . . . . . . . . . . . . . 18
|
| 137 | 136 | imp 124 |
. . . . . . . . . . . . . . . . 17
|
| 138 | 137 | adantr 276 |
. . . . . . . . . . . . . . . 16
|
| 139 | 114, 116, 138 | 3jca 1179 |
. . . . . . . . . . . . . . 15
|
| 140 | 139 | exp31 364 |
. . . . . . . . . . . . . 14
|
| 141 | 140 | 3adant2 1018 |
. . . . . . . . . . . . 13
|
| 142 | 11, 141 | sylbi 121 |
. . . . . . . . . . . 12
..^
|
| 143 | 1, 142 | syl 14 |
. . . . . . . . . . 11
..^
|
| 144 | 143 | com12 30 |
. . . . . . . . . 10
..^
|
| 145 | 12, 144 | sylbi 121 |
. . . . . . . . 9
..^
..^
|
| 146 | 145 | imp 124 |
. . . . . . . 8
..^ ..^
|
| 147 | 108, 146 | sylbid 150 |
. . . . . . 7
..^ ..^ |
| 148 | 147 | impcom 125 |
. . . . . 6
..^
..^
|
| 149 | elfzo1 10232 |
. . . . . 6
..^ | |
| 150 | 148, 149 | sylibr 134 |
. . . . 5
..^
..^
..^ |
| 151 | oveq1 5911 |
. . . . . . . 8
| |
| 152 | 1, 66 | syl 14 |
. . . . . . . . . 10
..^ |
| 153 | 4 | zcnd 9417 |
. . . . . . . . . 10
..^
|
| 154 | npcan 8207 |
. . . . . . . . . 10
| |
| 155 | 152, 153, 154 | syl2anr 290 |
. . . . . . . . 9
..^ ..^ |
| 156 | 155 | adantl 277 |
. . . . . . . 8
..^
..^
|
| 157 | 151, 156 | sylan9eqr 2244 |
. . . . . . 7
..^ ..^
|
| 158 | 157 | oveq1d 5919 |
. . . . . 6
..^ ..^
|
| 159 | 158 | eqeq2d 2201 |
. . . . 5
..^ ..^
|
| 160 | zmodidfzoimp 10397 |
. . . . . . . . 9
..^
| |
| 161 | 1, 160 | syl 14 |
. . . . . . . 8
..^ |
| 162 | 161 | adantl 277 |
. . . . . . 7
..^ ..^ |
| 163 | 162 | adantl 277 |
. . . . . 6
..^
..^
|
| 164 | 163 | eqcomd 2195 |
. . . . 5
..^
..^
|
| 165 | 150, 159, 164 | rspcedvd 2866 |
. . . 4
..^
..^
..^ |
| 166 | 165 | ex 115 |
. . 3
..^
..^ ..^ |
| 167 | 105, 166 | jaoi 717 |
. 2
..^ ..^
..^ |
| 168 | 8, 167 | mpcom 36 |
1
..^ ..^
..^ |
| Colors of variables: wff set class |
| Syntax hints: wn 3
wi 4
wa 104
wb 105 wo 709 DECID wdc 835
w3a 980
wceq 1364
wcel 2160
wne 2360
wrex 2469
cdif 3145
csn 3614
class class class wbr 4025 (class class class)co 5904
cc 7849
cr 7850
cc0 7851
c1 7852
caddc 7854 clt 8033 cle 8034 cmin 8169 cn 8960 cn0 9217 cz 9294 ..^cfzo 10184
cmo 10365 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-sep 4143 ax-pow 4199 ax-pr 4234 ax-un 4458 ax-setind 4561 ax-cnex 7942 ax-resscn 7943 ax-1cn 7944 ax-1re 7945 ax-icn 7946 ax-addcl 7947 ax-addrcl 7948 ax-mulcl 7949 ax-mulrcl 7950 ax-addcom 7951 ax-mulcom 7952 ax-addass 7953 ax-mulass 7954 ax-distr 7955 ax-i2m1 7956 ax-0lt1 7957 ax-1rid 7958 ax-0id 7959 ax-rnegex 7960 ax-precex 7961 ax-cnre 7962 ax-pre-ltirr 7963 ax-pre-ltwlin 7964 ax-pre-lttrn 7965 ax-pre-apti 7966 ax-pre-ltadd 7967 ax-pre-mulgt0 7968 ax-pre-mulext 7969 ax-arch 7970 |
| This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rmo 2476 df-rab 2477 df-v 2758 df-sbc 2982 df-csb 3077 df-dif 3150 df-un 3152 df-in 3154 df-ss 3161 df-pw 3599 df-sn 3620 df-pr 3621 df-op 3623 df-uni 3832 df-int 3867 df-iun 3910 df-br 4026 df-opab 4087 df-mpt 4088 df-id 4318 df-po 4321 df-iso 4322 df-xp 4657 df-rel 4658 df-cnv 4659 df-co 4660 df-dm 4661 df-rn 4662 df-res 4663 df-ima 4664 df-iota 5203 df-fun 5244 df-fn 5245 df-f 5246 df-fv 5250 df-riota 5859 df-ov 5907 df-oprab 5908 df-mpo 5909 df-1st 6173 df-2nd 6174 df-pnf 8035 df-mnf 8036 df-xr 8037 df-ltxr 8038 df-le 8039 df-sub 8171 df-neg 8172 df-reap 8573 df-ap 8580 df-div 8671 df-inn 8961 df-n0 9218 df-z 9295 df-uz 9570 df-q 9662 df-rp 9696 df-ico 9936 df-fz 10051 df-fzo 10185 df-fl 10313 df-mod 10366 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |