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

Theorem nfsum 15038
 Description: Bound-variable hypothesis builder for sum: if 𝑥 is (effectively) not free in 𝐴 and 𝐵, it is not free in Σ𝑘 ∈ 𝐴𝐵. Version of nfsum 15038 with a disjoint variable condition, which does not require ax-13 2391. (Contributed by NM, 11-Dec-2005.) (Revised by Gino Giotto, 24-Feb-2024.)
Hypotheses
Ref Expression
nfsum.1 𝑥𝐴
nfsum.2 𝑥𝐵
Assertion
Ref Expression
nfsum 𝑥Σ𝑘𝐴 𝐵
Distinct variable group:   𝑥,𝑘
Allowed substitution hints:   𝐴(𝑥,𝑘)   𝐵(𝑥,𝑘)

Proof of Theorem nfsum
Dummy variables 𝑓 𝑚 𝑛 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sum 15034 . 2 Σ𝑘𝐴 𝐵 = (℩𝑧(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
2 nfcv 2979 . . . . 5 𝑥
3 nfsum.1 . . . . . . 7 𝑥𝐴
4 nfcv 2979 . . . . . . 7 𝑥(ℤ𝑚)
53, 4nfss 3934 . . . . . 6 𝑥 𝐴 ⊆ (ℤ𝑚)
6 nfcv 2979 . . . . . . . 8 𝑥𝑚
7 nfcv 2979 . . . . . . . 8 𝑥 +
83nfcri 2967 . . . . . . . . . 10 𝑥 𝑛𝐴
9 nfcv 2979 . . . . . . . . . . 11 𝑥𝑛
10 nfsum.2 . . . . . . . . . . 11 𝑥𝐵
119, 10nfcsbw 3881 . . . . . . . . . 10 𝑥𝑛 / 𝑘𝐵
12 nfcv 2979 . . . . . . . . . 10 𝑥0
138, 11, 12nfif 4468 . . . . . . . . 9 𝑥if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)
142, 13nfmpt 5139 . . . . . . . 8 𝑥(𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))
156, 7, 14nfseq 13374 . . . . . . 7 𝑥seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)))
16 nfcv 2979 . . . . . . 7 𝑥
17 nfcv 2979 . . . . . . 7 𝑥𝑧
1815, 16, 17nfbr 5089 . . . . . 6 𝑥seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧
195, 18nfan 1900 . . . . 5 𝑥(𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧)
202, 19nfrex 3295 . . . 4 𝑥𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧)
21 nfcv 2979 . . . . 5 𝑥
22 nfcv 2979 . . . . . . . 8 𝑥𝑓
23 nfcv 2979 . . . . . . . 8 𝑥(1...𝑚)
2422, 23, 3nff1o 6595 . . . . . . 7 𝑥 𝑓:(1...𝑚)–1-1-onto𝐴
25 nfcv 2979 . . . . . . . . . 10 𝑥1
26 nfcv 2979 . . . . . . . . . . . 12 𝑥(𝑓𝑛)
2726, 10nfcsbw 3881 . . . . . . . . . . 11 𝑥(𝑓𝑛) / 𝑘𝐵
2821, 27nfmpt 5139 . . . . . . . . . 10 𝑥(𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
2925, 7, 28nfseq 13374 . . . . . . . . 9 𝑥seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))
3029, 6nffv 6662 . . . . . . . 8 𝑥(seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3130nfeq2 2996 . . . . . . 7 𝑥 𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3224, 31nfan 1900 . . . . . 6 𝑥(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3332nfex 2344 . . . . 5 𝑥𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3421, 33nfrex 3295 . . . 4 𝑥𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3520, 34nfor 1905 . . 3 𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
3635nfiotaw 6297 . 2 𝑥(℩𝑧(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
371, 36nfcxfr 2977 1 𝑥Σ𝑘𝐴 𝐵
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   ∨ wo 844   = wceq 1538  ∃wex 1781   ∈ wcel 2114  Ⅎwnfc 2960  ∃wrex 3131  ⦋csb 3855   ⊆ wss 3908  ifcif 4439   class class class wbr 5042   ↦ cmpt 5122  ℩cio 6291  –1-1-onto→wf1o 6333  ‘cfv 6334  (class class class)co 7140  0cc0 10526  1c1 10527   + caddc 10529  ℕcn 11625  ℤcz 11969  ℤ≥cuz 12231  ...cfz 12885  seqcseq 13364   ⇝ cli 14832  Σcsu 15033 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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-mpt 5123  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-ov 7143  df-oprab 7144  df-mpo 7145  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-seq 13365  df-sum 15034 This theorem is referenced by:  fsum2dlem  15116  fsumcom2  15120  fsumrlim  15157  fsumiun  15167  fsumcn  23473  fsum2cn  23474  nfitg1  24375  nfitg  24376  dvmptfsum  24576  fsumdvdscom  25768  binomcxplemdvsum  40993  binomcxplemnotnn0  40994  fsumcnf  41584  fsumiunss  42156  dvmptfprod  42526  sge0iunmptlemre  42993
 Copyright terms: Public domain W3C validator