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 syl5bb ( 𝑦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 syl6bir ( 𝑦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 syl5bi ( 𝑦R → ( ⟨ 𝑦 , 0R ⟩ ≠ 0 → ∃ 𝑥 ∈ ℝ ( ⟨ 𝑦 , 0R ⟩ · 𝑥 ) = 1 ) )
37 3 8 36 gencl ( 𝐴 ∈ ℝ → ( 𝐴 ≠ 0 → ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 ) )
38 37 imp ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 )