![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mulscld | Structured version Visualization version GIF version |
Description: The surreals are closed under multiplication. Theorem 8(i) of [Conway] p. 19. (Contributed by Scott Fenton, 6-Mar-2025.) |
Ref | Expression |
---|---|
mulscld.1 | ⊢ (𝜑 → 𝐴 ∈ No ) |
mulscld.2 | ⊢ (𝜑 → 𝐵 ∈ No ) |
Ref | Expression |
---|---|
mulscld | ⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ No ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mulscld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ No ) | |
2 | mulscld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ No ) | |
3 | mulscl 27519 | . 2 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ·s 𝐵) ∈ No ) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ No ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 (class class class)co 7394 No csur 27072 ·s cmuls 27491 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5357 ax-pr 5421 ax-un 7709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3964 df-nul 4320 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-ot 4632 df-uni 4903 df-int 4945 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5568 df-eprel 5574 df-po 5582 df-so 5583 df-fr 5625 df-se 5626 df-we 5627 df-xp 5676 df-rel 5677 df-cnv 5678 df-co 5679 df-dm 5680 df-rn 5681 df-res 5682 df-ima 5683 df-pred 6290 df-ord 6357 df-on 6358 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7350 df-ov 7397 df-oprab 7398 df-mpo 7399 df-1st 7959 df-2nd 7960 df-frecs 8250 df-wrecs 8281 df-recs 8355 df-1o 8450 df-2o 8451 df-nadd 8650 df-no 27075 df-slt 27076 df-bday 27077 df-sle 27177 df-sslt 27212 df-scut 27214 df-0s 27254 df-made 27271 df-old 27272 df-left 27274 df-right 27275 df-norec 27351 df-norec2 27362 df-adds 27373 df-negs 27425 df-subs 27426 df-muls 27492 |
This theorem is referenced by: slemuld 27523 mulscom 27524 ssltmul1 27531 ssltmul2 27532 mulsuniflem 27533 addsdilem3 27537 addsdilem4 27538 subsdid 27542 mulnegs1d 27544 mul2negsd 27546 mulsasslem3 27549 sltmul2 27552 slemul2d 27555 slemul1d 27556 sltmulneg1d 27557 mulscan2dlem 27559 mulscan2d 27560 norecdiv 27567 divsasswd 27579 precsexlem8 27589 precsexlem9 27590 precsexlem10 27591 precsexlem11 27592 |
Copyright terms: Public domain | W3C validator |