Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > moddvds | Unicode version |
Description: Two ways to say (mod ), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Ref | Expression |
---|---|
moddvds |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnq 9596 | . . . . . 6 | |
2 | 1 | adantr 274 | . . . . 5 |
3 | nngt0 8907 | . . . . . 6 | |
4 | 3 | adantr 274 | . . . . 5 |
5 | q0mod 10315 | . . . . 5 | |
6 | 2, 4, 5 | syl2anc 409 | . . . 4 |
7 | 6 | eqeq2d 2183 | . . 3 |
8 | zq 9589 | . . . . . . . . 9 | |
9 | 8 | ad2antrl 488 | . . . . . . . 8 |
10 | 9 | adantr 274 | . . . . . . 7 |
11 | zq 9589 | . . . . . . . . 9 | |
12 | 11 | ad2antll 489 | . . . . . . . 8 |
13 | 12 | adantr 274 | . . . . . . 7 |
14 | qnegcl 9599 | . . . . . . . 8 | |
15 | 13, 14 | syl 14 | . . . . . . 7 |
16 | 2 | adantr 274 | . . . . . . 7 |
17 | 4 | adantr 274 | . . . . . . 7 |
18 | simpr 109 | . . . . . . 7 | |
19 | 10, 13, 15, 16, 17, 18 | modqadd1 10321 | . . . . . 6 |
20 | 19 | ex 114 | . . . . 5 |
21 | simprl 527 | . . . . . . . . 9 | |
22 | 21 | zcnd 9339 | . . . . . . . 8 |
23 | simprr 528 | . . . . . . . . 9 | |
24 | 23 | zcnd 9339 | . . . . . . . 8 |
25 | 22, 24 | negsubd 8240 | . . . . . . 7 |
26 | 25 | oveq1d 5872 | . . . . . 6 |
27 | 24 | negidd 8224 | . . . . . . 7 |
28 | 27 | oveq1d 5872 | . . . . . 6 |
29 | 26, 28 | eqeq12d 2186 | . . . . 5 |
30 | 20, 29 | sylibd 148 | . . . 4 |
31 | 9 | adantr 274 | . . . . . . . 8 |
32 | 12 | adantr 274 | . . . . . . . 8 |
33 | qsubcl 9601 | . . . . . . . 8 | |
34 | 31, 32, 33 | syl2anc 409 | . . . . . . 7 |
35 | 0z 9227 | . . . . . . . 8 | |
36 | zq 9589 | . . . . . . . 8 | |
37 | 35, 36 | mp1i 10 | . . . . . . 7 |
38 | 2 | adantr 274 | . . . . . . 7 |
39 | 4 | adantr 274 | . . . . . . 7 |
40 | simpr 109 | . . . . . . 7 | |
41 | 34, 37, 32, 38, 39, 40 | modqadd1 10321 | . . . . . 6 |
42 | 41 | ex 114 | . . . . 5 |
43 | 22, 24 | npcand 8238 | . . . . . . 7 |
44 | 43 | oveq1d 5872 | . . . . . 6 |
45 | 24 | addid2d 8073 | . . . . . . 7 |
46 | 45 | oveq1d 5872 | . . . . . 6 |
47 | 44, 46 | eqeq12d 2186 | . . . . 5 |
48 | 42, 47 | sylibd 148 | . . . 4 |
49 | 30, 48 | impbid 128 | . . 3 |
50 | zsubcl 9257 | . . . 4 | |
51 | dvdsval3 11757 | . . . 4 | |
52 | 50, 51 | sylan2 284 | . . 3 |
53 | 7, 49, 52 | 3bitr4d 219 | . 2 |
54 | 53 | 3impb 1195 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 w3a 974 wceq 1349 wcel 2142 class class class wbr 3990 (class class class)co 5857 cc0 7778 caddc 7781 clt 7958 cmin 8094 cneg 8095 cn 8882 cz 9216 cq 9582 cmo 10282 cdvds 11753 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 610 ax-in2 611 ax-io 705 ax-5 1441 ax-7 1442 ax-gen 1443 ax-ie1 1487 ax-ie2 1488 ax-8 1498 ax-10 1499 ax-11 1500 ax-i12 1501 ax-bndl 1503 ax-4 1504 ax-17 1520 ax-i9 1524 ax-ial 1528 ax-i5r 1529 ax-13 2144 ax-14 2145 ax-ext 2153 ax-sep 4108 ax-pow 4161 ax-pr 4195 ax-un 4419 ax-setind 4522 ax-cnex 7869 ax-resscn 7870 ax-1cn 7871 ax-1re 7872 ax-icn 7873 ax-addcl 7874 ax-addrcl 7875 ax-mulcl 7876 ax-mulrcl 7877 ax-addcom 7878 ax-mulcom 7879 ax-addass 7880 ax-mulass 7881 ax-distr 7882 ax-i2m1 7883 ax-0lt1 7884 ax-1rid 7885 ax-0id 7886 ax-rnegex 7887 ax-precex 7888 ax-cnre 7889 ax-pre-ltirr 7890 ax-pre-ltwlin 7891 ax-pre-lttrn 7892 ax-pre-apti 7893 ax-pre-ltadd 7894 ax-pre-mulgt0 7895 ax-pre-mulext 7896 ax-arch 7897 |
This theorem depends on definitions: df-bi 116 df-3or 975 df-3an 976 df-tru 1352 df-fal 1355 df-nf 1455 df-sb 1757 df-eu 2023 df-mo 2024 df-clab 2158 df-cleq 2164 df-clel 2167 df-nfc 2302 df-ne 2342 df-nel 2437 df-ral 2454 df-rex 2455 df-reu 2456 df-rmo 2457 df-rab 2458 df-v 2733 df-sbc 2957 df-csb 3051 df-dif 3124 df-un 3126 df-in 3128 df-ss 3135 df-pw 3569 df-sn 3590 df-pr 3591 df-op 3593 df-uni 3798 df-int 3833 df-iun 3876 df-br 3991 df-opab 4052 df-mpt 4053 df-id 4279 df-po 4282 df-iso 4283 df-xp 4618 df-rel 4619 df-cnv 4620 df-co 4621 df-dm 4622 df-rn 4623 df-res 4624 df-ima 4625 df-iota 5162 df-fun 5202 df-fn 5203 df-f 5204 df-fv 5208 df-riota 5813 df-ov 5860 df-oprab 5861 df-mpo 5862 df-1st 6123 df-2nd 6124 df-pnf 7960 df-mnf 7961 df-xr 7962 df-ltxr 7963 df-le 7964 df-sub 8096 df-neg 8097 df-reap 8498 df-ap 8505 df-div 8594 df-inn 8883 df-n0 9140 df-z 9217 df-q 9583 df-rp 9615 df-fl 10230 df-mod 10283 df-dvds 11754 |
This theorem is referenced by: modm1div 11766 summodnegmod 11788 modmulconst 11789 addmodlteqALT 11823 dvdsmod 11826 congr 12058 cncongr1 12061 cncongr2 12062 crth 12182 eulerthlemh 12189 eulerthlemth 12190 prmdiv 12193 prmdiveq 12194 odzcllem 12200 odzdvds 12203 odzphi 12204 pockthlem 12312 lgslem1 13780 lgsmod 13806 lgsdirprm 13814 |
Copyright terms: Public domain | W3C validator |