![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nnmulcld | GIF version |
Description: Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nnge1d.1 | ⊢ (𝜑 → 𝐴 ∈ ℕ) |
nnmulcld.2 | ⊢ (𝜑 → 𝐵 ∈ ℕ) |
Ref | Expression |
---|---|
nnmulcld | ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnge1d.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℕ) | |
2 | nnmulcld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℕ) | |
3 | nnmulcl 8541 | . 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ) | |
4 | 1, 2, 3 | syl2anc 404 | 1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1445 (class class class)co 5690 · cmul 7452 ℕcn 8520 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 ax-cnex 7533 ax-resscn 7534 ax-1cn 7535 ax-1re 7536 ax-icn 7537 ax-addcl 7538 ax-addrcl 7539 ax-mulcl 7540 ax-mulcom 7543 ax-addass 7544 ax-mulass 7545 ax-distr 7546 ax-1rid 7549 ax-cnre 7553 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ral 2375 df-rex 2376 df-rab 2379 df-v 2635 df-un 3017 df-in 3019 df-ss 3026 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-int 3711 df-br 3868 df-iota 5014 df-fv 5057 df-ov 5693 df-inn 8521 |
This theorem is referenced by: qbtwnre 9817 bcval 10272 bcm1k 10283 bcp1n 10284 permnn 10294 cvg1nlemcxze 10530 cvg1nlemf 10531 cvg1nlemcau 10532 cvg1nlemres 10533 trireciplem 11043 efaddlem 11113 eftlub 11129 eirraplem 11213 modmulconst 11255 lcmval 11472 oddpwdclemxy 11574 oddpwdclemdc 11578 sqpweven 11580 2sqpwodd 11581 crth 11627 phimullem 11628 evenennn 11633 |
Copyright terms: Public domain | W3C validator |