| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > mulclpi | Unicode version | ||
| Description: Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.) |
| Ref | Expression |
|---|---|
| mulclpi |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mulpiord 7412 |
. 2
| |
| 2 | pinn 7404 |
. . . 4
| |
| 3 | pinn 7404 |
. . . 4
| |
| 4 | nnmcl 6557 |
. . . 4
| |
| 5 | 2, 3, 4 | syl2an 289 |
. . 3
|
| 6 | elni2 7409 |
. . . . . . 7
| |
| 7 | 6 | simprbi 275 |
. . . . . 6
|
| 8 | 7 | adantl 277 |
. . . . 5
|
| 9 | 3 | adantl 277 |
. . . . . 6
|
| 10 | 2 | adantr 276 |
. . . . . 6
|
| 11 | elni2 7409 |
. . . . . . . 8
| |
| 12 | 11 | simprbi 275 |
. . . . . . 7
|
| 13 | 12 | adantr 276 |
. . . . . 6
|
| 14 | nnmordi 6592 |
. . . . . 6
| |
| 15 | 9, 10, 13, 14 | syl21anc 1248 |
. . . . 5
|
| 16 | 8, 15 | mpd 13 |
. . . 4
|
| 17 | ne0i 3466 |
. . . 4
| |
| 18 | 16, 17 | syl 14 |
. . 3
|
| 19 | elni 7403 |
. . 3
| |
| 20 | 5, 18, 19 | sylanbrc 417 |
. 2
|
| 21 | 1, 20 | eqeltrd 2281 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-coll 4158 ax-sep 4161 ax-nul 4169 ax-pow 4217 ax-pr 4252 ax-un 4478 ax-setind 4583 ax-iinf 4634 |
| This theorem depends on definitions: df-bi 117 df-dc 836 df-3an 982 df-tru 1375 df-fal 1378 df-nf 1483 df-sb 1785 df-eu 2056 df-mo 2057 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ne 2376 df-ral 2488 df-rex 2489 df-reu 2490 df-rab 2492 df-v 2773 df-sbc 2998 df-csb 3093 df-dif 3167 df-un 3169 df-in 3171 df-ss 3178 df-nul 3460 df-pw 3617 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-int 3885 df-iun 3928 df-br 4044 df-opab 4105 df-mpt 4106 df-tr 4142 df-id 4338 df-iord 4411 df-on 4413 df-suc 4416 df-iom 4637 df-xp 4679 df-rel 4680 df-cnv 4681 df-co 4682 df-dm 4683 df-rn 4684 df-res 4685 df-ima 4686 df-iota 5229 df-fun 5270 df-fn 5271 df-f 5272 df-f1 5273 df-fo 5274 df-f1o 5275 df-fv 5276 df-ov 5937 df-oprab 5938 df-mpo 5939 df-1st 6216 df-2nd 6217 df-recs 6381 df-irdg 6446 df-oadd 6496 df-omul 6497 df-ni 7399 df-mi 7401 |
| This theorem is referenced by: mulasspig 7427 distrpig 7428 ltmpig 7434 enqer 7453 enqdc 7456 addcmpblnq 7462 mulcmpblnq 7463 addpipqqslem 7464 mulpipq2 7466 mulpipqqs 7468 ordpipqqs 7469 addclnq 7470 mulclnq 7471 addcomnqg 7476 addassnqg 7477 mulassnqg 7479 mulcanenq 7480 distrnqg 7482 recexnq 7485 nqtri3or 7491 ltdcnq 7492 ltsonq 7493 ltanqg 7495 ltmnqg 7496 1lt2nq 7501 ltexnqq 7503 archnqq 7512 addcmpblnq0 7538 mulcmpblnq0 7539 mulcanenq0ec 7540 addclnq0 7546 mulclnq0 7547 nqpnq0nq 7548 nqnq0a 7549 nqnq0m 7550 nq0m0r 7551 distrnq0 7554 addassnq0lemcl 7556 |
| Copyright terms: Public domain | W3C validator |