ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fsum3 GIF version

Theorem fsum3 11398
Description: The value of a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.)
Hypotheses
Ref Expression
fsum.1 (π‘˜ = (πΉβ€˜π‘›) β†’ 𝐡 = 𝐢)
fsum.2 (πœ‘ β†’ 𝑀 ∈ β„•)
fsum.3 (πœ‘ β†’ 𝐹:(1...𝑀)–1-1-onto→𝐴)
fsum.4 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝐡 ∈ β„‚)
fsum.5 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ (πΊβ€˜π‘›) = 𝐢)
Assertion
Ref Expression
fsum3 (πœ‘ β†’ Ξ£π‘˜ ∈ 𝐴 𝐡 = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€))
Distinct variable groups:   𝐴,π‘˜,𝑛   𝐡,𝑛   𝐢,π‘˜   π‘˜,𝐹,𝑛   π‘˜,𝐺,𝑛   π‘˜,𝑀,𝑛   πœ‘,π‘˜,𝑛
Allowed substitution hints:   𝐡(π‘˜)   𝐢(𝑛)

Proof of Theorem fsum3
Dummy variables 𝑓 𝑖 𝑗 π‘š 𝑒 π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sumdc 11365 . 2 Ξ£π‘˜ ∈ 𝐴 𝐡 = (β„©π‘₯(βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
2 nnuz 9566 . . . . 5 β„• = (β„€β‰₯β€˜1)
3 1zzd 9283 . . . . 5 (πœ‘ β†’ 1 ∈ β„€)
4 elnnuz 9567 . . . . . 6 (π‘₯ ∈ β„• ↔ π‘₯ ∈ (β„€β‰₯β€˜1))
52eqimss2i 3214 . . . . . . . . . 10 (β„€β‰₯β€˜1) βŠ† β„•
65sseli 3153 . . . . . . . . 9 (π‘₯ ∈ (β„€β‰₯β€˜1) β†’ π‘₯ ∈ β„•)
76adantl 277 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ π‘₯ ∈ β„•)
8 fveq2 5517 . . . . . . . . . . 11 (𝑛 = π‘₯ β†’ (πΊβ€˜π‘›) = (πΊβ€˜π‘₯))
98eleq1d 2246 . . . . . . . . . 10 (𝑛 = π‘₯ β†’ ((πΊβ€˜π‘›) ∈ β„‚ ↔ (πΊβ€˜π‘₯) ∈ β„‚))
10 fsum.1 . . . . . . . . . . . 12 (π‘˜ = (πΉβ€˜π‘›) β†’ 𝐡 = 𝐢)
11 fsum.2 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑀 ∈ β„•)
12 fsum.3 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹:(1...𝑀)–1-1-onto→𝐴)
13 fsum.4 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝐡 ∈ β„‚)
14 fsum.5 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ (πΊβ€˜π‘›) = 𝐢)
1510, 11, 12, 13, 14fsumgcl 11397 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) ∈ β„‚)
1615ad2antrr 488 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) ∈ β„‚)
17 1zzd 9283 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ 1 ∈ β„€)
1811nnzd 9377 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀 ∈ β„€)
1918ad2antrr 488 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ 𝑀 ∈ β„€)
20 eluzelz 9540 . . . . . . . . . . . . 13 (π‘₯ ∈ (β„€β‰₯β€˜1) β†’ π‘₯ ∈ β„€)
2120ad2antlr 489 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ π‘₯ ∈ β„€)
2217, 19, 213jca 1177 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ (1 ∈ β„€ ∧ 𝑀 ∈ β„€ ∧ π‘₯ ∈ β„€))
23 eluzle 9543 . . . . . . . . . . . . 13 (π‘₯ ∈ (β„€β‰₯β€˜1) β†’ 1 ≀ π‘₯)
2423ad2antlr 489 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ 1 ≀ π‘₯)
25 simpr 110 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ π‘₯ ≀ 𝑀)
2624, 25jca 306 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ (1 ≀ π‘₯ ∧ π‘₯ ≀ 𝑀))
27 elfz2 10018 . . . . . . . . . . 11 (π‘₯ ∈ (1...𝑀) ↔ ((1 ∈ β„€ ∧ 𝑀 ∈ β„€ ∧ π‘₯ ∈ β„€) ∧ (1 ≀ π‘₯ ∧ π‘₯ ≀ 𝑀)))
2822, 26, 27sylanbrc 417 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ π‘₯ ∈ (1...𝑀))
299, 16, 28rspcdva 2848 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ (πΊβ€˜π‘₯) ∈ β„‚)
30 0cnd 7953 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ Β¬ π‘₯ ≀ 𝑀) β†’ 0 ∈ β„‚)
317nnzd 9377 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ π‘₯ ∈ β„€)
3218adantr 276 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ 𝑀 ∈ β„€)
33 zdcle 9332 . . . . . . . . . 10 ((π‘₯ ∈ β„€ ∧ 𝑀 ∈ β„€) β†’ DECID π‘₯ ≀ 𝑀)
3431, 32, 33syl2anc 411 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ DECID π‘₯ ≀ 𝑀)
3529, 30, 34ifcldadc 3565 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ if(π‘₯ ≀ 𝑀, (πΊβ€˜π‘₯), 0) ∈ β„‚)
36 breq1 4008 . . . . . . . . . 10 (𝑛 = π‘₯ β†’ (𝑛 ≀ 𝑀 ↔ π‘₯ ≀ 𝑀))
3736, 8ifbieq1d 3558 . . . . . . . . 9 (𝑛 = π‘₯ β†’ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0) = if(π‘₯ ≀ 𝑀, (πΊβ€˜π‘₯), 0))
38 eqid 2177 . . . . . . . . 9 (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0))
3937, 38fvmptg 5595 . . . . . . . 8 ((π‘₯ ∈ β„• ∧ if(π‘₯ ≀ 𝑀, (πΊβ€˜π‘₯), 0) ∈ β„‚) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0))β€˜π‘₯) = if(π‘₯ ≀ 𝑀, (πΊβ€˜π‘₯), 0))
407, 35, 39syl2anc 411 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0))β€˜π‘₯) = if(π‘₯ ≀ 𝑀, (πΊβ€˜π‘₯), 0))
4140, 35eqeltrd 2254 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0))β€˜π‘₯) ∈ β„‚)
424, 41sylan2b 287 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0))β€˜π‘₯) ∈ β„‚)
432, 3, 42serf 10477 . . . 4 (πœ‘ β†’ seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0))):β„•βŸΆβ„‚)
4443, 11ffvelcdmd 5655 . . 3 (πœ‘ β†’ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) ∈ β„‚)
4544adantr 276 . . . . . . . 8 ((πœ‘ ∧ (βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))) β†’ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) ∈ β„‚)
46 eleq1w 2238 . . . . . . . . . . . . 13 (𝑛 = 𝑗 β†’ (𝑛 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
47 csbeq1 3062 . . . . . . . . . . . . 13 (𝑛 = 𝑗 β†’ ⦋𝑛 / π‘˜β¦Œπ΅ = ⦋𝑗 / π‘˜β¦Œπ΅)
4846, 47ifbieq1d 3558 . . . . . . . . . . . 12 (𝑛 = 𝑗 β†’ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0) = if(𝑗 ∈ 𝐴, ⦋𝑗 / π‘˜β¦Œπ΅, 0))
4948cbvmptv 4101 . . . . . . . . . . 11 (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0)) = (𝑗 ∈ β„€ ↦ if(𝑗 ∈ 𝐴, ⦋𝑗 / π‘˜β¦Œπ΅, 0))
5013ralrimiva 2550 . . . . . . . . . . . 12 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚)
51 nfcsb1v 3092 . . . . . . . . . . . . . 14 β„²π‘˜β¦‹π‘— / π‘˜β¦Œπ΅
5251nfel1 2330 . . . . . . . . . . . . 13 β„²π‘˜β¦‹π‘— / π‘˜β¦Œπ΅ ∈ β„‚
53 csbeq1a 3068 . . . . . . . . . . . . . 14 (π‘˜ = 𝑗 β†’ 𝐡 = ⦋𝑗 / π‘˜β¦Œπ΅)
5453eleq1d 2246 . . . . . . . . . . . . 13 (π‘˜ = 𝑗 β†’ (𝐡 ∈ β„‚ ↔ ⦋𝑗 / π‘˜β¦Œπ΅ ∈ β„‚))
5552, 54rspc 2837 . . . . . . . . . . . 12 (𝑗 ∈ 𝐴 β†’ (βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚ β†’ ⦋𝑗 / π‘˜β¦Œπ΅ ∈ β„‚))
5650, 55mpan9 281 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ 𝐴) β†’ ⦋𝑗 / π‘˜β¦Œπ΅ ∈ β„‚)
57 breq1 4008 . . . . . . . . . . . . 13 (𝑛 = 𝑖 β†’ (𝑛 ≀ (β™―β€˜π΄) ↔ 𝑖 ≀ (β™―β€˜π΄)))
58 fveq2 5517 . . . . . . . . . . . . . . 15 (𝑛 = 𝑖 β†’ (π‘“β€˜π‘›) = (π‘“β€˜π‘–))
5958csbeq1d 3066 . . . . . . . . . . . . . 14 (𝑛 = 𝑖 β†’ ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(π‘“β€˜π‘–) / π‘˜β¦Œπ΅)
60 csbco 3069 . . . . . . . . . . . . . 14 ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅ = ⦋(π‘“β€˜π‘–) / π‘˜β¦Œπ΅
6159, 60eqtr4di 2228 . . . . . . . . . . . . 13 (𝑛 = 𝑖 β†’ ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅)
6257, 61ifbieq1d 3558 . . . . . . . . . . . 12 (𝑛 = 𝑖 β†’ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0) = if(𝑖 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅, 0))
6362cbvmptv 4101 . . . . . . . . . . 11 (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)) = (𝑖 ∈ β„• ↦ if(𝑖 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅, 0))
6449, 56, 63, 63summodc 11394 . . . . . . . . . 10 (πœ‘ β†’ βˆƒ*π‘₯(βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘’ ∈ (β„€β‰₯β€˜π‘š)DECID 𝑒 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
65 eleq1w 2238 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑗 β†’ (𝑒 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
6665dcbid 838 . . . . . . . . . . . . . . 15 (𝑒 = 𝑗 β†’ (DECID 𝑒 ∈ 𝐴 ↔ DECID 𝑗 ∈ 𝐴))
6766cbvralv 2705 . . . . . . . . . . . . . 14 (βˆ€π‘’ ∈ (β„€β‰₯β€˜π‘š)DECID 𝑒 ∈ 𝐴 ↔ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴)
68673anbi2i 1191 . . . . . . . . . . . . 13 ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘’ ∈ (β„€β‰₯β€˜π‘š)DECID 𝑒 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ↔ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯))
6968rexbii 2484 . . . . . . . . . . . 12 (βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘’ ∈ (β„€β‰₯β€˜π‘š)DECID 𝑒 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ↔ βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯))
70 1zzd 9283 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘š ∈ β„• β†’ 1 ∈ β„€)
71 nnz 9275 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘š ∈ β„• β†’ π‘š ∈ β„€)
7270, 71fzfigd 10434 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘š ∈ β„• β†’ (1...π‘š) ∈ Fin)
73 fihasheqf1oi 10770 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...π‘š) ∈ Fin ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (β™―β€˜(1...π‘š)) = (β™―β€˜π΄))
7472, 73sylan 283 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (β™―β€˜(1...π‘š)) = (β™―β€˜π΄))
75 nnnn0 9186 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘š ∈ β„• β†’ π‘š ∈ β„•0)
7675adantr 276 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ π‘š ∈ β„•0)
77 hashfz1 10766 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘š ∈ β„•0 β†’ (β™―β€˜(1...π‘š)) = π‘š)
7876, 77syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (β™―β€˜(1...π‘š)) = π‘š)
7974, 78eqtr3d 2212 . . . . . . . . . . . . . . . . . . . . 21 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (β™―β€˜π΄) = π‘š)
8079breq2d 4017 . . . . . . . . . . . . . . . . . . . 20 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (𝑛 ≀ (β™―β€˜π΄) ↔ 𝑛 ≀ π‘š))
8180ifbid 3557 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0) = if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0))
8281mpteq2dv 4096 . . . . . . . . . . . . . . . . . 18 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))
8382seqeq3d 10456 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0))) = seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0))))
8483fveq1d 5519 . . . . . . . . . . . . . . . 16 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))
8584eqeq2d 2189 . . . . . . . . . . . . . . 15 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š) ↔ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))
8685pm5.32da 452 . . . . . . . . . . . . . 14 (π‘š ∈ β„• β†’ ((𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)) ↔ (𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
8786exbidv 1825 . . . . . . . . . . . . 13 (π‘š ∈ β„• β†’ (βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)) ↔ βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
8887rexbiia 2492 . . . . . . . . . . . 12 (βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)) ↔ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))
8969, 88orbi12i 764 . . . . . . . . . . 11 ((βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘’ ∈ (β„€β‰₯β€˜π‘š)DECID 𝑒 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))) ↔ (βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
9089mobii 2063 . . . . . . . . . 10 (βˆƒ*π‘₯(βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘’ ∈ (β„€β‰₯β€˜π‘š)DECID 𝑒 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))) ↔ βˆƒ*π‘₯(βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
9164, 90sylib 122 . . . . . . . . 9 (πœ‘ β†’ βˆƒ*π‘₯(βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
9291adantr 276 . . . . . . . 8 ((πœ‘ ∧ (βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))) β†’ βˆƒ*π‘₯(βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
93 simpr 110 . . . . . . . 8 ((πœ‘ ∧ (βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))) β†’ (βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
94 f1of 5463 . . . . . . . . . . . . . 14 (𝐹:(1...𝑀)–1-1-onto→𝐴 β†’ 𝐹:(1...𝑀)⟢𝐴)
9512, 94syl 14 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐹:(1...𝑀)⟢𝐴)
963, 18fzfigd 10434 . . . . . . . . . . . . 13 (πœ‘ β†’ (1...𝑀) ∈ Fin)
97 fex 5748 . . . . . . . . . . . . 13 ((𝐹:(1...𝑀)⟢𝐴 ∧ (1...𝑀) ∈ Fin) β†’ 𝐹 ∈ V)
9895, 96, 97syl2anc 411 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹 ∈ V)
9911, 2eleqtrdi 2270 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑀 ∈ (β„€β‰₯β€˜1))
10014ralrimiva 2550 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) = 𝐢)
101 nfv 1528 . . . . . . . . . . . . . . . . . 18 β„²π‘˜(πΊβ€˜π‘›) = 𝐢
102 nfcsb1v 3092 . . . . . . . . . . . . . . . . . . 19 β„²π‘›β¦‹π‘˜ / π‘›β¦ŒπΆ
103102nfeq2 2331 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑛(πΊβ€˜π‘˜) = β¦‹π‘˜ / π‘›β¦ŒπΆ
104 fveq2 5517 . . . . . . . . . . . . . . . . . . 19 (𝑛 = π‘˜ β†’ (πΊβ€˜π‘›) = (πΊβ€˜π‘˜))
105 csbeq1a 3068 . . . . . . . . . . . . . . . . . . 19 (𝑛 = π‘˜ β†’ 𝐢 = β¦‹π‘˜ / π‘›β¦ŒπΆ)
106104, 105eqeq12d 2192 . . . . . . . . . . . . . . . . . 18 (𝑛 = π‘˜ β†’ ((πΊβ€˜π‘›) = 𝐢 ↔ (πΊβ€˜π‘˜) = β¦‹π‘˜ / π‘›β¦ŒπΆ))
107101, 103, 106cbvral 2701 . . . . . . . . . . . . . . . . 17 (βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) = 𝐢 ↔ βˆ€π‘˜ ∈ (1...𝑀)(πΊβ€˜π‘˜) = β¦‹π‘˜ / π‘›β¦ŒπΆ)
108100, 107sylib 122 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ βˆ€π‘˜ ∈ (1...𝑀)(πΊβ€˜π‘˜) = β¦‹π‘˜ / π‘›β¦ŒπΆ)
109108r19.21bi 2565 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ (πΊβ€˜π‘˜) = β¦‹π‘˜ / π‘›β¦ŒπΆ)
110 elfznn 10057 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ (1...𝑀) β†’ π‘˜ ∈ β„•)
111110adantl 277 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ π‘˜ ∈ β„•)
112 elfzle2 10031 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∈ (1...𝑀) β†’ π‘˜ ≀ 𝑀)
113112adantl 277 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ π‘˜ ≀ 𝑀)
114113iftrued 3543 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ if(π‘˜ ≀ 𝑀, (πΊβ€˜π‘˜), 0) = (πΊβ€˜π‘˜))
115104eleq1d 2246 . . . . . . . . . . . . . . . . . . 19 (𝑛 = π‘˜ β†’ ((πΊβ€˜π‘›) ∈ β„‚ ↔ (πΊβ€˜π‘˜) ∈ β„‚))
11615adantr 276 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) ∈ β„‚)
117 simpr 110 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ π‘˜ ∈ (1...𝑀))
118115, 116, 117rspcdva 2848 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ (πΊβ€˜π‘˜) ∈ β„‚)
119114, 118eqeltrd 2254 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ if(π‘˜ ≀ 𝑀, (πΊβ€˜π‘˜), 0) ∈ β„‚)
120 breq1 4008 . . . . . . . . . . . . . . . . . . 19 (𝑛 = π‘˜ β†’ (𝑛 ≀ 𝑀 ↔ π‘˜ ≀ 𝑀))
121120, 104ifbieq1d 3558 . . . . . . . . . . . . . . . . . 18 (𝑛 = π‘˜ β†’ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0) = if(π‘˜ ≀ 𝑀, (πΊβ€˜π‘˜), 0))
122121, 38fvmptg 5595 . . . . . . . . . . . . . . . . 17 ((π‘˜ ∈ β„• ∧ if(π‘˜ ≀ 𝑀, (πΊβ€˜π‘˜), 0) ∈ β„‚) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0))β€˜π‘˜) = if(π‘˜ ≀ 𝑀, (πΊβ€˜π‘˜), 0))
123111, 119, 122syl2anc 411 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0))β€˜π‘˜) = if(π‘˜ ≀ 𝑀, (πΊβ€˜π‘˜), 0))
124123, 114eqtrd 2210 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0))β€˜π‘˜) = (πΊβ€˜π‘˜))
125113iftrued 3543 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ if(π‘˜ ≀ 𝑀, β¦‹π‘˜ / π‘›β¦ŒπΆ, 0) = β¦‹π‘˜ / π‘›β¦ŒπΆ)
12695ffvelcdmda 5654 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ (πΉβ€˜π‘›) ∈ 𝐴)
12710adantl 277 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) ∧ π‘˜ = (πΉβ€˜π‘›)) β†’ 𝐡 = 𝐢)
128126, 127csbied 3105 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = 𝐢)
12950adantr 276 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚)
130 nfcsb1v 3092 . . . . . . . . . . . . . . . . . . . . . . . . 25 β„²π‘˜β¦‹(πΉβ€˜π‘›) / π‘˜β¦Œπ΅
131130nfel1 2330 . . . . . . . . . . . . . . . . . . . . . . . 24 β„²π‘˜β¦‹(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ ∈ β„‚
132 csbeq1a 3068 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ = (πΉβ€˜π‘›) β†’ 𝐡 = ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅)
133132eleq1d 2246 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = (πΉβ€˜π‘›) β†’ (𝐡 ∈ β„‚ ↔ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ ∈ β„‚))
134131, 133rspc 2837 . . . . . . . . . . . . . . . . . . . . . . 23 ((πΉβ€˜π‘›) ∈ 𝐴 β†’ (βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚ β†’ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ ∈ β„‚))
135126, 129, 134sylc 62 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ ∈ β„‚)
136128, 135eqeltrrd 2255 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ 𝐢 ∈ β„‚)
137136ralrimiva 2550 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ βˆ€π‘› ∈ (1...𝑀)𝐢 ∈ β„‚)
138 nfv 1528 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘˜ 𝐢 ∈ β„‚
139102nfel1 2330 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘›β¦‹π‘˜ / π‘›β¦ŒπΆ ∈ β„‚
140105eleq1d 2246 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = π‘˜ β†’ (𝐢 ∈ β„‚ ↔ β¦‹π‘˜ / π‘›β¦ŒπΆ ∈ β„‚))
141138, 139, 140cbvral 2701 . . . . . . . . . . . . . . . . . . . 20 (βˆ€π‘› ∈ (1...𝑀)𝐢 ∈ β„‚ ↔ βˆ€π‘˜ ∈ (1...𝑀)β¦‹π‘˜ / π‘›β¦ŒπΆ ∈ β„‚)
142137, 141sylib 122 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ βˆ€π‘˜ ∈ (1...𝑀)β¦‹π‘˜ / π‘›β¦ŒπΆ ∈ β„‚)
143142r19.21bi 2565 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ β¦‹π‘˜ / π‘›β¦ŒπΆ ∈ β„‚)
144125, 143eqeltrd 2254 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ if(π‘˜ ≀ 𝑀, β¦‹π‘˜ / π‘›β¦ŒπΆ, 0) ∈ β„‚)
145 nfcv 2319 . . . . . . . . . . . . . . . . . 18 β„²π‘›π‘˜
146 nfv 1528 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑛 π‘˜ ≀ 𝑀
147 nfcv 2319 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑛0
148146, 102, 147nfif 3564 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑛if(π‘˜ ≀ 𝑀, β¦‹π‘˜ / π‘›β¦ŒπΆ, 0)
149120, 105ifbieq1d 3558 . . . . . . . . . . . . . . . . . 18 (𝑛 = π‘˜ β†’ if(𝑛 ≀ 𝑀, 𝐢, 0) = if(π‘˜ ≀ 𝑀, β¦‹π‘˜ / π‘›β¦ŒπΆ, 0))
150 eqid 2177 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0))
151145, 148, 149, 150fvmptf 5611 . . . . . . . . . . . . . . . . 17 ((π‘˜ ∈ β„• ∧ if(π‘˜ ≀ 𝑀, β¦‹π‘˜ / π‘›β¦ŒπΆ, 0) ∈ β„‚) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0))β€˜π‘˜) = if(π‘˜ ≀ 𝑀, β¦‹π‘˜ / π‘›β¦ŒπΆ, 0))
152111, 144, 151syl2anc 411 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0))β€˜π‘˜) = if(π‘˜ ≀ 𝑀, β¦‹π‘˜ / π‘›β¦ŒπΆ, 0))
153152, 125eqtrd 2210 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0))β€˜π‘˜) = β¦‹π‘˜ / π‘›β¦ŒπΆ)
154109, 124, 1533eqtr4d 2220 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0))β€˜π‘˜) = ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0))β€˜π‘˜))
155137ad2antrr 488 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ βˆ€π‘› ∈ (1...𝑀)𝐢 ∈ β„‚)
156 nfcsb1v 3092 . . . . . . . . . . . . . . . . . . . 20 Ⅎ𝑛⦋π‘₯ / π‘›β¦ŒπΆ
157156nfel1 2330 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑛⦋π‘₯ / π‘›β¦ŒπΆ ∈ β„‚
158 csbeq1a 3068 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = π‘₯ β†’ 𝐢 = ⦋π‘₯ / π‘›β¦ŒπΆ)
159158eleq1d 2246 . . . . . . . . . . . . . . . . . . 19 (𝑛 = π‘₯ β†’ (𝐢 ∈ β„‚ ↔ ⦋π‘₯ / π‘›β¦ŒπΆ ∈ β„‚))
160157, 159rspc 2837 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (1...𝑀) β†’ (βˆ€π‘› ∈ (1...𝑀)𝐢 ∈ β„‚ β†’ ⦋π‘₯ / π‘›β¦ŒπΆ ∈ β„‚))
16128, 155, 160sylc 62 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ ⦋π‘₯ / π‘›β¦ŒπΆ ∈ β„‚)
162161, 30, 34ifcldadc 3565 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ if(π‘₯ ≀ 𝑀, ⦋π‘₯ / π‘›β¦ŒπΆ, 0) ∈ β„‚)
163 nfcv 2319 . . . . . . . . . . . . . . . . 17 Ⅎ𝑛π‘₯
164 nfv 1528 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑛 π‘₯ ≀ 𝑀
165164, 156, 147nfif 3564 . . . . . . . . . . . . . . . . 17 Ⅎ𝑛if(π‘₯ ≀ 𝑀, ⦋π‘₯ / π‘›β¦ŒπΆ, 0)
16636, 158ifbieq1d 3558 . . . . . . . . . . . . . . . . 17 (𝑛 = π‘₯ β†’ if(𝑛 ≀ 𝑀, 𝐢, 0) = if(π‘₯ ≀ 𝑀, ⦋π‘₯ / π‘›β¦ŒπΆ, 0))
167163, 165, 166, 150fvmptf 5611 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ β„• ∧ if(π‘₯ ≀ 𝑀, ⦋π‘₯ / π‘›β¦ŒπΆ, 0) ∈ β„‚) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0))β€˜π‘₯) = if(π‘₯ ≀ 𝑀, ⦋π‘₯ / π‘›β¦ŒπΆ, 0))
1687, 162, 167syl2anc 411 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0))β€˜π‘₯) = if(π‘₯ ≀ 𝑀, ⦋π‘₯ / π‘›β¦ŒπΆ, 0))
169168, 162eqeltrd 2254 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0))β€˜π‘₯) ∈ β„‚)
170 addcl 7939 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (π‘₯ + 𝑦) ∈ β„‚)
171170adantl 277 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚)) β†’ (π‘₯ + 𝑦) ∈ β„‚)
17299, 154, 41, 169, 171seq3fveq 10474 . . . . . . . . . . . . 13 (πœ‘ β†’ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0)))β€˜π‘€))
17312, 172jca 306 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0)))β€˜π‘€)))
174 f1oeq1 5451 . . . . . . . . . . . . . 14 (𝑓 = 𝐹 β†’ (𝑓:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐹:(1...𝑀)–1-1-onto→𝐴))
175 fveq1 5516 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = 𝐹 β†’ (π‘“β€˜π‘›) = (πΉβ€˜π‘›))
176175csbeq1d 3066 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝐹 β†’ ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅)
177 vex 2742 . . . . . . . . . . . . . . . . . . . . . . 23 𝑓 ∈ V
178 vex 2742 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛 ∈ V
179177, 178fvex 5537 . . . . . . . . . . . . . . . . . . . . . 22 (π‘“β€˜π‘›) ∈ V
180175, 179eqeltrrdi 2269 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = 𝐹 β†’ (πΉβ€˜π‘›) ∈ V)
18110adantl 277 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 = 𝐹 ∧ π‘˜ = (πΉβ€˜π‘›)) β†’ 𝐡 = 𝐢)
182180, 181csbied 3105 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝐹 β†’ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = 𝐢)
183176, 182eqtrd 2210 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝐹 β†’ ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅ = 𝐢)
184183ifeq1d 3553 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝐹 β†’ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0) = if(𝑛 ≀ 𝑀, 𝐢, 0))
185184mpteq2dv 4096 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝐹 β†’ (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0)))
186185seqeq3d 10456 . . . . . . . . . . . . . . . 16 (𝑓 = 𝐹 β†’ seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0))) = seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0))))
187186fveq1d 5519 . . . . . . . . . . . . . . 15 (𝑓 = 𝐹 β†’ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0)))β€˜π‘€))
188187eqeq2d 2189 . . . . . . . . . . . . . 14 (𝑓 = 𝐹 β†’ ((seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘€) ↔ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0)))β€˜π‘€)))
189174, 188anbi12d 473 . . . . . . . . . . . . 13 (𝑓 = 𝐹 β†’ ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘€)) ↔ (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0)))β€˜π‘€))))
190189spcegv 2827 . . . . . . . . . . . 12 (𝐹 ∈ V β†’ ((𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0)))β€˜π‘€)) β†’ βˆƒπ‘“(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘€))))
19198, 173, 190sylc 62 . . . . . . . . . . 11 (πœ‘ β†’ βˆƒπ‘“(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘€)))
192 oveq2 5886 . . . . . . . . . . . . . . 15 (π‘š = 𝑀 β†’ (1...π‘š) = (1...𝑀))
193 f1oeq2 5452 . . . . . . . . . . . . . . 15 ((1...π‘š) = (1...𝑀) β†’ (𝑓:(1...π‘š)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑀)–1-1-onto→𝐴))
194192, 193syl 14 . . . . . . . . . . . . . 14 (π‘š = 𝑀 β†’ (𝑓:(1...π‘š)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑀)–1-1-onto→𝐴))
195 breq2 4009 . . . . . . . . . . . . . . . . . . 19 (π‘š = 𝑀 β†’ (𝑛 ≀ π‘š ↔ 𝑛 ≀ 𝑀))
196195ifbid 3557 . . . . . . . . . . . . . . . . . 18 (π‘š = 𝑀 β†’ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0) = if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0))
197196mpteq2dv 4096 . . . . . . . . . . . . . . . . 17 (π‘š = 𝑀 β†’ (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))
198197seqeq3d 10456 . . . . . . . . . . . . . . . 16 (π‘š = 𝑀 β†’ seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0))) = seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0))))
199 id 19 . . . . . . . . . . . . . . . 16 (π‘š = 𝑀 β†’ π‘š = 𝑀)
200198, 199fveq12d 5524 . . . . . . . . . . . . . . 15 (π‘š = 𝑀 β†’ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘€))
201200eqeq2d 2189 . . . . . . . . . . . . . 14 (π‘š = 𝑀 β†’ ((seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š) ↔ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘€)))
202194, 201anbi12d 473 . . . . . . . . . . . . 13 (π‘š = 𝑀 β†’ ((𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)) ↔ (𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘€))))
203202exbidv 1825 . . . . . . . . . . . 12 (π‘š = 𝑀 β†’ (βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)) ↔ βˆƒπ‘“(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘€))))
204203rspcev 2843 . . . . . . . . . . 11 ((𝑀 ∈ β„• ∧ βˆƒπ‘“(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘€))) β†’ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))
20511, 191, 204syl2anc 411 . . . . . . . . . 10 (πœ‘ β†’ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))
206205olcd 734 . . . . . . . . 9 (πœ‘ β†’ (βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
207206adantr 276 . . . . . . . 8 ((πœ‘ ∧ (βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))) β†’ (βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
208 breq2 4009 . . . . . . . . . . . 12 (π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) β†’ (seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯ ↔ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€)))
2092083anbi3d 1318 . . . . . . . . . . 11 (π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) β†’ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ↔ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€))))
210209rexbidv 2478 . . . . . . . . . 10 (π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) β†’ (βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ↔ βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€))))
211 eqeq1 2184 . . . . . . . . . . . . 13 (π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) β†’ (π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š) ↔ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))
212211anbi2d 464 . . . . . . . . . . . 12 (π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) β†’ ((𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)) ↔ (𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
213212exbidv 1825 . . . . . . . . . . 11 (π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) β†’ (βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)) ↔ βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
214213rexbidv 2478 . . . . . . . . . 10 (π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) β†’ (βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)) ↔ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
215210, 214orbi12d 793 . . . . . . . . 9 (π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) β†’ ((βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))) ↔ (βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))))
216215moi2 2920 . . . . . . . 8 ((((seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) ∈ β„‚ ∧ βˆƒ*π‘₯(βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))) ∧ ((βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))) ∧ (βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))) β†’ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€))
21745, 92, 93, 207, 216syl22anc 1239 . . . . . . 7 ((πœ‘ ∧ (βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))) β†’ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€))
218217ex 115 . . . . . 6 (πœ‘ β†’ ((βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))) β†’ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€)))
219206, 215syl5ibrcom 157 . . . . . 6 (πœ‘ β†’ (π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) β†’ (βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))))
220218, 219impbid 129 . . . . 5 (πœ‘ β†’ ((βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))) ↔ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€)))
221220adantr 276 . . . 4 ((πœ‘ ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) ∈ β„‚) β†’ ((βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))) ↔ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€)))
222221iota5 5200 . . 3 ((πœ‘ ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) ∈ β„‚) β†’ (β„©π‘₯(βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€))
22344, 222mpdan 421 . 2 (πœ‘ β†’ (β„©π‘₯(βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š)))) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€))
2241, 223eqtrid 2222 1 (πœ‘ β†’ Ξ£π‘˜ ∈ 𝐴 𝐡 = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€))
Colors of variables: wff set class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 708  DECID wdc 834   ∧ w3a 978   = wceq 1353  βˆƒwex 1492  βˆƒ*wmo 2027   ∈ wcel 2148  βˆ€wral 2455  βˆƒwrex 2456  Vcvv 2739  β¦‹csb 3059   βŠ† wss 3131  ifcif 3536   class class class wbr 4005   ↦ cmpt 4066  β„©cio 5178  βŸΆwf 5214  β€“1-1-ontoβ†’wf1o 5217  β€˜cfv 5218  (class class class)co 5878  Fincfn 6743  β„‚cc 7812  0cc0 7814  1c1 7815   + caddc 7817   ≀ cle 7996  β„•cn 8922  β„•0cn0 9179  β„€cz 9256  β„€β‰₯cuz 9531  ...cfz 10011  seqcseq 10448  β™―chash 10758   ⇝ cli 11289  Ξ£csu 11364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589  ax-cnex 7905  ax-resscn 7906  ax-1cn 7907  ax-1re 7908  ax-icn 7909  ax-addcl 7910  ax-addrcl 7911  ax-mulcl 7912  ax-mulrcl 7913  ax-addcom 7914  ax-mulcom 7915  ax-addass 7916  ax-mulass 7917  ax-distr 7918  ax-i2m1 7919  ax-0lt1 7920  ax-1rid 7921  ax-0id 7922  ax-rnegex 7923  ax-precex 7924  ax-cnre 7925  ax-pre-ltirr 7926  ax-pre-ltwlin 7927  ax-pre-lttrn 7928  ax-pre-apti 7929  ax-pre-ltadd 7930  ax-pre-mulgt0 7931  ax-pre-mulext 7932  ax-arch 7933  ax-caucvg 7934
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-if 3537  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-po 4298  df-iso 4299  df-iord 4368  df-on 4370  df-ilim 4371  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-isom 5227  df-riota 5834  df-ov 5881  df-oprab 5882  df-mpo 5883  df-1st 6144  df-2nd 6145  df-recs 6309  df-irdg 6374  df-frec 6395  df-1o 6420  df-oadd 6424  df-er 6538  df-en 6744  df-dom 6745  df-fin 6746  df-pnf 7997  df-mnf 7998  df-xr 7999  df-ltxr 8000  df-le 8001  df-sub 8133  df-neg 8134  df-reap 8535  df-ap 8542  df-div 8633  df-inn 8923  df-2 8981  df-3 8982  df-4 8983  df-n0 9180  df-z 9257  df-uz 9532  df-q 9623  df-rp 9657  df-fz 10012  df-fzo 10146  df-seqfrec 10449  df-exp 10523  df-ihash 10759  df-cj 10854  df-re 10855  df-im 10856  df-rsqrt 11010  df-abs 11011  df-clim 11290  df-sumdc 11365
This theorem is referenced by:  isumz  11400  fsumf1o  11401  fsumcl2lem  11409  fsumadd  11417  sumsnf  11420  fsummulc2  11459
  Copyright terms: Public domain W3C validator