Step | Hyp | Ref
| Expression |
1 | | elreal 10887 |
. . . 4
⊢ (𝐴 ∈ ℝ ↔
∃𝑦 ∈
R 〈𝑦,
0R〉 = 𝐴) |
2 | | df-rex 3070 |
. . . 4
⊢
(∃𝑦 ∈
R 〈𝑦,
0R〉 = 𝐴 ↔ ∃𝑦(𝑦 ∈ R ∧ 〈𝑦,
0R〉 = 𝐴)) |
3 | 1, 2 | bitri 274 |
. . 3
⊢ (𝐴 ∈ ℝ ↔
∃𝑦(𝑦 ∈ R ∧ 〈𝑦,
0R〉 = 𝐴)) |
4 | | neeq1 3006 |
. . . 4
⊢
(〈𝑦,
0R〉 = 𝐴 → (〈𝑦, 0R〉 ≠ 0
↔ 𝐴 ≠
0)) |
5 | | oveq1 7282 |
. . . . . 6
⊢
(〈𝑦,
0R〉 = 𝐴 → (〈𝑦, 0R〉 ·
𝑥) = (𝐴 · 𝑥)) |
6 | 5 | eqeq1d 2740 |
. . . . 5
⊢
(〈𝑦,
0R〉 = 𝐴 → ((〈𝑦, 0R〉 ·
𝑥) = 1 ↔ (𝐴 · 𝑥) = 1)) |
7 | 6 | rexbidv 3226 |
. . . 4
⊢
(〈𝑦,
0R〉 = 𝐴 → (∃𝑥 ∈ ℝ (〈𝑦, 0R〉 ·
𝑥) = 1 ↔ ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)) |
8 | 4, 7 | imbi12d 345 |
. . 3
⊢
(〈𝑦,
0R〉 = 𝐴 → ((〈𝑦, 0R〉 ≠ 0
→ ∃𝑥 ∈
ℝ (〈𝑦,
0R〉 · 𝑥) = 1) ↔ (𝐴 ≠ 0 → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1))) |
9 | | df-0 10878 |
. . . . . . 7
⊢ 0 =
〈0R,
0R〉 |
10 | 9 | eqeq2i 2751 |
. . . . . 6
⊢
(〈𝑦,
0R〉 = 0 ↔ 〈𝑦, 0R〉 =
〈0R,
0R〉) |
11 | | vex 3436 |
. . . . . . 7
⊢ 𝑦 ∈ V |
12 | 11 | eqresr 10893 |
. . . . . 6
⊢
(〈𝑦,
0R〉 = 〈0R,
0R〉 ↔ 𝑦 =
0R) |
13 | 10, 12 | bitri 274 |
. . . . 5
⊢
(〈𝑦,
0R〉 = 0 ↔ 𝑦 =
0R) |
14 | 13 | necon3bii 2996 |
. . . 4
⊢
(〈𝑦,
0R〉 ≠ 0 ↔ 𝑦 ≠
0R) |
15 | | recexsr 10863 |
. . . . . 6
⊢ ((𝑦 ∈ R ∧
𝑦 ≠
0R) → ∃𝑧 ∈ R (𝑦 ·R 𝑧) =
1R) |
16 | 15 | ex 413 |
. . . . 5
⊢ (𝑦 ∈ R →
(𝑦 ≠
0R → ∃𝑧 ∈ R (𝑦 ·R 𝑧) =
1R)) |
17 | | opelreal 10886 |
. . . . . . . . . 10
⊢
(〈𝑧,
0R〉 ∈ ℝ ↔ 𝑧 ∈ R) |
18 | 17 | anbi1i 624 |
. . . . . . . . 9
⊢
((〈𝑧,
0R〉 ∈ ℝ ∧ (〈𝑦,
0R〉 · 〈𝑧, 0R〉) = 1)
↔ (𝑧 ∈
R ∧ (〈𝑦, 0R〉 ·
〈𝑧,
0R〉) = 1)) |
19 | | mulresr 10895 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ R ∧
𝑧 ∈ R)
→ (〈𝑦,
0R〉 · 〈𝑧, 0R〉) =
〈(𝑦
·R 𝑧),
0R〉) |
20 | 19 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ R ∧
𝑧 ∈ R)
→ ((〈𝑦,
0R〉 · 〈𝑧, 0R〉) = 1
↔ 〈(𝑦
·R 𝑧), 0R〉 =
1)) |
21 | | df-1 10879 |
. . . . . . . . . . . . 13
⊢ 1 =
〈1R,
0R〉 |
22 | 21 | eqeq2i 2751 |
. . . . . . . . . . . 12
⊢
(〈(𝑦
·R 𝑧), 0R〉 = 1
↔ 〈(𝑦
·R 𝑧), 0R〉 =
〈1R,
0R〉) |
23 | | ovex 7308 |
. . . . . . . . . . . . 13
⊢ (𝑦
·R 𝑧) ∈ V |
24 | 23 | eqresr 10893 |
. . . . . . . . . . . 12
⊢
(〈(𝑦
·R 𝑧), 0R〉 =
〈1R, 0R〉 ↔
(𝑦
·R 𝑧) =
1R) |
25 | 22, 24 | bitri 274 |
. . . . . . . . . . 11
⊢
(〈(𝑦
·R 𝑧), 0R〉 = 1
↔ (𝑦
·R 𝑧) =
1R) |
26 | 20, 25 | bitrdi 287 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ R ∧
𝑧 ∈ R)
→ ((〈𝑦,
0R〉 · 〈𝑧, 0R〉) = 1
↔ (𝑦
·R 𝑧) =
1R)) |
27 | 26 | pm5.32da 579 |
. . . . . . . . 9
⊢ (𝑦 ∈ R →
((𝑧 ∈ R
∧ (〈𝑦,
0R〉 · 〈𝑧, 0R〉) = 1)
↔ (𝑧 ∈
R ∧ (𝑦
·R 𝑧) =
1R))) |
28 | 18, 27 | bitrid 282 |
. . . . . . . 8
⊢ (𝑦 ∈ R →
((〈𝑧,
0R〉 ∈ ℝ ∧ (〈𝑦,
0R〉 · 〈𝑧, 0R〉) = 1)
↔ (𝑧 ∈
R ∧ (𝑦
·R 𝑧) =
1R))) |
29 | | oveq2 7283 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑧, 0R〉 →
(〈𝑦,
0R〉 · 𝑥) = (〈𝑦, 0R〉 ·
〈𝑧,
0R〉)) |
30 | 29 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑧, 0R〉 →
((〈𝑦,
0R〉 · 𝑥) = 1 ↔ (〈𝑦, 0R〉 ·
〈𝑧,
0R〉) = 1)) |
31 | 30 | rspcev 3561 |
. . . . . . . 8
⊢
((〈𝑧,
0R〉 ∈ ℝ ∧ (〈𝑦,
0R〉 · 〈𝑧, 0R〉) = 1)
→ ∃𝑥 ∈
ℝ (〈𝑦,
0R〉 · 𝑥) = 1) |
32 | 28, 31 | syl6bir 253 |
. . . . . . 7
⊢ (𝑦 ∈ R →
((𝑧 ∈ R
∧ (𝑦
·R 𝑧) = 1R) →
∃𝑥 ∈ ℝ
(〈𝑦,
0R〉 · 𝑥) = 1)) |
33 | 32 | expd 416 |
. . . . . 6
⊢ (𝑦 ∈ R →
(𝑧 ∈ R
→ ((𝑦
·R 𝑧) = 1R →
∃𝑥 ∈ ℝ
(〈𝑦,
0R〉 · 𝑥) = 1))) |
34 | 33 | rexlimdv 3212 |
. . . . 5
⊢ (𝑦 ∈ R →
(∃𝑧 ∈
R (𝑦
·R 𝑧) = 1R →
∃𝑥 ∈ ℝ
(〈𝑦,
0R〉 · 𝑥) = 1)) |
35 | 16, 34 | syld 47 |
. . . 4
⊢ (𝑦 ∈ R →
(𝑦 ≠
0R → ∃𝑥 ∈ ℝ (〈𝑦, 0R〉 ·
𝑥) = 1)) |
36 | 14, 35 | syl5bi 241 |
. . 3
⊢ (𝑦 ∈ R →
(〈𝑦,
0R〉 ≠ 0 → ∃𝑥 ∈ ℝ (〈𝑦, 0R〉 ·
𝑥) = 1)) |
37 | 3, 8, 36 | gencl 3471 |
. 2
⊢ (𝐴 ∈ ℝ → (𝐴 ≠ 0 → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)) |
38 | 37 | imp 407 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1) |