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

Theorem nfsumOLD 15048
 Description: Obsolete version of nfsum 15047 as of 24-Feb-2024. Bound-variable hypothesis builder for sum: if 𝑥 is (effectively) not free in 𝐴 and 𝐵, it is not free in Σ𝑘 ∈ 𝐴𝐵. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
nfsumOLD.1 𝑥𝐴
nfsumOLD.2 𝑥𝐵
Assertion
Ref Expression
nfsumOLD 𝑥Σ𝑘𝐴 𝐵

Proof of Theorem nfsumOLD
Dummy variables 𝑓 𝑚 𝑛 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sum 15043 . 2 Σ𝑘𝐴 𝐵 = (℩𝑧(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
2 nfcv 2982 . . . . 5 𝑥
3 nfsumOLD.1 . . . . . . 7 𝑥𝐴
4 nfcv 2982 . . . . . . 7 𝑥(ℤ𝑚)
53, 4nfss 3945 . . . . . 6 𝑥 𝐴 ⊆ (ℤ𝑚)
6 nfcv 2982 . . . . . . . 8 𝑥𝑚
7 nfcv 2982 . . . . . . . 8 𝑥 +
83nfcri 2969 . . . . . . . . . 10 𝑥 𝑛𝐴
9 nfcv 2982 . . . . . . . . . . 11 𝑥𝑛
10 nfsumOLD.2 . . . . . . . . . . 11 𝑥𝐵
119, 10nfcsb 3893 . . . . . . . . . 10 𝑥𝑛 / 𝑘𝐵
12 nfcv 2982 . . . . . . . . . 10 𝑥0
138, 11, 12nfif 4479 . . . . . . . . 9 𝑥if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)
142, 13nfmpt 5149 . . . . . . . 8 𝑥(𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))
156, 7, 14nfseq 13383 . . . . . . 7 𝑥seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)))
16 nfcv 2982 . . . . . . 7 𝑥
17 nfcv 2982 . . . . . . 7 𝑥𝑧
1815, 16, 17nfbr 5099 . . . . . 6 𝑥seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧
195, 18nfan 1901 . . . . 5 𝑥(𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧)
202, 19nfrex 3301 . . . 4 𝑥𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧)
21 nfcv 2982 . . . . 5 𝑥
22 nfcv 2982 . . . . . . . 8 𝑥𝑓
23 nfcv 2982 . . . . . . . 8 𝑥(1...𝑚)
2422, 23, 3nff1o 6604 . . . . . . 7 𝑥 𝑓:(1...𝑚)–1-1-onto𝐴
25 nfcv 2982 . . . . . . . . . 10 𝑥1
26 nfcv 2982 . . . . . . . . . . . 12 𝑥(𝑓𝑛)
2726, 10nfcsb 3893 . . . . . . . . . . 11 𝑥(𝑓𝑛) / 𝑘𝐵
2821, 27nfmpt 5149 . . . . . . . . . 10 𝑥(𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
2925, 7, 28nfseq 13383 . . . . . . . . 9 𝑥seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))
3029, 6nffv 6671 . . . . . . . 8 𝑥(seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3130nfeq2 2999 . . . . . . 7 𝑥 𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3224, 31nfan 1901 . . . . . 6 𝑥(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3332nfex 2345 . . . . 5 𝑥𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3421, 33nfrex 3301 . . . 4 𝑥𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3520, 34nfor 1906 . . 3 𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
3635nfiota 6308 . 2 𝑥(℩𝑧(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
371, 36nfcxfr 2980 1 𝑥Σ𝑘𝐴 𝐵
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   ∨ wo 844   = wceq 1538  ∃wex 1781   ∈ wcel 2115  Ⅎwnfc 2962  ∃wrex 3134  ⦋csb 3866   ⊆ wss 3919  ifcif 4450   class class class wbr 5052   ↦ cmpt 5132  ℩cio 6300  –1-1-onto→wf1o 6342  ‘cfv 6343  (class class class)co 7149  0cc0 10535  1c1 10536   + caddc 10538  ℕcn 11634  ℤcz 11978  ℤ≥cuz 12240  ...cfz 12894  seqcseq 13373   ⇝ cli 14841  Σcsu 15042 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-13 2392  ax-ext 2796 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 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-ov 7152  df-oprab 7153  df-mpo 7154  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-seq 13374  df-sum 15043 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator