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

Theorem nnmulcl 8127
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 5551 . . . . 5  |-  ( x  =  1  ->  ( A  x.  x )  =  ( A  x.  1 ) )
21eleq1d 2148 . . . 4  |-  ( x  =  1  ->  (
( A  x.  x
)  e.  NN  <->  ( A  x.  1 )  e.  NN ) )
32imbi2d 228 . . 3  |-  ( x  =  1  ->  (
( A  e.  NN  ->  ( A  x.  x
)  e.  NN )  <-> 
( A  e.  NN  ->  ( A  x.  1 )  e.  NN ) ) )
4 oveq2 5551 . . . . 5  |-  ( x  =  y  ->  ( A  x.  x )  =  ( A  x.  y ) )
54eleq1d 2148 . . . 4  |-  ( x  =  y  ->  (
( A  x.  x
)  e.  NN  <->  ( A  x.  y )  e.  NN ) )
65imbi2d 228 . . 3  |-  ( x  =  y  ->  (
( A  e.  NN  ->  ( A  x.  x
)  e.  NN )  <-> 
( A  e.  NN  ->  ( A  x.  y
)  e.  NN ) ) )
7 oveq2 5551 . . . . 5  |-  ( x  =  ( y  +  1 )  ->  ( A  x.  x )  =  ( A  x.  ( y  +  1 ) ) )
87eleq1d 2148 . . . 4  |-  ( x  =  ( y  +  1 )  ->  (
( A  x.  x
)  e.  NN  <->  ( A  x.  ( y  +  1 ) )  e.  NN ) )
98imbi2d 228 . . 3  |-  ( x  =  ( y  +  1 )  ->  (
( A  e.  NN  ->  ( A  x.  x
)  e.  NN )  <-> 
( A  e.  NN  ->  ( A  x.  (
y  +  1 ) )  e.  NN ) ) )
10 oveq2 5551 . . . . 5  |-  ( x  =  B  ->  ( A  x.  x )  =  ( A  x.  B ) )
1110eleq1d 2148 . . . 4  |-  ( x  =  B  ->  (
( A  x.  x
)  e.  NN  <->  ( A  x.  B )  e.  NN ) )
1211imbi2d 228 . . 3  |-  ( x  =  B  ->  (
( A  e.  NN  ->  ( A  x.  x
)  e.  NN )  <-> 
( A  e.  NN  ->  ( A  x.  B
)  e.  NN ) ) )
13 nncn 8114 . . . 4  |-  ( A  e.  NN  ->  A  e.  CC )
14 mulid1 7178 . . . . . 6  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )
1514eleq1d 2148 . . . . 5  |-  ( A  e.  CC  ->  (
( A  x.  1 )  e.  NN  <->  A  e.  NN ) )
1615biimprd 156 . . . 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 8126 . . . . . . . 8  |-  ( ( ( A  x.  y
)  e.  NN  /\  A  e.  NN )  ->  ( ( A  x.  y )  +  A
)  e.  NN )
1918ancoms 264 . . . . . . 7  |-  ( ( A  e.  NN  /\  ( A  x.  y
)  e.  NN )  ->  ( ( A  x.  y )  +  A )  e.  NN )
20 nncn 8114 . . . . . . . . 9  |-  ( y  e.  NN  ->  y  e.  CC )
21 ax-1cn 7131 . . . . . . . . . . 11  |-  1  e.  CC
22 adddi 7167 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  y  e.  CC  /\  1  e.  CC )  ->  ( A  x.  ( y  +  1 ) )  =  ( ( A  x.  y )  +  ( A  x.  1 ) ) )
2321, 22mp3an3 1258 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  y  e.  CC )  ->  ( A  x.  (
y  +  1 ) )  =  ( ( A  x.  y )  +  ( A  x.  1 ) ) )
2414oveq2d 5559 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
( A  x.  y
)  +  ( A  x.  1 ) )  =  ( ( A  x.  y )  +  A ) )
2524adantr 270 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  y  e.  CC )  ->  ( ( A  x.  y )  +  ( A  x.  1 ) )  =  ( ( A  x.  y )  +  A ) )
2623, 25eqtrd 2114 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  y  e.  CC )  ->  ( A  x.  (
y  +  1 ) )  =  ( ( A  x.  y )  +  A ) )
2713, 20, 26syl2an 283 . . . . . . . 8  |-  ( ( A  e.  NN  /\  y  e.  NN )  ->  ( A  x.  (
y  +  1 ) )  =  ( ( A  x.  y )  +  A ) )
2827eleq1d 2148 . . . . . . 7  |-  ( ( A  e.  NN  /\  y  e.  NN )  ->  ( ( A  x.  ( y  +  1 ) )  e.  NN  <->  ( ( A  x.  y
)  +  A )  e.  NN ) )
2919, 28syl5ibr 154 . . . . . 6  |-  ( ( A  e.  NN  /\  y  e.  NN )  ->  ( ( A  e.  NN  /\  ( A  x.  y )  e.  NN )  ->  ( A  x.  ( y  +  1 ) )  e.  NN ) )
3029exp4b 359 . . . . 5  |-  ( A  e.  NN  ->  (
y  e.  NN  ->  ( A  e.  NN  ->  ( ( A  x.  y
)  e.  NN  ->  ( A  x.  ( y  +  1 ) )  e.  NN ) ) ) )
3130pm2.43b 51 . . . 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 8122 . 2  |-  ( B  e.  NN  ->  ( A  e.  NN  ->  ( A  x.  B )  e.  NN ) )
3433impcom 123 1  |-  ( ( A  e.  NN  /\  B  e.  NN )  ->  ( A  x.  B
)  e.  NN )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    = wceq 1285    e. wcel 1434  (class class class)co 5543   CCcc 7041   1c1 7044    + caddc 7046    x. cmul 7048   NNcn 8106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3904  ax-cnex 7129  ax-resscn 7130  ax-1cn 7131  ax-1re 7132  ax-icn 7133  ax-addcl 7134  ax-addrcl 7135  ax-mulcl 7136  ax-mulcom 7139  ax-addass 7140  ax-mulass 7141  ax-distr 7142  ax-1rid 7145  ax-cnre 7149
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-rex 2355  df-rab 2358  df-v 2604  df-un 2978  df-in 2980  df-ss 2987  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-int 3645  df-br 3794  df-iota 4897  df-fv 4940  df-ov 5546  df-inn 8107
This theorem is referenced by:  nnmulcli  8128  nndivtr  8147  nnmulcld  8154  nn0mulcl  8391  qaddcl  8801  qmulcl  8803  modqmulnn  9424  nnexpcl  9586  nnsqcl  9642  faccl  9759  facdiv  9762  faclbnd3  9767  bcrpcl  9777  lcmgcdlem  10603  lcmgcdnn  10608
  Copyright terms: Public domain W3C validator