| Step | Hyp | Ref
| Expression |
| 1 | | elreal 11171 |
. . . 4
⊢ (𝐴 ∈ ℝ ↔
∃𝑦 ∈
R 〈𝑦,
0R〉 = 𝐴) |
| 2 | | df-rex 3071 |
. . . 4
⊢
(∃𝑦 ∈
R 〈𝑦,
0R〉 = 𝐴 ↔ ∃𝑦(𝑦 ∈ R ∧ 〈𝑦,
0R〉 = 𝐴)) |
| 3 | 1, 2 | bitri 275 |
. . 3
⊢ (𝐴 ∈ ℝ ↔
∃𝑦(𝑦 ∈ R ∧ 〈𝑦,
0R〉 = 𝐴)) |
| 4 | | neeq1 3003 |
. . . 4
⊢
(〈𝑦,
0R〉 = 𝐴 → (〈𝑦, 0R〉 ≠ 0
↔ 𝐴 ≠
0)) |
| 5 | | oveq1 7438 |
. . . . . 6
⊢
(〈𝑦,
0R〉 = 𝐴 → (〈𝑦, 0R〉 ·
𝑥) = (𝐴 · 𝑥)) |
| 6 | 5 | eqeq1d 2739 |
. . . . 5
⊢
(〈𝑦,
0R〉 = 𝐴 → ((〈𝑦, 0R〉 ·
𝑥) = 1 ↔ (𝐴 · 𝑥) = 1)) |
| 7 | 6 | rexbidv 3179 |
. . . 4
⊢
(〈𝑦,
0R〉 = 𝐴 → (∃𝑥 ∈ ℝ (〈𝑦, 0R〉 ·
𝑥) = 1 ↔ ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)) |
| 8 | 4, 7 | imbi12d 344 |
. . 3
⊢
(〈𝑦,
0R〉 = 𝐴 → ((〈𝑦, 0R〉 ≠ 0
→ ∃𝑥 ∈
ℝ (〈𝑦,
0R〉 · 𝑥) = 1) ↔ (𝐴 ≠ 0 → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1))) |
| 9 | | df-0 11162 |
. . . . . . 7
⊢ 0 =
〈0R,
0R〉 |
| 10 | 9 | eqeq2i 2750 |
. . . . . 6
⊢
(〈𝑦,
0R〉 = 0 ↔ 〈𝑦, 0R〉 =
〈0R,
0R〉) |
| 11 | | vex 3484 |
. . . . . . 7
⊢ 𝑦 ∈ V |
| 12 | 11 | eqresr 11177 |
. . . . . 6
⊢
(〈𝑦,
0R〉 = 〈0R,
0R〉 ↔ 𝑦 =
0R) |
| 13 | 10, 12 | bitri 275 |
. . . . 5
⊢
(〈𝑦,
0R〉 = 0 ↔ 𝑦 =
0R) |
| 14 | 13 | necon3bii 2993 |
. . . 4
⊢
(〈𝑦,
0R〉 ≠ 0 ↔ 𝑦 ≠
0R) |
| 15 | | recexsr 11147 |
. . . . . 6
⊢ ((𝑦 ∈ R ∧
𝑦 ≠
0R) → ∃𝑧 ∈ R (𝑦 ·R 𝑧) =
1R) |
| 16 | 15 | ex 412 |
. . . . 5
⊢ (𝑦 ∈ R →
(𝑦 ≠
0R → ∃𝑧 ∈ R (𝑦 ·R 𝑧) =
1R)) |
| 17 | | opelreal 11170 |
. . . . . . . . . 10
⊢
(〈𝑧,
0R〉 ∈ ℝ ↔ 𝑧 ∈ R) |
| 18 | 17 | anbi1i 624 |
. . . . . . . . 9
⊢
((〈𝑧,
0R〉 ∈ ℝ ∧ (〈𝑦,
0R〉 · 〈𝑧, 0R〉) = 1)
↔ (𝑧 ∈
R ∧ (〈𝑦, 0R〉 ·
〈𝑧,
0R〉) = 1)) |
| 19 | | mulresr 11179 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ R ∧
𝑧 ∈ R)
→ (〈𝑦,
0R〉 · 〈𝑧, 0R〉) =
〈(𝑦
·R 𝑧),
0R〉) |
| 20 | 19 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ R ∧
𝑧 ∈ R)
→ ((〈𝑦,
0R〉 · 〈𝑧, 0R〉) = 1
↔ 〈(𝑦
·R 𝑧), 0R〉 =
1)) |
| 21 | | df-1 11163 |
. . . . . . . . . . . . 13
⊢ 1 =
〈1R,
0R〉 |
| 22 | 21 | eqeq2i 2750 |
. . . . . . . . . . . 12
⊢
(〈(𝑦
·R 𝑧), 0R〉 = 1
↔ 〈(𝑦
·R 𝑧), 0R〉 =
〈1R,
0R〉) |
| 23 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ (𝑦
·R 𝑧) ∈ V |
| 24 | 23 | eqresr 11177 |
. . . . . . . . . . . 12
⊢
(〈(𝑦
·R 𝑧), 0R〉 =
〈1R, 0R〉 ↔
(𝑦
·R 𝑧) =
1R) |
| 25 | 22, 24 | bitri 275 |
. . . . . . . . . . 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 283 |
. . . . . . . 8
⊢ (𝑦 ∈ R →
((〈𝑧,
0R〉 ∈ ℝ ∧ (〈𝑦,
0R〉 · 〈𝑧, 0R〉) = 1)
↔ (𝑧 ∈
R ∧ (𝑦
·R 𝑧) =
1R))) |
| 29 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑧, 0R〉 →
(〈𝑦,
0R〉 · 𝑥) = (〈𝑦, 0R〉 ·
〈𝑧,
0R〉)) |
| 30 | 29 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑧, 0R〉 →
((〈𝑦,
0R〉 · 𝑥) = 1 ↔ (〈𝑦, 0R〉 ·
〈𝑧,
0R〉) = 1)) |
| 31 | 30 | rspcev 3622 |
. . . . . . . 8
⊢
((〈𝑧,
0R〉 ∈ ℝ ∧ (〈𝑦,
0R〉 · 〈𝑧, 0R〉) = 1)
→ ∃𝑥 ∈
ℝ (〈𝑦,
0R〉 · 𝑥) = 1) |
| 32 | 28, 31 | biimtrrdi 254 |
. . . . . . 7
⊢ (𝑦 ∈ R →
((𝑧 ∈ R
∧ (𝑦
·R 𝑧) = 1R) →
∃𝑥 ∈ ℝ
(〈𝑦,
0R〉 · 𝑥) = 1)) |
| 33 | 32 | expd 415 |
. . . . . 6
⊢ (𝑦 ∈ R →
(𝑧 ∈ R
→ ((𝑦
·R 𝑧) = 1R →
∃𝑥 ∈ ℝ
(〈𝑦,
0R〉 · 𝑥) = 1))) |
| 34 | 33 | rexlimdv 3153 |
. . . . 5
⊢ (𝑦 ∈ R →
(∃𝑧 ∈
R (𝑦
·R 𝑧) = 1R →
∃𝑥 ∈ ℝ
(〈𝑦,
0R〉 · 𝑥) = 1)) |
| 35 | 16, 34 | syld 47 |
. . . 4
⊢ (𝑦 ∈ R →
(𝑦 ≠
0R → ∃𝑥 ∈ ℝ (〈𝑦, 0R〉 ·
𝑥) = 1)) |
| 36 | 14, 35 | biimtrid 242 |
. . 3
⊢ (𝑦 ∈ R →
(〈𝑦,
0R〉 ≠ 0 → ∃𝑥 ∈ ℝ (〈𝑦, 0R〉 ·
𝑥) = 1)) |
| 37 | 3, 8, 36 | gencl 3523 |
. 2
⊢ (𝐴 ∈ ℝ → (𝐴 ≠ 0 → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)) |
| 38 | 37 | imp 406 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1) |