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

Theorem fsum3 11394
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 11361 . 2 Ξ£π‘˜ ∈ 𝐴 𝐡 = (β„©π‘₯(βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
2 nnuz 9562 . . . . 5 β„• = (β„€β‰₯β€˜1)
3 1zzd 9279 . . . . 5 (πœ‘ β†’ 1 ∈ β„€)
4 elnnuz 9563 . . . . . 6 (π‘₯ ∈ β„• ↔ π‘₯ ∈ (β„€β‰₯β€˜1))
52eqimss2i 3212 . . . . . . . . . 10 (β„€β‰₯β€˜1) βŠ† β„•
65sseli 3151 . . . . . . . . 9 (π‘₯ ∈ (β„€β‰₯β€˜1) β†’ π‘₯ ∈ β„•)
76adantl 277 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ π‘₯ ∈ β„•)
8 fveq2 5515 . . . . . . . . . . 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 11393 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) ∈ β„‚)
1615ad2antrr 488 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) ∈ β„‚)
17 1zzd 9279 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ 1 ∈ β„€)
1811nnzd 9373 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀 ∈ β„€)
1918ad2antrr 488 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ 𝑀 ∈ β„€)
20 eluzelz 9536 . . . . . . . . . . . . 13 (π‘₯ ∈ (β„€β‰₯β€˜1) β†’ π‘₯ ∈ β„€)
2120ad2antlr 489 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ π‘₯ ∈ β„€)
2217, 19, 213jca 1177 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ (1 ∈ β„€ ∧ 𝑀 ∈ β„€ ∧ π‘₯ ∈ β„€))
23 eluzle 9539 . . . . . . . . . . . . 13 (π‘₯ ∈ (β„€β‰₯β€˜1) β†’ 1 ≀ π‘₯)
2423ad2antlr 489 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ 1 ≀ π‘₯)
25 simpr 110 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ π‘₯ ≀ 𝑀)
2624, 25jca 306 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ (1 ≀ π‘₯ ∧ π‘₯ ≀ 𝑀))
27 elfz2 10014 . . . . . . . . . . 11 (π‘₯ ∈ (1...𝑀) ↔ ((1 ∈ β„€ ∧ 𝑀 ∈ β„€ ∧ π‘₯ ∈ β„€) ∧ (1 ≀ π‘₯ ∧ π‘₯ ≀ 𝑀)))
2822, 26, 27sylanbrc 417 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ π‘₯ ∈ (1...𝑀))
299, 16, 28rspcdva 2846 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ (πΊβ€˜π‘₯) ∈ β„‚)
30 0cnd 7949 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ Β¬ π‘₯ ≀ 𝑀) β†’ 0 ∈ β„‚)
317nnzd 9373 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ π‘₯ ∈ β„€)
3218adantr 276 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ 𝑀 ∈ β„€)
33 zdcle 9328 . . . . . . . . . 10 ((π‘₯ ∈ β„€ ∧ 𝑀 ∈ β„€) β†’ DECID π‘₯ ≀ 𝑀)
3431, 32, 33syl2anc 411 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ DECID π‘₯ ≀ 𝑀)
3529, 30, 34ifcldadc 3563 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ if(π‘₯ ≀ 𝑀, (πΊβ€˜π‘₯), 0) ∈ β„‚)
36 breq1 4006 . . . . . . . . . 10 (𝑛 = π‘₯ β†’ (𝑛 ≀ 𝑀 ↔ π‘₯ ≀ 𝑀))
3736, 8ifbieq1d 3556 . . . . . . . . 9 (𝑛 = π‘₯ β†’ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0) = if(π‘₯ ≀ 𝑀, (πΊβ€˜π‘₯), 0))
38 eqid 2177 . . . . . . . . 9 (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0))
3937, 38fvmptg 5592 . . . . . . . 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 10473 . . . 4 (πœ‘ β†’ seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0))):β„•βŸΆβ„‚)
4443, 11ffvelcdmd 5652 . . 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 3060 . . . . . . . . . . . . 13 (𝑛 = 𝑗 β†’ ⦋𝑛 / π‘˜β¦Œπ΅ = ⦋𝑗 / π‘˜β¦Œπ΅)
4846, 47ifbieq1d 3556 . . . . . . . . . . . 12 (𝑛 = 𝑗 β†’ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0) = if(𝑗 ∈ 𝐴, ⦋𝑗 / π‘˜β¦Œπ΅, 0))
4948cbvmptv 4099 . . . . . . . . . . 11 (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0)) = (𝑗 ∈ β„€ ↦ if(𝑗 ∈ 𝐴, ⦋𝑗 / π‘˜β¦Œπ΅, 0))
5013ralrimiva 2550 . . . . . . . . . . . 12 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚)
51 nfcsb1v 3090 . . . . . . . . . . . . . 14 β„²π‘˜β¦‹π‘— / π‘˜β¦Œπ΅
5251nfel1 2330 . . . . . . . . . . . . 13 β„²π‘˜β¦‹π‘— / π‘˜β¦Œπ΅ ∈ β„‚
53 csbeq1a 3066 . . . . . . . . . . . . . 14 (π‘˜ = 𝑗 β†’ 𝐡 = ⦋𝑗 / π‘˜β¦Œπ΅)
5453eleq1d 2246 . . . . . . . . . . . . 13 (π‘˜ = 𝑗 β†’ (𝐡 ∈ β„‚ ↔ ⦋𝑗 / π‘˜β¦Œπ΅ ∈ β„‚))
5552, 54rspc 2835 . . . . . . . . . . . 12 (𝑗 ∈ 𝐴 β†’ (βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚ β†’ ⦋𝑗 / π‘˜β¦Œπ΅ ∈ β„‚))
5650, 55mpan9 281 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ 𝐴) β†’ ⦋𝑗 / π‘˜β¦Œπ΅ ∈ β„‚)
57 breq1 4006 . . . . . . . . . . . . 13 (𝑛 = 𝑖 β†’ (𝑛 ≀ (β™―β€˜π΄) ↔ 𝑖 ≀ (β™―β€˜π΄)))
58 fveq2 5515 . . . . . . . . . . . . . . 15 (𝑛 = 𝑖 β†’ (π‘“β€˜π‘›) = (π‘“β€˜π‘–))
5958csbeq1d 3064 . . . . . . . . . . . . . 14 (𝑛 = 𝑖 β†’ ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(π‘“β€˜π‘–) / π‘˜β¦Œπ΅)
60 csbco 3067 . . . . . . . . . . . . . 14 ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅ = ⦋(π‘“β€˜π‘–) / π‘˜β¦Œπ΅
6159, 60eqtr4di 2228 . . . . . . . . . . . . 13 (𝑛 = 𝑖 β†’ ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅)
6257, 61ifbieq1d 3556 . . . . . . . . . . . 12 (𝑛 = 𝑖 β†’ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0) = if(𝑖 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅, 0))
6362cbvmptv 4099 . . . . . . . . . . 11 (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)) = (𝑖 ∈ β„• ↦ if(𝑖 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅, 0))
6449, 56, 63, 63summodc 11390 . . . . . . . . . 10 (πœ‘ β†’ βˆƒ*π‘₯(βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘’ ∈ (β„€β‰₯β€˜π‘š)DECID 𝑒 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
65 eleq1w 2238 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑗 β†’ (𝑒 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
6665dcbid 838 . . . . . . . . . . . . . . 15 (𝑒 = 𝑗 β†’ (DECID 𝑒 ∈ 𝐴 ↔ DECID 𝑗 ∈ 𝐴))
6766cbvralv 2703 . . . . . . . . . . . . . 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 9279 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘š ∈ β„• β†’ 1 ∈ β„€)
71 nnz 9271 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘š ∈ β„• β†’ π‘š ∈ β„€)
7270, 71fzfigd 10430 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘š ∈ β„• β†’ (1...π‘š) ∈ Fin)
73 fihasheqf1oi 10766 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...π‘š) ∈ Fin ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (β™―β€˜(1...π‘š)) = (β™―β€˜π΄))
7472, 73sylan 283 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (β™―β€˜(1...π‘š)) = (β™―β€˜π΄))
75 nnnn0 9182 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘š ∈ β„• β†’ π‘š ∈ β„•0)
7675adantr 276 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ π‘š ∈ β„•0)
77 hashfz1 10762 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘š ∈ β„•0 β†’ (β™―β€˜(1...π‘š)) = π‘š)
7876, 77syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (β™―β€˜(1...π‘š)) = π‘š)
7974, 78eqtr3d 2212 . . . . . . . . . . . . . . . . . . . . 21 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (β™―β€˜π΄) = π‘š)
8079breq2d 4015 . . . . . . . . . . . . . . . . . . . 20 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (𝑛 ≀ (β™―β€˜π΄) ↔ 𝑛 ≀ π‘š))
8180ifbid 3555 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0) = if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0))
8281mpteq2dv 4094 . . . . . . . . . . . . . . . . . 18 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))
8382seqeq3d 10452 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0))) = seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0))))
8483fveq1d 5517 . . . . . . . . . . . . . . . 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 5461 . . . . . . . . . . . . . 14 (𝐹:(1...𝑀)–1-1-onto→𝐴 β†’ 𝐹:(1...𝑀)⟢𝐴)
9512, 94syl 14 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐹:(1...𝑀)⟢𝐴)
963, 18fzfigd 10430 . . . . . . . . . . . . 13 (πœ‘ β†’ (1...𝑀) ∈ Fin)
97 fex 5745 . . . . . . . . . . . . 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 3090 . . . . . . . . . . . . . . . . . . 19 β„²π‘›β¦‹π‘˜ / π‘›β¦ŒπΆ
103102nfeq2 2331 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑛(πΊβ€˜π‘˜) = β¦‹π‘˜ / π‘›β¦ŒπΆ
104 fveq2 5515 . . . . . . . . . . . . . . . . . . 19 (𝑛 = π‘˜ β†’ (πΊβ€˜π‘›) = (πΊβ€˜π‘˜))
105 csbeq1a 3066 . . . . . . . . . . . . . . . . . . 19 (𝑛 = π‘˜ β†’ 𝐢 = β¦‹π‘˜ / π‘›β¦ŒπΆ)
106104, 105eqeq12d 2192 . . . . . . . . . . . . . . . . . 18 (𝑛 = π‘˜ β†’ ((πΊβ€˜π‘›) = 𝐢 ↔ (πΊβ€˜π‘˜) = β¦‹π‘˜ / π‘›β¦ŒπΆ))
107101, 103, 106cbvral 2699 . . . . . . . . . . . . . . . . 17 (βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) = 𝐢 ↔ βˆ€π‘˜ ∈ (1...𝑀)(πΊβ€˜π‘˜) = β¦‹π‘˜ / π‘›β¦ŒπΆ)
108100, 107sylib 122 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ βˆ€π‘˜ ∈ (1...𝑀)(πΊβ€˜π‘˜) = β¦‹π‘˜ / π‘›β¦ŒπΆ)
109108r19.21bi 2565 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ (πΊβ€˜π‘˜) = β¦‹π‘˜ / π‘›β¦ŒπΆ)
110 elfznn 10053 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ (1...𝑀) β†’ π‘˜ ∈ β„•)
111110adantl 277 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ π‘˜ ∈ β„•)
112 elfzle2 10027 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∈ (1...𝑀) β†’ π‘˜ ≀ 𝑀)
113112adantl 277 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ π‘˜ ≀ 𝑀)
114113iftrued 3541 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ if(π‘˜ ≀ 𝑀, (πΊβ€˜π‘˜), 0) = (πΊβ€˜π‘˜))
115104eleq1d 2246 . . . . . . . . . . . . . . . . . . 19 (𝑛 = π‘˜ β†’ ((πΊβ€˜π‘›) ∈ β„‚ ↔ (πΊβ€˜π‘˜) ∈ β„‚))
11615adantr 276 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) ∈ β„‚)
117 simpr 110 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ π‘˜ ∈ (1...𝑀))
118115, 116, 117rspcdva 2846 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ (πΊβ€˜π‘˜) ∈ β„‚)
119114, 118eqeltrd 2254 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ if(π‘˜ ≀ 𝑀, (πΊβ€˜π‘˜), 0) ∈ β„‚)
120 breq1 4006 . . . . . . . . . . . . . . . . . . 19 (𝑛 = π‘˜ β†’ (𝑛 ≀ 𝑀 ↔ π‘˜ ≀ 𝑀))
121120, 104ifbieq1d 3556 . . . . . . . . . . . . . . . . . 18 (𝑛 = π‘˜ β†’ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0) = if(π‘˜ ≀ 𝑀, (πΊβ€˜π‘˜), 0))
122121, 38fvmptg 5592 . . . . . . . . . . . . . . . . 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 3541 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ (1...𝑀)) β†’ if(π‘˜ ≀ 𝑀, β¦‹π‘˜ / π‘›β¦ŒπΆ, 0) = β¦‹π‘˜ / π‘›β¦ŒπΆ)
12695ffvelcdmda 5651 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ (πΉβ€˜π‘›) ∈ 𝐴)
12710adantl 277 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) ∧ π‘˜ = (πΉβ€˜π‘›)) β†’ 𝐡 = 𝐢)
128126, 127csbied 3103 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = 𝐢)
12950adantr 276 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚)
130 nfcsb1v 3090 . . . . . . . . . . . . . . . . . . . . . . . . 25 β„²π‘˜β¦‹(πΉβ€˜π‘›) / π‘˜β¦Œπ΅
131130nfel1 2330 . . . . . . . . . . . . . . . . . . . . . . . 24 β„²π‘˜β¦‹(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ ∈ β„‚
132 csbeq1a 3066 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ = (πΉβ€˜π‘›) β†’ 𝐡 = ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅)
133132eleq1d 2246 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = (πΉβ€˜π‘›) β†’ (𝐡 ∈ β„‚ ↔ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ ∈ β„‚))
134131, 133rspc 2835 . . . . . . . . . . . . . . . . . . . . . . 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 2699 . . . . . . . . . . . . . . . . . . . 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 3562 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑛if(π‘˜ ≀ 𝑀, β¦‹π‘˜ / π‘›β¦ŒπΆ, 0)
149120, 105ifbieq1d 3556 . . . . . . . . . . . . . . . . . 18 (𝑛 = π‘˜ β†’ if(𝑛 ≀ 𝑀, 𝐢, 0) = if(π‘˜ ≀ 𝑀, β¦‹π‘˜ / π‘›β¦ŒπΆ, 0))
150 eqid 2177 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0))
151145, 148, 149, 150fvmptf 5608 . . . . . . . . . . . . . . . . 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 3090 . . . . . . . . . . . . . . . . . . . 20 Ⅎ𝑛⦋π‘₯ / π‘›β¦ŒπΆ
157156nfel1 2330 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑛⦋π‘₯ / π‘›β¦ŒπΆ ∈ β„‚
158 csbeq1a 3066 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = π‘₯ β†’ 𝐢 = ⦋π‘₯ / π‘›β¦ŒπΆ)
159158eleq1d 2246 . . . . . . . . . . . . . . . . . . 19 (𝑛 = π‘₯ β†’ (𝐢 ∈ β„‚ ↔ ⦋π‘₯ / π‘›β¦ŒπΆ ∈ β„‚))
160157, 159rspc 2835 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (1...𝑀) β†’ (βˆ€π‘› ∈ (1...𝑀)𝐢 ∈ β„‚ β†’ ⦋π‘₯ / π‘›β¦ŒπΆ ∈ β„‚))
16128, 155, 160sylc 62 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) ∧ π‘₯ ≀ 𝑀) β†’ ⦋π‘₯ / π‘›β¦ŒπΆ ∈ β„‚)
162161, 30, 34ifcldadc 3563 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (β„€β‰₯β€˜1)) β†’ if(π‘₯ ≀ 𝑀, ⦋π‘₯ / π‘›β¦ŒπΆ, 0) ∈ β„‚)
163 nfcv 2319 . . . . . . . . . . . . . . . . 17 Ⅎ𝑛π‘₯
164 nfv 1528 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑛 π‘₯ ≀ 𝑀
165164, 156, 147nfif 3562 . . . . . . . . . . . . . . . . 17 Ⅎ𝑛if(π‘₯ ≀ 𝑀, ⦋π‘₯ / π‘›β¦ŒπΆ, 0)
16636, 158ifbieq1d 3556 . . . . . . . . . . . . . . . . 17 (𝑛 = π‘₯ β†’ if(𝑛 ≀ 𝑀, 𝐢, 0) = if(π‘₯ ≀ 𝑀, ⦋π‘₯ / π‘›β¦ŒπΆ, 0))
167163, 165, 166, 150fvmptf 5608 . . . . . . . . . . . . . . . 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 7935 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (π‘₯ + 𝑦) ∈ β„‚)
171170adantl 277 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚)) β†’ (π‘₯ + 𝑦) ∈ β„‚)
17299, 154, 41, 169, 171seq3fveq 10470 . . . . . . . . . . . . 13 (πœ‘ β†’ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0)))β€˜π‘€))
17312, 172jca 306 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 0)))β€˜π‘€) = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0)))β€˜π‘€)))
174 f1oeq1 5449 . . . . . . . . . . . . . 14 (𝑓 = 𝐹 β†’ (𝑓:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐹:(1...𝑀)–1-1-onto→𝐴))
175 fveq1 5514 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = 𝐹 β†’ (π‘“β€˜π‘›) = (πΉβ€˜π‘›))
176175csbeq1d 3064 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝐹 β†’ ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅)
177 vex 2740 . . . . . . . . . . . . . . . . . . . . . . 23 𝑓 ∈ V
178 vex 2740 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛 ∈ V
179177, 178fvex 5535 . . . . . . . . . . . . . . . . . . . . . 22 (π‘“β€˜π‘›) ∈ V
180175, 179eqeltrrdi 2269 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = 𝐹 β†’ (πΉβ€˜π‘›) ∈ V)
18110adantl 277 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 = 𝐹 ∧ π‘˜ = (πΉβ€˜π‘›)) β†’ 𝐡 = 𝐢)
182180, 181csbied 3103 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝐹 β†’ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = 𝐢)
183176, 182eqtrd 2210 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝐹 β†’ ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅ = 𝐢)
184183ifeq1d 3551 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝐹 β†’ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0) = if(𝑛 ≀ 𝑀, 𝐢, 0))
185184mpteq2dv 4094 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝐹 β†’ (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0)))
186185seqeq3d 10452 . . . . . . . . . . . . . . . 16 (𝑓 = 𝐹 β†’ seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0))) = seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, 𝐢, 0))))
187186fveq1d 5517 . . . . . . . . . . . . . . 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 2825 . . . . . . . . . . . 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 5882 . . . . . . . . . . . . . . 15 (π‘š = 𝑀 β†’ (1...π‘š) = (1...𝑀))
193 f1oeq2 5450 . . . . . . . . . . . . . . 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 4007 . . . . . . . . . . . . . . . . . . 19 (π‘š = 𝑀 β†’ (𝑛 ≀ π‘š ↔ 𝑛 ≀ 𝑀))
196195ifbid 3555 . . . . . . . . . . . . . . . . . 18 (π‘š = 𝑀 β†’ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0) = if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0))
197196mpteq2dv 4094 . . . . . . . . . . . . . . . . 17 (π‘š = 𝑀 β†’ (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))
198197seqeq3d 10452 . . . . . . . . . . . . . . . 16 (π‘š = 𝑀 β†’ seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0))) = seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0))))
199 id 19 . . . . . . . . . . . . . . . 16 (π‘š = 𝑀 β†’ π‘š = 𝑀)
200198, 199fveq12d 5522 . . . . . . . . . . . . . . 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 2841 . . . . . . . . . . 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 4007 . . . . . . . . . . . 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 2918 . . . . . . . 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 5198 . . 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 2737  β¦‹csb 3057   βŠ† wss 3129  ifcif 3534   class class class wbr 4003   ↦ cmpt 4064  β„©cio 5176  βŸΆwf 5212  β€“1-1-ontoβ†’wf1o 5215  β€˜cfv 5216  (class class class)co 5874  Fincfn 6739  β„‚cc 7808  0cc0 7810  1c1 7811   + caddc 7813   ≀ cle 7992  β„•cn 8918  β„•0cn0 9175  β„€cz 9252  β„€β‰₯cuz 9527  ...cfz 10007  seqcseq 10444  β™―chash 10754   ⇝ cli 11285  Ξ£csu 11360
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 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-mulrcl 7909  ax-addcom 7910  ax-mulcom 7911  ax-addass 7912  ax-mulass 7913  ax-distr 7914  ax-i2m1 7915  ax-0lt1 7916  ax-1rid 7917  ax-0id 7918  ax-rnegex 7919  ax-precex 7920  ax-cnre 7921  ax-pre-ltirr 7922  ax-pre-ltwlin 7923  ax-pre-lttrn 7924  ax-pre-apti 7925  ax-pre-ltadd 7926  ax-pre-mulgt0 7927  ax-pre-mulext 7928  ax-arch 7929  ax-caucvg 7930
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 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-po 4296  df-iso 4297  df-iord 4366  df-on 4368  df-ilim 4369  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-isom 5225  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-irdg 6370  df-frec 6391  df-1o 6416  df-oadd 6420  df-er 6534  df-en 6740  df-dom 6741  df-fin 6742  df-pnf 7993  df-mnf 7994  df-xr 7995  df-ltxr 7996  df-le 7997  df-sub 8129  df-neg 8130  df-reap 8531  df-ap 8538  df-div 8629  df-inn 8919  df-2 8977  df-3 8978  df-4 8979  df-n0 9176  df-z 9253  df-uz 9528  df-q 9619  df-rp 9653  df-fz 10008  df-fzo 10142  df-seqfrec 10445  df-exp 10519  df-ihash 10755  df-cj 10850  df-re 10851  df-im 10852  df-rsqrt 11006  df-abs 11007  df-clim 11286  df-sumdc 11361
This theorem is referenced by:  isumz  11396  fsumf1o  11397  fsumcl2lem  11405  fsumadd  11413  sumsnf  11416  fsummulc2  11455
  Copyright terms: Public domain W3C validator