trirec0 - Mathbox for Jim Kingdon

	Mathbox for Jim Kingdon		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > Mathboxes > trirec0		Unicode version

Theorem trirec0 13556

Description: Every real number having a reciprocal or equaling zero is equivalent to real number trichotomy.

This is the key part of the definition of what is known as a discrete field, so "the real numbers are a discrete field" can be taken as an equivalent way to state real trichotomy (see further discussion at trilpo 13555). (Contributed by Jim Kingdon, 10-Jun-2024.)

**Assertion**
Ref	Expression
trirec0	$\/$ $\/$ $\/$

Distinct variable group:

Proof of Theorem trirec0 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 519	. . . . . 6 $/\$ $\/$ $\/$ $/\$
2		simpr 109	. . . . . . 7 $/\$ $\/$ $\/$ $/\$
3	1, 2	lt0ap0d 8503	. . . . . 6 $/\$ $\/$ $\/$ $/\$ #
4		rerecclap 8582	. . . . . . 7 $/\$ #
5		recn 7844	. . . . . . . 8
6		recidap 8538	. . . . . . . 8 $/\$ #
7	5, 6	sylan 281	. . . . . . 7 $/\$ #
8		oveq2 5822	. . . . . . . . 9
9	8	eqeq1d 2163	. . . . . . . 8
10	9	rspcev 2813	. . . . . . 7 $/\$
11	4, 7, 10	syl2anc 409	. . . . . 6 $/\$ #
12	1, 3, 11	syl2anc 409	. . . . 5 $/\$ $\/$ $\/$ $/\$
13	12	orcd 723	. . . 4 $/\$ $\/$ $\/$ $/\$ $\/$
14		simpr 109	. . . . 5 $/\$ $\/$ $\/$ $/\$
15	14	olcd 724	. . . 4 $/\$ $\/$ $\/$ $/\$ $\/$
16		simpll 519	. . . . . 6 $/\$ $\/$ $\/$ $/\$
17		simpr 109	. . . . . . 7 $/\$ $\/$ $\/$ $/\$
18	16, 17	gt0ap0d 8483	. . . . . 6 $/\$ $\/$ $\/$ $/\$ #
19	16, 18, 11	syl2anc 409	. . . . 5 $/\$ $\/$ $\/$ $/\$
20	19	orcd 723	. . . 4 $/\$ $\/$ $\/$ $/\$ $\/$
21		0re 7857	. . . . . 6
22		breq2 3965	. . . . . . . 8
23		eqeq2 2164	. . . . . . . 8
24		breq1 3964	. . . . . . . 8
25	22, 23, 24	3orbi123d 1290	. . . . . . 7 $\/$ $\/$ $\/$ $\/$
26	25	rspcv 2809	. . . . . 6 $\/$ $\/$ $\/$ $\/$
27	21, 26	ax-mp 5	. . . . 5 $\/$ $\/$ $\/$ $\/$
28	27	adantl 275	. . . 4 $/\$ $\/$ $\/$ $\/$ $\/$
29	13, 15, 20, 28	mpjao3dan 1286	. . 3 $/\$ $\/$ $\/$ $\/$
30	29	ralimiaa 2516	. 2 $\/$ $\/$ $\/$
31		oveq1 5821	. . . . . . 7
32	31	eqeq1d 2163	. . . . . 6
33	32	rexbidv 2455	. . . . 5
34		eqeq1 2161	. . . . 5
35	33, 34	orbi12d 783	. . . 4 $\/$ $\/$
36	35	cbvralv 2677	. . 3 $\/$ $\/$
37		nfcv 2296	. . . . . . . . 9
38		nfre1 2497	. . . . . . . . . 10
39		nfv 1505	. . . . . . . . . 10
40	38, 39	nfor 1551	. . . . . . . . 9 $\/$
41	37, 40	nfralya 2494	. . . . . . . 8 $\/$
42		nfv 1505	. . . . . . . 8 $/\$
43	41, 42	nfan 1542	. . . . . . 7 $\/$ $/\$ $/\$
44		nfv 1505	. . . . . . 7 $\/$ $\/$
45		simpr 109	. . . . . . . . . . 11 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
46		simprr 522	. . . . . . . . . . . . . 14 $\/$ $/\$ $/\$
47	46	ad2antrr 480	. . . . . . . . . . . . 13 $\/$ $/\$ $/\$ $/\$ $/\$
48	47	adantr 274	. . . . . . . . . . . 12 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
49		simprl 521	. . . . . . . . . . . . . 14 $\/$ $/\$ $/\$
50	49	ad2antrr 480	. . . . . . . . . . . . 13 $\/$ $/\$ $/\$ $/\$ $/\$
51	50	adantr 274	. . . . . . . . . . . 12 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
52	48, 51	sublt0d 8424	. . . . . . . . . . 11 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
53	45, 52	mpbid 146	. . . . . . . . . 10 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
54	53	3mix3d 1159	. . . . . . . . 9 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
55		simpr 109	. . . . . . . . . . 11 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
56	50	adantr 274	. . . . . . . . . . . 12 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
57	47	adantr 274	. . . . . . . . . . . 12 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
58	56, 57	posdifd 8386	. . . . . . . . . . 11 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
59	55, 58	mpbird 166	. . . . . . . . . 10 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
60	59	3mix1d 1157	. . . . . . . . 9 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
61	47	recnd 7885	. . . . . . . . . . . 12 $\/$ $/\$ $/\$ $/\$ $/\$
62	50	recnd 7885	. . . . . . . . . . . 12 $\/$ $/\$ $/\$ $/\$ $/\$
63	61, 62	subcld 8165	. . . . . . . . . . 11 $\/$ $/\$ $/\$ $/\$ $/\$
64		simplr 520	. . . . . . . . . . . 12 $\/$ $/\$ $/\$ $/\$ $/\$
65	64	recnd 7885	. . . . . . . . . . 11 $\/$ $/\$ $/\$ $/\$ $/\$
66		simpr 109	. . . . . . . . . . . 12 $\/$ $/\$ $/\$ $/\$ $/\$
67		1ap0 8444	. . . . . . . . . . . 12 #
68	66, 67	eqbrtrdi 3999	. . . . . . . . . . 11 $\/$ $/\$ $/\$ $/\$ $/\$ #
69	63, 65, 68	mulap0bad 8512	. . . . . . . . . 10 $\/$ $/\$ $/\$ $/\$ $/\$ #
70	46, 49	resubcld 8235	. . . . . . . . . . . 12 $\/$ $/\$ $/\$
71	70	ad2antrr 480	. . . . . . . . . . 11 $\/$ $/\$ $/\$ $/\$ $/\$
72		reaplt 8442	. . . . . . . . . . 11 $/\$ # $\/$
73	71, 21, 72	sylancl 410	. . . . . . . . . 10 $\/$ $/\$ $/\$ $/\$ $/\$ # $\/$
74	69, 73	mpbid 146	. . . . . . . . 9 $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
75	54, 60, 74	mpjaodan 788	. . . . . . . 8 $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
76	75	exp31 362	. . . . . . 7 $\/$ $/\$ $/\$ $\/$ $\/$
77	43, 44, 76	rexlimd 2568	. . . . . 6 $\/$ $/\$ $/\$ $\/$ $\/$
78	77	imp 123	. . . . 5 $\/$ $/\$ $/\$ $/\$ $\/$ $\/$
79	46	recnd 7885	. . . . . . . . 9 $\/$ $/\$ $/\$
80	79	adantr 274	. . . . . . . 8 $\/$ $/\$ $/\$ $/\$
81	49	recnd 7885	. . . . . . . . 9 $\/$ $/\$ $/\$
82	81	adantr 274	. . . . . . . 8 $\/$ $/\$ $/\$ $/\$
83		simpr 109	. . . . . . . 8 $\/$ $/\$ $/\$ $/\$
84	80, 82, 83	subeq0d 8173	. . . . . . 7 $\/$ $/\$ $/\$ $/\$
85	84	equcomd 1684	. . . . . 6 $\/$ $/\$ $/\$ $/\$
86	85	3mix2d 1158	. . . . 5 $\/$ $/\$ $/\$ $/\$ $\/$ $\/$
87		oveq1 5821	. . . . . . . . 9
88	87	eqeq1d 2163	. . . . . . . 8
89	88	rexbidv 2455	. . . . . . 7
90		eqeq1 2161	. . . . . . 7
91	89, 90	orbi12d 783	. . . . . 6 $\/$ $\/$
92		simpl 108	. . . . . 6 $\/$ $/\$ $/\$ $\/$
93	91, 92, 70	rspcdva 2818	. . . . 5 $\/$ $/\$ $/\$ $\/$
94	78, 86, 93	mpjaodan 788	. . . 4 $\/$ $/\$ $/\$ $\/$ $\/$
95	94	ralrimivva 2536	. . 3 $\/$ $\/$ $\/$
96	36, 95	sylbi 120	. 2 $\/$ $\/$ $\/$
97	30, 96	impbii 125	1 $\/$ $\/$ $\/$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 698 $\/$ w3o 962

wceq 1332

wcel 2125

wral 2432

wrex 2433 class class class wbr 3961 (class class class)co 5814

cc 7709

cr 7710

cc0 7711

c1 7712

cmul 7716

clt 7891

cmin 8025 # cap 8435

cdiv 8524

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-13 2127 ax-14 2128 ax-ext 2136 ax-sep 4078 ax-pow 4130 ax-pr 4164 ax-un 4388 ax-setind 4490 ax-cnex 7802 ax-resscn 7803 ax-1cn 7804 ax-1re 7805 ax-icn 7806 ax-addcl 7807 ax-addrcl 7808 ax-mulcl 7809 ax-mulrcl 7810 ax-addcom 7811 ax-mulcom 7812 ax-addass 7813 ax-mulass 7814 ax-distr 7815 ax-i2m1 7816 ax-0lt1 7817 ax-1rid 7818 ax-0id 7819 ax-rnegex 7820 ax-precex 7821 ax-cnre 7822 ax-pre-ltirr 7823 ax-pre-ltwlin 7824 ax-pre-lttrn 7825 ax-pre-apti 7826 ax-pre-ltadd 7827 ax-pre-mulgt0 7828 ax-pre-mulext 7829

This theorem depends on definitions: df-bi 116 df-3or 964 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1740 df-eu 2006 df-mo 2007 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ne 2325 df-nel 2420 df-ral 2437 df-rex 2438 df-reu 2439 df-rmo 2440 df-rab 2441 df-v 2711 df-sbc 2934 df-dif 3100 df-un 3102 df-in 3104 df-ss 3111 df-pw 3541 df-sn 3562 df-pr 3563 df-op 3565 df-uni 3769 df-br 3962 df-opab 4022 df-id 4248 df-po 4251 df-iso 4252 df-xp 4585 df-rel 4586 df-cnv 4587 df-co 4588 df-dm 4589 df-iota 5128 df-fun 5165 df-fv 5171 df-riota 5770 df-ov 5817 df-oprab 5818 df-mpo 5819 df-pnf 7893 df-mnf 7894 df-xr 7895 df-ltxr 7896 df-le 7897 df-sub 8027 df-neg 8028 df-reap 8429 df-ap 8436 df-div 8525

This theorem is referenced by: trirec0xor 13557

W3C validator