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 10381 |
. . . . . . . 8
..^
| |
| 2 | 1 | 3ad2ant1 1044 |
. . . . . . 7
..^ ..^ |
| 3 | zq 9859 |
. . . . . . 7
 | |
| 4 | 2, 3 | syl 14 |
. . . . . 6
..^ ..^ |
| 5 | simp3 1025 |
. . . . . . 7
..^ ..^ | |
| 6 | zq 9859 |
. . . . . . 7
| |
| 7 | 5, 6 | syl 14 |
. . . . . 6
..^ ..^ |
| 8 | elfzo0 10420 |
. . . . . . . . . 10
..^ 
  | |
| 9 | 8 | biimpi 120 |
. . . . . . . . 9
..^
|
| 10 | 9 | 3ad2ant1 1044 |
. . . . . . . 8
..^ ..^
|
| 11 | 10 | simp2d 1036 |
. . . . . . 7
..^ ..^ |
| 12 | nnq 9866 |
. . . . . . 7
| |
| 13 | 11, 12 | syl 14 |
. . . . . 6
..^ ..^ |
| 14 | 11 | nngt0d 9186 |
. . . . . 6
..^ ..^ |
| 15 | modqaddmod 10624 |
. . . . . 6
| |
| 16 | 4, 7, 13, 14, 15 | syl22anc 1274 |
. . . . 5
..^ ..^
|
| 17 | 16 | eqcomd 2237 |
. . . 4
..^ ..^ |
| 18 | elfzoelz 10381 |
. . . . . . . 8
..^
| |
| 19 | 18 | 3ad2ant2 1045 |
. . . . . . 7
..^ ..^ |
| 20 | zq 9859 |
. . . . . . 7
| |
| 21 | 19, 20 | syl 14 |
. . . . . 6
..^ ..^ |
| 22 | modqaddmod 10624 |
. . . . . 6
| |
| 23 | 21, 7, 13, 14, 22 | syl22anc 1274 |
. . . . 5
..^ ..^
|
| 24 | 23 | eqcomd 2237 |
. . . 4
..^ ..^ |
| 25 | 17, 24 | eqeq12d 2246 |
. . 3
..^ ..^ |
| 26 | 2, 11 | zmodcld 10606 |
. . . . . . . . 9
..^ ..^ |
| 27 | 26 | nn0zd 9599 |
. . . . . . . 8
..^ ..^ |
| 28 | 27, 5 | zaddcld 9605 |
. . . . . . 7
..^ ..^ |
| 29 | 28, 11 | zmodcld 10606 |
. . . . . 6
..^ ..^ |
| 30 | 29 | nn0cnd 9456 |
. . . . 5
..^ ..^  |
| 31 | 19, 11 | zmodcld 10606 |
. . . . . . . . 9
..^ ..^ |
| 32 | 31 | nn0zd 9599 |
. . . . . . . 8
..^ ..^ |
| 33 | 32, 5 | zaddcld 9605 |
. . . . . . 7
..^ ..^ |
| 34 | 33, 11 | zmodcld 10606 |
. . . . . 6
..^ ..^ |
| 35 | 34 | nn0cnd 9456 |
. . . . 5
..^ ..^ |
| 36 | 30, 35 | subeq0ad 8499 |
. . . 4
..^ ..^  |
| 37 | oveq1 6024 |
. . . . 5
| |
| 38 | 4, 13, 14 | modqcld 10589 |
. . . . . . . . . 10
..^ ..^ |
| 39 | qaddcl 9868 |
. . . . . . . . . 10
| |
| 40 | 38, 7, 39 | syl2anc 411 |
. . . . . . . . 9
..^ ..^ |
| 41 | 21, 13, 14 | modqcld 10589 |
. . . . . . . . . 10
..^ ..^ |
| 42 | qaddcl 9868 |
. . . . . . . . . 10
| |
| 43 | 41, 7, 42 | syl2anc 411 |
. . . . . . . . 9
..^ ..^ |
| 44 | modqsubmodmod 10644 |
. . . . . . . . 9
| |
| 45 | 40, 43, 13, 14, 44 | syl22anc 1274 |
. . . . . . . 8
..^ ..^ |
| 46 | 26 | nn0cnd 9456 |
. . . . . . . . . 10
..^ ..^ |
| 47 | 31 | nn0cnd 9456 |
. . . . . . . . . 10
..^ ..^ |
| 48 | 5 | zcnd 9602 |
. . . . . . . . . 10
..^ ..^ |
| 49 | 46, 47, 48 | pnpcan2d 8527 |
. . . . . . . . 9
..^ ..^ |
| 50 | 49 | oveq1d 6032 |
. . . . . . . 8
..^ ..^ |
| 51 | 45, 50 | eqtrd 2264 |
. . . . . . 7
..^ ..^ |
| 52 | q0mod 10616 |
. . . . . . . 8
| |
| 53 | 13, 14, 52 | syl2anc 411 |
. . . . . . 7
..^ ..^ |
| 54 | 51, 53 | eqeq12d 2246 |
. . . . . 6
..^ ..^ |
| 55 | zmodidfzoimp 10615 |
. . . . . . . . . . 11
..^
| |
| 56 | 55 | 3ad2ant1 1044 |
. . . . . . . . . 10
..^ ..^ |
| 57 | zmodidfzoimp 10615 |
. . . . . . . . . . 11
..^
| |
| 58 | 57 | 3ad2ant2 1045 |
. . . . . . . . . 10
..^ ..^ |
| 59 | 56, 58 | oveq12d 6035 |
. . . . . . . . 9
..^ ..^
|
| 60 | 59 | oveq1d 6032 |
. . . . . . . 8
..^ ..^ |
| 61 | 60 | eqeq1d 2240 |
. . . . . . 7
..^ ..^ |
| 62 | qsubcl 9871 |
. . . . . . . . . 10
| |
| 63 | 4, 21, 62 | syl2anc 411 |
. . . . . . . . 9
..^ ..^ |
| 64 | modq0 10590 |
. . . . . . . . 9
 | |
| 65 | 63, 13, 14, 64 | syl3anc 1273 |
. . . . . . . 8
..^ ..^ |
| 66 | 2, 19 | zsubcld 9606 |
. . . . . . . . . 10
..^ ..^ |
| 67 | zdiv 9567 |
. . . . . . . . . 10
  | |
| 68 | 11, 66, 67 | syl2anc 411 |
. . . . . . . . 9
..^ ..^ |
| 69 | simpr 110 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
| |
| 70 | 69 | oveq2d 6033 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 71 | 11 | nncnd 9156 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
| 72 | 71 | mul01d 8571 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
| 73 | 72 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 74 | 70, 73 | eqtrd 2264 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 75 | 74 | eqeq1d 2240 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 76 | eqcom 2233 |
. . . . . . . . . . . . . . . 16
| |
| 77 | 10 | simp1d 1035 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
| 78 | 77 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
|
| 79 | 78 | nn0cnd 9456 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
| 80 | elfzo0 10420 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
| |
| 81 | 80 | biimpi 120 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
| 82 | 81 | 3ad2ant2 1045 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^
|
| 83 | 82 | simp1d 1035 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
| 84 | 83 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
|
| 85 | 84 | nn0cnd 9456 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
| 86 | 79, 85 | subeq0ad 8499 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 87 | 86 | biimpd 144 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 88 | 76, 87 | biimtrid 152 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 89 | 75, 88 | sylbid 150 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 90 | 89 | imp 124 |
. . . . . . . . . . . . 13
..^ ..^ |
| 91 | 90 | an32s 570 |
. . . . . . . . . . . 12
..^ ..^ |
| 92 | subfzo0 10487 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
| |
| 93 | 92 | 3adant3 1043 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 94 | 93 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 95 | 94 | simprd 114 |
. . . . . . . . . . . . . . 15
..^ ..^ |
| 96 | simplr 529 |
. . . . . . . . . . . . . . 15
..^ ..^
| |
| 97 | 71 | mulridd 8195 |
. . . . . . . . . . . . . . . 16
..^ ..^  |
| 98 | 97 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 99 | 95, 96, 98 | 3brtr4d 4120 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 100 | simpllr 536 |
. . . . . . . . . . . . . . . 16
..^ ..^ | |
| 101 | 100 | zred 9601 |
. . . . . . . . . . . . . . 15
..^ ..^  |
| 102 | 1red 8193 |
. . . . . . . . . . . . . . 15
..^ ..^ | |
| 103 | 11 | nnrpd 9928 |
. . . . . . . . . . . . . . . 16
..^ ..^  |
| 104 | 103 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
..^ ..^ |
| 105 | 101, 102, 104 | ltmul2d 9973 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 106 | 99, 105 | mpbird 167 |
. . . . . . . . . . . . 13
..^ ..^ |
| 107 | simpr 110 |
. . . . . . . . . . . . . . 15
..^ ..^ | |
| 108 | 107 | nnge1d 9185 |
. . . . . . . . . . . . . 14
..^ ..^  |
| 109 | 102, 101, 108 | lensymd 8300 |
. . . . . . . . . . . . 13
..^ ..^  |
| 110 | 106, 109 | pm2.21dd 625 |
. . . . . . . . . . . 12
..^ ..^ |
| 111 | 93 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 112 | 111 | simpld 112 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 113 | simplr 529 |
. . . . . . . . . . . . . . . 16
..^ ..^
| |
| 114 | 112, 113 | breqtrrd 4116 |
. . . . . . . . . . . . . . 15
..^ ..^ |
| 115 | 11 | nnzd 9600 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
| 116 | 115 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
| 117 | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ | |
| 118 | 116, 117 | zmulcld 9607 |
. . . . . . . . . . . . . . . . . 18
..^
..^
|
| 119 | 118 | zred 9601 |
. . . . . . . . . . . . . . . . 17
..^
..^
|
| 120 | 119 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 121 | 11 | nnred 9155 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
| 122 | 121 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 123 | 120, 122 | possumd 8748 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 124 | 114, 123 | mpbird 167 |
. . . . . . . . . . . . . 14
..^ ..^ |
| 125 | 97 | eqcomd 2237 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
| 126 | 125 | oveq2d 6033 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 127 | 126 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
..^ ..^ |
| 128 | 71 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 129 | 117 | zcnd 9602 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
| 130 | 129 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 131 | 1cnd 8194 |
. . . . . . . . . . . . . . . 16
..^ ..^ | |
| 132 | 128, 130, 131 | adddid 8203 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 133 | 127, 132 | eqtr4d 2267 |
. . . . . . . . . . . . . 14
..^ ..^ |
| 134 | 124, 133 | breqtrd 4114 |
. . . . . . . . . . . . 13
..^ ..^ |
| 135 | 117 | peano2zd 9604 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
| 136 | 116, 135 | zmulcld 9607 |
. . . . . . . . . . . . . . . 16
..^
..^
|
| 137 | 136 | zred 9601 |
. . . . . . . . . . . . . . 15
..^
..^
|
| 138 | 137 | ad2antrr 488 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 139 | 0red 8179 |
. . . . . . . . . . . . . 14
..^ ..^ | |
| 140 | 71 | adantr 276 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
| 141 | 135 | zcnd 9602 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
| 142 | 140, 141 | mulcomd 8200 |
. . . . . . . . . . . . . . . 16
..^
..^
|
| 143 | 142 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 144 | 135 | zred 9601 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
| 145 | 144 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 146 | zcn 9483 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 147 | 1cnd 8194 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 148 | 146, 147 | addcomd 8329 |
. . . . . . . . . . . . . . . . . . 19
|
| 149 | 147, 146 | subnegd 8496 |
. . . . . . . . . . . . . . . . . . 19
|
| 150 | 148, 149 | eqtr4d 2267 |
. . . . . . . . . . . . . . . . . 18
|
| 151 | 150 | ad3antlr 493 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
| 152 | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ | |
| 153 | 152 | nnge1d 9185 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
| 154 | 1red 8193 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ | |
| 155 | 152 | nnred 9155 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
| 156 | 154, 155 | suble0d 8715 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
| 157 | 153, 156 | mpbird 167 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 158 | 151, 157 | eqbrtrd 4110 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 159 | 11 | nnnn0d 9454 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
| 160 | 159 | nn0ge0d 9457 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
| 161 | 160 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
| 162 | mulle0r 9123 |
. . . . . . . . . . . . . . . 16
| |
| 163 | 145, 122, 158, 161, 162 | syl22anc 1274 |
. . . . . . . . . . . . . . 15
..^ ..^ |
| 164 | 143, 163 | eqbrtrd 4110 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 165 | 138, 139, 164 | lensymd 8300 |
. . . . . . . . . . . . 13
..^ ..^ |
| 166 | 134, 165 | pm2.21dd 625 |
. . . . . . . . . . . 12
..^ ..^ |
| 167 | elz 9480 |
. . . . . . . . . . . . . 14
 | |
| 168 | 167 | simprbi 275 |
. . . . . . . . . . . . 13
|
| 169 | 168 | ad2antlr 489 |
. . . . . . . . . . . 12
..^ ..^
|
| 170 | 91, 110, 166, 169 | mpjao3dan 1343 |
. . . . . . . . . . 11
..^ ..^
|
| 171 | 170 | ex 115 |
. . . . . . . . . 10
..^
..^
|
| 172 | 171 | rexlimdva 2650 |
. . . . . . . . 9
..^ ..^ |
| 173 | 68, 172 | sylbird 170 |
. . . . . . . 8
..^ ..^
|
| 174 | 65, 173 | sylbid 150 |
. . . . . . 7
..^ ..^
|
| 175 | 61, 174 | sylbid 150 |
. . . . . 6
..^ ..^
|
| 176 | 54, 175 | sylbid 150 |
. . . . 5
..^ ..^
|
| 177 | 37, 176 | syl5 32 |
. . . 4
..^ ..^ |
| 178 | 36, 177 | sylbird 170 |
. . 3
..^ ..^
|
| 179 | 25, 178 | sylbid 150 |
. 2
..^ ..^
|
| 180 | oveq1 6024 |
. . 3
| |
| 181 | 180 | oveq1d 6032 |
. 2
|
| 182 | 179, 181 | impbid1 142 |
1
..^ ..^
|
| Colors of variables: wff set class |
| Syntax hints: wi 4
wa 104
wb 105 w3o 1003 w3a 1004 wceq 1397 wcel 2202 wrex 2511 class class class wbr 4088
(class class class)co 6017 cc 8029 cr 8030 cc0 8031 c1 8032 caddc 8034 cmul 8036 clt 8213 cle 8214 cmin 8349 cneg 8350 cdiv 8851 cn 9142 cn0 9401 cz 9478 cq 9852 crp 9887 ..^cfzo 10376
cmo 10583 |
| 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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-sep 4207 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-cnex 8122 ax-resscn 8123 ax-1cn 8124 ax-1re 8125 ax-icn 8126 ax-addcl 8127 ax-addrcl 8128 ax-mulcl 8129 ax-mulrcl 8130 ax-addcom 8131 ax-mulcom 8132 ax-addass 8133 ax-mulass 8134 ax-distr 8135 ax-i2m1 8136 ax-0lt1 8137 ax-1rid 8138 ax-0id 8139 ax-rnegex 8140 ax-precex 8141 ax-cnre 8142 ax-pre-ltirr 8143 ax-pre-ltwlin 8144 ax-pre-lttrn 8145 ax-pre-apti 8146 ax-pre-ltadd 8147 ax-pre-mulgt0 8148 ax-pre-mulext 8149 ax-arch 8150 |
| This theorem depends on definitions: df-bi 117 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rmo 2518 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-id 4390 df-po 4393 df-iso 4394 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-fv 5334 df-riota 5970 df-ov 6020 df-oprab 6021 df-mpo 6022 df-1st 6302 df-2nd 6303 df-pnf 8215 df-mnf 8216 df-xr 8217 df-ltxr 8218 df-le 8219 df-sub 8351 df-neg 8352 df-reap 8754 df-ap 8761 df-div 8852 df-inn 9143 df-n0 9402 df-z 9479 df-uz 9755 df-q 9853 df-rp 9888 df-fz 10243 df-fzo 10377 df-fl 10529 df-mod 10584 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |