Step |
Hyp |
Ref |
Expression |
1 |
|
ax-rrecex |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 ) |
2 |
|
eqcom |
⊢ ( 𝑥 = ( 1 / 𝐴 ) ↔ ( 1 / 𝐴 ) = 𝑥 ) |
3 |
|
1cnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℂ ) |
4 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ ) |
5 |
4
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ ) |
6 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ ) |
7 |
6
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℂ ) |
8 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ≠ 0 ) |
9 |
|
divmul |
⊢ ( ( 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( 1 / 𝐴 ) = 𝑥 ↔ ( 𝐴 · 𝑥 ) = 1 ) ) |
10 |
3 5 7 8 9
|
syl112anc |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → ( ( 1 / 𝐴 ) = 𝑥 ↔ ( 𝐴 · 𝑥 ) = 1 ) ) |
11 |
2 10
|
syl5bb |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 = ( 1 / 𝐴 ) ↔ ( 𝐴 · 𝑥 ) = 1 ) ) |
12 |
11
|
rexbidva |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ∃ 𝑥 ∈ ℝ 𝑥 = ( 1 / 𝐴 ) ↔ ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 ) ) |
13 |
1 12
|
mpbird |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℝ 𝑥 = ( 1 / 𝐴 ) ) |
14 |
|
risset |
⊢ ( ( 1 / 𝐴 ) ∈ ℝ ↔ ∃ 𝑥 ∈ ℝ 𝑥 = ( 1 / 𝐴 ) ) |
15 |
13 14
|
sylibr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℝ ) |