![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ax-precex | GIF version |
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.) |
Ref | Expression |
---|---|
ax-precex | ⊢ ((A ∈ ℝ ∧ 0 <ℝ A) → ∃x ∈ ℝ (0 <ℝ x ∧ (A · x) = 1)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . . 4 class A | |
2 | cr 6710 | . . . 4 class ℝ | |
3 | 1, 2 | wcel 1390 | . . 3 wff A ∈ ℝ |
4 | cc0 6711 | . . . 4 class 0 | |
5 | cltrr 6715 | . . . 4 class <ℝ | |
6 | 4, 1, 5 | wbr 3755 | . . 3 wff 0 <ℝ A |
7 | 3, 6 | wa 97 | . 2 wff (A ∈ ℝ ∧ 0 <ℝ A) |
8 | vx | . . . . . 6 setvar x | |
9 | 8 | cv 1241 | . . . . 5 class x |
10 | 4, 9, 5 | wbr 3755 | . . . 4 wff 0 <ℝ x |
11 | cmul 6716 | . . . . . 6 class · | |
12 | 1, 9, 11 | co 5455 | . . . . 5 class (A · x) |
13 | c1 6712 | . . . . 5 class 1 | |
14 | 12, 13 | wceq 1242 | . . . 4 wff (A · x) = 1 |
15 | 10, 14 | wa 97 | . . 3 wff (0 <ℝ x ∧ (A · x) = 1) |
16 | 15, 8, 2 | wrex 2301 | . 2 wff ∃x ∈ ℝ (0 <ℝ x ∧ (A · x) = 1) |
17 | 7, 16 | wi 4 | 1 wff ((A ∈ ℝ ∧ 0 <ℝ A) → ∃x ∈ ℝ (0 <ℝ x ∧ (A · x) = 1)) |
Colors of variables: wff set class |
This axiom is referenced by: recexre 7362 recexgt0 7364 |
Copyright terms: Public domain | W3C validator |