This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axrrecex

Description: Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rrecex . (Contributed by NM, 15-May-1996) (New usage is discouraged.)

Ref Expression
Assertion axrrecex ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 )

Proof

Step Hyp Ref Expression
1 elreal ⊢ ( 𝐴 ∈ ℝ ↔ ∃ 𝑦 ∈ R ⟨ 𝑦 , 0R ⟩ = 𝐴 )
2 df-rex ⊢ ( ∃ 𝑦 ∈ R ⟨ 𝑦 , 0R ⟩ = 𝐴 ↔ ∃ 𝑦 ( 𝑦 ∈ R ∧ ⟨ 𝑦 , 0R ⟩ = 𝐴 ) )
3 1 2 bitri ⊢ ( 𝐴 ∈ ℝ ↔ ∃ 𝑦 ( 𝑦 ∈ R ∧ ⟨ 𝑦 , 0R ⟩ = 𝐴 ) )
4 neeq1 ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐴 → ( ⟨ 𝑦 , 0R ⟩ ≠ 0 ↔ 𝐴 ≠ 0 ) )
5 oveq1 ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐴 → ( ⟨ 𝑦 , 0R ⟩ · 𝑥 ) = ( 𝐴 · 𝑥 ) )
6 5 eqeq1d ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐴 → ( ( ⟨ 𝑦 , 0R ⟩ · 𝑥 ) = 1 ↔ ( 𝐴 · 𝑥 ) = 1 ) )
7 6 rexbidv ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐴 → ( ∃ 𝑥 ∈ ℝ ( ⟨ 𝑦 , 0R ⟩ · 𝑥 ) = 1 ↔ ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 ) )
8 4 7 imbi12d ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐴 → ( ( ⟨ 𝑦 , 0R ⟩ ≠ 0 → ∃ 𝑥 ∈ ℝ ( ⟨ 𝑦 , 0R ⟩ · 𝑥 ) = 1 ) ↔ ( 𝐴 ≠ 0 → ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 ) ) )
9 df-0 ⊢ 0 = ⟨ 0R , 0R ⟩
10 9 eqeq2i ⊢ ( ⟨ 𝑦 , 0R ⟩ = 0 ↔ ⟨ 𝑦 , 0R ⟩ = ⟨ 0R , 0R ⟩ )
11 vex ⊢ 𝑦 ∈ V
12 11 eqresr ⊢ ( ⟨ 𝑦 , 0R ⟩ = ⟨ 0R , 0R ⟩ ↔ 𝑦 = 0R )
13 10 12 bitri ⊢ ( ⟨ 𝑦 , 0R ⟩ = 0 ↔ 𝑦 = 0R )
14 13 necon3bii ⊢ ( ⟨ 𝑦 , 0R ⟩ ≠ 0 ↔ 𝑦 ≠ 0R )
15 recexsr ⊢ ( ( 𝑦 ∈ R ∧ 𝑦 ≠ 0R ) → ∃ 𝑧 ∈ R ( 𝑦 ·R 𝑧 ) = 1R )
16 15 ex ⊢ ( 𝑦 ∈ R → ( 𝑦 ≠ 0R → ∃ 𝑧 ∈ R ( 𝑦 ·R 𝑧 ) = 1R ) )
17 opelreal ⊢ ( ⟨ 𝑧 , 0R ⟩ ∈ ℝ ↔ 𝑧 ∈ R )
18 17 anbi1i ⊢ ( ( ⟨ 𝑧 , 0R ⟩ ∈ ℝ ∧ ( ⟨ 𝑦 , 0R ⟩ · ⟨ 𝑧 , 0R ⟩ ) = 1 ) ↔ ( 𝑧 ∈ R ∧ ( ⟨ 𝑦 , 0R ⟩ · ⟨ 𝑧 , 0R ⟩ ) = 1 ) )
19 mulresr ⊢ ( ( 𝑦 ∈ R ∧ 𝑧 ∈ R ) → ( ⟨ 𝑦 , 0R ⟩ · ⟨ 𝑧 , 0R ⟩ ) = ⟨ ( 𝑦 ·R 𝑧 ) , 0R ⟩ )
20 19 eqeq1d ⊢ ( ( 𝑦 ∈ R ∧ 𝑧 ∈ R ) → ( ( ⟨ 𝑦 , 0R ⟩ · ⟨ 𝑧 , 0R ⟩ ) = 1 ↔ ⟨ ( 𝑦 ·R 𝑧 ) , 0R ⟩ = 1 ) )
21 df-1 ⊢ 1 = ⟨ 1R , 0R ⟩
22 21 eqeq2i ⊢ ( ⟨ ( 𝑦 ·R 𝑧 ) , 0R ⟩ = 1 ↔ ⟨ ( 𝑦 ·R 𝑧 ) , 0R ⟩ = ⟨ 1R , 0R ⟩ )
23 ovex ⊢ ( 𝑦 ·R 𝑧 ) ∈ V
24 23 eqresr ⊢ ( ⟨ ( 𝑦 ·R 𝑧 ) , 0R ⟩ = ⟨ 1R , 0R ⟩ ↔ ( 𝑦 ·R 𝑧 ) = 1R )
25 22 24 bitri ⊢ ( ⟨ ( 𝑦 ·R 𝑧 ) , 0R ⟩ = 1 ↔ ( 𝑦 ·R 𝑧 ) = 1R )
26 20 25 bitrdi ⊢ ( ( 𝑦 ∈ R ∧ 𝑧 ∈ R ) → ( ( ⟨ 𝑦 , 0R ⟩ · ⟨ 𝑧 , 0R ⟩ ) = 1 ↔ ( 𝑦 ·R 𝑧 ) = 1R ) )
27 26 pm5.32da ⊢ ( 𝑦 ∈ R → ( ( 𝑧 ∈ R ∧ ( ⟨ 𝑦 , 0R ⟩ · ⟨ 𝑧 , 0R ⟩ ) = 1 ) ↔ ( 𝑧 ∈ R ∧ ( 𝑦 ·R 𝑧 ) = 1R ) ) )
28 18 27 bitrid ⊢ ( 𝑦 ∈ R → ( ( ⟨ 𝑧 , 0R ⟩ ∈ ℝ ∧ ( ⟨ 𝑦 , 0R ⟩ · ⟨ 𝑧 , 0R ⟩ ) = 1 ) ↔ ( 𝑧 ∈ R ∧ ( 𝑦 ·R 𝑧 ) = 1R ) ) )
29 oveq2 ⊢ ( 𝑥 = ⟨ 𝑧 , 0R ⟩ → ( ⟨ 𝑦 , 0R ⟩ · 𝑥 ) = ( ⟨ 𝑦 , 0R ⟩ · ⟨ 𝑧 , 0R ⟩ ) )
30 29 eqeq1d ⊢ ( 𝑥 = ⟨ 𝑧 , 0R ⟩ → ( ( ⟨ 𝑦 , 0R ⟩ · 𝑥 ) = 1 ↔ ( ⟨ 𝑦 , 0R ⟩ · ⟨ 𝑧 , 0R ⟩ ) = 1 ) )
31 30 rspcev ⊢ ( ( ⟨ 𝑧 , 0R ⟩ ∈ ℝ ∧ ( ⟨ 𝑦 , 0R ⟩ · ⟨ 𝑧 , 0R ⟩ ) = 1 ) → ∃ 𝑥 ∈ ℝ ( ⟨ 𝑦 , 0R ⟩ · 𝑥 ) = 1 )
32 28 31 biimtrrdi ⊢ ( 𝑦 ∈ R → ( ( 𝑧 ∈ R ∧ ( 𝑦 ·R 𝑧 ) = 1R ) → ∃ 𝑥 ∈ ℝ ( ⟨ 𝑦 , 0R ⟩ · 𝑥 ) = 1 ) )
33 32 expd ⊢ ( 𝑦 ∈ R → ( 𝑧 ∈ R → ( ( 𝑦 ·R 𝑧 ) = 1R → ∃ 𝑥 ∈ ℝ ( ⟨ 𝑦 , 0R ⟩ · 𝑥 ) = 1 ) ) )
34 33 rexlimdv ⊢ ( 𝑦 ∈ R → ( ∃ 𝑧 ∈ R ( 𝑦 ·R 𝑧 ) = 1R → ∃ 𝑥 ∈ ℝ ( ⟨ 𝑦 , 0R ⟩ · 𝑥 ) = 1 ) )
35 16 34 syld ⊢ ( 𝑦 ∈ R → ( 𝑦 ≠ 0R → ∃ 𝑥 ∈ ℝ ( ⟨ 𝑦 , 0R ⟩ · 𝑥 ) = 1 ) )
36 14 35 biimtrid ⊢ ( 𝑦 ∈ R → ( ⟨ 𝑦 , 0R ⟩ ≠ 0 → ∃ 𝑥 ∈ ℝ ( ⟨ 𝑦 , 0R ⟩ · 𝑥 ) = 1 ) )
37 3 8 36 gencl ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ≠ 0 → ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 ) )
38 37 imp ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 )