HomeRelated theorems
GIF version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: Closure law for multiplication in the real subfield of complex numbers. Axiom 8 of 25 for real and complex numbers, derived from ZF set theory. |
| Ref | Expression |
|---|---|
| axmulrcl | ⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A · B) ∈ ℝ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elreal 5222 | . 2 ⊢ (A ∈ ℝ ↔ ∃x(x ∈ R ⋀ ⟨x, 0R⟩ = A)) | |
| 2 | elreal 5222 | . 2 ⊢ (B ∈ ℝ ↔ ∃y(y ∈ R ⋀ ⟨y, 0R⟩ = B)) | |
| 3 | opreq1 3953 | . . 3 ⊢ (⟨x, 0R⟩ = A → (⟨x, 0R⟩ · ⟨y, 0R⟩) = (A · ⟨y, 0R⟩)) | |
| 4 | 3 | eleq1d 1532 | . 2 ⊢ (⟨x, 0R⟩ = A → ((⟨x, 0R⟩ · ⟨y, 0R⟩) ∈ ℝ ↔ (A · ⟨y, 0R⟩) ∈ ℝ)) |
| 5 | opreq2 3954 | . . 3 ⊢ (⟨y, 0R⟩ = B → (A · ⟨y, 0R⟩) = (A · B)) | |
| 6 | 5 | eleq1d 1532 | . 2 ⊢ (⟨y, 0R⟩ = B → ((A · ⟨y, 0R⟩) ∈ ℝ ↔ (A · B) ∈ ℝ)) |
| 7 | visset 1804 | . . . 4 ⊢ y ∈ V | |
| 8 | 7 | mulresr 5229 | . . 3 ⊢ ((x ∈ R ⋀ y ∈ R) → (⟨x, 0R⟩ · ⟨y, 0R⟩) = ⟨(x ·R y), 0R⟩) |
| 9 | mulclsr 5165 | . . . 4 ⊢ ((x ∈ R ⋀ y ∈ R) → (x ·R y) ∈ R) | |
| 10 | opelreal 5221 | . . . 4 ⊢ (⟨(x ·R y), 0R⟩ ∈ ℝ ↔ (x ·R y) ∈ R) | |
| 11 | 9, 10 | sylibr 200 | . . 3 ⊢ ((x ∈ R ⋀ y ∈ R) → ⟨(x ·R y), 0R⟩ ∈ ℝ) |
| 12 | 8, 11 | eqeltrd 1540 | . 2 ⊢ ((x ∈ R ⋀ y ∈ R) → (⟨x, 0R⟩ · ⟨y, 0R⟩) ∈ ℝ) |
| 13 | 1, 2, 4, 6, 12 | 2gencl 1820 | 1 ⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A · B) ∈ ℝ) |
| Colors of variables: wff set class |
| Syntax hints: → wi 3 ⋀ wa 223 = wceq 953 ∈ wcel 955 ⟨cop 2401 (class class class)co 3948 Rcnr 4965 0Rc0r 4966 ·R cmr 4970 ℝcr 5205 · cmul 5211 |
| This theorem is referenced by: remulclt 5276 remulcl 5307 1re 5407 axmulgt0 5478 recextlem2 5656 recext 5657 lemul1t 5788 ltmul12it 5797 lemul12ait 5798 lemul12itOLD 5799 mulgt1t 5801 ltdivmult 5819 ledivmult 5820 lt2mul2divt 5822 lemuldivt 5824 ltdiv23t 5840 lediv23t 5841 avglet 5991 zmulclt 6127 qbtwnre 6216 rpmulclt 6228 reexpclt 6512 expubndt 6539 bernneq 6583 expnbndt 6585 discrlem3 6588 sqr0 6602 sqrlem5 6607 sqrlem6 6608 sqrlem12 6614 faclbnd 6882 faclbnd3 6884 faclbnd5 6890 faclbnd6 6891 facavgt 6892 climmullem4 7059 cvgcmp2clem 7118 cvgratlem1ALT 7182 cvgratlem1 7185 cvgratlem4 7188 erelem1 7261 abspef01tlub 7336 efcnlem2 7360 sin01bndlem2 7410 cos01bndlem2 7412 cos01gt0 7419 sin02gt0 7420 znnen 7445 ruclem13 7465 bl2in 7783 nmoub3i 8368 blocni 8396 ubthlem12 8471 ubthlem13 8472 ubthlem14 8473 minveclem21 8496 minveclem25 8500 minveclem26 8501 minveclem27 8502 htthlem6 8555 htthlem8 8557 sinperlem1 8605 sinq12gt0t 8625 relogexpt 8696 logexptOLD 8712 bcs2t 8970 occllem6 9094 pjthlem8 9141 pjthlem10 9143 nmopub2tALT 9750 nmfnleub2t 9766 nmophm 9876 bdophm 9877 lnopcon 9878 lnfncon 9905 cnlnadjlem2 9916 cnlnadjlem7 9921 nmopadjlem 9937 nmopcoadj 9948 branmfnt 9951 leopnmidt 9982 cdj1 10265 cdj3lem2b 10269 cdj3 10273 mslb1 10473 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-9 962 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-rep 2683 ax-sep 2693 ax-nul 2700 ax-pow 2732 ax-pr 2769 ax-un 2857 ax-inf2 4597 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 774 df-3an 775 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-ral 1641 df-rex 1642 df-reu 1643 df-rab 1644 df-v 1803 df-sbc 1932 df-csb 1992 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-pss 2045 df-nul 2271 df-if 2352 df-pw 2392 df-sn 2402 df-pr 2403 df-tp 2405 df-op 2406 df-uni 2494 df-int 2524 df-iun 2558 df-br 2610 df-opab 2657 df-tr 2671 df-eprel 2821 df-id 2824 df-po 2831 df-so 2841 df-fr 2907 df-we 2924 df-ord 2941 df-on 2942 df-lim 2943 df-suc 2944 df-om 3122 df-xp 3174 df-rel 3175 df-cnv 3176 df-co 3177 df-dm 3178 df-rn 3179 df-res 3180 df-ima 3181 df-fun 3182 df-fn 3183 df-f 3184 df-fv 3188 df-rdg 3917 df-opr 3950 df-oprab 3951 df-1st 4063 df-2nd 4064 df-1o 4117 df-oadd 4119 df-omul 4120 df-er 4245 df-ec 4247 df-qs 4250 df-ni 4972 df-pli 4973 df-mi 4974 df-lti 4975 df-plpq 5007 df-mpq 5008 df-enq 5009 df-nq 5010 df-plq 5011 df-mq 5012 df-rq 5013 df-ltq 5014 df-1q 5015 df-np 5058 df-1p 5059 df-plp 5060 df-mp 5061 df-ltp 5062 df-plpr 5136 df-mpr 5137 df-enr 5138 df-nr 5139 df-plr 5140 df-mr 5141 df-0r 5143 df-m1r 5145 df-c 5212 df-r 5216 df-mul 5218 |