MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axrrecex Structured version   Visualization version   GIF version

Theorem axrrecex 9672
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 9696. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
Assertion
Ref Expression
axrrecex ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)
Distinct variable group:   𝑥,𝐴

Proof of Theorem axrrecex
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elreal 9640 . . . 4 (𝐴 ∈ ℝ ↔ ∃𝑦R𝑦, 0R⟩ = 𝐴)
2 df-rex 2797 . . . 4 (∃𝑦R𝑦, 0R⟩ = 𝐴 ↔ ∃𝑦(𝑦R ∧ ⟨𝑦, 0R⟩ = 𝐴))
31, 2bitri 259 . . 3 (𝐴 ∈ ℝ ↔ ∃𝑦(𝑦R ∧ ⟨𝑦, 0R⟩ = 𝐴))
4 neeq1 2739 . . . 4 (⟨𝑦, 0R⟩ = 𝐴 → (⟨𝑦, 0R⟩ ≠ 0 ↔ 𝐴 ≠ 0))
5 oveq1 6370 . . . . . 6 (⟨𝑦, 0R⟩ = 𝐴 → (⟨𝑦, 0R⟩ · 𝑥) = (𝐴 · 𝑥))
65eqeq1d 2507 . . . . 5 (⟨𝑦, 0R⟩ = 𝐴 → ((⟨𝑦, 0R⟩ · 𝑥) = 1 ↔ (𝐴 · 𝑥) = 1))
76rexbidv 2927 . . . 4 (⟨𝑦, 0R⟩ = 𝐴 → (∃𝑥 ∈ ℝ (⟨𝑦, 0R⟩ · 𝑥) = 1 ↔ ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1))
84, 7imbi12d 329 . . 3 (⟨𝑦, 0R⟩ = 𝐴 → ((⟨𝑦, 0R⟩ ≠ 0 → ∃𝑥 ∈ ℝ (⟨𝑦, 0R⟩ · 𝑥) = 1) ↔ (𝐴 ≠ 0 → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)))
9 df-0 9631 . . . . . . 7 0 = ⟨0R, 0R
109eqeq2i 2517 . . . . . 6 (⟨𝑦, 0R⟩ = 0 ↔ ⟨𝑦, 0R⟩ = ⟨0R, 0R⟩)
11 vex 3069 . . . . . . 7 𝑦 ∈ V
1211eqresr 9646 . . . . . 6 (⟨𝑦, 0R⟩ = ⟨0R, 0R⟩ ↔ 𝑦 = 0R)
1310, 12bitri 259 . . . . 5 (⟨𝑦, 0R⟩ = 0 ↔ 𝑦 = 0R)
1413necon3bii 2729 . . . 4 (⟨𝑦, 0R⟩ ≠ 0 ↔ 𝑦 ≠ 0R)
15 recexsr 9616 . . . . . 6 ((𝑦R𝑦 ≠ 0R) → ∃𝑧R (𝑦 ·R 𝑧) = 1R)
1615ex 443 . . . . 5 (𝑦R → (𝑦 ≠ 0R → ∃𝑧R (𝑦 ·R 𝑧) = 1R))
17 opelreal 9639 . . . . . . . . . 10 (⟨𝑧, 0R⟩ ∈ ℝ ↔ 𝑧R)
1817anbi1i 718 . . . . . . . . 9 ((⟨𝑧, 0R⟩ ∈ ℝ ∧ (⟨𝑦, 0R⟩ · ⟨𝑧, 0R⟩) = 1) ↔ (𝑧R ∧ (⟨𝑦, 0R⟩ · ⟨𝑧, 0R⟩) = 1))
19 mulresr 9648 . . . . . . . . . . . 12 ((𝑦R𝑧R) → (⟨𝑦, 0R⟩ · ⟨𝑧, 0R⟩) = ⟨(𝑦 ·R 𝑧), 0R⟩)
2019eqeq1d 2507 . . . . . . . . . . 11 ((𝑦R𝑧R) → ((⟨𝑦, 0R⟩ · ⟨𝑧, 0R⟩) = 1 ↔ ⟨(𝑦 ·R 𝑧), 0R⟩ = 1))
21 df-1 9632 . . . . . . . . . . . . 13 1 = ⟨1R, 0R
2221eqeq2i 2517 . . . . . . . . . . . 12 (⟨(𝑦 ·R 𝑧), 0R⟩ = 1 ↔ ⟨(𝑦 ·R 𝑧), 0R⟩ = ⟨1R, 0R⟩)
23 ovex 6391 . . . . . . . . . . . . 13 (𝑦 ·R 𝑧) ∈ V
2423eqresr 9646 . . . . . . . . . . . 12 (⟨(𝑦 ·R 𝑧), 0R⟩ = ⟨1R, 0R⟩ ↔ (𝑦 ·R 𝑧) = 1R)
2522, 24bitri 259 . . . . . . . . . . 11 (⟨(𝑦 ·R 𝑧), 0R⟩ = 1 ↔ (𝑦 ·R 𝑧) = 1R)
2620, 25syl6bb 271 . . . . . . . . . 10 ((𝑦R𝑧R) → ((⟨𝑦, 0R⟩ · ⟨𝑧, 0R⟩) = 1 ↔ (𝑦 ·R 𝑧) = 1R))
2726pm5.32da 662 . . . . . . . . 9 (𝑦R → ((𝑧R ∧ (⟨𝑦, 0R⟩ · ⟨𝑧, 0R⟩) = 1) ↔ (𝑧R ∧ (𝑦 ·R 𝑧) = 1R)))
2818, 27syl5bb 267 . . . . . . . 8 (𝑦R → ((⟨𝑧, 0R⟩ ∈ ℝ ∧ (⟨𝑦, 0R⟩ · ⟨𝑧, 0R⟩) = 1) ↔ (𝑧R ∧ (𝑦 ·R 𝑧) = 1R)))
29 oveq2 6371 . . . . . . . . . 10 (𝑥 = ⟨𝑧, 0R⟩ → (⟨𝑦, 0R⟩ · 𝑥) = (⟨𝑦, 0R⟩ · ⟨𝑧, 0R⟩))
3029eqeq1d 2507 . . . . . . . . 9 (𝑥 = ⟨𝑧, 0R⟩ → ((⟨𝑦, 0R⟩ · 𝑥) = 1 ↔ (⟨𝑦, 0R⟩ · ⟨𝑧, 0R⟩) = 1))
3130rspcev 3171 . . . . . . . 8 ((⟨𝑧, 0R⟩ ∈ ℝ ∧ (⟨𝑦, 0R⟩ · ⟨𝑧, 0R⟩) = 1) → ∃𝑥 ∈ ℝ (⟨𝑦, 0R⟩ · 𝑥) = 1)
3228, 31syl6bir 239 . . . . . . 7 (𝑦R → ((𝑧R ∧ (𝑦 ·R 𝑧) = 1R) → ∃𝑥 ∈ ℝ (⟨𝑦, 0R⟩ · 𝑥) = 1))
3332expd 445 . . . . . 6 (𝑦R → (𝑧R → ((𝑦 ·R 𝑧) = 1R → ∃𝑥 ∈ ℝ (⟨𝑦, 0R⟩ · 𝑥) = 1)))
3433rexlimdv 2905 . . . . 5 (𝑦R → (∃𝑧R (𝑦 ·R 𝑧) = 1R → ∃𝑥 ∈ ℝ (⟨𝑦, 0R⟩ · 𝑥) = 1))
3516, 34syld 45 . . . 4 (𝑦R → (𝑦 ≠ 0R → ∃𝑥 ∈ ℝ (⟨𝑦, 0R⟩ · 𝑥) = 1))
3614, 35syl5bi 227 . . 3 (𝑦R → (⟨𝑦, 0R⟩ ≠ 0 → ∃𝑥 ∈ ℝ (⟨𝑦, 0R⟩ · 𝑥) = 1))
373, 8, 36gencl 3098 . 2 (𝐴 ∈ ℝ → (𝐴 ≠ 0 → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1))
3837imp 438 1 ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 378   = wceq 1468  wex 1692  wcel 1937  wne 2675  wrex 2792  cop 4001  (class class class)co 6363  Rcnr 9375  0Rc0r 9376  1Rc1r 9377   ·R cmr 9380  cr 9623  0cc0 9624  1c1 9625   · cmul 9629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680  ax-un 6659  ax-inf2 8231
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3068  df-sbc 3292  df-csb 3386  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-int 4265  df-iun 4309  df-br 4435  df-opab 4494  df-mpt 4495  df-tr 4531  df-eprel 4791  df-id 4795  df-po 4801  df-so 4802  df-fr 4839  df-we 4841  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-pred 5431  df-ord 5477  df-on 5478  df-lim 5479  df-suc 5480  df-iota 5597  df-fun 5635  df-fn 5636  df-f 5637  df-f1 5638  df-fo 5639  df-f1o 5640  df-fv 5641  df-ov 6366  df-oprab 6367  df-mpt2 6368  df-om 6770  df-1st 6870  df-2nd 6871  df-wrecs 7105  df-recs 7167  df-rdg 7205  df-1o 7259  df-oadd 7263  df-omul 7264  df-er 7440  df-ec 7442  df-qs 7446  df-ni 9382  df-pli 9383  df-mi 9384  df-lti 9385  df-plpq 9418  df-mpq 9419  df-ltpq 9420  df-enq 9421  df-nq 9422  df-erq 9423  df-plq 9424  df-mq 9425  df-1nq 9426  df-rq 9427  df-ltnq 9428  df-np 9491  df-1p 9492  df-plp 9493  df-mp 9494  df-ltp 9495  df-enr 9565  df-nr 9566  df-plr 9567  df-mr 9568  df-ltr 9569  df-0r 9570  df-1r 9571  df-m1r 9572  df-c 9630  df-0 9631  df-1 9632  df-r 9634  df-mul 9636
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator