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

Axiom ax-precex 6793
Description: Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 6764. (Contributed by Jim Kingdon, 6-Feb-2020.)
Assertion
Ref Expression
ax-precex  RR  0  <RR  RR  0  <RR  x.  1
Distinct variable group:   ,

Detailed syntax breakdown of Axiom ax-precex
StepHypRef Expression
1 cA . . . 4
2 cr 6710 . . . 4  RR
31, 2wcel 1390 . . 3  RR
4 cc0 6711 . . . 4  0
5 cltrr 6715 . . . 4  <RR
64, 1, 5wbr 3755 . . 3  0  <RR
73, 6wa 97 . 2  RR  0  <RR
8 vx . . . . . 6  setvar
98cv 1241 . . . . 5
104, 9, 5wbr 3755 . . . 4  0  <RR
11 cmul 6716 . . . . . 6  x.
121, 9, 11co 5455 . . . . 5  x.
13 c1 6712 . . . . 5  1
1412, 13wceq 1242 . . . 4  x.  1
1510, 14wa 97 . . 3 
0  <RR  x.  1
1615, 8, 2wrex 2301 . 2  RR  0  <RR  x.  1
177, 16wi 4 1  RR  0  <RR  RR  0  <RR  x.  1
Colors of variables: wff set class
This axiom is referenced by:  recexre  7362  recexgt0  7364
  Copyright terms: Public domain W3C validator