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 )