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 14755 |
. . . 4
..^
  
| |
| 2 | reurex 3009 |
. . . 4
| |
| 3 | prmz 14626 |
. . . . . . . . . . 11
 | |
| 4 | 3 | 3ad2ant1 1029 |
. . . . . . . . . 10
..^ ..^ |
| 5 | 4 | adantl 468 |
. . . . . . . . 9
..^ ..^
|
| 6 | elfzelz 11800 |
. . . . . . . . . . 11
| |
| 7 | 6 | adantr 467 |
. . . . . . . . . 10
|
| 8 | elfzoelz 11920 |
. . . . . . . . . . 11
..^
| |
| 9 | 8 | 3ad2ant3 1031 |
. . . . . . . . . 10
..^ ..^ |
| 10 | zmulcl 10985 |
. . . . . . . . . 10
| |
| 11 | 7, 9, 10 | syl2an 480 |
. . . . . . . . 9
..^ ..^
|
| 12 | 5, 11 | zsubcld 11045 |
. . . . . . . 8
..^ ..^
|
| 13 | prmnn 14625 |
. . . . . . . . . 10
 | |
| 14 | 13 | 3ad2ant1 1029 |
. . . . . . . . 9
..^ ..^ |
| 15 | 14 | adantl 468 |
. . . . . . . 8
..^ ..^
|
| 16 | zmodfzo 12119 |
. . . . . . . 8
..^ | |
| 17 | 12, 15, 16 | syl2anc 667 |
. . . . . . 7
..^ ..^
..^ |
| 18 | 8 | zred 11040 |
. . . . . . . . . . 11
..^
 |
| 19 | 18 | 3ad2ant3 1031 |
. . . . . . . . . 10
..^ ..^ |
| 20 | 19 | adantl 468 |
. . . . . . . . 9
..^ ..^
|
| 21 | 13 | nnred 10624 |
. . . . . . . . . . . 12
|
| 22 | 21 | 3ad2ant1 1029 |
. . . . . . . . . . 11
..^ ..^ |
| 23 | 22 | adantl 468 |
. . . . . . . . . 10
..^ ..^
|
| 24 | 6 | zred 11040 |
. . . . . . . . . . . 12
|
| 25 | 24 | adantr 467 |
. . . . . . . . . . 11
|
| 26 | remulcl 9624 |
. . . . . . . . . . 11
| |
| 27 | 25, 19, 26 | syl2an 480 |
. . . . . . . . . 10
..^ ..^
|
| 28 | 23, 27 | resubcld 10047 |
. . . . . . . . 9
..^ ..^
|
| 29 | elfzoelz 11920 |
. . . . . . . . . . 11
..^
| |
| 30 | 29 | 3ad2ant2 1030 |
. . . . . . . . . 10
..^ ..^ |
| 31 | 30 | adantl 468 |
. . . . . . . . 9
..^ ..^
|
| 32 | 13 | nnrpd 11339 |
. . . . . . . . . . 11
 |
| 33 | 32 | 3ad2ant1 1029 |
. . . . . . . . . 10
..^ ..^ |
| 34 | 33 | adantl 468 |
. . . . . . . . 9
..^ ..^
|
| 35 | modaddmulmod 12156 |
. . . . . . . . 9
| |
| 36 | 20, 28, 31, 34, 35 | syl31anc 1271 |
. . . . . . . 8
..^ ..^
|
| 37 | 13 | nncnd 10625 |
. . . . . . . . . . . . 13
 |
| 38 | 37 | 3ad2ant1 1029 |
. . . . . . . . . . . 12
..^ ..^ |
| 39 | 38 | adantl 468 |
. . . . . . . . . . 11
..^ ..^
|
| 40 | 6 | zcnd 11041 |
. . . . . . . . . . . . 13
|
| 41 | 40 | adantr 467 |
. . . . . . . . . . . 12
|
| 42 | 8 | zcnd 11041 |
. . . . . . . . . . . . 13
..^
|
| 43 | 42 | 3ad2ant3 1031 |
. . . . . . . . . . . 12
..^ ..^ |
| 44 | mulcl 9623 |
. . . . . . . . . . . 12
| |
| 45 | 41, 43, 44 | syl2an 480 |
. . . . . . . . . . 11
..^ ..^
|
| 46 | 29 | zcnd 11041 |
. . . . . . . . . . . . 13
..^
|
| 47 | 46 | 3ad2ant2 1030 |
. . . . . . . . . . . 12
..^ ..^ |
| 48 | 47 | adantl 468 |
. . . . . . . . . . 11
..^ ..^
|
| 49 | 39, 45, 48 | subdird 10075 |
. . . . . . . . . 10
..^ ..^
|
| 50 | 49 | oveq2d 6306 |
. . . . . . . . 9
..^ ..^
|
| 51 | 50 | oveq1d 6305 |
. . . . . . . 8
..^ ..^
|
| 52 | mulcom 9625 |
. . . . . . . . . . . . . . . . . . 19
| |
| 53 | 37, 46, 52 | syl2an 480 |
. . . . . . . . . . . . . . . . . 18
..^
|
| 54 | 53 | oveq1d 6305 |
. . . . . . . . . . . . . . . . 17
..^
|
| 55 | mulmod0 12104 |
. . . . . . . . . . . . . . . . . 18
| |
| 56 | 29, 32, 55 | syl2anr 481 |
. . . . . . . . . . . . . . . . 17
..^
|
| 57 | 54, 56 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
..^
|
| 58 | 57 | 3adant3 1028 |
. . . . . . . . . . . . . . 15
..^ ..^ |
| 59 | 58 | adantl 468 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 60 | 41 | adantr 467 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 61 | 43 | adantl 468 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 62 | 60, 61, 48 | mul32d 9843 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 63 | 62 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 64 | 29 | zred 11040 |
. . . . . . . . . . . . . . . . . 18
..^
|
| 65 | 64 | 3ad2ant2 1030 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
| 66 | remulcl 9624 |
. . . . . . . . . . . . . . . . 17
| |
| 67 | 25, 65, 66 | syl2an 480 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 68 | 9 | adantl 468 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 69 | modmulmod 12155 |
. . . . . . . . . . . . . . . 16
| |
| 70 | 67, 68, 34, 69 | syl3anc 1268 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 71 | 63, 70 | eqtr4d 2488 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 72 | 59, 71 | oveq12d 6308 |
. . . . . . . . . . . . 13
..^ ..^
|
| 73 | 72 | oveq1d 6305 |
. . . . . . . . . . . 12
..^ ..^
|
| 74 | remulcl 9624 |
. . . . . . . . . . . . . . . 16
| |
| 75 | 21, 64, 74 | syl2an 480 |
. . . . . . . . . . . . . . 15
..^
|
| 76 | 75 | 3adant3 1028 |
. . . . . . . . . . . . . 14
..^ ..^ |
| 77 | 76 | adantl 468 |
. . . . . . . . . . . . 13
..^ ..^
|
| 78 | 65 | adantl 468 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 79 | 27, 78 | remulcld 9671 |
. . . . . . . . . . . . 13
..^ ..^
|
| 80 | modsubmodmod 12149 |
. . . . . . . . . . . . 13
| |
| 81 | 77, 79, 34, 80 | syl3anc 1268 |
. . . . . . . . . . . 12
..^ ..^
|
| 82 | mulcom 9625 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 83 | 47, 40, 82 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^
|
| 84 | 83 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^
|
| 85 | 84 | eqeq1d 2453 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ 
|
| 86 | 85 | biimpd 211 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
| 87 | 86 | impancom 442 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
| 88 | 87 | imp 431 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 89 | 88 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 90 | 89 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 91 | 90 | oveq2d 6306 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 92 | 91 | oveq1d 6305 |
. . . . . . . . . . . . 13
..^ ..^
|
| 93 | 61 | mulid2d 9661 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 94 | 93 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 95 | 32, 18 | anim12ci 571 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 96 | elfzo2 11923 |
. . . . . . . . . . . . . . . . . . . . . 22
..^  
 | |
| 97 | eluz2 11165 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 | |
| 98 | 0red 9644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 99 | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 100 | zre 10941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 101 | 98, 99, 100 | 3jca 1188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 102 | 101 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 103 | 0le1 10137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 104 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 105 | 104 | anim1i 572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 106 | letr 9727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 107 | 102, 105, 106 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 108 | 107 | 3adant1 1026 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 109 | 97, 108 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 110 | 109 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 111 | simp3 1010 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 112 | 110, 111 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 113 | 96, 112 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
| 114 | 113 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 115 | 95, 114 | jca 535 |
. . . . . . . . . . . . . . . . . . 19
..^
|
| 116 | 115 | 3adant2 1027 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
| 117 | 116 | adantl 468 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
| 118 | modid 12121 |
. . . . . . . . . . . . . . . . 17
| |
| 119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
| 120 | 94, 119 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
..^ ..^
|
| 121 | 120 | oveq2d 6306 |
. . . . . . . . . . . . . 14
..^ ..^
|
| 122 | 121 | oveq1d 6305 |
. . . . . . . . . . . . 13
..^ ..^
|
| 123 | 92, 122 | eqtrd 2485 |
. . . . . . . . . . . 12
..^ ..^
|
| 124 | 73, 81, 123 | 3eqtr3d 2493 |
. . . . . . . . . . 11
..^ ..^
|
| 125 | 124 | oveq2d 6306 |
. . . . . . . . . 10
..^ ..^
|
| 126 | 125 | oveq1d 6305 |
. . . . . . . . 9
..^ ..^
|
| 127 | 77, 79 | resubcld 10047 |
. . . . . . . . . 10
..^ ..^
|
| 128 | modadd2mod 12140 |
. . . . . . . . . 10
| |
| 129 | 127, 20, 34, 128 | syl3anc 1268 |
. . . . . . . . 9
..^ ..^
|
| 130 | 0red 9644 |
. . . . . . . . . . . . . . . 16
..^
| |
| 131 | 130, 18 | resubcld 10047 |
. . . . . . . . . . . . . . 15
..^
|
| 132 | 131 | adantl 468 |
. . . . . . . . . . . . . 14
..^
|
| 133 | 18 | adantl 468 |
. . . . . . . . . . . . . 14
..^
|
| 134 | 32 | adantr 467 |
. . . . . . . . . . . . . 14
..^
|
| 135 | 132, 133, 134 | 3jca 1188 |
. . . . . . . . . . . . 13
..^
|
| 136 | 135 | 3adant2 1027 |
. . . . . . . . . . . 12
..^ ..^ |
| 137 | 136 | adantl 468 |
. . . . . . . . . . 11
..^ ..^
|
| 138 | modadd2mod 12140 |
. . . . . . . . . . 11
| |
| 139 | 137, 138 | syl 17 |
. . . . . . . . . 10
..^ ..^
|
| 140 | 0cnd 9636 |
. . . . . . . . . . . . . 14
..^
| |
| 141 | 42, 140 | pncan3d 9989 |
. . . . . . . . . . . . 13
..^
|
| 142 | 141 | 3ad2ant3 1031 |
. . . . . . . . . . . 12
..^ ..^ |
| 143 | 142 | adantl 468 |
. . . . . . . . . . 11
..^ ..^
|
| 144 | 143 | oveq1d 6305 |
. . . . . . . . . 10
..^ ..^
|
| 145 | 0mod 12128 |
. . . . . . . . . . . . 13
| |
| 146 | 32, 145 | syl 17 |
. . . . . . . . . . . 12
|
| 147 | 146 | 3ad2ant1 1029 |
. . . . . . . . . . 11
..^ ..^ |
| 148 | 147 | adantl 468 |
. . . . . . . . . 10
..^ ..^
|
| 149 | 139, 144, 148 | 3eqtrd 2489 |
. . . . . . . . 9
..^ ..^
|
| 150 | 126, 129, 149 | 3eqtr3d 2493 |
. . . . . . . 8
..^ ..^
|
| 151 | 36, 51, 150 | 3eqtrd 2489 |
. . . . . . 7
..^ ..^
|
| 152 | oveq1 6297 |
. . . . . . . . . . 11
| |
| 153 | 152 | oveq2d 6306 |
. . . . . . . . . 10
|
| 154 | 153 | oveq1d 6305 |
. . . . . . . . 9
|
| 155 | 154 | eqeq1d 2453 |
. . . . . . . 8
|
| 156 | 155 | rspcev 3150 |
. . . . . . 7
..^
..^ |
| 157 | 17, 151, 156 | syl2anc 667 |
. . . . . 6
..^ ..^
..^ |
| 158 | 157 | ex 436 |
. . . . 5
..^ ..^ ..^ |
| 159 | 158 | rexlimiva 2875 |
. . . 4
..^ ..^
..^ |
| 160 | 1, 2, 159 | 3syl 18 |
. . 3
..^
..^ ..^ ..^ |
| 161 | 160 | 3adant3 1028 |
. 2
..^ ..^
..^ ..^ ..^ |
| 162 | 161 | pm2.43i 49 |
1
..^ ..^ ..^ |
| Colors of variables: wff setvar class |
| Syntax hints: wi 4
wa 371
w3a 985
wceq 1444
wcel 1887
wrex 2738
wreu 2739
class class class wbr 4402 cfv 5582 (class class class)co 6290
cc 9537
cr 9538
cc0 9539
c1 9540
caddc 9542 cmul 9544 clt 9675 cle 9676 cmin 9860 cn 10609 cz 10937 cuz 11159 crp 11302 cfz 11784 ..^cfzo 11915
cmo 12096
cprime 14622 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617 |
| This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-er 7363 df-map 7474 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-sup 7956 df-inf 7957 df-card 8373 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-n0 10870 df-z 10938 df-uz 11160 df-rp 11303 df-fz 11785 df-fzo 11916 df-fl 12028 df-mod 12097 df-seq 12214 df-exp 12273 df-hash 12516 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-dvds 14306 df-gcd 14469 df-prm 14623 df-phi 14714 |
| This theorem is referenced by: nnnn0modprm0 14757 |
| Copyright terms: Public domain | W3C validator |