ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nnmulcl Unicode version

Theorem nnmulcl 8764
Description: Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.)
Assertion
Ref Expression
nnmulcl  |-  ( ( A  e.  NN  /\  B  e.  NN )  ->  ( A  x.  B
)  e.  NN )

Proof of Theorem nnmulcl
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 5789 . . . . 5  |-  ( x  =  1  ->  ( A  x.  x )  =  ( A  x.  1 ) )
21eleq1d 2209 . . . 4  |-  ( x  =  1  ->  (
( A  x.  x
)  e.  NN  <->  ( A  x.  1 )  e.  NN ) )
32imbi2d 229 . . 3  |-  ( x  =  1  ->  (
( A  e.  NN  ->  ( A  x.  x
)  e.  NN )  <-> 
( A  e.  NN  ->  ( A  x.  1 )  e.  NN ) ) )
4 oveq2 5789 . . . . 5  |-  ( x  =  y  ->  ( A  x.  x )  =  ( A  x.  y ) )
54eleq1d 2209 . . . 4  |-  ( x  =  y  ->  (
( A  x.  x
)  e.  NN  <->  ( A  x.  y )  e.  NN ) )
65imbi2d 229 . . 3  |-  ( x  =  y  ->  (
( A  e.  NN  ->  ( A  x.  x
)  e.  NN )  <-> 
( A  e.  NN  ->  ( A  x.  y
)  e.  NN ) ) )
7 oveq2 5789 . . . . 5  |-  ( x  =  ( y  +  1 )  ->  ( A  x.  x )  =  ( A  x.  ( y  +  1 ) ) )
87eleq1d 2209 . . . 4  |-  ( x  =  ( y  +  1 )  ->  (
( A  x.  x
)  e.  NN  <->  ( A  x.  ( y  +  1 ) )  e.  NN ) )
98imbi2d 229 . . 3  |-  ( x  =  ( y  +  1 )  ->  (
( A  e.  NN  ->  ( A  x.  x
)  e.  NN )  <-> 
( A  e.  NN  ->  ( A  x.  (
y  +  1 ) )  e.  NN ) ) )
10 oveq2 5789 . . . . 5  |-  ( x  =  B  ->  ( A  x.  x )  =  ( A  x.  B ) )
1110eleq1d 2209 . . . 4  |-  ( x  =  B  ->  (
( A  x.  x
)  e.  NN  <->  ( A  x.  B )  e.  NN ) )
1211imbi2d 229 . . 3  |-  ( x  =  B  ->  (
( A  e.  NN  ->  ( A  x.  x
)  e.  NN )  <-> 
( A  e.  NN  ->  ( A  x.  B
)  e.  NN ) ) )
13 nncn 8751 . . . 4  |-  ( A  e.  NN  ->  A  e.  CC )
14 mulid1 7786 . . . . . 6  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )
1514eleq1d 2209 . . . . 5  |-  ( A  e.  CC  ->  (
( A  x.  1 )  e.  NN  <->  A  e.  NN ) )
1615biimprd 157 . . . 4  |-  ( A  e.  CC  ->  ( A  e.  NN  ->  ( A  x.  1 )  e.  NN ) )
1713, 16mpcom 36 . . 3  |-  ( A  e.  NN  ->  ( A  x.  1 )  e.  NN )
18 nnaddcl 8763 . . . . . . . 8  |-  ( ( ( A  x.  y
)  e.  NN  /\  A  e.  NN )  ->  ( ( A  x.  y )  +  A
)  e.  NN )
1918ancoms 266 . . . . . . 7  |-  ( ( A  e.  NN  /\  ( A  x.  y
)  e.  NN )  ->  ( ( A  x.  y )  +  A )  e.  NN )
20 nncn 8751 . . . . . . . . 9  |-  ( y  e.  NN  ->  y  e.  CC )
21 ax-1cn 7736 . . . . . . . . . . 11  |-  1  e.  CC
22 adddi 7775 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  y  e.  CC  /\  1  e.  CC )  ->  ( A  x.  ( y  +  1 ) )  =  ( ( A  x.  y )  +  ( A  x.  1 ) ) )
2321, 22mp3an3 1305 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  y  e.  CC )  ->  ( A  x.  (
y  +  1 ) )  =  ( ( A  x.  y )  +  ( A  x.  1 ) ) )
2414oveq2d 5797 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
( A  x.  y
)  +  ( A  x.  1 ) )  =  ( ( A  x.  y )  +  A ) )
2524adantr 274 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  y  e.  CC )  ->  ( ( A  x.  y )  +  ( A  x.  1 ) )  =  ( ( A  x.  y )  +  A ) )
2623, 25eqtrd 2173 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  y  e.  CC )  ->  ( A  x.  (
y  +  1 ) )  =  ( ( A  x.  y )  +  A ) )
2713, 20, 26syl2an 287 . . . . . . . 8  |-  ( ( A  e.  NN  /\  y  e.  NN )  ->  ( A  x.  (
y  +  1 ) )  =  ( ( A  x.  y )  +  A ) )
2827eleq1d 2209 . . . . . . 7  |-  ( ( A  e.  NN  /\  y  e.  NN )  ->  ( ( A  x.  ( y  +  1 ) )  e.  NN  <->  ( ( A  x.  y
)  +  A )  e.  NN ) )
2919, 28syl5ibr 155 . . . . . 6  |-  ( ( A  e.  NN  /\  y  e.  NN )  ->  ( ( A  e.  NN  /\  ( A  x.  y )  e.  NN )  ->  ( A  x.  ( y  +  1 ) )  e.  NN ) )
3029exp4b 365 . . . . 5  |-  ( A  e.  NN  ->  (
y  e.  NN  ->  ( A  e.  NN  ->  ( ( A  x.  y
)  e.  NN  ->  ( A  x.  ( y  +  1 ) )  e.  NN ) ) ) )
3130pm2.43b 52 . . . 4  |-  ( y  e.  NN  ->  ( A  e.  NN  ->  ( ( A  x.  y
)  e.  NN  ->  ( A  x.  ( y  +  1 ) )  e.  NN ) ) )
3231a2d 26 . . 3  |-  ( y  e.  NN  ->  (
( A  e.  NN  ->  ( A  x.  y
)  e.  NN )  ->  ( A  e.  NN  ->  ( A  x.  ( y  +  1 ) )  e.  NN ) ) )
333, 6, 9, 12, 17, 32nnind 8759 . 2  |-  ( B  e.  NN  ->  ( A  e.  NN  ->  ( A  x.  B )  e.  NN ) )
3433impcom 124 1  |-  ( ( A  e.  NN  /\  B  e.  NN )  ->  ( A  x.  B
)  e.  NN )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1332    e. wcel 1481  (class class class)co 5781   CCcc 7641   1c1 7644    + caddc 7646    x. cmul 7648   NNcn 8743
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-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053  ax-cnex 7734  ax-resscn 7735  ax-1cn 7736  ax-1re 7737  ax-icn 7738  ax-addcl 7739  ax-addrcl 7740  ax-mulcl 7741  ax-mulcom 7744  ax-addass 7745  ax-mulass 7746  ax-distr 7747  ax-1rid 7750  ax-cnre 7754
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2691  df-un 3079  df-in 3081  df-ss 3088  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-int 3779  df-br 3937  df-iota 5095  df-fv 5138  df-ov 5784  df-inn 8744
This theorem is referenced by:  nnmulcli  8765  nndivtr  8785  nnmulcld  8792  nn0mulcl  9036  qaddcl  9453  qmulcl  9455  modqmulnn  10145  nnexpcl  10336  nnsqcl  10392  faccl  10512  facdiv  10515  faclbnd3  10520  bcrpcl  10530  trirecip  11301  lcmgcdlem  11792  lcmgcdnn  11797
  Copyright terms: Public domain W3C validator