dich0 - Intuitionistic Logic Explorer

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

Theorem dich0 15405

Description: Real number dichotomy stated in terms of two real numbers or a real number and zero. (Contributed by Jim Kingdon, 22-Jul-2025.)

**Assertion**
Ref	Expression
dich0	$\/$ $\/$

**Proof of Theorem dich0**
Step	Hyp	Ref	Expression
1		breq1 4092	. . . . . 6
2		breq2 4093	. . . . . 6
3	1, 2	orbi12d 800	. . . . 5 $\/$ $\/$
4		simpl 109	. . . . 5 $\/$ $/\$ $/\$ $\/$
5		resubcl 8448	. . . . . 6 $/\$
6	5	adantl 277	. . . . 5 $\/$ $/\$ $/\$
7	3, 4, 6	rspcdva 2914	. . . 4 $\/$ $/\$ $/\$ $\/$
8		simprl 531	. . . . . 6 $\/$ $/\$ $/\$
9		simprr 533	. . . . . 6 $\/$ $/\$ $/\$
10	8, 9	suble0d 8721	. . . . 5 $\/$ $/\$ $/\$
11	8, 9	subge0d 8720	. . . . 5 $\/$ $/\$ $/\$
12	10, 11	orbi12d 800	. . . 4 $\/$ $/\$ $/\$ $\/$ $\/$
13	7, 12	mpbid 147	. . 3 $\/$ $/\$ $/\$ $\/$
14	13	ralrimivva 2613	. 2 $\/$ $\/$
15		breq2 4093	. . . . 5
16		breq1 4092	. . . . 5
17	15, 16	orbi12d 800	. . . 4 $\/$ $\/$
18		breq1 4092	. . . . . . 7
19		breq2 4093	. . . . . . 7
20	18, 19	orbi12d 800	. . . . . 6 $\/$ $\/$
21	20	ralbidv 2531	. . . . 5 $\/$ $\/$
22	21	rspccva 2908	. . . 4 $\/$ $/\$ $\/$
23		0red 8185	. . . 4 $\/$ $/\$
24	17, 22, 23	rspcdva 2914	. . 3 $\/$ $/\$ $\/$
25	24	ralrimiva 2604	. 2 $\/$ $\/$
26	14, 25	impbii 126	1 $\/$ $\/$

Colors of variables: wff set class

Syntax hints: $/\$ wa 104

wb 105 $\/$ wo 715

wceq 1397

wcel 2201

wral 2509 class class class wbr 4089 (class class class)co 6023

cr 8036

cc0 8037

cle 8220

cmin 8355

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-in1 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2203 ax-14 2204 ax-ext 2212 ax-sep 4208 ax-pow 4266 ax-pr 4301 ax-un 4532 ax-setind 4637 ax-cnex 8128 ax-resscn 8129 ax-1cn 8130 ax-1re 8131 ax-icn 8132 ax-addcl 8133 ax-addrcl 8134 ax-mulcl 8135 ax-addcom 8137 ax-addass 8139 ax-distr 8141 ax-i2m1 8142 ax-0id 8145 ax-rnegex 8146 ax-cnre 8148 ax-pre-ltadd 8153

This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1810 df-eu 2081 df-mo 2082 df-clab 2217 df-cleq 2223 df-clel 2226 df-nfc 2362 df-ne 2402 df-nel 2497 df-ral 2514 df-rex 2515 df-reu 2516 df-rab 2518 df-v 2803 df-sbc 3031 df-dif 3201 df-un 3203 df-in 3205 df-ss 3212 df-pw 3655 df-sn 3676 df-pr 3677 df-op 3679 df-uni 3895 df-br 4090 df-opab 4152 df-id 4392 df-xp 4733 df-rel 4734 df-cnv 4735 df-co 4736 df-dm 4737 df-iota 5288 df-fun 5330 df-fv 5336 df-riota 5976 df-ov 6026 df-oprab 6027 df-mpo 6028 df-pnf 8221 df-mnf 8222 df-xr 8223 df-ltxr 8224 df-le 8225 df-sub 8357 df-neg 8358

This theorem is referenced by: ivthdich 15406