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

Theorem trirec0 13410
 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 13409). (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.
StepHypRef Expression
1 simpll 519 . . . . . 6
2 simpr 109 . . . . . . 7
31, 2lt0ap0d 8434 . . . . . 6 #
4 rerecclap 8513 . . . . . . 7 #
5 recn 7776 . . . . . . . 8
6 recidap 8469 . . . . . . . 8 #
75, 6sylan 281 . . . . . . 7 #
8 oveq2 5789 . . . . . . . . 9
98eqeq1d 2149 . . . . . . . 8
109rspcev 2792 . . . . . . 7
114, 7, 10syl2anc 409 . . . . . 6 #
121, 3, 11syl2anc 409 . . . . 5
1312orcd 723 . . . 4
14 simpr 109 . . . . 5
1514olcd 724 . . . 4
16 simpll 519 . . . . . 6
17 simpr 109 . . . . . . 7
1816, 17gt0ap0d 8414 . . . . . 6 #
1916, 18, 11syl2anc 409 . . . . 5
2019orcd 723 . . . 4
21 0re 7789 . . . . . 6
22 breq2 3940 . . . . . . . 8
23 eqeq2 2150 . . . . . . . 8
24 breq1 3939 . . . . . . . 8
2522, 23, 243orbi123d 1290 . . . . . . 7
2625rspcv 2788 . . . . . 6
2721, 26ax-mp 5 . . . . 5
2827adantl 275 . . . 4
2913, 15, 20, 28mpjao3dan 1286 . . 3
3029ralimiaa 2497 . 2
31 oveq1 5788 . . . . . . 7
3231eqeq1d 2149 . . . . . 6
3332rexbidv 2439 . . . . 5
34 eqeq1 2147 . . . . 5
3533, 34orbi12d 783 . . . 4
3635cbvralv 2657 . . 3
37 nfcv 2282 . . . . . . . . 9
38 nfre1 2479 . . . . . . . . . 10
39 nfv 1509 . . . . . . . . . 10
4038, 39nfor 1554 . . . . . . . . 9
4137, 40nfralya 2476 . . . . . . . 8
42 nfv 1509 . . . . . . . 8
4341, 42nfan 1545 . . . . . . 7
44 nfv 1509 . . . . . . 7
45 simpr 109 . . . . . . . . . . 11
46 simprr 522 . . . . . . . . . . . . . 14
4746ad2antrr 480 . . . . . . . . . . . . 13
4847adantr 274 . . . . . . . . . . . 12
49 simprl 521 . . . . . . . . . . . . . 14
5049ad2antrr 480 . . . . . . . . . . . . 13
5150adantr 274 . . . . . . . . . . . 12
5248, 51sublt0d 8355 . . . . . . . . . . 11
5345, 52mpbid 146 . . . . . . . . . 10
54533mix3d 1159 . . . . . . . . 9
55 simpr 109 . . . . . . . . . . 11
5650adantr 274 . . . . . . . . . . . 12
5747adantr 274 . . . . . . . . . . . 12
5856, 57posdifd 8317 . . . . . . . . . . 11
5955, 58mpbird 166 . . . . . . . . . 10
60593mix1d 1157 . . . . . . . . 9
6147recnd 7817 . . . . . . . . . . . 12
6250recnd 7817 . . . . . . . . . . . 12
6361, 62subcld 8096 . . . . . . . . . . 11
64 simplr 520 . . . . . . . . . . . 12
6564recnd 7817 . . . . . . . . . . 11
66 simpr 109 . . . . . . . . . . . 12
67 1ap0 8375 . . . . . . . . . . . 12 #
6866, 67eqbrtrdi 3974 . . . . . . . . . . 11 #
6963, 65, 68mulap0bad 8443 . . . . . . . . . 10 #
7046, 49resubcld 8166 . . . . . . . . . . . 12
7170ad2antrr 480 . . . . . . . . . . 11
72 reaplt 8373 . . . . . . . . . . 11 #
7371, 21, 72sylancl 410 . . . . . . . . . 10 #
7469, 73mpbid 146 . . . . . . . . 9
7554, 60, 74mpjaodan 788 . . . . . . . 8
7675exp31 362 . . . . . . 7
7743, 44, 76rexlimd 2549 . . . . . 6
7877imp 123 . . . . 5
7946recnd 7817 . . . . . . . . 9
8079adantr 274 . . . . . . . 8
8149recnd 7817 . . . . . . . . 9
8281adantr 274 . . . . . . . 8
83 simpr 109 . . . . . . . 8
8480, 82, 83subeq0d 8104 . . . . . . 7
8584equcomd 1684 . . . . . 6
86853mix2d 1158 . . . . 5
87 oveq1 5788 . . . . . . . . 9
8887eqeq1d 2149 . . . . . . . 8
8988rexbidv 2439 . . . . . . 7
90 eqeq1 2147 . . . . . . 7
9189, 90orbi12d 783 . . . . . 6
92 simpl 108 . . . . . 6
9391, 92, 70rspcdva 2797 . . . . 5
9478, 86, 93mpjaodan 788 . . . 4
9594ralrimivva 2517 . . 3
9636, 95sylbi 120 . 2
9730, 96impbii 125 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   wo 698   w3o 962   wceq 1332   wcel 1481  wral 2417  wrex 2418   class class class wbr 3936  (class class class)co 5781  cc 7641  cr 7642  cc0 7643  c1 7644   cmul 7648   clt 7823   cmin 7956   # cap 8366   cdiv 8455 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 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459  ax-cnex 7734  ax-resscn 7735  ax-1cn 7736  ax-1re 7737  ax-icn 7738  ax-addcl 7739  ax-addrcl 7740  ax-mulcl 7741  ax-mulrcl 7742  ax-addcom 7743  ax-mulcom 7744  ax-addass 7745  ax-mulass 7746  ax-distr 7747  ax-i2m1 7748  ax-0lt1 7749  ax-1rid 7750  ax-0id 7751  ax-rnegex 7752  ax-precex 7753  ax-cnre 7754  ax-pre-ltirr 7755  ax-pre-ltwlin 7756  ax-pre-lttrn 7757  ax-pre-apti 7758  ax-pre-ltadd 7759  ax-pre-mulgt0 7760  ax-pre-mulext 7761 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 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rmo 2425  df-rab 2426  df-v 2691  df-sbc 2913  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-br 3937  df-opab 3997  df-id 4222  df-po 4225  df-iso 4226  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-iota 5095  df-fun 5132  df-fv 5138  df-riota 5737  df-ov 5784  df-oprab 5785  df-mpo 5786  df-pnf 7825  df-mnf 7826  df-xr 7827  df-ltxr 7828  df-le 7829  df-sub 7958  df-neg 7959  df-reap 8360  df-ap 8367  df-div 8456 This theorem is referenced by:  trirec0xor  13411
 Copyright terms: Public domain W3C validator