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

Theorem mulpiord 7089
Description: Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.)
Assertion
Ref Expression
mulpiord  |-  ( ( A  e.  N.  /\  B  e.  N. )  ->  ( A  .N  B
)  =  ( A  .o  B ) )

Proof of Theorem mulpiord
StepHypRef Expression
1 opelxpi 4539 . 2  |-  ( ( A  e.  N.  /\  B  e.  N. )  -> 
<. A ,  B >.  e.  ( N.  X.  N. ) )
2 fvres 5411 . . 3  |-  ( <. A ,  B >.  e.  ( N.  X.  N. )  ->  ( (  .o  |`  ( N.  X.  N. ) ) `  <. A ,  B >. )  =  (  .o  `  <. A ,  B >. )
)
3 df-ov 5743 . . . 4  |-  ( A  .N  B )  =  (  .N  `  <. A ,  B >. )
4 df-mi 7078 . . . . 5  |-  .N  =  (  .o  |`  ( N.  X.  N. ) )
54fveq1i 5388 . . . 4  |-  (  .N 
`  <. A ,  B >. )  =  ( (  .o  |`  ( N.  X.  N. ) ) `  <. A ,  B >. )
63, 5eqtri 2136 . . 3  |-  ( A  .N  B )  =  ( (  .o  |`  ( N.  X.  N. ) ) `
 <. A ,  B >. )
7 df-ov 5743 . . 3  |-  ( A  .o  B )  =  (  .o  `  <. A ,  B >. )
82, 6, 73eqtr4g 2173 . 2  |-  ( <. A ,  B >.  e.  ( N.  X.  N. )  ->  ( A  .N  B )  =  ( A  .o  B ) )
91, 8syl 14 1  |-  ( ( A  e.  N.  /\  B  e.  N. )  ->  ( A  .N  B
)  =  ( A  .o  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1314    e. wcel 1463   <.cop 3498    X. cxp 4505    |` cres 4509   ` cfv 5091  (class class class)co 5740    .o comu 6277   N.cnpi 7044    .N cmi 7046
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-rex 2397  df-v 2660  df-un 3043  df-in 3045  df-ss 3052  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-br 3898  df-opab 3958  df-xp 4513  df-res 4519  df-iota 5056  df-fv 5099  df-ov 5743  df-mi 7078
This theorem is referenced by:  mulidpi  7090  mulclpi  7100  mulcompig  7103  mulasspig  7104  distrpig  7105  mulcanpig  7107  ltmpig  7111  archnqq  7189  enq0enq  7203  addcmpblnq0  7215  mulcmpblnq0  7216  mulcanenq0ec  7217  addclnq0  7223  mulclnq0  7224  nqpnq0nq  7225  nqnq0a  7226  nqnq0m  7227  nq0m0r  7228  distrnq0  7231  addassnq0lemcl  7233
  Copyright terms: Public domain W3C validator