![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mul02 | Structured version Visualization version GIF version |
Description: Multiplication by 0. Theorem I.6 of [Apostol] p. 18. Based on ideas by Eric Schmidt. (Contributed by NM, 10-Aug-1999.) (Revised by Scott Fenton, 3-Jan-2013.) |
Ref | Expression |
---|---|
mul02 | ⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnre 11195 | . 2 ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | |
2 | 0cn 11190 | . . . . . . 7 ⊢ 0 ∈ ℂ | |
3 | recn 11184 | . . . . . . 7 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ) | |
4 | ax-icn 11153 | . . . . . . . 8 ⊢ i ∈ ℂ | |
5 | recn 11184 | . . . . . . . 8 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ) | |
6 | mulcl 11178 | . . . . . . . 8 ⊢ ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ) | |
7 | 4, 5, 6 | sylancr 587 | . . . . . . 7 ⊢ (𝑦 ∈ ℝ → (i · 𝑦) ∈ ℂ) |
8 | adddi 11183 | . . . . . . 7 ⊢ ((0 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → (0 · (𝑥 + (i · 𝑦))) = ((0 · 𝑥) + (0 · (i · 𝑦)))) | |
9 | 2, 3, 7, 8 | mp3an3an 1467 | . . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 · (𝑥 + (i · 𝑦))) = ((0 · 𝑥) + (0 · (i · 𝑦)))) |
10 | mul02lem2 11375 | . . . . . . 7 ⊢ (𝑥 ∈ ℝ → (0 · 𝑥) = 0) | |
11 | mul12 11363 | . . . . . . . . 9 ⊢ ((0 ∈ ℂ ∧ i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (0 · (i · 𝑦)) = (i · (0 · 𝑦))) | |
12 | 2, 4, 5, 11 | mp3an12i 1465 | . . . . . . . 8 ⊢ (𝑦 ∈ ℝ → (0 · (i · 𝑦)) = (i · (0 · 𝑦))) |
13 | mul02lem2 11375 | . . . . . . . . 9 ⊢ (𝑦 ∈ ℝ → (0 · 𝑦) = 0) | |
14 | 13 | oveq2d 7410 | . . . . . . . 8 ⊢ (𝑦 ∈ ℝ → (i · (0 · 𝑦)) = (i · 0)) |
15 | 12, 14 | eqtrd 2772 | . . . . . . 7 ⊢ (𝑦 ∈ ℝ → (0 · (i · 𝑦)) = (i · 0)) |
16 | 10, 15 | oveqan12d 7413 | . . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((0 · 𝑥) + (0 · (i · 𝑦))) = (0 + (i · 0))) |
17 | 9, 16 | eqtrd 2772 | . . . . 5 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 · (𝑥 + (i · 𝑦))) = (0 + (i · 0))) |
18 | cnre 11195 | . . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 0 = (𝑥 + (i · 𝑦))) | |
19 | 2, 18 | ax-mp 5 | . . . . . . 7 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 0 = (𝑥 + (i · 𝑦)) |
20 | oveq2 7402 | . . . . . . . . . 10 ⊢ (0 = (𝑥 + (i · 𝑦)) → (0 · 0) = (0 · (𝑥 + (i · 𝑦)))) | |
21 | 20 | eqeq1d 2734 | . . . . . . . . 9 ⊢ (0 = (𝑥 + (i · 𝑦)) → ((0 · 0) = (0 + (i · 0)) ↔ (0 · (𝑥 + (i · 𝑦))) = (0 + (i · 0)))) |
22 | 17, 21 | syl5ibrcom 246 | . . . . . . . 8 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 = (𝑥 + (i · 𝑦)) → (0 · 0) = (0 + (i · 0)))) |
23 | 22 | rexlimivv 3199 | . . . . . . 7 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 0 = (𝑥 + (i · 𝑦)) → (0 · 0) = (0 + (i · 0))) |
24 | 19, 23 | ax-mp 5 | . . . . . 6 ⊢ (0 · 0) = (0 + (i · 0)) |
25 | 0re 11200 | . . . . . . 7 ⊢ 0 ∈ ℝ | |
26 | mul02lem2 11375 | . . . . . . 7 ⊢ (0 ∈ ℝ → (0 · 0) = 0) | |
27 | 25, 26 | ax-mp 5 | . . . . . 6 ⊢ (0 · 0) = 0 |
28 | 24, 27 | eqtr3i 2762 | . . . . 5 ⊢ (0 + (i · 0)) = 0 |
29 | 17, 28 | eqtrdi 2788 | . . . 4 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 · (𝑥 + (i · 𝑦))) = 0) |
30 | oveq2 7402 | . . . . 5 ⊢ (𝐴 = (𝑥 + (i · 𝑦)) → (0 · 𝐴) = (0 · (𝑥 + (i · 𝑦)))) | |
31 | 30 | eqeq1d 2734 | . . . 4 ⊢ (𝐴 = (𝑥 + (i · 𝑦)) → ((0 · 𝐴) = 0 ↔ (0 · (𝑥 + (i · 𝑦))) = 0)) |
32 | 29, 31 | syl5ibrcom 246 | . . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = (𝑥 + (i · 𝑦)) → (0 · 𝐴) = 0)) |
33 | 32 | rexlimivv 3199 | . 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)) → (0 · 𝐴) = 0) |
34 | 1, 33 | syl 17 | 1 ⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∃wrex 3070 (class class class)co 7394 ℂcc 11092 ℝcr 11093 0cc0 11094 ici 11096 + caddc 11097 · cmul 11099 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5293 ax-nul 5300 ax-pow 5357 ax-pr 5421 ax-un 7709 ax-resscn 11151 ax-1cn 11152 ax-icn 11153 ax-addcl 11154 ax-addrcl 11155 ax-mulcl 11156 ax-mulrcl 11157 ax-mulcom 11158 ax-addass 11159 ax-mulass 11160 ax-distr 11161 ax-i2m1 11162 ax-1ne0 11163 ax-1rid 11164 ax-rnegex 11165 ax-rrecex 11166 ax-cnre 11167 ax-pre-lttri 11168 ax-pre-lttrn 11169 ax-pre-ltadd 11170 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4320 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-br 5143 df-opab 5205 df-mpt 5226 df-id 5568 df-po 5582 df-so 5583 df-xp 5676 df-rel 5677 df-cnv 5678 df-co 5679 df-dm 5680 df-rn 5681 df-res 5682 df-ima 5683 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-ov 7397 df-er 8688 df-en 8925 df-dom 8926 df-sdom 8927 df-pnf 11234 df-mnf 11235 df-ltxr 11237 |
This theorem is referenced by: mul01 11377 cnegex2 11380 mul02i 11387 mul02d 11396 bcval5 14262 fsumconst 15720 demoivreALT 16128 nnnn0modprm0 16723 cnfldmulg 20913 itg2mulc 25196 dvcmulf 25393 coe0 25701 plymul0or 25725 sineq0 25964 jensen 26422 musumsum 26625 lgsne0 26767 brbtwn2 28092 ax5seglem4 28119 axeuclidlem 28149 axeuclid 28150 axcontlem2 28152 axcontlem4 28154 eulerpartlemb 33262 expgrowth 42929 dvcosax 44479 |
Copyright terms: Public domain | W3C validator |