Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pcmul | Unicode version |
Description: Multiplication property of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
Ref | Expression |
---|---|
pcmul |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2171 | . . 3 | |
2 | eqid 2171 | . . 3 | |
3 | eqid 2171 | . . 3 | |
4 | 1, 2, 3 | pcpremul 12251 | . 2 |
5 | 1 | pczpre 12255 | . . . 4 |
6 | 5 | 3adant3 1013 | . . 3 |
7 | 2 | pczpre 12255 | . . . 4 |
8 | 7 | 3adant2 1012 | . . 3 |
9 | 6, 8 | oveq12d 5875 | . 2 |
10 | zmulcl 9269 | . . . . . 6 | |
11 | 10 | ad2ant2r 507 | . . . . 5 |
12 | zcn 9221 | . . . . . . . 8 | |
13 | 12 | ad2antrr 486 | . . . . . . 7 |
14 | zcn 9221 | . . . . . . . 8 | |
15 | 14 | ad2antrl 488 | . . . . . . 7 |
16 | simplr 526 | . . . . . . . 8 | |
17 | simpll 525 | . . . . . . . . 9 | |
18 | 0zd 9228 | . . . . . . . . 9 | |
19 | zapne 9290 | . . . . . . . . 9 # | |
20 | 17, 18, 19 | syl2anc 409 | . . . . . . . 8 # |
21 | 16, 20 | mpbird 166 | . . . . . . 7 # |
22 | simprr 528 | . . . . . . . 8 | |
23 | simprl 527 | . . . . . . . . 9 | |
24 | zapne 9290 | . . . . . . . . 9 # | |
25 | 23, 18, 24 | syl2anc 409 | . . . . . . . 8 # |
26 | 22, 25 | mpbird 166 | . . . . . . 7 # |
27 | 13, 15, 21, 26 | mulap0d 8580 | . . . . . 6 # |
28 | zapne 9290 | . . . . . . 7 # | |
29 | 11, 18, 28 | syl2anc 409 | . . . . . 6 # |
30 | 27, 29 | mpbid 146 | . . . . 5 |
31 | 11, 30 | jca 304 | . . . 4 |
32 | 3 | pczpre 12255 | . . . 4 |
33 | 31, 32 | sylan2 284 | . . 3 |
34 | 33 | 3impb 1195 | . 2 |
35 | 4, 9, 34 | 3eqtr4rd 2215 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 w3a 974 wceq 1349 wcel 2142 wne 2341 crab 2453 class class class wbr 3990 (class class class)co 5857 csup 6963 cc 7776 cr 7777 cc0 7778 caddc 7781 cmul 7783 clt 7958 # cap 8504 cn0 9139 cz 9216 cexp 10479 cdvds 11753 cprime 12065 cpc 12242 |
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-coll 4105 ax-sep 4108 ax-nul 4116 ax-pow 4161 ax-pr 4195 ax-un 4419 ax-setind 4522 ax-iinf 4573 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 ax-caucvg 7898 |
This theorem depends on definitions: df-bi 116 df-dc 831 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-nul 3416 df-if 3528 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-tr 4089 df-id 4279 df-po 4282 df-iso 4283 df-iord 4352 df-on 4354 df-ilim 4355 df-suc 4357 df-iom 4576 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-f1 5205 df-fo 5206 df-f1o 5207 df-fv 5208 df-isom 5209 df-riota 5813 df-ov 5860 df-oprab 5861 df-mpo 5862 df-1st 6123 df-2nd 6124 df-recs 6288 df-frec 6374 df-1o 6399 df-2o 6400 df-er 6517 df-en 6723 df-sup 6965 df-inf 6966 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-2 8941 df-3 8942 df-4 8943 df-n0 9140 df-z 9217 df-uz 9492 df-q 9583 df-rp 9615 df-fz 9970 df-fzo 10103 df-fl 10230 df-mod 10283 df-seqfrec 10406 df-exp 10480 df-cj 10810 df-re 10811 df-im 10812 df-rsqrt 10966 df-abs 10967 df-dvds 11754 df-gcd 11902 df-prm 12066 df-pc 12243 |
This theorem is referenced by: pcqmul 12261 pcaddlem 12296 pcmpt 12299 pcfac 12306 pcbc 12307 lgsdi 13817 |
Copyright terms: Public domain | W3C validator |