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 14340 |
. . . 4
..^
  
| |
| 2 | reurex 3074 |
. . . 4
| |
| 3 | prmz 14232 |
. . . . . . . . . . 11
 | |
| 4 | 3 | 3ad2ant1 1017 |
. . . . . . . . . 10
..^ ..^ |
| 5 | 4 | adantl 466 |
. . . . . . . . 9
..^ ..^
|
| 6 | elfzelz 11713 |
. . . . . . . . . . 11
| |
| 7 | 6 | adantr 465 |
. . . . . . . . . 10
|
| 8 | elfzoelz 11825 |
. . . . . . . . . . 11
..^
| |
| 9 | 8 | 3ad2ant3 1019 |
. . . . . . . . . 10
..^ ..^ |
| 10 | zmulcl 10933 |
. . . . . . . . . 10
| |
| 11 | 7, 9, 10 | syl2an 477 |
. . . . . . . . 9
..^ ..^
|
| 12 | 5, 11 | zsubcld 10995 |
. . . . . . . 8
..^ ..^
|
| 13 | prmnn 14231 |
. . . . . . . . . 10
 | |
| 14 | 13 | 3ad2ant1 1017 |
. . . . . . . . 9
..^ ..^ |
| 15 | 14 | adantl 466 |
. . . . . . . 8
..^ ..^
|
| 16 | zmodfzo 12020 |
. . . . . . . 8
..^ | |
| 17 | 12, 15, 16 | syl2anc 661 |
. . . . . . 7
..^ ..^
..^ |
| 18 | 8 | zred 10990 |
. . . . . . . . . . 11
..^
 |
| 19 | 18 | 3ad2ant3 1019 |
. . . . . . . . . 10
..^ ..^ |
| 20 | 19 | adantl 466 |
. . . . . . . . 9
..^ ..^
|
| 21 | 13 | nnred 10571 |
. . . . . . . . . . . 12
|
| 22 | 21 | 3ad2ant1 1017 |
. . . . . . . . . . 11
..^ ..^ |
| 23 | 22 | adantl 466 |
. . . . . . . . . 10
..^ ..^
|
| 24 | 6 | zred 10990 |
. . . . . . . . . . . 12
|
| 25 | 24 | adantr 465 |
. . . . . . . . . . 11
|
| 26 | remulcl 9594 |
. . . . . . . . . . 11
| |
| 27 | 25, 19, 26 | syl2an 477 |
. . . . . . . . . 10
..^ ..^
|
| 28 | 23, 27 | resubcld 10008 |
. . . . . . . . 9
..^ ..^
|
| 29 | elfzoelz 11825 |
. . . . . . . . . . 11
..^
| |
| 30 | 29 | 3ad2ant2 1018 |
. . . . . . . . . 10
..^ ..^ |
| 31 | 30 | adantl 466 |
. . . . . . . . 9
..^ ..^
|
| 32 | 13 | nnrpd 11280 |
. . . . . . . . . . 11
 |
| 33 | 32 | 3ad2ant1 1017 |
. . . . . . . . . 10
..^ ..^ |
| 34 | 33 | adantl 466 |
. . . . . . . . 9
..^ ..^
|
| 35 | modaddmulmod 12055 |
. . . . . . . . 9
| |
| 36 | 20, 28, 31, 34, 35 | syl31anc 1231 |
. . . . . . . 8
..^ ..^
|
| 37 | 13 | nncnd 10572 |
. . . . . . . . . . . . 13
 |
| 38 | 37 | 3ad2ant1 1017 |
. . . . . . . . . . . 12
..^ ..^ |
| 39 | 38 | adantl 466 |
. . . . . . . . . . 11
..^ ..^
|
| 40 | 6 | zcnd 10991 |
. . . . . . . . . . . . 13
|
| 41 | 40 | adantr 465 |
. . . . . . . . . . . 12
|
| 42 | 8 | zcnd 10991 |
. . . . . . . . . . . . 13
..^
|
| 43 | 42 | 3ad2ant3 1019 |
. . . . . . . . . . . 12
..^ ..^ |
| 44 | mulcl 9593 |
. . . . . . . . . . . 12
| |
| 45 | 41, 43, 44 | syl2an 477 |
. . . . . . . . . . 11
..^ ..^
|
| 46 | 29 | zcnd 10991 |
. . . . . . . . . . . . 13
..^
|
| 47 | 46 | 3ad2ant2 1018 |
. . . . . . . . . . . 12
..^ ..^ |
| 48 | 47 | adantl 466 |
. . . . . . . . . . 11
..^ ..^
|
| 49 | 39, 45, 48 | subdird 10034 |
. . . . . . . . . 10
..^ ..^
|
| 50 | 49 | oveq2d 6312 |
. . . . . . . . 9
..^ ..^
|
| 51 | 50 | oveq1d 6311 |
. . . . . . . 8
..^ ..^
|
| 52 | mulcom 9595 |
. . . . . . . . . . . . . . . . . . 19
| |
| 53 | 37, 46, 52 | syl2an 477 |
. . . . . . . . . . . . . . . . . 18
..^
|
| 54 | 53 | oveq1d 6311 |
. . . . . . . . . . . . . . . . 17
..^
|
| 55 | modidmul0 12024 |
. . . . . . . . . . . . . . . . . 18
| |
| 56 | 29, 13, 55 | syl2anr 478 |
. . . . . . . . . . . . . . . . 17
..^
|
| 57 | 54, 56 | eqtrd 2498 |
. . . . . . . . . . . . . . . 16
..^
|
| 58 | 57 | 3adant3 1016 |
. . . . . . . . . . . . . . 15
..^ ..^ |
| 59 | 58 | adantl 466 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 60 | 41 | adantr 465 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 61 | 43 | adantl 466 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 62 | 60, 61, 48 | mul32d 9807 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 63 | 62 | oveq1d 6311 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 64 | 29 | zred 10990 |
. . . . . . . . . . . . . . . . . 18
..^
|
| 65 | 64 | 3ad2ant2 1018 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
| 66 | remulcl 9594 |
. . . . . . . . . . . . . . . . 17
| |
| 67 | 25, 65, 66 | syl2an 477 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 68 | 9 | adantl 466 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 69 | modmulmod 12054 |
. . . . . . . . . . . . . . . 16
| |
| 70 | 67, 68, 34, 69 | syl3anc 1228 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 71 | 63, 70 | eqtr4d 2501 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 72 | 59, 71 | oveq12d 6314 |
. . . . . . . . . . . . 13
..^ ..^
|
| 73 | 72 | oveq1d 6311 |
. . . . . . . . . . . 12
..^ ..^
|
| 74 | remulcl 9594 |
. . . . . . . . . . . . . . . 16
| |
| 75 | 21, 64, 74 | syl2an 477 |
. . . . . . . . . . . . . . 15
..^
|
| 76 | 75 | 3adant3 1016 |
. . . . . . . . . . . . . 14
..^ ..^ |
| 77 | 76 | adantl 466 |
. . . . . . . . . . . . 13
..^ ..^
|
| 78 | 65 | adantl 466 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 79 | 27, 78 | remulcld 9641 |
. . . . . . . . . . . . 13
..^ ..^
|
| 80 | modsubmodmod 12048 |
. . . . . . . . . . . . 13
| |
| 81 | 77, 79, 34, 80 | syl3anc 1228 |
. . . . . . . . . . . 12
..^ ..^
|
| 82 | mulcom 9595 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 83 | 47, 40, 82 | syl2anr 478 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^
|
| 84 | 83 | oveq1d 6311 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^
|
| 85 | 84 | eqeq1d 2459 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ 
|
| 86 | 85 | biimpd 207 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
| 87 | 86 | impancom 440 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
| 88 | 87 | imp 429 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 89 | 88 | oveq1d 6311 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 90 | 89 | oveq1d 6311 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 91 | 90 | oveq2d 6312 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 92 | 91 | oveq1d 6311 |
. . . . . . . . . . . . 13
..^ ..^
|
| 93 | 61 | mulid2d 9631 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 94 | 93 | oveq1d 6311 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 95 | 32, 18 | anim12ci 567 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 96 | elfzo2 11828 |
. . . . . . . . . . . . . . . . . . . . . 22
..^  
 | |
| 97 | eluz2 11112 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 | |
| 98 | 0red 9614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 99 | 1red 9628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 100 | zre 10889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 101 | 98, 99, 100 | 3jca 1176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 102 | 101 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 103 | 0le1 10097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 104 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 105 | 104 | anim1i 568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 106 | letr 9695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 107 | 102, 105, 106 | sylc 60 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 108 | 107 | 3adant1 1014 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 109 | 97, 108 | sylbi 195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 110 | 109 | 3ad2ant1 1017 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 111 | simp3 998 |
. . . . . . . . . . . . . . . . . . . . . . 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 1015 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
| 117 | 116 | adantl 466 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 118 | modid 12022 |
. . . . . . . . . . . . . . . . 17
| |
| 119 | 117, 118 | syl 16 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 120 | 94, 119 | eqtrd 2498 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 121 | 120 | oveq2d 6312 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 122 | 121 | oveq1d 6311 |
. . . . . . . . . . . . 13
..^ ..^
|
| 123 | 92, 122 | eqtrd 2498 |
. . . . . . . . . . . 12
..^ ..^
|
| 124 | 73, 81, 123 | 3eqtr3d 2506 |
. . . . . . . . . . 11
..^ ..^
|
| 125 | 124 | oveq2d 6312 |
. . . . . . . . . 10
..^ ..^
|
| 126 | 125 | oveq1d 6311 |
. . . . . . . . 9
..^ ..^
|
| 127 | 77, 79 | resubcld 10008 |
. . . . . . . . . 10
..^ ..^
|
| 128 | modadd2mod 12039 |
. . . . . . . . . 10
| |
| 129 | 127, 20, 34, 128 | syl3anc 1228 |
. . . . . . . . 9
..^ ..^
|
| 130 | 0red 9614 |
. . . . . . . . . . . . . . . 16
..^
| |
| 131 | 130, 18 | resubcld 10008 |
. . . . . . . . . . . . . . 15
..^
|
| 132 | 131 | adantl 466 |
. . . . . . . . . . . . . 14
..^
|
| 133 | 18 | adantl 466 |
. . . . . . . . . . . . . 14
..^
|
| 134 | 32 | adantr 465 |
. . . . . . . . . . . . . 14
..^
|
| 135 | 132, 133, 134 | 3jca 1176 |
. . . . . . . . . . . . 13
..^
|
| 136 | 135 | 3adant2 1015 |
. . . . . . . . . . . 12
..^ ..^ |
| 137 | 136 | adantl 466 |
. . . . . . . . . . 11
..^ ..^
|
| 138 | modadd2mod 12039 |
. . . . . . . . . . 11
| |
| 139 | 137, 138 | syl 16 |
. . . . . . . . . 10
..^ ..^
|
| 140 | 0cnd 9606 |
. . . . . . . . . . . . . 14
..^
| |
| 141 | 42, 140 | pncan3d 9953 |
. . . . . . . . . . . . 13
..^
|
| 142 | 141 | 3ad2ant3 1019 |
. . . . . . . . . . . 12
..^ ..^ |
| 143 | 142 | adantl 466 |
. . . . . . . . . . 11
..^ ..^
|
| 144 | 143 | oveq1d 6311 |
. . . . . . . . . 10
..^ ..^
|
| 145 | 0mod 12029 |
. . . . . . . . . . . . 13
| |
| 146 | 32, 145 | syl 16 |
. . . . . . . . . . . 12
|
| 147 | 146 | 3ad2ant1 1017 |
. . . . . . . . . . 11
..^ ..^ |
| 148 | 147 | adantl 466 |
. . . . . . . . . 10
..^ ..^
|
| 149 | 139, 144, 148 | 3eqtrd 2502 |
. . . . . . . . 9
..^ ..^
|
| 150 | 126, 129, 149 | 3eqtr3d 2506 |
. . . . . . . 8
..^ ..^
|
| 151 | 36, 51, 150 | 3eqtrd 2502 |
. . . . . . 7
..^ ..^
|
| 152 | oveq1 6303 |
. . . . . . . . . . 11
| |
| 153 | 152 | oveq2d 6312 |
. . . . . . . . . 10
|
| 154 | 153 | oveq1d 6311 |
. . . . . . . . 9
|
| 155 | 154 | eqeq1d 2459 |
. . . . . . . 8
|
| 156 | 155 | rspcev 3210 |
. . . . . . 7
..^
..^ |
| 157 | 17, 151, 156 | syl2anc 661 |
. . . . . 6
..^ ..^
..^ |
| 158 | 157 | ex 434 |
. . . . 5
..^ ..^ ..^ |
| 159 | 158 | rexlimiva 2945 |
. . . 4
..^ ..^
..^ |
| 160 | 1, 2, 159 | 3syl 20 |
. . 3
..^
..^ ..^ ..^ |
| 161 | 160 | 3adant3 1016 |
. 2
..^ ..^
..^ ..^ ..^ |
| 162 | 161 | pm2.43i 47 |
1
..^ ..^ ..^ |
| Colors of variables: wff setvar class |
| Syntax hints: wi 4
wa 369
w3a 973
wceq 1395
wcel 1819
wrex 2808
wreu 2809
class class class wbr 4456 cfv 5594 (class class class)co 6296
cc 9507
cr 9508
cc0 9509
c1 9510
caddc 9512 cmul 9514 clt 9645 cle 9646 cmin 9824 cn 10556 cz 10885 cuz 11106 crp 11245 cfz 11697 ..^cfzo 11820
cmo 11998
cprime 14228 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587 |
| This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-map 7440 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-sup 7919 df-card 8337 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-n0 10817 df-z 10886 df-uz 11107 df-rp 11246 df-fz 11698 df-fzo 11821 df-fl 11931 df-mod 11999 df-seq 12110 df-exp 12169 df-hash 12408 df-cj 12943 df-re 12944 df-im 12945 df-sqrt 13079 df-abs 13080 df-dvds 13998 df-gcd 14156 df-prm 14229 df-phi 14307 |
| This theorem is referenced by: nnnn0modprm0 14342 |
| Copyright terms: Public domain | W3C validator |