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

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

Detailed syntax breakdown of Axiom ax-precex
StepHypRef Expression
1 cA . . . 4 class A
2 cr 6690 . . . 4 class
31, 2wcel 1390 . . 3 wff A
4 cc0 6691 . . . 4 class 0
5 cltrr 6695 . . . 4 class <
64, 1, 5wbr 3755 . . 3 wff 0 < A
73, 6wa 97 . 2 wff (A 0 < A)
8 vx . . . . . 6 setvar x
98cv 1241 . . . . 5 class x
104, 9, 5wbr 3755 . . . 4 wff 0 < x
11 cmul 6696 . . . . . 6 class ·
121, 9, 11co 5455 . . . . 5 class (A · x)
13 c1 6692 . . . . 5 class 1
1412, 13wceq 1242 . . . 4 wff (A · x) = 1
1510, 14wa 97 . . 3 wff (0 < x (A · x) = 1)
1615, 8, 2wrex 2301 . 2 wff x ℝ (0 < x (A · x) = 1)
177, 16wi 4 1 wff ((A 0 < A) → x ℝ (0 < x (A · x) = 1))
Colors of variables: wff set class
This axiom is referenced by:  recexre  7342  recexgt0  7344
  Copyright terms: Public domain W3C validator