Nearby theorems
|
|
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > ILE Home > Th. List > addmodlteq | Unicode version | ||
| Description: Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. (Contributed by AV, 20-Mar-2021.) |
| Ref | Expression |
|---|---|
| addmodlteq |
     ..^  ![/\](wedge.gif "/\"){kind=small}  ..^       
|
is distinct from all other
variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elfzoelz 10024 |
. . . . . . . 8
..^
| |
| 2 | 1 | 3ad2ant1 1003 |
. . . . . . 7
..^ ..^ |
| 3 | zq 9513 |
. . . . . . 7
 | |
| 4 | 2, 3 | syl 14 |
. . . . . 6
..^ ..^ |
| 5 | simp3 984 |
. . . . . . 7
..^ ..^ | |
| 6 | zq 9513 |
. . . . . . 7
| |
| 7 | 5, 6 | syl 14 |
. . . . . 6
..^ ..^ |
| 8 | elfzo0 10059 |
. . . . . . . . . 10
..^ 
  | |
| 9 | 8 | biimpi 119 |
. . . . . . . . 9
..^
|
| 10 | 9 | 3ad2ant1 1003 |
. . . . . . . 8
..^ ..^
|
| 11 | 10 | simp2d 995 |
. . . . . . 7
..^ ..^ |
| 12 | nnq 9520 |
. . . . . . 7
| |
| 13 | 11, 12 | syl 14 |
. . . . . 6
..^ ..^ |
| 14 | 11 | nngt0d 8856 |
. . . . . 6
..^ ..^ |
| 15 | modqaddmod 10240 |
. . . . . 6
| |
| 16 | 4, 7, 13, 14, 15 | syl22anc 1218 |
. . . . 5
..^ ..^
|
| 17 | 16 | eqcomd 2160 |
. . . 4
..^ ..^ |
| 18 | elfzoelz 10024 |
. . . . . . . 8
..^
| |
| 19 | 18 | 3ad2ant2 1004 |
. . . . . . 7
..^ ..^ |
| 20 | zq 9513 |
. . . . . . 7
| |
| 21 | 19, 20 | syl 14 |
. . . . . 6
..^ ..^ |
| 22 | modqaddmod 10240 |
. . . . . 6
| |
| 23 | 21, 7, 13, 14, 22 | syl22anc 1218 |
. . . . 5
..^ ..^
|
| 24 | 23 | eqcomd 2160 |
. . . 4
..^ ..^ |
| 25 | 17, 24 | eqeq12d 2169 |
. . 3
..^ ..^ |
| 26 | 2, 11 | zmodcld 10222 |
. . . . . . . . 9
..^ ..^ |
| 27 | 26 | nn0zd 9263 |
. . . . . . . 8
..^ ..^ |
| 28 | 27, 5 | zaddcld 9269 |
. . . . . . 7
..^ ..^ |
| 29 | 28, 11 | zmodcld 10222 |
. . . . . 6
..^ ..^ |
| 30 | 29 | nn0cnd 9124 |
. . . . 5
..^ ..^  |
| 31 | 19, 11 | zmodcld 10222 |
. . . . . . . . 9
..^ ..^ |
| 32 | 31 | nn0zd 9263 |
. . . . . . . 8
..^ ..^ |
| 33 | 32, 5 | zaddcld 9269 |
. . . . . . 7
..^ ..^ |
| 34 | 33, 11 | zmodcld 10222 |
. . . . . 6
..^ ..^ |
| 35 | 34 | nn0cnd 9124 |
. . . . 5
..^ ..^ |
| 36 | 30, 35 | subeq0ad 8175 |
. . . 4
..^ ..^  |
| 37 | oveq1 5821 |
. . . . 5
| |
| 38 | 4, 13, 14 | modqcld 10205 |
. . . . . . . . . 10
..^ ..^ |
| 39 | qaddcl 9522 |
. . . . . . . . . 10
| |
| 40 | 38, 7, 39 | syl2anc 409 |
. . . . . . . . 9
..^ ..^ |
| 41 | 21, 13, 14 | modqcld 10205 |
. . . . . . . . . 10
..^ ..^ |
| 42 | qaddcl 9522 |
. . . . . . . . . 10
| |
| 43 | 41, 7, 42 | syl2anc 409 |
. . . . . . . . 9
..^ ..^ |
| 44 | modqsubmodmod 10260 |
. . . . . . . . 9
| |
| 45 | 40, 43, 13, 14, 44 | syl22anc 1218 |
. . . . . . . 8
..^ ..^ |
| 46 | 26 | nn0cnd 9124 |
. . . . . . . . . 10
..^ ..^ |
| 47 | 31 | nn0cnd 9124 |
. . . . . . . . . 10
..^ ..^ |
| 48 | 5 | zcnd 9266 |
. . . . . . . . . 10
..^ ..^ |
| 49 | 46, 47, 48 | pnpcan2d 8203 |
. . . . . . . . 9
..^ ..^ |
| 50 | 49 | oveq1d 5829 |
. . . . . . . 8
..^ ..^ |
| 51 | 45, 50 | eqtrd 2187 |
. . . . . . 7
..^ ..^ |
| 52 | q0mod 10232 |
. . . . . . . 8
| |
| 53 | 13, 14, 52 | syl2anc 409 |
. . . . . . 7
..^ ..^ |
| 54 | 51, 53 | eqeq12d 2169 |
. . . . . 6
..^ ..^ |
| 55 | zmodidfzoimp 10231 |
. . . . . . . . . . 11
..^
| |
| 56 | 55 | 3ad2ant1 1003 |
. . . . . . . . . 10
..^ ..^ |
| 57 | zmodidfzoimp 10231 |
. . . . . . . . . . 11
..^
| |
| 58 | 57 | 3ad2ant2 1004 |
. . . . . . . . . 10
..^ ..^ |
| 59 | 56, 58 | oveq12d 5832 |
. . . . . . . . 9
..^ ..^
|
| 60 | 59 | oveq1d 5829 |
. . . . . . . 8
..^ ..^ |
| 61 | 60 | eqeq1d 2163 |
. . . . . . 7
..^ ..^ |
| 62 | qsubcl 9525 |
. . . . . . . . . 10
| |
| 63 | 4, 21, 62 | syl2anc 409 |
. . . . . . . . 9
..^ ..^ |
| 64 | modq0 10206 |
. . . . . . . . 9
 | |
| 65 | 63, 13, 14, 64 | syl3anc 1217 |
. . . . . . . 8
..^ ..^ |
| 66 | 2, 19 | zsubcld 9270 |
. . . . . . . . . 10
..^ ..^ |
| 67 | zdiv 9231 |
. . . . . . . . . 10
  | |
| 68 | 11, 66, 67 | syl2anc 409 |
. . . . . . . . 9
..^ ..^ |
| 69 | simpr 109 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
| |
| 70 | 69 | oveq2d 5830 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 71 | 11 | nncnd 8826 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
| 72 | 71 | mul01d 8247 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
| 73 | 72 | ad2antrr 480 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 74 | 70, 73 | eqtrd 2187 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 75 | 74 | eqeq1d 2163 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 76 | eqcom 2156 |
. . . . . . . . . . . . . . . 16
| |
| 77 | 10 | simp1d 994 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
| 78 | 77 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
|
| 79 | 78 | nn0cnd 9124 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
| 80 | elfzo0 10059 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
| |
| 81 | 80 | biimpi 119 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
| 82 | 81 | 3ad2ant2 1004 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^
|
| 83 | 82 | simp1d 994 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
| 84 | 83 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
|
| 85 | 84 | nn0cnd 9124 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
| 86 | 79, 85 | subeq0ad 8175 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 87 | 86 | biimpd 143 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 88 | 76, 87 | syl5bi 151 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 89 | 75, 88 | sylbid 149 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 90 | 89 | imp 123 |
. . . . . . . . . . . . 13
..^ ..^ |
| 91 | 90 | an32s 558 |
. . . . . . . . . . . 12
..^ ..^ |
| 92 | subfzo0 10119 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
| |
| 93 | 92 | 3adant3 1002 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 94 | 93 | ad3antrrr 484 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 95 | 94 | simprd 113 |
. . . . . . . . . . . . . . 15
..^ ..^ |
| 96 | simplr 520 |
. . . . . . . . . . . . . . 15
..^ ..^
| |
| 97 | 71 | mulid1d 7874 |
. . . . . . . . . . . . . . . 16
..^ ..^  |
| 98 | 97 | ad3antrrr 484 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 99 | 95, 96, 98 | 3brtr4d 3992 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 100 | simpllr 524 |
. . . . . . . . . . . . . . . 16
..^ ..^ | |
| 101 | 100 | zred 9265 |
. . . . . . . . . . . . . . 15
..^ ..^  |
| 102 | 1red 7872 |
. . . . . . . . . . . . . . 15
..^ ..^ | |
| 103 | 11 | nnrpd 9579 |
. . . . . . . . . . . . . . . 16
..^ ..^  |
| 104 | 103 | ad3antrrr 484 |
. . . . . . . . . . . . . . 15
..^ ..^ |
| 105 | 101, 102, 104 | ltmul2d 9624 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 106 | 99, 105 | mpbird 166 |
. . . . . . . . . . . . 13
..^ ..^ |
| 107 | simpr 109 |
. . . . . . . . . . . . . . 15
..^ ..^ | |
| 108 | 107 | nnge1d 8855 |
. . . . . . . . . . . . . 14
..^ ..^  |
| 109 | 102, 101, 108 | lensymd 7976 |
. . . . . . . . . . . . 13
..^ ..^  |
| 110 | 106, 109 | pm2.21dd 610 |
. . . . . . . . . . . 12
..^ ..^ |
| 111 | 93 | ad3antrrr 484 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 112 | 111 | simpld 111 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 113 | simplr 520 |
. . . . . . . . . . . . . . . 16
..^ ..^
| |
| 114 | 112, 113 | breqtrrd 3988 |
. . . . . . . . . . . . . . 15
..^ ..^ |
| 115 | 11 | nnzd 9264 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
| 116 | 115 | adantr 274 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
| 117 | simpr 109 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ | |
| 118 | 116, 117 | zmulcld 9271 |
. . . . . . . . . . . . . . . . . 18
..^
..^
|
| 119 | 118 | zred 9265 |
. . . . . . . . . . . . . . . . 17
..^
..^
|
| 120 | 119 | ad2antrr 480 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 121 | 11 | nnred 8825 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
| 122 | 121 | ad3antrrr 484 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 123 | 120, 122 | possumd 8423 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 124 | 114, 123 | mpbird 166 |
. . . . . . . . . . . . . 14
..^ ..^ |
| 125 | 97 | eqcomd 2160 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
| 126 | 125 | oveq2d 5830 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 127 | 126 | ad3antrrr 484 |
. . . . . . . . . . . . . . 15
..^ ..^ |
| 128 | 71 | ad3antrrr 484 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 129 | 117 | zcnd 9266 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
| 130 | 129 | ad2antrr 480 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 131 | 1cnd 7873 |
. . . . . . . . . . . . . . . 16
..^ ..^ | |
| 132 | 128, 130, 131 | adddid 7881 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 133 | 127, 132 | eqtr4d 2190 |
. . . . . . . . . . . . . 14
..^ ..^ |
| 134 | 124, 133 | breqtrd 3986 |
. . . . . . . . . . . . 13
..^ ..^ |
| 135 | 117 | peano2zd 9268 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
| 136 | 116, 135 | zmulcld 9271 |
. . . . . . . . . . . . . . . 16
..^
..^
|
| 137 | 136 | zred 9265 |
. . . . . . . . . . . . . . 15
..^
..^
|
| 138 | 137 | ad2antrr 480 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 139 | 0red 7858 |
. . . . . . . . . . . . . 14
..^ ..^ | |
| 140 | 71 | adantr 274 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
| 141 | 135 | zcnd 9266 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
| 142 | 140, 141 | mulcomd 7878 |
. . . . . . . . . . . . . . . 16
..^
..^
|
| 143 | 142 | ad2antrr 480 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 144 | 135 | zred 9265 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
| 145 | 144 | ad2antrr 480 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 146 | zcn 9151 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 147 | 1cnd 7873 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 148 | 146, 147 | addcomd 8005 |
. . . . . . . . . . . . . . . . . . 19
|
| 149 | 147, 146 | subnegd 8172 |
. . . . . . . . . . . . . . . . . . 19
|
| 150 | 148, 149 | eqtr4d 2190 |
. . . . . . . . . . . . . . . . . 18
|
| 151 | 150 | ad3antlr 485 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
| 152 | simpr 109 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ | |
| 153 | 152 | nnge1d 8855 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
| 154 | 1red 7872 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ | |
| 155 | 152 | nnred 8825 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
| 156 | 154, 155 | suble0d 8390 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
| 157 | 153, 156 | mpbird 166 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 158 | 151, 157 | eqbrtrd 3982 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 159 | 11 | nnnn0d 9122 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
| 160 | 159 | nn0ge0d 9125 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
| 161 | 160 | ad3antrrr 484 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 162 | mulle0r 8794 |
. . . . . . . . . . . . . . . 16
| |
| 163 | 145, 122, 158, 161, 162 | syl22anc 1218 |
. . . . . . . . . . . . . . 15
..^ ..^ |
| 164 | 143, 163 | eqbrtrd 3982 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 165 | 138, 139, 164 | lensymd 7976 |
. . . . . . . . . . . . 13
..^ ..^ |
| 166 | 134, 165 | pm2.21dd 610 |
. . . . . . . . . . . 12
..^ ..^ |
| 167 | elz 9148 |
. . . . . . . . . . . . . 14
 | |
| 168 | 167 | simprbi 273 |
. . . . . . . . . . . . 13
|
| 169 | 168 | ad2antlr 481 |
. . . . . . . . . . . 12
..^ ..^
|
| 170 | 91, 110, 166, 169 | mpjao3dan 1286 |
. . . . . . . . . . 11
..^ ..^
|
| 171 | 170 | ex 114 |
. . . . . . . . . 10
..^
..^
|
| 172 | 171 | rexlimdva 2571 |
. . . . . . . . 9
..^ ..^ |
| 173 | 68, 172 | sylbird 169 |
. . . . . . . 8
..^ ..^
|
| 174 | 65, 173 | sylbid 149 |
. . . . . . 7
..^ ..^
|
| 175 | 61, 174 | sylbid 149 |
. . . . . 6
..^ ..^
|
| 176 | 54, 175 | sylbid 149 |
. . . . 5
..^ ..^
|
| 177 | 37, 176 | syl5 32 |
. . . 4
..^ ..^ |
| 178 | 36, 177 | sylbird 169 |
. . 3
..^ ..^
|
| 179 | 25, 178 | sylbid 149 |
. 2
..^ ..^
|
| 180 | oveq1 5821 |
. . 3
| |
| 181 | 180 | oveq1d 5829 |
. 2
|
| 182 | 179, 181 | impbid1 141 |
1
..^ ..^
|
| Colors of variables: wff set class |
| Syntax hints: wi 4
wa 103
wb 104 w3o 962 w3a 963 wceq 1332 wcel 2125 wrex 2433 class class class wbr 3961
(class class class)co 5814 cc 7709 cr 7710 cc0 7711 c1 7712 caddc 7714 cmul 7716 clt 7891 cle 7892 cmin 8025 cneg 8026 cdiv 8524 cn 8812 cn0 9069 cz 9146 cq 9506 crp 9538 ..^cfzo 10019
cmo 10199 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-13 2127 ax-14 2128 ax-ext 2136 ax-sep 4078 ax-pow 4130 ax-pr 4164 ax-un 4388 ax-setind 4490 ax-cnex 7802 ax-resscn 7803 ax-1cn 7804 ax-1re 7805 ax-icn 7806 ax-addcl 7807 ax-addrcl 7808 ax-mulcl 7809 ax-mulrcl 7810 ax-addcom 7811 ax-mulcom 7812 ax-addass 7813 ax-mulass 7814 ax-distr 7815 ax-i2m1 7816 ax-0lt1 7817 ax-1rid 7818 ax-0id 7819 ax-rnegex 7820 ax-precex 7821 ax-cnre 7822 ax-pre-ltirr 7823 ax-pre-ltwlin 7824 ax-pre-lttrn 7825 ax-pre-apti 7826 ax-pre-ltadd 7827 ax-pre-mulgt0 7828 ax-pre-mulext 7829 ax-arch 7830 |
| This theorem depends on definitions: df-bi 116 df-3or 964 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1740 df-eu 2006 df-mo 2007 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ne 2325 df-nel 2420 df-ral 2437 df-rex 2438 df-reu 2439 df-rmo 2440 df-rab 2441 df-v 2711 df-sbc 2934 df-csb 3028 df-dif 3100 df-un 3102 df-in 3104 df-ss 3111 df-pw 3541 df-sn 3562 df-pr 3563 df-op 3565 df-uni 3769 df-int 3804 df-iun 3847 df-br 3962 df-opab 4022 df-mpt 4023 df-id 4248 df-po 4251 df-iso 4252 df-xp 4585 df-rel 4586 df-cnv 4587 df-co 4588 df-dm 4589 df-rn 4590 df-res 4591 df-ima 4592 df-iota 5128 df-fun 5165 df-fn 5166 df-f 5167 df-fv 5171 df-riota 5770 df-ov 5817 df-oprab 5818 df-mpo 5819 df-1st 6078 df-2nd 6079 df-pnf 7893 df-mnf 7894 df-xr 7895 df-ltxr 7896 df-le 7897 df-sub 8027 df-neg 8028 df-reap 8429 df-ap 8436 df-div 8525 df-inn 8813 df-n0 9070 df-z 9147 df-uz 9419 df-q 9507 df-rp 9539 df-fz 9891 df-fzo 10020 df-fl 10147 df-mod 10200 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |