| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > mulpiord | GIF version | ||
| Description: Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) |
| Ref | Expression |
|---|---|
| mulpiord | ⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) = (𝐴 ·o 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | opelxpi 4707 | . 2 ⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → 〈𝐴, 𝐵〉 ∈ (N × N)) | |
| 2 | fvres 5600 | . . 3 ⊢ (〈𝐴, 𝐵〉 ∈ (N × N) → (( ·o ↾ (N × N))‘〈𝐴, 𝐵〉) = ( ·o ‘〈𝐴, 𝐵〉)) | |
| 3 | df-ov 5947 | . . . 4 ⊢ (𝐴 ·N 𝐵) = ( ·N ‘〈𝐴, 𝐵〉) | |
| 4 | df-mi 7419 | . . . . 5 ⊢ ·N = ( ·o ↾ (N × N)) | |
| 5 | 4 | fveq1i 5577 | . . . 4 ⊢ ( ·N ‘〈𝐴, 𝐵〉) = (( ·o ↾ (N × N))‘〈𝐴, 𝐵〉) |
| 6 | 3, 5 | eqtri 2226 | . . 3 ⊢ (𝐴 ·N 𝐵) = (( ·o ↾ (N × N))‘〈𝐴, 𝐵〉) |
| 7 | df-ov 5947 | . . 3 ⊢ (𝐴 ·o 𝐵) = ( ·o ‘〈𝐴, 𝐵〉) | |
| 8 | 2, 6, 7 | 3eqtr4g 2263 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (N × N) → (𝐴 ·N 𝐵) = (𝐴 ·o 𝐵)) |
| 9 | 1, 8 | syl 14 | 1 ⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) = (𝐴 ·o 𝐵)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ wa 104 = wceq 1373 ∈ wcel 2176 〈cop 3636 × cxp 4673 ↾ cres 4677 ‘cfv 5271 (class class class)co 5944 ·o comu 6500 Ncnpi 7385 ·N cmi 7387 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-14 2179 ax-ext 2187 ax-sep 4162 ax-pow 4218 ax-pr 4253 |
| This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ral 2489 df-rex 2490 df-v 2774 df-un 3170 df-in 3172 df-ss 3179 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-br 4045 df-opab 4106 df-xp 4681 df-res 4687 df-iota 5232 df-fv 5279 df-ov 5947 df-mi 7419 |
| This theorem is referenced by: mulidpi 7431 mulclpi 7441 mulcompig 7444 mulasspig 7445 distrpig 7446 mulcanpig 7448 ltmpig 7452 archnqq 7530 enq0enq 7544 addcmpblnq0 7556 mulcmpblnq0 7557 mulcanenq0ec 7558 addclnq0 7564 mulclnq0 7565 nqpnq0nq 7566 nqnq0a 7567 nqnq0m 7568 nq0m0r 7569 distrnq0 7572 addassnq0lemcl 7574 |
| Copyright terms: Public domain | W3C validator |