| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > nnmulcl | Unicode version | ||
| Description: Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.) |
| Ref | Expression |
|---|---|
| nnmulcl |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | oveq2 5952 |
. . . . 5
| |
| 2 | 1 | eleq1d 2274 |
. . . 4
|
| 3 | 2 | imbi2d 230 |
. . 3
|
| 4 | oveq2 5952 |
. . . . 5
| |
| 5 | 4 | eleq1d 2274 |
. . . 4
|
| 6 | 5 | imbi2d 230 |
. . 3
|
| 7 | oveq2 5952 |
. . . . 5
| |
| 8 | 7 | eleq1d 2274 |
. . . 4
|
| 9 | 8 | imbi2d 230 |
. . 3
|
| 10 | oveq2 5952 |
. . . . 5
| |
| 11 | 10 | eleq1d 2274 |
. . . 4
|
| 12 | 11 | imbi2d 230 |
. . 3
|
| 13 | nncn 9044 |
. . . 4
| |
| 14 | mulrid 8069 |
. . . . . 6
| |
| 15 | 14 | eleq1d 2274 |
. . . . 5
|
| 16 | 15 | biimprd 158 |
. . . 4
|
| 17 | 13, 16 | mpcom 36 |
. . 3
|
| 18 | nnaddcl 9056 |
. . . . . . . 8
| |
| 19 | 18 | ancoms 268 |
. . . . . . 7
|
| 20 | nncn 9044 |
. . . . . . . . 9
| |
| 21 | ax-1cn 8018 |
. . . . . . . . . . 11
| |
| 22 | adddi 8057 |
. . . . . . . . . . 11
| |
| 23 | 21, 22 | mp3an3 1339 |
. . . . . . . . . 10
|
| 24 | 14 | oveq2d 5960 |
. . . . . . . . . . 11
|
| 25 | 24 | adantr 276 |
. . . . . . . . . 10
|
| 26 | 23, 25 | eqtrd 2238 |
. . . . . . . . 9
|
| 27 | 13, 20, 26 | syl2an 289 |
. . . . . . . 8
|
| 28 | 27 | eleq1d 2274 |
. . . . . . 7
|
| 29 | 19, 28 | imbitrrid 156 |
. . . . . 6
|
| 30 | 29 | exp4b 367 |
. . . . 5
|
| 31 | 30 | pm2.43b 52 |
. . . 4
|
| 32 | 31 | a2d 26 |
. . 3
|
| 33 | 3, 6, 9, 12, 17, 32 | nnind 9052 |
. 2
|
| 34 | 33 | impcom 125 |
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-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 ax-sep 4162 ax-cnex 8016 ax-resscn 8017 ax-1cn 8018 ax-1re 8019 ax-icn 8020 ax-addcl 8021 ax-addrcl 8022 ax-mulcl 8023 ax-mulcom 8026 ax-addass 8027 ax-mulass 8028 ax-distr 8029 ax-1rid 8032 ax-cnre 8036 |
| This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ral 2489 df-rex 2490 df-rab 2493 df-v 2774 df-un 3170 df-in 3172 df-ss 3179 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-int 3886 df-br 4045 df-iota 5232 df-fv 5279 df-ov 5947 df-inn 9037 |
| This theorem is referenced by: nnmulcli 9058 nndivtr 9078 nnmulcld 9085 nn0mulcl 9331 qaddcl 9756 qmulcl 9758 modqmulnn 10487 nnexpcl 10697 nnsqcl 10754 faccl 10880 facdiv 10883 faclbnd3 10888 bcrpcl 10898 trirecip 11812 fprodnncl 11921 lcmgcdlem 12399 lcmgcdnn 12404 pcmptcl 12665 pcmpt 12666 4sqlem12 12725 mulgnnass 13493 lgseisenlem1 15547 lgseisenlem2 15548 lgseisenlem3 15549 lgseisenlem4 15550 lgsquadlem1 15554 lgsquadlem2 15555 |
| Copyright terms: Public domain | W3C validator |