Step | Hyp | Ref
| Expression |
1 | | elreal 6727 |
. . . 4
⊢ (A ∈ ℝ ↔
∃y ∈ R 〈y, 0R〉 = A) |
2 | | df-rex 2306 |
. . . 4
⊢ (∃y ∈ R 〈y, 0R〉 = A ↔ ∃y(y ∈
R ∧ 〈y, 0R〉 = A)) |
3 | 1, 2 | bitri 173 |
. . 3
⊢ (A ∈ ℝ ↔
∃y(y ∈ R ∧ 〈y,
0R〉 = A)) |
4 | | breq2 3759 |
. . . 4
⊢
(〈y,
0R〉 = A
→ (0 <ℝ 〈y,
0R〉 ↔ 0 <ℝ A)) |
5 | | oveq1 5462 |
. . . . . . 7
⊢
(〈y,
0R〉 = A
→ (〈y,
0R〉 · x) = (A ·
x)) |
6 | 5 | eqeq1d 2045 |
. . . . . 6
⊢
(〈y,
0R〉 = A
→ ((〈y,
0R〉 · x) = 1 ↔ (A
· x) = 1)) |
7 | 6 | anbi2d 437 |
. . . . 5
⊢
(〈y,
0R〉 = A
→ ((0 <ℝ x ∧ (〈y,
0R〉 · x) = 1) ↔ (0 <ℝ x ∧ (A · x) =
1))) |
8 | 7 | rexbidv 2321 |
. . . 4
⊢
(〈y,
0R〉 = A
→ (∃x ∈ ℝ (0
<ℝ x ∧ (〈y,
0R〉 · x) = 1) ↔ ∃x ∈ ℝ (0 <ℝ x ∧ (A · x) =
1))) |
9 | 4, 8 | imbi12d 223 |
. . 3
⊢
(〈y,
0R〉 = A
→ ((0 <ℝ 〈y,
0R〉 → ∃x ∈ ℝ (0 <ℝ x ∧ (〈y, 0R〉 ·
x) = 1)) ↔ (0 <ℝ
A → ∃x ∈ ℝ (0 <ℝ x ∧ (A · x) =
1)))) |
10 | | df-0 6718 |
. . . . . 6
⊢ 0 =
〈0R,
0R〉 |
11 | 10 | breq1i 3762 |
. . . . 5
⊢ (0
<ℝ 〈y,
0R〉 ↔ 〈0R,
0R〉 <ℝ 〈y,
0R〉) |
12 | | ltresr 6736 |
. . . . 5
⊢
(〈0R, 0R〉
<ℝ 〈y,
0R〉 ↔ 0R
<R y) |
13 | 11, 12 | bitri 173 |
. . . 4
⊢ (0
<ℝ 〈y,
0R〉 ↔ 0R
<R y) |
14 | | recexgt0sr 6701 |
. . . . 5
⊢
(0R <R y → ∃z ∈ R (0R
<R z ∧ (y
·R z) =
1R)) |
15 | | opelreal 6726 |
. . . . . . . . . 10
⊢
(〈z,
0R〉 ∈ ℝ
↔ z ∈ R) |
16 | 15 | anbi1i 431 |
. . . . . . . . 9
⊢
((〈z,
0R〉 ∈ ℝ
∧ (0 <ℝ 〈z, 0R〉 ∧ (〈y,
0R〉 · 〈z, 0R〉) = 1)) ↔
(z ∈
R ∧ (0 <ℝ
〈z, 0R〉
∧ (〈y, 0R〉 ·
〈z, 0R〉)
= 1))) |
17 | 10 | breq1i 3762 |
. . . . . . . . . . . . 13
⊢ (0
<ℝ 〈z,
0R〉 ↔ 〈0R,
0R〉 <ℝ 〈z,
0R〉) |
18 | | ltresr 6736 |
. . . . . . . . . . . . 13
⊢
(〈0R, 0R〉
<ℝ 〈z,
0R〉 ↔ 0R
<R z) |
19 | 17, 18 | bitri 173 |
. . . . . . . . . . . 12
⊢ (0
<ℝ 〈z,
0R〉 ↔ 0R
<R z) |
20 | 19 | a1i 9 |
. . . . . . . . . . 11
⊢
((y ∈ R ∧ z ∈ R) → (0 <ℝ
〈z, 0R〉
↔ 0R <R z)) |
21 | | mulresr 6735 |
. . . . . . . . . . . . 13
⊢
((y ∈ R ∧ z ∈ R) → (〈y, 0R〉 ·
〈z, 0R〉)
= 〈(y
·R z),
0R〉) |
22 | 21 | eqeq1d 2045 |
. . . . . . . . . . . 12
⊢
((y ∈ R ∧ z ∈ R) → ((〈y, 0R〉 ·
〈z, 0R〉)
= 1 ↔ 〈(y
·R z),
0R〉 = 1)) |
23 | | df-1 6719 |
. . . . . . . . . . . . . 14
⊢ 1 =
〈1R,
0R〉 |
24 | 23 | eqeq2i 2047 |
. . . . . . . . . . . . 13
⊢
(〈(y
·R z),
0R〉 = 1 ↔ 〈(y ·R z), 0R〉 =
〈1R,
0R〉) |
25 | | eqid 2037 |
. . . . . . . . . . . . . 14
⊢
0R =
0R |
26 | | 1sr 6679 |
. . . . . . . . . . . . . . 15
⊢
1R ∈
R |
27 | | 0r 6678 |
. . . . . . . . . . . . . . 15
⊢
0R ∈
R |
28 | | opthg2 3967 |
. . . . . . . . . . . . . . 15
⊢
((1R ∈
R ∧ 0R
∈ R) → (〈(y ·R z), 0R〉 =
〈1R, 0R〉 ↔
((y ·R
z) = 1R ∧ 0R =
0R))) |
29 | 26, 27, 28 | mp2an 402 |
. . . . . . . . . . . . . 14
⊢
(〈(y
·R z),
0R〉 = 〈1R,
0R〉 ↔ ((y ·R z) = 1R ∧ 0R =
0R)) |
30 | 25, 29 | mpbiran2 847 |
. . . . . . . . . . . . 13
⊢
(〈(y
·R z),
0R〉 = 〈1R,
0R〉 ↔ (y
·R z) =
1R) |
31 | 24, 30 | bitri 173 |
. . . . . . . . . . . 12
⊢
(〈(y
·R z),
0R〉 = 1 ↔ (y ·R z) = 1R) |
32 | 22, 31 | syl6bb 185 |
. . . . . . . . . . 11
⊢
((y ∈ R ∧ z ∈ R) → ((〈y, 0R〉 ·
〈z, 0R〉)
= 1 ↔ (y
·R z) =
1R)) |
33 | 20, 32 | anbi12d 442 |
. . . . . . . . . 10
⊢
((y ∈ R ∧ z ∈ R) → ((0
<ℝ 〈z,
0R〉 ∧
(〈y, 0R〉
· 〈z,
0R〉) = 1) ↔ (0R
<R z ∧ (y
·R z) =
1R))) |
34 | 33 | pm5.32da 425 |
. . . . . . . . 9
⊢ (y ∈
R → ((z ∈ R ∧ (0 <ℝ 〈z, 0R〉 ∧ (〈y,
0R〉 · 〈z, 0R〉) = 1)) ↔
(z ∈
R ∧ (0R
<R z ∧ (y
·R z) =
1R)))) |
35 | 16, 34 | syl5bb 181 |
. . . . . . . 8
⊢ (y ∈
R → ((〈z,
0R〉 ∈ ℝ
∧ (0 <ℝ 〈z, 0R〉 ∧ (〈y,
0R〉 · 〈z, 0R〉) = 1)) ↔
(z ∈
R ∧ (0R
<R z ∧ (y
·R z) =
1R)))) |
36 | | breq2 3759 |
. . . . . . . . . 10
⊢ (x = 〈z,
0R〉 → (0 <ℝ x ↔ 0 <ℝ 〈z,
0R〉)) |
37 | | oveq2 5463 |
. . . . . . . . . . 11
⊢ (x = 〈z,
0R〉 → (〈y, 0R〉 ·
x) = (〈y, 0R〉 ·
〈z,
0R〉)) |
38 | 37 | eqeq1d 2045 |
. . . . . . . . . 10
⊢ (x = 〈z,
0R〉 → ((〈y, 0R〉 ·
x) = 1 ↔ (〈y, 0R〉 ·
〈z, 0R〉)
= 1)) |
39 | 36, 38 | anbi12d 442 |
. . . . . . . . 9
⊢ (x = 〈z,
0R〉 → ((0 <ℝ x ∧ (〈y, 0R〉 ·
x) = 1) ↔ (0 <ℝ
〈z, 0R〉
∧ (〈y, 0R〉 ·
〈z, 0R〉)
= 1))) |
40 | 39 | rspcev 2650 |
. . . . . . . 8
⊢
((〈z,
0R〉 ∈ ℝ
∧ (0 <ℝ 〈z, 0R〉 ∧ (〈y,
0R〉 · 〈z, 0R〉) = 1)) →
∃x ∈ ℝ (0 <ℝ x ∧ (〈y, 0R〉 ·
x) = 1)) |
41 | 35, 40 | syl6bir 153 |
. . . . . . 7
⊢ (y ∈
R → ((z ∈ R ∧ (0R
<R z ∧ (y
·R z) =
1R)) → ∃x ∈ ℝ (0 <ℝ x ∧ (〈y, 0R〉 ·
x) = 1))) |
42 | 41 | expd 245 |
. . . . . 6
⊢ (y ∈
R → (z ∈ R →
((0R <R z ∧ (y ·R z) = 1R) → ∃x ∈ ℝ (0 <ℝ x ∧ (〈y, 0R〉 ·
x) = 1)))) |
43 | 42 | rexlimdv 2426 |
. . . . 5
⊢ (y ∈
R → (∃z ∈
R (0R <R
z ∧
(y ·R
z) = 1R) →
∃x ∈ ℝ (0 <ℝ x ∧ (〈y, 0R〉 ·
x) = 1))) |
44 | 14, 43 | syl5 28 |
. . . 4
⊢ (y ∈
R → (0R
<R y →
∃x ∈ ℝ (0 <ℝ x ∧ (〈y, 0R〉 ·
x) = 1))) |
45 | 13, 44 | syl5bi 141 |
. . 3
⊢ (y ∈
R → (0 <ℝ 〈y, 0R〉 → ∃x ∈ ℝ (0 <ℝ x ∧ (〈y, 0R〉 ·
x) = 1))) |
46 | 3, 9, 45 | gencl 2580 |
. 2
⊢ (A ∈ ℝ →
(0 <ℝ A → ∃x ∈ ℝ (0 <ℝ x ∧ (A · x) =
1))) |
47 | 46 | imp 115 |
1
⊢
((A ∈ ℝ ∧ 0
<ℝ A) → ∃x ∈ ℝ (0 <ℝ x ∧ (A · x) =
1)) |