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

Theorem nfsum 15535
Description: Bound-variable hypothesis builder for sum: if 𝑥 is (effectively) not free in 𝐴 and 𝐵, it is not free in Σ𝑘𝐴𝐵. Version of nfsum 15535 with a disjoint variable condition, which does not require ax-13 2372. (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 15531 . 2 Σ𝑘𝐴 𝐵 = (℩𝑧(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
2 nfcv 2906 . . . . 5 𝑥
3 nfsum.1 . . . . . . 7 𝑥𝐴
4 nfcv 2906 . . . . . . 7 𝑥(ℤ𝑚)
53, 4nfss 3935 . . . . . 6 𝑥 𝐴 ⊆ (ℤ𝑚)
6 nfcv 2906 . . . . . . . 8 𝑥𝑚
7 nfcv 2906 . . . . . . . 8 𝑥 +
83nfcri 2893 . . . . . . . . . 10 𝑥 𝑛𝐴
9 nfcv 2906 . . . . . . . . . . 11 𝑥𝑛
10 nfsum.2 . . . . . . . . . . 11 𝑥𝐵
119, 10nfcsbw 3881 . . . . . . . . . 10 𝑥𝑛 / 𝑘𝐵
12 nfcv 2906 . . . . . . . . . 10 𝑥0
138, 11, 12nfif 4515 . . . . . . . . 9 𝑥if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)
142, 13nfmpt 5211 . . . . . . . 8 𝑥(𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))
156, 7, 14nfseq 13871 . . . . . . 7 𝑥seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)))
16 nfcv 2906 . . . . . . 7 𝑥
17 nfcv 2906 . . . . . . 7 𝑥𝑧
1815, 16, 17nfbr 5151 . . . . . 6 𝑥seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧
195, 18nfan 1903 . . . . 5 𝑥(𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧)
202, 19nfrexw 3295 . . . 4 𝑥𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧)
21 nfcv 2906 . . . . 5 𝑥
22 nfcv 2906 . . . . . . . 8 𝑥𝑓
23 nfcv 2906 . . . . . . . 8 𝑥(1...𝑚)
2422, 23, 3nff1o 6780 . . . . . . 7 𝑥 𝑓:(1...𝑚)–1-1-onto𝐴
25 nfcv 2906 . . . . . . . . . 10 𝑥1
26 nfcv 2906 . . . . . . . . . . . 12 𝑥(𝑓𝑛)
2726, 10nfcsbw 3881 . . . . . . . . . . 11 𝑥(𝑓𝑛) / 𝑘𝐵
2821, 27nfmpt 5211 . . . . . . . . . 10 𝑥(𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
2925, 7, 28nfseq 13871 . . . . . . . . 9 𝑥seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))
3029, 6nffv 6850 . . . . . . . 8 𝑥(seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3130nfeq2 2923 . . . . . . 7 𝑥 𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3224, 31nfan 1903 . . . . . 6 𝑥(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3332nfex 2319 . . . . 5 𝑥𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3421, 33nfrexw 3295 . . . 4 𝑥𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3520, 34nfor 1908 . . 3 𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
3635nfiotaw 6450 . 2 𝑥(℩𝑧(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
371, 36nfcxfr 2904 1 𝑥Σ𝑘𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wa 397  wo 846   = wceq 1542  wex 1782  wcel 2107  wnfc 2886  wrex 3072  csb 3854  wss 3909  ifcif 4485   class class class wbr 5104  cmpt 5187  cio 6444  1-1-ontowf1o 6493  cfv 6494  (class class class)co 7352  0cc0 11010  1c1 11011   + caddc 11013  cn 12112  cz 12458  cuz 12722  ...cfz 13379  seqcseq 13861  cli 15326  Σcsu 15530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-opab 5167  df-mpt 5188  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6252  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-ov 7355  df-oprab 7356  df-mpo 7357  df-frecs 8205  df-wrecs 8236  df-recs 8310  df-rdg 8349  df-seq 13862  df-sum 15531
This theorem is referenced by:  fsum2dlem  15615  fsumcom2  15619  fsumrlim  15656  fsumiun  15666  fsumcn  24185  fsum2cn  24186  nfitg1  25090  nfitg  25091  dvmptfsum  25291  fsumdvdscom  26486  binomcxplemdvsum  42540  binomcxplemnotnn0  42541  fsumcnf  43131  fsumiunss  43711  dvmptfprod  44081  sge0iunmptlemre  44551
  Copyright terms: Public domain W3C validator