Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
| Mirrors > Home > MPE Home > Th. List > modprm0 | Structured version Unicode version | |
| Description: For two positive integers less than a given prime number there is always a nonnegative integer (less than the given prime number) so that the sum of one of the two positive integers and the other of the positive integers multiplied by the nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 17-May-2018.) |
| Ref | Expression |
|---|---|
| modprm0 |
     ![/\](wedge.gif "/\"){kind=small}   ..^  ..^     ..^     |
, , ,
is distinct from all other
variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reumodprminv 13872 |
. . . 4
..^
  
| |
| 2 | reurex 2937 |
. . . 4
| |
| 3 | prmz 13767 |
. . . . . . . . . . 11
 | |
| 4 | 3 | 3ad2ant1 1009 |
. . . . . . . . . 10
..^ ..^ |
| 5 | 4 | adantl 466 |
. . . . . . . . 9
..^ ..^
|
| 6 | elfzelz 11453 |
. . . . . . . . . . 11
| |
| 7 | 6 | adantr 465 |
. . . . . . . . . 10
|
| 8 | elfzoelz 11553 |
. . . . . . . . . . 11
..^
| |
| 9 | 8 | 3ad2ant3 1011 |
. . . . . . . . . 10
..^ ..^ |
| 10 | zmulcl 10693 |
. . . . . . . . . 10
| |
| 11 | 7, 9, 10 | syl2an 477 |
. . . . . . . . 9
..^ ..^
|
| 12 | 5, 11 | zsubcld 10752 |
. . . . . . . 8
..^ ..^
|
| 13 | prmnn 13766 |
. . . . . . . . . 10
 | |
| 14 | 13 | 3ad2ant1 1009 |
. . . . . . . . 9
..^ ..^ |
| 15 | 14 | adantl 466 |
. . . . . . . 8
..^ ..^
|
| 16 | zmodfzo 11730 |
. . . . . . . 8
..^ | |
| 17 | 12, 15, 16 | syl2anc 661 |
. . . . . . 7
..^ ..^
..^ |
| 18 | 8 | zred 10747 |
. . . . . . . . . . 11
..^
 |
| 19 | 18 | 3ad2ant3 1011 |
. . . . . . . . . 10
..^ ..^ |
| 20 | 19 | adantl 466 |
. . . . . . . . 9
..^ ..^
|
| 21 | 13 | nnred 10337 |
. . . . . . . . . . . 12
|
| 22 | 21 | 3ad2ant1 1009 |
. . . . . . . . . . 11
..^ ..^ |
| 23 | 22 | adantl 466 |
. . . . . . . . . 10
..^ ..^
|
| 24 | 6 | zred 10747 |
. . . . . . . . . . . 12
|
| 25 | 24 | adantr 465 |
. . . . . . . . . . 11
|
| 26 | remulcl 9367 |
. . . . . . . . . . 11
| |
| 27 | 25, 19, 26 | syl2an 477 |
. . . . . . . . . 10
..^ ..^
|
| 28 | 23, 27 | resubcld 9776 |
. . . . . . . . 9
..^ ..^
|
| 29 | elfzoelz 11553 |
. . . . . . . . . . 11
..^
| |
| 30 | 29 | 3ad2ant2 1010 |
. . . . . . . . . 10
..^ ..^ |
| 31 | 30 | adantl 466 |
. . . . . . . . 9
..^ ..^
|
| 32 | 13 | nnrpd 11026 |
. . . . . . . . . . 11
 |
| 33 | 32 | 3ad2ant1 1009 |
. . . . . . . . . 10
..^ ..^ |
| 34 | 33 | adantl 466 |
. . . . . . . . 9
..^ ..^
|
| 35 | modaddmulmod 11765 |
. . . . . . . . 9
| |
| 36 | 20, 28, 31, 34, 35 | syl31anc 1221 |
. . . . . . . 8
..^ ..^
|
| 37 | 13 | nncnd 10338 |
. . . . . . . . . . . . 13
 |
| 38 | 37 | 3ad2ant1 1009 |
. . . . . . . . . . . 12
..^ ..^ |
| 39 | 38 | adantl 466 |
. . . . . . . . . . 11
..^ ..^
|
| 40 | 6 | zcnd 10748 |
. . . . . . . . . . . . 13
|
| 41 | 40 | adantr 465 |
. . . . . . . . . . . 12
|
| 42 | 8 | zcnd 10748 |
. . . . . . . . . . . . 13
..^
|
| 43 | 42 | 3ad2ant3 1011 |
. . . . . . . . . . . 12
..^ ..^ |
| 44 | mulcl 9366 |
. . . . . . . . . . . 12
| |
| 45 | 41, 43, 44 | syl2an 477 |
. . . . . . . . . . 11
..^ ..^
|
| 46 | 29 | zcnd 10748 |
. . . . . . . . . . . . 13
..^
|
| 47 | 46 | 3ad2ant2 1010 |
. . . . . . . . . . . 12
..^ ..^ |
| 48 | 47 | adantl 466 |
. . . . . . . . . . 11
..^ ..^
|
| 49 | 39, 45, 48 | subdird 9801 |
. . . . . . . . . 10
..^ ..^
|
| 50 | 49 | oveq2d 6107 |
. . . . . . . . 9
..^ ..^
|
| 51 | 50 | oveq1d 6106 |
. . . . . . . 8
..^ ..^
|
| 52 | mulcom 9368 |
. . . . . . . . . . . . . . . . . . 19
| |
| 53 | 37, 46, 52 | syl2an 477 |
. . . . . . . . . . . . . . . . . 18
..^
|
| 54 | 53 | oveq1d 6106 |
. . . . . . . . . . . . . . . . 17
..^
|
| 55 | modidmul0 11734 |
. . . . . . . . . . . . . . . . . 18
| |
| 56 | 29, 13, 55 | syl2anr 478 |
. . . . . . . . . . . . . . . . 17
..^
|
| 57 | 54, 56 | eqtrd 2475 |
. . . . . . . . . . . . . . . 16
..^
|
| 58 | 57 | 3adant3 1008 |
. . . . . . . . . . . . . . 15
..^ ..^ |
| 59 | 58 | adantl 466 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 60 | 41 | adantr 465 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 61 | 43 | adantl 466 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 62 | 60, 61, 48 | mul32d 9579 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 63 | 62 | oveq1d 6106 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 64 | 29 | zred 10747 |
. . . . . . . . . . . . . . . . . 18
..^
|
| 65 | 64 | 3ad2ant2 1010 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
| 66 | remulcl 9367 |
. . . . . . . . . . . . . . . . 17
| |
| 67 | 25, 65, 66 | syl2an 477 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 68 | 9 | adantl 466 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 69 | modmulmod 11764 |
. . . . . . . . . . . . . . . 16
| |
| 70 | 67, 68, 34, 69 | syl3anc 1218 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 71 | 63, 70 | eqtr4d 2478 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 72 | 59, 71 | oveq12d 6109 |
. . . . . . . . . . . . 13
..^ ..^
|
| 73 | 72 | oveq1d 6106 |
. . . . . . . . . . . 12
..^ ..^
|
| 74 | remulcl 9367 |
. . . . . . . . . . . . . . . 16
| |
| 75 | 21, 64, 74 | syl2an 477 |
. . . . . . . . . . . . . . 15
..^
|
| 76 | 75 | 3adant3 1008 |
. . . . . . . . . . . . . 14
..^ ..^ |
| 77 | 76 | adantl 466 |
. . . . . . . . . . . . 13
..^ ..^
|
| 78 | 65 | adantl 466 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 79 | 27, 78 | remulcld 9414 |
. . . . . . . . . . . . 13
..^ ..^
|
| 80 | modsubmodmod 11758 |
. . . . . . . . . . . . 13
| |
| 81 | 77, 79, 34, 80 | syl3anc 1218 |
. . . . . . . . . . . 12
..^ ..^
|
| 82 | mulcom 9368 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 83 | 47, 40, 82 | syl2anr 478 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^
|
| 84 | 83 | oveq1d 6106 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^
|
| 85 | 84 | eqeq1d 2451 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ 
|
| 86 | 85 | biimpd 207 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
| 87 | 86 | impancom 440 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
| 88 | 87 | imp 429 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 89 | 88 | oveq1d 6106 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 90 | 89 | oveq1d 6106 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 91 | 90 | oveq2d 6107 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 92 | 91 | oveq1d 6106 |
. . . . . . . . . . . . 13
..^ ..^
|
| 93 | 61 | mulid2d 9404 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 94 | 93 | oveq1d 6106 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 95 | 32, 18 | anim12ci 567 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 96 | elfzo2 11556 |
. . . . . . . . . . . . . . . . . . . . . 22
..^  
 | |
| 97 | eluz2 10867 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 | |
| 98 | 0red 9387 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 99 | 1red 9401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 100 | zre 10650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 101 | 98, 99, 100 | 3jca 1168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 102 | 101 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 103 | 0le1 9863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 104 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 105 | 104 | anim1i 568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 106 | letr 9468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 107 | 102, 105, 106 | sylc 60 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 108 | 107 | 3adant1 1006 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 109 | 97, 108 | sylbi 195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 110 | 109 | 3ad2ant1 1009 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 111 | simp3 990 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 112 | 110, 111 | jca 532 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 113 | 96, 112 | sylbi 195 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 114 | 113 | adantl 466 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 115 | 95, 114 | jca 532 |
. . . . . . . . . . . . . . . . . . 19
..^
|
| 116 | 115 | 3adant2 1007 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
| 117 | 116 | adantl 466 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 118 | modid 11732 |
. . . . . . . . . . . . . . . . 17
| |
| 119 | 117, 118 | syl 16 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 120 | 94, 119 | eqtrd 2475 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 121 | 120 | oveq2d 6107 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 122 | 121 | oveq1d 6106 |
. . . . . . . . . . . . 13
..^ ..^
|
| 123 | 92, 122 | eqtrd 2475 |
. . . . . . . . . . . 12
..^ ..^
|
| 124 | 73, 81, 123 | 3eqtr3d 2483 |
. . . . . . . . . . 11
..^ ..^
|
| 125 | 124 | oveq2d 6107 |
. . . . . . . . . 10
..^ ..^
|
| 126 | 125 | oveq1d 6106 |
. . . . . . . . 9
..^ ..^
|
| 127 | 77, 79 | resubcld 9776 |
. . . . . . . . . 10
..^ ..^
|
| 128 | modadd2mod 11749 |
. . . . . . . . . 10
| |
| 129 | 127, 20, 34, 128 | syl3anc 1218 |
. . . . . . . . 9
..^ ..^
|
| 130 | 0red 9387 |
. . . . . . . . . . . . . . . 16
..^
| |
| 131 | 130, 18 | resubcld 9776 |
. . . . . . . . . . . . . . 15
..^
|
| 132 | 131 | adantl 466 |
. . . . . . . . . . . . . 14
..^
|
| 133 | 18 | adantl 466 |
. . . . . . . . . . . . . 14
..^
|
| 134 | 32 | adantr 465 |
. . . . . . . . . . . . . 14
..^
|
| 135 | 132, 133, 134 | 3jca 1168 |
. . . . . . . . . . . . 13
..^
|
| 136 | 135 | 3adant2 1007 |
. . . . . . . . . . . 12
..^ ..^ |
| 137 | 136 | adantl 466 |
. . . . . . . . . . 11
..^ ..^
|
| 138 | modadd2mod 11749 |
. . . . . . . . . . 11
| |
| 139 | 137, 138 | syl 16 |
. . . . . . . . . 10
..^ ..^
|
| 140 | 0cnd 9379 |
. . . . . . . . . . . . . 14
..^
| |
| 141 | 42, 140 | pncan3d 9722 |
. . . . . . . . . . . . 13
..^
|
| 142 | 141 | 3ad2ant3 1011 |
. . . . . . . . . . . 12
..^ ..^ |
| 143 | 142 | adantl 466 |
. . . . . . . . . . 11
..^ ..^
|
| 144 | 143 | oveq1d 6106 |
. . . . . . . . . 10
..^ ..^
|
| 145 | 0mod 11739 |
. . . . . . . . . . . . 13
| |
| 146 | 32, 145 | syl 16 |
. . . . . . . . . . . 12
|
| 147 | 146 | 3ad2ant1 1009 |
. . . . . . . . . . 11
..^ ..^ |
| 148 | 147 | adantl 466 |
. . . . . . . . . 10
..^ ..^
|
| 149 | 139, 144, 148 | 3eqtrd 2479 |
. . . . . . . . 9
..^ ..^
|
| 150 | 126, 129, 149 | 3eqtr3d 2483 |
. . . . . . . 8
..^ ..^
|
| 151 | 36, 51, 150 | 3eqtrd 2479 |
. . . . . . 7
..^ ..^
|
| 152 | oveq1 6098 |
. . . . . . . . . . 11
| |
| 153 | 152 | oveq2d 6107 |
. . . . . . . . . 10
|
| 154 | 153 | oveq1d 6106 |
. . . . . . . . 9
|
| 155 | 154 | eqeq1d 2451 |
. . . . . . . 8
|
| 156 | 155 | rspcev 3073 |
. . . . . . 7
..^
..^ |
| 157 | 17, 151, 156 | syl2anc 661 |
. . . . . 6
..^ ..^
..^ |
| 158 | 157 | ex 434 |
. . . . 5
..^ ..^ ..^ |
| 159 | 158 | rexlimiva 2836 |
. . . 4
..^ ..^
..^ |
| 160 | 1, 2, 159 | 3syl 20 |
. . 3
..^
..^ ..^ ..^ |
| 161 | 160 | 3adant3 1008 |
. 2
..^ ..^
..^ ..^ ..^ |
| 162 | 161 | pm2.43i 47 |
1
..^ ..^ ..^ |
| Colors of variables: wff setvar class |
| Syntax hints: wi 4
wa 369
w3a 965
wceq 1369
wcel 1756
wrex 2716
wreu 2717
class class class wbr 4292 cfv 5418 (class class class)co 6091
cc 9280
cr 9281
cc0 9282
c1 9283
caddc 9285 cmul 9287 clt 9418 cle 9419 cmin 9595 cn 10322 cz 10646 cuz 10861 crp 10991 cfz 11437 ..^cfzo 11548
cmo 11708
cprime 13763 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4403 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372 ax-cnex 9338 ax-resscn 9339 ax-1cn 9340 ax-icn 9341 ax-addcl 9342 ax-addrcl 9343 ax-mulcl 9344 ax-mulrcl 9345 ax-mulcom 9346 ax-addass 9347 ax-mulass 9348 ax-distr 9349 ax-i2m1 9350 ax-1ne0 9351 ax-1rid 9352 ax-rnegex 9353 ax-rrecex 9354 ax-cnre 9355 ax-pre-lttri 9356 ax-pre-lttrn 9357 ax-pre-ltadd 9358 ax-pre-mulgt0 9359 ax-pre-sup 9360 |
| This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-nel 2609 df-ral 2720 df-rex 2721 df-reu 2722 df-rmo 2723 df-rab 2724 df-v 2974 df-sbc 3187 df-csb 3289 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-pss 3344 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-tp 3882 df-op 3884 df-uni 4092 df-int 4129 df-iun 4173 df-br 4293 df-opab 4351 df-mpt 4352 df-tr 4386 df-eprel 4632 df-id 4636 df-po 4641 df-so 4642 df-fr 4679 df-we 4681 df-ord 4722 df-on 4723 df-lim 4724 df-suc 4725 df-xp 4846 df-rel 4847 df-cnv 4848 df-co 4849 df-dm 4850 df-rn 4851 df-res 4852 df-ima 4853 df-iota 5381 df-fun 5420 df-fn 5421 df-f 5422 df-f1 5423 df-fo 5424 df-f1o 5425 df-fv 5426 df-riota 6052 df-ov 6094 df-oprab 6095 df-mpt2 6096 df-om 6477 df-1st 6577 df-2nd 6578 df-recs 6832 df-rdg 6866 df-1o 6920 df-2o 6921 df-oadd 6924 df-er 7101 df-map 7216 df-en 7311 df-dom 7312 df-sdom 7313 df-fin 7314 df-sup 7691 df-card 8109 df-cda 8337 df-pnf 9420 df-mnf 9421 df-xr 9422 df-ltxr 9423 df-le 9424 df-sub 9597 df-neg 9598 df-div 9994 df-nn 10323 df-2 10380 df-3 10381 df-n0 10580 df-z 10647 df-uz 10862 df-rp 10992 df-fz 11438 df-fzo 11549 df-fl 11642 df-mod 11709 df-seq 11807 df-exp 11866 df-hash 12104 df-cj 12588 df-re 12589 df-im 12590 df-sqr 12724 df-abs 12725 df-dvds 13536 df-gcd 13691 df-prm 13764 df-phi 13841 |
| This theorem is referenced by: nnnn0modprm0 13874 |
| Copyright terms: Public domain | W3C validator |