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

Theorem mulpiord 6855
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 4459 . 2  |-  ( ( A  e.  N.  /\  B  e.  N. )  -> 
<. A ,  B >.  e.  ( N.  X.  N. ) )
2 fvres 5313 . . 3  |-  ( <. A ,  B >.  e.  ( N.  X.  N. )  ->  ( (  .o  |`  ( N.  X.  N. ) ) `  <. A ,  B >. )  =  (  .o  `  <. A ,  B >. )
)
3 df-ov 5637 . . . 4  |-  ( A  .N  B )  =  (  .N  `  <. A ,  B >. )
4 df-mi 6844 . . . . 5  |-  .N  =  (  .o  |`  ( N.  X.  N. ) )
54fveq1i 5290 . . . 4  |-  (  .N 
`  <. A ,  B >. )  =  ( (  .o  |`  ( N.  X.  N. ) ) `  <. A ,  B >. )
63, 5eqtri 2108 . . 3  |-  ( A  .N  B )  =  ( (  .o  |`  ( N.  X.  N. ) ) `
 <. A ,  B >. )
7 df-ov 5637 . . 3  |-  ( A  .o  B )  =  (  .o  `  <. A ,  B >. )
82, 6, 73eqtr4g 2145 . 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 102    = wceq 1289    e. wcel 1438   <.cop 3444    X. cxp 4426    |` cres 4430   ` cfv 5002  (class class class)co 5634    .o comu 6161   N.cnpi 6810    .N cmi 6812
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 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-pow 4001  ax-pr 4027
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-opab 3892  df-xp 4434  df-res 4440  df-iota 4967  df-fv 5010  df-ov 5637  df-mi 6844
This theorem is referenced by:  mulidpi  6856  mulclpi  6866  mulcompig  6869  mulasspig  6870  distrpig  6871  mulcanpig  6873  ltmpig  6877  archnqq  6955  enq0enq  6969  addcmpblnq0  6981  mulcmpblnq0  6982  mulcanenq0ec  6983  addclnq0  6989  mulclnq0  6990  nqpnq0nq  6991  nqnq0a  6992  nqnq0m  6993  nq0m0r  6994  distrnq0  6997  addassnq0lemcl  6999
  Copyright terms: Public domain W3C validator