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 3258 |
. . . 4
..^ ..^ | |
| 2 | elfzoelz 10147 |
. . . 4
..^
 | |
| 3 | 1, 2 | syl 14 |
. . 3
..^ |
| 4 | elfzoelz 10147 |
. . 3
..^
| |
| 5 | zdcle 9329 |
. . . 4
DECID  | |
| 6 | exmiddc 836 |
. . . 4
DECID 
 | |
| 7 | 5, 6 | syl 14 |
. . 3
|
| 8 | 3, 4, 7 | syl2anr 290 |
. 2
..^ ..^ |
| 9 | zleloe 9300 |
. . . . . 6
 
| |
| 10 | 3, 4, 9 | syl2anr 290 |
. . . . 5
..^ ..^
|
| 11 | elfzo0 10182 |
. . . . . . . . . . . . 13
..^ 
 | |
| 12 | elfzo0 10182 |
. . . . . . . . . . . . . . . 16
..^
| |
| 13 | nn0cn 9186 |
. . . . . . . . . . . . . . . . . . . . . . 23
 | |
| 14 | 13 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 15 | 14 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 16 | nn0cn 9186 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 17 | 16 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 18 | 17 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 19 | nncn 8927 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 20 | 19 | 3ad2ant2 1019 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 21 | 20 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 22 | 15, 18, 21 | subadd23d 8290 |
. . . . . . . . . . . . . . . . . . . 20
|
| 23 | simpl 109 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 24 | nn0z 9273 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 25 | nnz 9272 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 26 | znnsub 9304 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 27 | 24, 25, 26 | syl2an 289 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 28 | 27 | biimp3a 1345 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 29 | nn0nnaddcl 9207 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 30 | 23, 28, 29 | syl2anr 290 |
. . . . . . . . . . . . . . . . . . . 20
|
| 31 | 22, 30 | eqeltrd 2254 |
. . . . . . . . . . . . . . . . . . 19
|
| 32 | 31 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
|
| 33 | simp2 998 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 34 | 33 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
|
| 35 | 34 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
|
| 36 | nn0re 9185 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 | |
| 37 | 36 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 38 | 37 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 39 | nn0re 9185 |
. . . . . . . . . . . . . . . . . . . . . . . 24
| |
| 40 | 39 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 41 | 40 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 42 | 38, 41 | sublt0d 8527 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 43 | 42 | bicomd 141 |
. . . . . . . . . . . . . . . . . . . 20
|
| 44 | 43 | biimpa 296 |
. . . . . . . . . . . . . . . . . . 19
|
| 45 | resubcl 8221 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 46 | 37, 40, 45 | syl2anr 290 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 47 | nnre 8926 |
. . . . . . . . . . . . . . . . . . . . . . . 24
| |
| 48 | 47 | 3ad2ant2 1019 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 49 | 48 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 50 | 46, 49 | jca 306 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 51 | 50 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
|
| 52 | ltaddnegr 8382 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 53 | 51, 52 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
|
| 54 | 44, 53 | mpbid 147 |
. . . . . . . . . . . . . . . . . 18
|
| 55 | elfzo1 10190 |
. . . . . . . . . . . . . . . . . 18
..^ | |
| 56 | 32, 35, 54, 55 | syl3anbrc 1181 |
. . . . . . . . . . . . . . . . 17
..^ |
| 57 | 56 | exp31 364 |
. . . . . . . . . . . . . . . 16
..^ |
| 58 | 12, 57 | sylbi 121 |
. . . . . . . . . . . . . . 15
..^
..^ |
| 59 | 58 | com12 30 |
. . . . . . . . . . . . . 14
..^ ..^ |
| 60 | 59 | 3adant2 1016 |
. . . . . . . . . . . . 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 5882 |
. . . . . . . . . . . 12
| |
| 66 | 2 | zcnd 9376 |
. . . . . . . . . . . . . . . . . . . . . 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 1177 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 73 | 72 | ex 115 |
. . . . . . . . . . . . . . . . . . 19
..^
|
| 74 | 1, 73 | syl 14 |
. . . . . . . . . . . . . . . . . 18
..^ |
| 75 | 74 | com12 30 |
. . . . . . . . . . . . . . . . 17
..^
|
| 76 | 75 | 3adant3 1017 |
. . . . . . . . . . . . . . . 16
..^
|
| 77 | 12, 76 | sylbi 121 |
. . . . . . . . . . . . . . 15
..^
..^
|
| 78 | 77 | imp 124 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 79 | 78 | adantl 277 |
. . . . . . . . . . . . 13
..^
..^
|
| 80 | nppcan 8179 |
. . . . . . . . . . . . 13
| |
| 81 | 79, 80 | syl 14 |
. . . . . . . . . . . 12
..^
..^
|
| 82 | 65, 81 | sylan9eqr 2232 |
. . . . . . . . . . 11
..^
..^ |
| 83 | 82 | oveq1d 5890 |
. . . . . . . . . 10
..^
..^
|
| 84 | 83 | eqeq2d 2189 |
. . . . . . . . 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 10373 |
. . . . . . . . . . 11
| |
| 91 | 90 | eqcomd 2183 |
. . . . . . . . . 10
|
| 92 | 89, 91 | syl 14 |
. . . . . . . . 9
..^
..^
|
| 93 | 64, 84, 92 | rspcedvd 2848 |
. . . . . . . 8
..^
..^
..^ |
| 94 | 93 | ex 115 |
. . . . . . 7
..^
..^ ..^ |
| 95 | eldifsn 3720 |
. . . . . . . . . 10
..^
..^  | |
| 96 | eqneqall 2357 |
. . . . . . . . . . . 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 716 |
. . . . . 6
..^ ..^ ..^ |
| 103 | 102 | com12 30 |
. . . . 5
..^ ..^ ..^ |
| 104 | 10, 103 | sylbid 150 |
. . . 4
..^ ..^ ..^ |
| 105 | 104 | com12 30 |
. . 3
..^
..^ ..^ |
| 106 | zltnle 9299 |
. . . . . . . . . 10
| |
| 107 | 4, 3, 106 | syl2an 289 |
. . . . . . . . 9
..^ ..^
|
| 108 | 107 | bicomd 141 |
. . . . . . . 8
..^ ..^ |
| 109 | 24 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . 18
|
| 110 | nn0z 9273 |
. . . . . . . . . . . . . . . . . . 19
| |
| 111 | 110 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
|
| 112 | znnsub 9304 |
. . . . . . . . . . . . . . . . . 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 9201 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 118 | 117 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 119 | 118 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 120 | subge02 8435 |
. . . . . . . . . . . . . . . . . . . . . 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 1177 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 127 | 45 | ancoms 268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 128 | 127 | 3adant3 1017 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 129 | simp2 998 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 130 | simp3 999 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 131 | 128, 129, 130 | 3jca 1177 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 132 | 126, 131 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 133 | lelttr 8046 |
. . . . . . . . . . . . . . . . . . . . 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 1177 |
. . . . . . . . . . . . . . 15
|
| 140 | 139 | exp31 364 |
. . . . . . . . . . . . . 14
|
| 141 | 140 | 3adant2 1016 |
. . . . . . . . . . . . 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 10190 |
. . . . . 6
..^ | |
| 150 | 148, 149 | sylibr 134 |
. . . . 5
..^
..^
..^ |
| 151 | oveq1 5882 |
. . . . . . . 8
| |
| 152 | 1, 66 | syl 14 |
. . . . . . . . . 10
..^ |
| 153 | 4 | zcnd 9376 |
. . . . . . . . . 10
..^
|
| 154 | npcan 8166 |
. . . . . . . . . 10
| |
| 155 | 152, 153, 154 | syl2anr 290 |
. . . . . . . . 9
..^ ..^ |
| 156 | 155 | adantl 277 |
. . . . . . . 8
..^
..^
|
| 157 | 151, 156 | sylan9eqr 2232 |
. . . . . . 7
..^ ..^
|
| 158 | 157 | oveq1d 5890 |
. . . . . 6
..^ ..^
|
| 159 | 158 | eqeq2d 2189 |
. . . . 5
..^ ..^
|
| 160 | zmodidfzoimp 10354 |
. . . . . . . . 9
..^
| |
| 161 | 1, 160 | syl 14 |
. . . . . . . 8
..^ |
| 162 | 161 | adantl 277 |
. . . . . . 7
..^ ..^ |
| 163 | 162 | adantl 277 |
. . . . . 6
..^
..^
|
| 164 | 163 | eqcomd 2183 |
. . . . 5
..^
..^
|
| 165 | 150, 159, 164 | rspcedvd 2848 |
. . . 4
..^
..^
..^ |
| 166 | 165 | ex 115 |
. . 3
..^
..^ ..^ |
| 167 | 105, 166 | jaoi 716 |
. 2
..^ ..^
..^ |
| 168 | 8, 167 | mpcom 36 |
1
..^ ..^
..^ |
| Colors of variables: wff set class |
| Syntax hints: wn 3
wi 4
wa 104
wb 105 wo 708 DECID wdc 834
w3a 978
wceq 1353
wcel 2148
wne 2347
wrex 2456
cdif 3127
csn 3593
class class class wbr 4004 (class class class)co 5875
cc 7809
cr 7810
cc0 7811
c1 7812
caddc 7814 clt 7992 cle 7993 cmin 8128 cn 8919 cn0 9176 cz 9253 ..^cfzo 10142
cmo 10322 |
| 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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-sep 4122 ax-pow 4175 ax-pr 4210 ax-un 4434 ax-setind 4537 ax-cnex 7902 ax-resscn 7903 ax-1cn 7904 ax-1re 7905 ax-icn 7906 ax-addcl 7907 ax-addrcl 7908 ax-mulcl 7909 ax-mulrcl 7910 ax-addcom 7911 ax-mulcom 7912 ax-addass 7913 ax-mulass 7914 ax-distr 7915 ax-i2m1 7916 ax-0lt1 7917 ax-1rid 7918 ax-0id 7919 ax-rnegex 7920 ax-precex 7921 ax-cnre 7922 ax-pre-ltirr 7923 ax-pre-ltwlin 7924 ax-pre-lttrn 7925 ax-pre-apti 7926 ax-pre-ltadd 7927 ax-pre-mulgt0 7928 ax-pre-mulext 7929 ax-arch 7930 |
| This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2740 df-sbc 2964 df-csb 3059 df-dif 3132 df-un 3134 df-in 3136 df-ss 3143 df-pw 3578 df-sn 3599 df-pr 3600 df-op 3602 df-uni 3811 df-int 3846 df-iun 3889 df-br 4005 df-opab 4066 df-mpt 4067 df-id 4294 df-po 4297 df-iso 4298 df-xp 4633 df-rel 4634 df-cnv 4635 df-co 4636 df-dm 4637 df-rn 4638 df-res 4639 df-ima 4640 df-iota 5179 df-fun 5219 df-fn 5220 df-f 5221 df-fv 5225 df-riota 5831 df-ov 5878 df-oprab 5879 df-mpo 5880 df-1st 6141 df-2nd 6142 df-pnf 7994 df-mnf 7995 df-xr 7996 df-ltxr 7997 df-le 7998 df-sub 8130 df-neg 8131 df-reap 8532 df-ap 8539 df-div 8630 df-inn 8920 df-n0 9177 df-z 9254 df-uz 9529 df-q 9620 df-rp 9654 df-ico 9894 df-fz 10009 df-fzo 10143 df-fl 10270 df-mod 10323 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |