Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > modprm0 | Structured version Visualization 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 14834 |
. . . 4
..^
  
| |
| 2 | reurex 2995 |
. . . 4
| |
| 3 | prmz 14705 |
. . . . . . . . . . 11
 | |
| 4 | 3 | 3ad2ant1 1051 |
. . . . . . . . . 10
..^ ..^ |
| 5 | 4 | adantl 473 |
. . . . . . . . 9
..^ ..^
|
| 6 | elfzelz 11826 |
. . . . . . . . . . 11
| |
| 7 | 6 | adantr 472 |
. . . . . . . . . 10
|
| 8 | elfzoelz 11947 |
. . . . . . . . . . 11
..^
| |
| 9 | 8 | 3ad2ant3 1053 |
. . . . . . . . . 10
..^ ..^ |
| 10 | zmulcl 11009 |
. . . . . . . . . 10
| |
| 11 | 7, 9, 10 | syl2an 485 |
. . . . . . . . 9
..^ ..^
|
| 12 | 5, 11 | zsubcld 11068 |
. . . . . . . 8
..^ ..^
|
| 13 | prmnn 14704 |
. . . . . . . . . 10
 | |
| 14 | 13 | 3ad2ant1 1051 |
. . . . . . . . 9
..^ ..^ |
| 15 | 14 | adantl 473 |
. . . . . . . 8
..^ ..^
|
| 16 | zmodfzo 12152 |
. . . . . . . 8
..^ | |
| 17 | 12, 15, 16 | syl2anc 673 |
. . . . . . 7
..^ ..^
..^ |
| 18 | 8 | zred 11063 |
. . . . . . . . . . 11
..^
 |
| 19 | 18 | 3ad2ant3 1053 |
. . . . . . . . . 10
..^ ..^ |
| 20 | 19 | adantl 473 |
. . . . . . . . 9
..^ ..^
|
| 21 | 13 | nnred 10646 |
. . . . . . . . . . . 12
|
| 22 | 21 | 3ad2ant1 1051 |
. . . . . . . . . . 11
..^ ..^ |
| 23 | 22 | adantl 473 |
. . . . . . . . . 10
..^ ..^
|
| 24 | 6 | zred 11063 |
. . . . . . . . . . . 12
|
| 25 | 24 | adantr 472 |
. . . . . . . . . . 11
|
| 26 | remulcl 9642 |
. . . . . . . . . . 11
| |
| 27 | 25, 19, 26 | syl2an 485 |
. . . . . . . . . 10
..^ ..^
|
| 28 | 23, 27 | resubcld 10068 |
. . . . . . . . 9
..^ ..^
|
| 29 | elfzoelz 11947 |
. . . . . . . . . . 11
..^
| |
| 30 | 29 | 3ad2ant2 1052 |
. . . . . . . . . 10
..^ ..^ |
| 31 | 30 | adantl 473 |
. . . . . . . . 9
..^ ..^
|
| 32 | 13 | nnrpd 11362 |
. . . . . . . . . . 11
 |
| 33 | 32 | 3ad2ant1 1051 |
. . . . . . . . . 10
..^ ..^ |
| 34 | 33 | adantl 473 |
. . . . . . . . 9
..^ ..^
|
| 35 | modaddmulmod 12190 |
. . . . . . . . 9
| |
| 36 | 20, 28, 31, 34, 35 | syl31anc 1295 |
. . . . . . . 8
..^ ..^
|
| 37 | 13 | nncnd 10647 |
. . . . . . . . . . . . 13
 |
| 38 | 37 | 3ad2ant1 1051 |
. . . . . . . . . . . 12
..^ ..^ |
| 39 | 38 | adantl 473 |
. . . . . . . . . . 11
..^ ..^
|
| 40 | 6 | zcnd 11064 |
. . . . . . . . . . . . 13
|
| 41 | 40 | adantr 472 |
. . . . . . . . . . . 12
|
| 42 | 8 | zcnd 11064 |
. . . . . . . . . . . . 13
..^
|
| 43 | 42 | 3ad2ant3 1053 |
. . . . . . . . . . . 12
..^ ..^ |
| 44 | mulcl 9641 |
. . . . . . . . . . . 12
| |
| 45 | 41, 43, 44 | syl2an 485 |
. . . . . . . . . . 11
..^ ..^
|
| 46 | 29 | zcnd 11064 |
. . . . . . . . . . . . 13
..^
|
| 47 | 46 | 3ad2ant2 1052 |
. . . . . . . . . . . 12
..^ ..^ |
| 48 | 47 | adantl 473 |
. . . . . . . . . . 11
..^ ..^
|
| 49 | 39, 45, 48 | subdird 10096 |
. . . . . . . . . 10
..^ ..^
|
| 50 | 49 | oveq2d 6324 |
. . . . . . . . 9
..^ ..^
|
| 51 | 50 | oveq1d 6323 |
. . . . . . . 8
..^ ..^
|
| 52 | mulcom 9643 |
. . . . . . . . . . . . . . . . . . 19
| |
| 53 | 37, 46, 52 | syl2an 485 |
. . . . . . . . . . . . . . . . . 18
..^
|
| 54 | 53 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
..^
|
| 55 | mulmod0 12137 |
. . . . . . . . . . . . . . . . . 18
| |
| 56 | 29, 32, 55 | syl2anr 486 |
. . . . . . . . . . . . . . . . 17
..^
|
| 57 | 54, 56 | eqtrd 2505 |
. . . . . . . . . . . . . . . 16
..^
|
| 58 | 57 | 3adant3 1050 |
. . . . . . . . . . . . . . 15
..^ ..^ |
| 59 | 58 | adantl 473 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 60 | 41 | adantr 472 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 61 | 43 | adantl 473 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 62 | 60, 61, 48 | mul32d 9861 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 63 | 62 | oveq1d 6323 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 64 | 29 | zred 11063 |
. . . . . . . . . . . . . . . . . 18
..^
|
| 65 | 64 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
| 66 | remulcl 9642 |
. . . . . . . . . . . . . . . . 17
| |
| 67 | 25, 65, 66 | syl2an 485 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 68 | 9 | adantl 473 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 69 | modmulmod 12189 |
. . . . . . . . . . . . . . . 16
| |
| 70 | 67, 68, 34, 69 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 71 | 63, 70 | eqtr4d 2508 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 72 | 59, 71 | oveq12d 6326 |
. . . . . . . . . . . . 13
..^ ..^
|
| 73 | 72 | oveq1d 6323 |
. . . . . . . . . . . 12
..^ ..^
|
| 74 | remulcl 9642 |
. . . . . . . . . . . . . . . 16
| |
| 75 | 21, 64, 74 | syl2an 485 |
. . . . . . . . . . . . . . 15
..^
|
| 76 | 75 | 3adant3 1050 |
. . . . . . . . . . . . . 14
..^ ..^ |
| 77 | 76 | adantl 473 |
. . . . . . . . . . . . 13
..^ ..^
|
| 78 | 65 | adantl 473 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 79 | 27, 78 | remulcld 9689 |
. . . . . . . . . . . . 13
..^ ..^
|
| 80 | modsubmodmod 12183 |
. . . . . . . . . . . . 13
| |
| 81 | 77, 79, 34, 80 | syl3anc 1292 |
. . . . . . . . . . . 12
..^ ..^
|
| 82 | mulcom 9643 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 83 | 47, 40, 82 | syl2anr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^
|
| 84 | 83 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^
|
| 85 | 84 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ 
|
| 86 | 85 | biimpd 212 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
| 87 | 86 | impancom 447 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
| 88 | 87 | imp 436 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 89 | 88 | oveq1d 6323 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 90 | 89 | oveq1d 6323 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 91 | 90 | oveq2d 6324 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 92 | 91 | oveq1d 6323 |
. . . . . . . . . . . . 13
..^ ..^
|
| 93 | 61 | mulid2d 9679 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 94 | 93 | oveq1d 6323 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 95 | 32, 18 | anim12ci 577 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 96 | elfzo2 11950 |
. . . . . . . . . . . . . . . . . . . . . 22
..^  
 | |
| 97 | eluz2 11188 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 | |
| 98 | 0red 9662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 99 | 1red 9676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 100 | zre 10965 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 101 | 98, 99, 100 | 3jca 1210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 102 | 101 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 103 | 0le1 10158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 104 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 105 | 104 | anim1i 578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 106 | letr 9745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 107 | 102, 105, 106 | sylc 61 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 108 | 107 | 3adant1 1048 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 109 | 97, 108 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 110 | 109 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 111 | simp3 1032 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 112 | 110, 111 | jca 541 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 113 | 96, 112 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 114 | 113 | adantl 473 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 115 | 95, 114 | jca 541 |
. . . . . . . . . . . . . . . . . . 19
..^
|
| 116 | 115 | 3adant2 1049 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
| 117 | 116 | adantl 473 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 118 | modid 12154 |
. . . . . . . . . . . . . . . . 17
| |
| 119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 120 | 94, 119 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 121 | 120 | oveq2d 6324 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 122 | 121 | oveq1d 6323 |
. . . . . . . . . . . . 13
..^ ..^
|
| 123 | 92, 122 | eqtrd 2505 |
. . . . . . . . . . . 12
..^ ..^
|
| 124 | 73, 81, 123 | 3eqtr3d 2513 |
. . . . . . . . . . 11
..^ ..^
|
| 125 | 124 | oveq2d 6324 |
. . . . . . . . . 10
..^ ..^
|
| 126 | 125 | oveq1d 6323 |
. . . . . . . . 9
..^ ..^
|
| 127 | 77, 79 | resubcld 10068 |
. . . . . . . . . 10
..^ ..^
|
| 128 | modadd2mod 12174 |
. . . . . . . . . 10
| |
| 129 | 127, 20, 34, 128 | syl3anc 1292 |
. . . . . . . . 9
..^ ..^
|
| 130 | 0red 9662 |
. . . . . . . . . . . . . . . 16
..^
| |
| 131 | 130, 18 | resubcld 10068 |
. . . . . . . . . . . . . . 15
..^
|
| 132 | 131 | adantl 473 |
. . . . . . . . . . . . . 14
..^
|
| 133 | 18 | adantl 473 |
. . . . . . . . . . . . . 14
..^
|
| 134 | 32 | adantr 472 |
. . . . . . . . . . . . . 14
..^
|
| 135 | 132, 133, 134 | 3jca 1210 |
. . . . . . . . . . . . 13
..^
|
| 136 | 135 | 3adant2 1049 |
. . . . . . . . . . . 12
..^ ..^ |
| 137 | 136 | adantl 473 |
. . . . . . . . . . 11
..^ ..^
|
| 138 | modadd2mod 12174 |
. . . . . . . . . . 11
| |
| 139 | 137, 138 | syl 17 |
. . . . . . . . . 10
..^ ..^
|
| 140 | 0cnd 9654 |
. . . . . . . . . . . . . 14
..^
| |
| 141 | 42, 140 | pncan3d 10008 |
. . . . . . . . . . . . 13
..^
|
| 142 | 141 | 3ad2ant3 1053 |
. . . . . . . . . . . 12
..^ ..^ |
| 143 | 142 | adantl 473 |
. . . . . . . . . . 11
..^ ..^
|
| 144 | 143 | oveq1d 6323 |
. . . . . . . . . 10
..^ ..^
|
| 145 | 0mod 12161 |
. . . . . . . . . . . . 13
| |
| 146 | 32, 145 | syl 17 |
. . . . . . . . . . . 12
|
| 147 | 146 | 3ad2ant1 1051 |
. . . . . . . . . . 11
..^ ..^ |
| 148 | 147 | adantl 473 |
. . . . . . . . . 10
..^ ..^
|
| 149 | 139, 144, 148 | 3eqtrd 2509 |
. . . . . . . . 9
..^ ..^
|
| 150 | 126, 129, 149 | 3eqtr3d 2513 |
. . . . . . . 8
..^ ..^
|
| 151 | 36, 51, 150 | 3eqtrd 2509 |
. . . . . . 7
..^ ..^
|
| 152 | oveq1 6315 |
. . . . . . . . . . 11
| |
| 153 | 152 | oveq2d 6324 |
. . . . . . . . . 10
|
| 154 | 153 | oveq1d 6323 |
. . . . . . . . 9
|
| 155 | 154 | eqeq1d 2473 |
. . . . . . . 8
|
| 156 | 155 | rspcev 3136 |
. . . . . . 7
..^
..^ |
| 157 | 17, 151, 156 | syl2anc 673 |
. . . . . 6
..^ ..^
..^ |
| 158 | 157 | ex 441 |
. . . . 5
..^ ..^ ..^ |
| 159 | 158 | rexlimiva 2868 |
. . . 4
..^ ..^
..^ |
| 160 | 1, 2, 159 | 3syl 18 |
. . 3
..^
..^ ..^ ..^ |
| 161 | 160 | 3adant3 1050 |
. 2
..^ ..^
..^ ..^ ..^ |
| 162 | 161 | pm2.43i 48 |
1
..^ ..^ ..^ |
| Colors of variables: wff setvar class |
| Syntax hints: wi 4
wa 376
w3a 1007
wceq 1452
wcel 1904
wrex 2757
wreu 2758
class class class wbr 4395 cfv 5589 (class class class)co 6308
cc 9555
cr 9556
cc0 9557
c1 9558
caddc 9560 cmul 9562 clt 9693 cle 9694 cmin 9880 cn 10631 cz 10961 cuz 11182 crp 11325 cfz 11810 ..^cfzo 11942
cmo 12129
cprime 14701 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 |
| This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-sup 7974 df-inf 7975 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-rp 11326 df-fz 11811 df-fzo 11943 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-hash 12554 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-dvds 14383 df-gcd 14548 df-prm 14702 df-phi 14793 |
| This theorem is referenced by: nnnn0modprm0 14836 |
| Copyright terms: Public domain | W3C validator |