Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2099 ∅c0 4318
𝒫 cpw 4598 class class class wbr 5142
(class class class)co 7414
No csur 27566 <<s csslt 27706 |s cscut 27708 0s
c0s 27748 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906
ax-6 1964 ax-7 2004 ax-8 2101
ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pr 5423 ax-un 7734 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2937 df-ral 3058 df-rex 3067 df-rmo 3372 df-reu 3373 df-rab 3429 df-v 3472 df-sbc 3776 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3964 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-tp 4629 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-ord 6366 df-on 6367 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-1o 8480 df-2o 8481 df-no 27569 df-slt 27570 df-bday 27571 df-sslt 27707 df-scut 27709 df-0s 27750 |
This theorem is referenced by: 1sno
27753 0slt1s
27755 bday1s
27757 cuteq0
27758 cuteq1
27759 sgt0ne0
27760 made0
27793 right1s
27815 0elold
27828 addsrid
27874 addslid
27878 addsproplem2
27880 addsfo
27893 sltaddpos1d
27921 sltaddpos2d
27922 addsgt0d
27924 negs0s
27932 negsproplem2
27934 negsproplem6
27938 negscl
27941 negsid
27946 negsdi
27955 slt0neg2d
27956 negsval2
27967 subsid1
27969 posdifsd
27997 sltsubposd
27998 muls01
28005 mulsrid
28006 mulsproplem2
28010 mulsproplem3
28011 mulsproplem4
28012 mulsproplem5
28013 mulsproplem6
28014 mulsproplem7
28015 mulsproplem8
28016 mulscl
28027 sltmul
28029 slemuld
28031 muls02
28034 mulsgt0
28037 mulsge0d
28039 sltmulneg1d
28069 mulscan2d
28072 slemul1ad
28075 sltmul12ad
28076 muls0ord
28078 precsexlem8
28105 precsexlem9
28106 precsexlem11
28108 recsex
28110 abs0s
28129 abssnid
28130 absmuls
28131 abssge0
28132 abssneg
28134 sleabs
28135 0ons
28142 om2noseqlt
28165 peano5n0s
28184 n0ssno
28185 0n0s
28192 peano2n0s
28193 dfn0s2
28194 n0sind
28195 n0scut
28196 n0sge0
28199 nnsgt0
28200 elnns2
28202 nnsrecgt0d
28212 seqn0sfn
28213 recut
28217 0reno
28218 |