Mathbox for Jim Kingdon |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > Mathboxes > nconstwlpolem0 | GIF version |
Description: Lemma for nconstwlpo 13599. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
Ref | Expression |
---|---|
nconstwlpolem0.g | ⊢ (𝜑 → 𝐺:ℕ⟶{0, 1}) |
nconstwlpolem0.a | ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐺‘𝑖)) |
nconstwlpolem0.0 | ⊢ (𝜑 → ∀𝑥 ∈ ℕ (𝐺‘𝑥) = 0) |
Ref | Expression |
---|---|
nconstwlpolem0 | ⊢ (𝜑 → 𝐴 = 0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nconstwlpolem0.a | . . 3 ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐺‘𝑖)) | |
2 | fveqeq2 5474 | . . . . . . 7 ⊢ (𝑥 = 𝑖 → ((𝐺‘𝑥) = 0 ↔ (𝐺‘𝑖) = 0)) | |
3 | nconstwlpolem0.0 | . . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ ℕ (𝐺‘𝑥) = 0) | |
4 | 3 | adantr 274 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ∀𝑥 ∈ ℕ (𝐺‘𝑥) = 0) |
5 | simpr 109 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ) | |
6 | 2, 4, 5 | rspcdva 2821 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐺‘𝑖) = 0) |
7 | 6 | oveq2d 5834 | . . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐺‘𝑖)) = ((1 / (2↑𝑖)) · 0)) |
8 | 2nn 8977 | . . . . . . . . . 10 ⊢ 2 ∈ ℕ | |
9 | 8 | a1i 9 | . . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 2 ∈ ℕ) |
10 | 5 | nnnn0d 9126 | . . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ0) |
11 | 9, 10 | nnexpcld 10555 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (2↑𝑖) ∈ ℕ) |
12 | 11 | nnrecred 8863 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ) |
13 | 12 | recnd 7889 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℂ) |
14 | 13 | mul01d 8251 | . . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · 0) = 0) |
15 | 7, 14 | eqtrd 2190 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐺‘𝑖)) = 0) |
16 | 15 | sumeq2dv 11247 | . . 3 ⊢ (𝜑 → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐺‘𝑖)) = Σ𝑖 ∈ ℕ 0) |
17 | 1, 16 | syl5eq 2202 | . 2 ⊢ (𝜑 → 𝐴 = Σ𝑖 ∈ ℕ 0) |
18 | 1z 9176 | . . . . 5 ⊢ 1 ∈ ℤ | |
19 | nnuz 9457 | . . . . . 6 ⊢ ℕ = (ℤ≥‘1) | |
20 | 19 | eqimssi 3184 | . . . . 5 ⊢ ℕ ⊆ (ℤ≥‘1) |
21 | elnnuz 9458 | . . . . . . . . 9 ⊢ (𝑗 ∈ ℕ ↔ 𝑗 ∈ (ℤ≥‘1)) | |
22 | 21 | biimpri 132 | . . . . . . . 8 ⊢ (𝑗 ∈ (ℤ≥‘1) → 𝑗 ∈ ℕ) |
23 | 22 | orcd 723 | . . . . . . 7 ⊢ (𝑗 ∈ (ℤ≥‘1) → (𝑗 ∈ ℕ ∨ ¬ 𝑗 ∈ ℕ)) |
24 | df-dc 821 | . . . . . . 7 ⊢ (DECID 𝑗 ∈ ℕ ↔ (𝑗 ∈ ℕ ∨ ¬ 𝑗 ∈ ℕ)) | |
25 | 23, 24 | sylibr 133 | . . . . . 6 ⊢ (𝑗 ∈ (ℤ≥‘1) → DECID 𝑗 ∈ ℕ) |
26 | 25 | rgen 2510 | . . . . 5 ⊢ ∀𝑗 ∈ (ℤ≥‘1)DECID 𝑗 ∈ ℕ |
27 | 18, 20, 26 | 3pm3.2i 1160 | . . . 4 ⊢ (1 ∈ ℤ ∧ ℕ ⊆ (ℤ≥‘1) ∧ ∀𝑗 ∈ (ℤ≥‘1)DECID 𝑗 ∈ ℕ) |
28 | 27 | orci 721 | . . 3 ⊢ ((1 ∈ ℤ ∧ ℕ ⊆ (ℤ≥‘1) ∧ ∀𝑗 ∈ (ℤ≥‘1)DECID 𝑗 ∈ ℕ) ∨ ℕ ∈ Fin) |
29 | isumz 11268 | . . 3 ⊢ (((1 ∈ ℤ ∧ ℕ ⊆ (ℤ≥‘1) ∧ ∀𝑗 ∈ (ℤ≥‘1)DECID 𝑗 ∈ ℕ) ∨ ℕ ∈ Fin) → Σ𝑖 ∈ ℕ 0 = 0) | |
30 | 28, 29 | ax-mp 5 | . 2 ⊢ Σ𝑖 ∈ ℕ 0 = 0 |
31 | 17, 30 | eqtrdi 2206 | 1 ⊢ (𝜑 → 𝐴 = 0) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ∨ wo 698 DECID wdc 820 ∧ w3a 963 = wceq 1335 ∈ wcel 2128 ∀wral 2435 ⊆ wss 3102 {cpr 3561 ⟶wf 5163 ‘cfv 5167 (class class class)co 5818 Fincfn 6678 0cc0 7715 1c1 7716 · cmul 7720 / cdiv 8528 ℕcn 8816 2c2 8867 ℤcz 9150 ℤ≥cuz 9422 ↑cexp 10400 Σcsu 11232 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-13 2130 ax-14 2131 ax-ext 2139 ax-coll 4079 ax-sep 4082 ax-nul 4090 ax-pow 4134 ax-pr 4168 ax-un 4392 ax-setind 4494 ax-iinf 4545 ax-cnex 7806 ax-resscn 7807 ax-1cn 7808 ax-1re 7809 ax-icn 7810 ax-addcl 7811 ax-addrcl 7812 ax-mulcl 7813 ax-mulrcl 7814 ax-addcom 7815 ax-mulcom 7816 ax-addass 7817 ax-mulass 7818 ax-distr 7819 ax-i2m1 7820 ax-0lt1 7821 ax-1rid 7822 ax-0id 7823 ax-rnegex 7824 ax-precex 7825 ax-cnre 7826 ax-pre-ltirr 7827 ax-pre-ltwlin 7828 ax-pre-lttrn 7829 ax-pre-apti 7830 ax-pre-ltadd 7831 ax-pre-mulgt0 7832 ax-pre-mulext 7833 ax-arch 7834 ax-caucvg 7835 |
This theorem depends on definitions: df-bi 116 df-dc 821 df-3or 964 df-3an 965 df-tru 1338 df-fal 1341 df-nf 1441 df-sb 1743 df-eu 2009 df-mo 2010 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ne 2328 df-nel 2423 df-ral 2440 df-rex 2441 df-reu 2442 df-rmo 2443 df-rab 2444 df-v 2714 df-sbc 2938 df-csb 3032 df-dif 3104 df-un 3106 df-in 3108 df-ss 3115 df-nul 3395 df-if 3506 df-pw 3545 df-sn 3566 df-pr 3567 df-op 3569 df-uni 3773 df-int 3808 df-iun 3851 df-br 3966 df-opab 4026 df-mpt 4027 df-tr 4063 df-id 4252 df-po 4255 df-iso 4256 df-iord 4325 df-on 4327 df-ilim 4328 df-suc 4330 df-iom 4548 df-xp 4589 df-rel 4590 df-cnv 4591 df-co 4592 df-dm 4593 df-rn 4594 df-res 4595 df-ima 4596 df-iota 5132 df-fun 5169 df-fn 5170 df-f 5171 df-f1 5172 df-fo 5173 df-f1o 5174 df-fv 5175 df-isom 5176 df-riota 5774 df-ov 5821 df-oprab 5822 df-mpo 5823 df-1st 6082 df-2nd 6083 df-recs 6246 df-irdg 6311 df-frec 6332 df-1o 6357 df-oadd 6361 df-er 6473 df-en 6679 df-dom 6680 df-fin 6681 df-pnf 7897 df-mnf 7898 df-xr 7899 df-ltxr 7900 df-le 7901 df-sub 8031 df-neg 8032 df-reap 8433 df-ap 8440 df-div 8529 df-inn 8817 df-2 8875 df-3 8876 df-4 8877 df-n0 9074 df-z 9151 df-uz 9423 df-q 9511 df-rp 9543 df-fz 9895 df-fzo 10024 df-seqfrec 10327 df-exp 10401 df-ihash 10632 df-cj 10724 df-re 10725 df-im 10726 df-rsqrt 10880 df-abs 10881 df-clim 11158 df-sumdc 11233 |
This theorem is referenced by: nconstwlpolem 13598 |
Copyright terms: Public domain | W3C validator |