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

Theorem mulpiord 6163
Description: Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.)
Assertion
Ref Expression
mulpiord ((A N B N) → (A ·N B) = (A ·𝑜 B))

Proof of Theorem mulpiord
StepHypRef Expression
1 opelxpi 4291 . 2 ((A N B N) → ⟨A, B (N × N))
2 fvres 5111 . . 3 (⟨A, B (N × N) → (( ·𝑜 ↾ (N × N))‘⟨A, B⟩) = ( ·𝑜 ‘⟨A, B⟩))
3 df-ov 5427 . . . 4 (A ·N B) = ( ·N ‘⟨A, B⟩)
4 df-mi 6152 . . . . 5 ·N = ( ·𝑜 ↾ (N × N))
54fveq1i 5092 . . . 4 ( ·N ‘⟨A, B⟩) = (( ·𝑜 ↾ (N × N))‘⟨A, B⟩)
63, 5eqtri 2033 . . 3 (A ·N B) = (( ·𝑜 ↾ (N × N))‘⟨A, B⟩)
7 df-ov 5427 . . 3 (A ·𝑜 B) = ( ·𝑜 ‘⟨A, B⟩)
82, 6, 73eqtr4g 2070 . 2 (⟨A, B (N × N) → (A ·N B) = (A ·𝑜 B))
91, 8syl 14 1 ((A N B N) → (A ·N B) = (A ·𝑜 B))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   = wceq 1223   wcel 1366  cop 3342   × cxp 4258  cres 4262  cfv 4817  (class class class)co 5424   ·𝑜 comu 5902  Ncnpi 6118   ·N cmi 6120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-14 1378  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995  ax-sep 3838  ax-pow 3890  ax-pr 3907
This theorem depends on definitions:  df-bi 110  df-3an 869  df-tru 1226  df-nf 1323  df-sb 1619  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-ral 2280  df-rex 2281  df-v 2528  df-un 2890  df-in 2892  df-ss 2899  df-pw 3325  df-sn 3345  df-pr 3346  df-op 3348  df-uni 3544  df-br 3728  df-opab 3782  df-xp 4266  df-res 4272  df-iota 4782  df-fv 4825  df-ov 5427  df-mi 6152
This theorem is referenced by:  mulidpi  6164  mulclpi  6174  mulcompig  6177  mulasspig  6178  distrpig  6179  mulcanpig  6181  ltmpig  6185  archnqq  6260  enq0enq  6272  addcmpblnq0  6284  mulcmpblnq0  6285  mulcanenq0ec  6286  addclnq0  6292  mulclnq0  6293  nqpnq0nq  6294  nqnq0a  6295  nqnq0m  6296  nq0m0r  6297  distrnq0  6300  addassnq0lemcl  6302
  Copyright terms: Public domain W3C validator