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

Theorem fprodseq 11604
Description: The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.)
Hypotheses
Ref Expression
fprod.1 (π‘˜ = (πΉβ€˜π‘›) β†’ 𝐡 = 𝐢)
fprod.2 (πœ‘ β†’ 𝑀 ∈ β„•)
fprod.3 (πœ‘ β†’ 𝐹:(1...𝑀)–1-1-onto→𝐴)
fprod.4 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝐡 ∈ β„‚)
fprod.5 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ (πΊβ€˜π‘›) = 𝐢)
Assertion
Ref Expression
fprodseq (πœ‘ β†’ βˆπ‘˜ ∈ 𝐴 𝐡 = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))
Distinct variable groups:   𝐴,π‘˜,𝑛   𝐡,𝑛   𝐢,π‘˜   π‘˜,𝐹,𝑛   π‘˜,𝐺,𝑛   π‘˜,𝑀,𝑛   πœ‘,π‘˜,𝑛
Allowed substitution hints:   𝐡(π‘˜)   𝐢(𝑛)

Proof of Theorem fprodseq
Dummy variables 𝑓 𝑖 𝑗 π‘š π‘₯ 𝑝 π‘ž 𝑒 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-proddc 11572 . 2 βˆπ‘˜ ∈ 𝐴 𝐡 = (β„©π‘₯(βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))
2 nnuz 9576 . . . . 5 β„• = (β„€β‰₯β€˜1)
3 1zzd 9293 . . . . 5 (πœ‘ β†’ 1 ∈ β„€)
4 eqid 2187 . . . . . . 7 (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))
5 breq1 4018 . . . . . . . 8 (𝑛 = 𝑝 β†’ (𝑛 ≀ 𝑀 ↔ 𝑝 ≀ 𝑀))
6 fveq2 5527 . . . . . . . 8 (𝑛 = 𝑝 β†’ (πΊβ€˜π‘›) = (πΊβ€˜π‘))
75, 6ifbieq1d 3568 . . . . . . 7 (𝑛 = 𝑝 β†’ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1) = if(𝑝 ≀ 𝑀, (πΊβ€˜π‘), 1))
8 simpr 110 . . . . . . 7 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ 𝑝 ∈ β„•)
9 simpll 527 . . . . . . . . 9 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ 𝑀) β†’ πœ‘)
108anim1i 340 . . . . . . . . . 10 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ 𝑀) β†’ (𝑝 ∈ β„• ∧ 𝑝 ≀ 𝑀))
11 fprod.2 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀 ∈ β„•)
1211nnzd 9387 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑀 ∈ β„€)
13 fznn 10102 . . . . . . . . . . . 12 (𝑀 ∈ β„€ β†’ (𝑝 ∈ (1...𝑀) ↔ (𝑝 ∈ β„• ∧ 𝑝 ≀ 𝑀)))
1412, 13syl 14 . . . . . . . . . . 11 (πœ‘ β†’ (𝑝 ∈ (1...𝑀) ↔ (𝑝 ∈ β„• ∧ 𝑝 ≀ 𝑀)))
1514ad2antrr 488 . . . . . . . . . 10 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ 𝑀) β†’ (𝑝 ∈ (1...𝑀) ↔ (𝑝 ∈ β„• ∧ 𝑝 ≀ 𝑀)))
1610, 15mpbird 167 . . . . . . . . 9 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ 𝑀) β†’ 𝑝 ∈ (1...𝑀))
176eleq1d 2256 . . . . . . . . . 10 (𝑛 = 𝑝 β†’ ((πΊβ€˜π‘›) ∈ β„‚ ↔ (πΊβ€˜π‘) ∈ β„‚))
18 fprod.1 . . . . . . . . . . . 12 (π‘˜ = (πΉβ€˜π‘›) β†’ 𝐡 = 𝐢)
19 fprod.3 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹:(1...𝑀)–1-1-onto→𝐴)
20 fprod.4 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝐡 ∈ β„‚)
21 fprod.5 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ (πΊβ€˜π‘›) = 𝐢)
2218, 11, 19, 20, 21fsumgcl 11407 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) ∈ β„‚)
2322adantr 276 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ (1...𝑀)) β†’ βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) ∈ β„‚)
24 simpr 110 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ (1...𝑀)) β†’ 𝑝 ∈ (1...𝑀))
2517, 23, 24rspcdva 2858 . . . . . . . . 9 ((πœ‘ ∧ 𝑝 ∈ (1...𝑀)) β†’ (πΊβ€˜π‘) ∈ β„‚)
269, 16, 25syl2anc 411 . . . . . . . 8 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ 𝑀) β†’ (πΊβ€˜π‘) ∈ β„‚)
27 1cnd 7986 . . . . . . . 8 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ Β¬ 𝑝 ≀ 𝑀) β†’ 1 ∈ β„‚)
288nnzd 9387 . . . . . . . . 9 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ 𝑝 ∈ β„€)
2912adantr 276 . . . . . . . . 9 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ 𝑀 ∈ β„€)
30 zdcle 9342 . . . . . . . . 9 ((𝑝 ∈ β„€ ∧ 𝑀 ∈ β„€) β†’ DECID 𝑝 ≀ 𝑀)
3128, 29, 30syl2anc 411 . . . . . . . 8 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ DECID 𝑝 ≀ 𝑀)
3226, 27, 31ifcldadc 3575 . . . . . . 7 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ if(𝑝 ≀ 𝑀, (πΊβ€˜π‘), 1) ∈ β„‚)
334, 7, 8, 32fvmptd3 5622 . . . . . 6 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))β€˜π‘) = if(𝑝 ≀ 𝑀, (πΊβ€˜π‘), 1))
3433, 32eqeltrd 2264 . . . . 5 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))β€˜π‘) ∈ β„‚)
352, 3, 34prodf 11559 . . . 4 (πœ‘ β†’ seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))):β„•βŸΆβ„‚)
3635, 11ffvelcdmd 5665 . . 3 (πœ‘ β†’ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) ∈ β„‚)
37 eleq1w 2248 . . . . . . . . . . . . 13 (𝑖 = 𝑗 β†’ (𝑖 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
3837dcbid 839 . . . . . . . . . . . 12 (𝑖 = 𝑗 β†’ (DECID 𝑖 ∈ 𝐴 ↔ DECID 𝑗 ∈ 𝐴))
3938cbvralv 2715 . . . . . . . . . . 11 (βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴 ↔ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴)
4039anbi2i 457 . . . . . . . . . 10 ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ↔ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴))
4140anbi1i 458 . . . . . . . . 9 (((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ↔ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)))
4241rexbii 2494 . . . . . . . 8 (βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ↔ βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)))
43 nnnn0 9196 . . . . . . . . . . . . . . . . . . . . 21 (π‘š ∈ β„• β†’ π‘š ∈ β„•0)
44 hashfz1 10776 . . . . . . . . . . . . . . . . . . . . 21 (π‘š ∈ β„•0 β†’ (β™―β€˜(1...π‘š)) = π‘š)
4543, 44syl 14 . . . . . . . . . . . . . . . . . . . 20 (π‘š ∈ β„• β†’ (β™―β€˜(1...π‘š)) = π‘š)
4645adantr 276 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (β™―β€˜(1...π‘š)) = π‘š)
47 1zzd 9293 . . . . . . . . . . . . . . . . . . . . 21 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ 1 ∈ β„€)
48 nnz 9285 . . . . . . . . . . . . . . . . . . . . . 22 (π‘š ∈ β„• β†’ π‘š ∈ β„€)
4948adantr 276 . . . . . . . . . . . . . . . . . . . . 21 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ π‘š ∈ β„€)
5047, 49fzfigd 10444 . . . . . . . . . . . . . . . . . . . 20 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (1...π‘š) ∈ Fin)
51 simpr 110 . . . . . . . . . . . . . . . . . . . 20 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ 𝑓:(1...π‘š)–1-1-onto→𝐴)
5250, 51fihasheqf1od 10782 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (β™―β€˜(1...π‘š)) = (β™―β€˜π΄))
5346, 52eqtr3d 2222 . . . . . . . . . . . . . . . . . 18 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ π‘š = (β™―β€˜π΄))
5453breq2d 4027 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (𝑛 ≀ π‘š ↔ 𝑛 ≀ (β™―β€˜π΄)))
5554ifbid 3567 . . . . . . . . . . . . . . . 16 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1) = if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1))
5655mpteq2dv 4106 . . . . . . . . . . . . . . 15 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))
5756seqeq3d 10466 . . . . . . . . . . . . . 14 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1))) = seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1))))
5857fveq1d 5529 . . . . . . . . . . . . 13 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))
5958eqeq2d 2199 . . . . . . . . . . . 12 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š) ↔ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)))
6059pm5.32da 452 . . . . . . . . . . 11 (π‘š ∈ β„• β†’ ((𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)) ↔ (𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))
6160exbidv 1835 . . . . . . . . . 10 (π‘š ∈ β„• β†’ (βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)) ↔ βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))
6261rexbiia 2502 . . . . . . . . 9 (βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)) ↔ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)))
6362bicomi 132 . . . . . . . 8 (βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)) ↔ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)))
6442, 63orbi12i 765 . . . . . . 7 ((βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))) ↔ (βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))
65 f1of 5473 . . . . . . . . . . . . 13 (𝐹:(1...𝑀)–1-1-onto→𝐴 β†’ 𝐹:(1...𝑀)⟢𝐴)
6619, 65syl 14 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹:(1...𝑀)⟢𝐴)
673, 12fzfigd 10444 . . . . . . . . . . . 12 (πœ‘ β†’ (1...𝑀) ∈ Fin)
68 fex 5758 . . . . . . . . . . . 12 ((𝐹:(1...𝑀)⟢𝐴 ∧ (1...𝑀) ∈ Fin) β†’ 𝐹 ∈ V)
6966, 67, 68syl2anc 411 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹 ∈ V)
7011, 2eleqtrdi 2280 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀 ∈ (β„€β‰₯β€˜1))
71 fveq2 5527 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑒 β†’ (πΉβ€˜π‘›) = (πΉβ€˜π‘’))
7271csbeq1d 3076 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑒 β†’ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅)
73 fveq2 5527 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑒 β†’ (πΊβ€˜π‘›) = (πΊβ€˜π‘’))
7472, 73eqeq12d 2202 . . . . . . . . . . . . . . 15 (𝑛 = 𝑒 β†’ (⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = (πΊβ€˜π‘›) ↔ ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅ = (πΊβ€˜π‘’)))
7566ffvelcdmda 5664 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ (πΉβ€˜π‘›) ∈ 𝐴)
7618adantl 277 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) ∧ π‘˜ = (πΉβ€˜π‘›)) β†’ 𝐡 = 𝐢)
7775, 76csbied 3115 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = 𝐢)
7877, 21eqtr4d 2223 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = (πΊβ€˜π‘›))
7978ralrimiva 2560 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ βˆ€π‘› ∈ (1...𝑀)⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = (πΊβ€˜π‘›))
8079adantr 276 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ βˆ€π‘› ∈ (1...𝑀)⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = (πΊβ€˜π‘›))
81 simpr 110 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ 𝑒 ∈ (1...𝑀))
8274, 80, 81rspcdva 2858 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅ = (πΊβ€˜π‘’))
83 eqid 2187 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))
84 breq1 4018 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑒 β†’ (𝑛 ≀ (β™―β€˜π΄) ↔ 𝑒 ≀ (β™―β€˜π΄)))
8584, 72ifbieq1d 3568 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑒 β†’ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1) = if(𝑒 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅, 1))
86 elfznn 10067 . . . . . . . . . . . . . . . . 17 (𝑒 ∈ (1...𝑀) β†’ 𝑒 ∈ β„•)
8786adantl 277 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ 𝑒 ∈ β„•)
88 elfzle2 10041 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ (1...𝑀) β†’ 𝑒 ≀ 𝑀)
8988adantl 277 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ 𝑒 ≀ 𝑀)
9011nnnn0d 9242 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 𝑀 ∈ β„•0)
91 hashfz1 10776 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ β„•0 β†’ (β™―β€˜(1...𝑀)) = 𝑀)
9290, 91syl 14 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (β™―β€˜(1...𝑀)) = 𝑀)
9367, 19fihasheqf1od 10782 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (β™―β€˜(1...𝑀)) = (β™―β€˜π΄))
9492, 93eqtr3d 2222 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝑀 = (β™―β€˜π΄))
9594adantr 276 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ 𝑀 = (β™―β€˜π΄))
9689, 95breqtrd 4041 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ 𝑒 ≀ (β™―β€˜π΄))
9796iftrued 3553 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ if(𝑒 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅, 1) = ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅)
9897, 82eqtrd 2220 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ if(𝑒 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅, 1) = (πΊβ€˜π‘’))
9973eleq1d 2256 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑒 β†’ ((πΊβ€˜π‘›) ∈ β„‚ ↔ (πΊβ€˜π‘’) ∈ β„‚))
10022adantr 276 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) ∈ β„‚)
10199, 100, 81rspcdva 2858 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ (πΊβ€˜π‘’) ∈ β„‚)
10298, 101eqeltrd 2264 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ if(𝑒 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅, 1) ∈ β„‚)
10383, 85, 87, 102fvmptd3 5622 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))β€˜π‘’) = if(𝑒 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅, 1))
104103, 97eqtrd 2220 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))β€˜π‘’) = ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅)
105 breq1 4018 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑒 β†’ (𝑛 ≀ 𝑀 ↔ 𝑒 ≀ 𝑀))
106105, 73ifbieq1d 3568 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑒 β†’ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1) = if(𝑒 ≀ 𝑀, (πΊβ€˜π‘’), 1))
10789iftrued 3553 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ if(𝑒 ≀ 𝑀, (πΊβ€˜π‘’), 1) = (πΊβ€˜π‘’))
108107, 101eqeltrd 2264 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ if(𝑒 ≀ 𝑀, (πΊβ€˜π‘’), 1) ∈ β„‚)
1094, 106, 87, 108fvmptd3 5622 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))β€˜π‘’) = if(𝑒 ≀ 𝑀, (πΊβ€˜π‘’), 1))
110109, 107eqtrd 2220 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))β€˜π‘’) = (πΊβ€˜π‘’))
11182, 104, 1103eqtr4rd 2231 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))β€˜π‘’) = ((𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))β€˜π‘’))
112 elnnuz 9577 . . . . . . . . . . . . . 14 (𝑝 ∈ β„• ↔ 𝑝 ∈ (β„€β‰₯β€˜1))
113112, 34sylan2br 288 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑝 ∈ (β„€β‰₯β€˜1)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))β€˜π‘) ∈ β„‚)
114 breq1 4018 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑝 β†’ (𝑛 ≀ (β™―β€˜π΄) ↔ 𝑝 ≀ (β™―β€˜π΄)))
115 fveq2 5527 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑝 β†’ (πΉβ€˜π‘›) = (πΉβ€˜π‘))
116115csbeq1d 3076 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑝 β†’ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅)
117114, 116ifbieq1d 3568 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑝 β†’ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1) = if(𝑝 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅, 1))
118 simpll 527 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ (β™―β€˜π΄)) β†’ πœ‘)
119 simpr 110 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ (β™―β€˜π΄)) β†’ 𝑝 ≀ (β™―β€˜π΄))
12094breq2d 4027 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑝 ≀ 𝑀 ↔ 𝑝 ≀ (β™―β€˜π΄)))
121120ad2antrr 488 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ (β™―β€˜π΄)) β†’ (𝑝 ≀ 𝑀 ↔ 𝑝 ≀ (β™―β€˜π΄)))
122119, 121mpbird 167 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ (β™―β€˜π΄)) β†’ 𝑝 ≀ 𝑀)
123122, 16syldan 282 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ (β™―β€˜π΄)) β†’ 𝑝 ∈ (1...𝑀))
12466ffvelcdmda 5664 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ (1...𝑀)) β†’ (πΉβ€˜π‘) ∈ 𝐴)
12520ralrimiva 2560 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚)
126125adantr 276 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ (1...𝑀)) β†’ βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚)
127 nfcsb1v 3102 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘˜β¦‹(πΉβ€˜π‘) / π‘˜β¦Œπ΅
128127nfel1 2340 . . . . . . . . . . . . . . . . . . . 20 β„²π‘˜β¦‹(πΉβ€˜π‘) / π‘˜β¦Œπ΅ ∈ β„‚
129 csbeq1a 3078 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ = (πΉβ€˜π‘) β†’ 𝐡 = ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅)
130129eleq1d 2256 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = (πΉβ€˜π‘) β†’ (𝐡 ∈ β„‚ ↔ ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅ ∈ β„‚))
131128, 130rspc 2847 . . . . . . . . . . . . . . . . . . 19 ((πΉβ€˜π‘) ∈ 𝐴 β†’ (βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚ β†’ ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅ ∈ β„‚))
132124, 126, 131sylc 62 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑝 ∈ (1...𝑀)) β†’ ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅ ∈ β„‚)
133118, 123, 132syl2anc 411 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ (β™―β€˜π΄)) β†’ ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅ ∈ β„‚)
134 1cnd 7986 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ Β¬ 𝑝 ≀ (β™―β€˜π΄)) β†’ 1 ∈ β„‚)
13594, 12eqeltrrd 2265 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (β™―β€˜π΄) ∈ β„€)
136135adantr 276 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ (β™―β€˜π΄) ∈ β„€)
137 zdcle 9342 . . . . . . . . . . . . . . . . . 18 ((𝑝 ∈ β„€ ∧ (β™―β€˜π΄) ∈ β„€) β†’ DECID 𝑝 ≀ (β™―β€˜π΄))
13828, 136, 137syl2anc 411 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ DECID 𝑝 ≀ (β™―β€˜π΄))
139133, 134, 138ifcldadc 3575 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ if(𝑝 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅, 1) ∈ β„‚)
14083, 117, 8, 139fvmptd3 5622 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))β€˜π‘) = if(𝑝 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅, 1))
141140, 139eqeltrd 2264 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))β€˜π‘) ∈ β„‚)
142112, 141sylan2br 288 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑝 ∈ (β„€β‰₯β€˜1)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))β€˜π‘) ∈ β„‚)
143 mulcl 7951 . . . . . . . . . . . . . 14 ((𝑝 ∈ β„‚ ∧ π‘ž ∈ β„‚) β†’ (𝑝 Β· π‘ž) ∈ β„‚)
144143adantl 277 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑝 ∈ β„‚ ∧ π‘ž ∈ β„‚)) β†’ (𝑝 Β· π‘ž) ∈ β„‚)
14570, 111, 113, 142, 144seq3fveq 10484 . . . . . . . . . . . 12 (πœ‘ β†’ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€))
14619, 145jca 306 . . . . . . . . . . 11 (πœ‘ β†’ (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€)))
147 f1oeq1 5461 . . . . . . . . . . . 12 (𝑓 = 𝐹 β†’ (𝑓:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐹:(1...𝑀)–1-1-onto→𝐴))
148 fveq1 5526 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝐹 β†’ (π‘“β€˜π‘›) = (πΉβ€˜π‘›))
149148csbeq1d 3076 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝐹 β†’ ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅)
150149ifeq1d 3563 . . . . . . . . . . . . . . . 16 (𝑓 = 𝐹 β†’ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1) = if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))
151150mpteq2dv 4106 . . . . . . . . . . . . . . 15 (𝑓 = 𝐹 β†’ (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1)))
152151seqeq3d 10466 . . . . . . . . . . . . . 14 (𝑓 = 𝐹 β†’ seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1))) = seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))))
153152fveq1d 5529 . . . . . . . . . . . . 13 (𝑓 = 𝐹 β†’ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€))
154153eqeq2d 2199 . . . . . . . . . . . 12 (𝑓 = 𝐹 β†’ ((seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€) ↔ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€)))
155147, 154anbi12d 473 . . . . . . . . . . 11 (𝑓 = 𝐹 β†’ ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€)) ↔ (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€))))
15669, 146, 155spcedv 2838 . . . . . . . . . 10 (πœ‘ β†’ βˆƒπ‘“(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€)))
157 oveq2 5896 . . . . . . . . . . . . . 14 (π‘š = 𝑀 β†’ (1...π‘š) = (1...𝑀))
158157f1oeq2d 5469 . . . . . . . . . . . . 13 (π‘š = 𝑀 β†’ (𝑓:(1...π‘š)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑀)–1-1-onto→𝐴))
159 fveq2 5527 . . . . . . . . . . . . . 14 (π‘š = 𝑀 β†’ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€))
160159eqeq2d 2199 . . . . . . . . . . . . 13 (π‘š = 𝑀 β†’ ((seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š) ↔ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€)))
161158, 160anbi12d 473 . . . . . . . . . . . 12 (π‘š = 𝑀 β†’ ((𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)) ↔ (𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€))))
162161exbidv 1835 . . . . . . . . . . 11 (π‘š = 𝑀 β†’ (βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)) ↔ βˆƒπ‘“(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€))))
163162rspcev 2853 . . . . . . . . . 10 ((𝑀 ∈ β„• ∧ βˆƒπ‘“(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€))) β†’ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)))
16411, 156, 163syl2anc 411 . . . . . . . . 9 (πœ‘ β†’ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)))
165164olcd 735 . . . . . . . 8 (πœ‘ β†’ (βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))
166 nfcv 2329 . . . . . . . . . . . . . 14 Ⅎ𝑗if(π‘˜ ∈ 𝐴, 𝐡, 1)
167 nfv 1538 . . . . . . . . . . . . . . 15 β„²π‘˜ 𝑗 ∈ 𝐴
168 nfcsb1v 3102 . . . . . . . . . . . . . . 15 β„²π‘˜β¦‹π‘— / π‘˜β¦Œπ΅
169 nfcv 2329 . . . . . . . . . . . . . . 15 β„²π‘˜1
170167, 168, 169nfif 3574 . . . . . . . . . . . . . 14 β„²π‘˜if(𝑗 ∈ 𝐴, ⦋𝑗 / π‘˜β¦Œπ΅, 1)
171 eleq1w 2248 . . . . . . . . . . . . . . 15 (π‘˜ = 𝑗 β†’ (π‘˜ ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
172 csbeq1a 3078 . . . . . . . . . . . . . . 15 (π‘˜ = 𝑗 β†’ 𝐡 = ⦋𝑗 / π‘˜β¦Œπ΅)
173171, 172ifbieq1d 3568 . . . . . . . . . . . . . 14 (π‘˜ = 𝑗 β†’ if(π‘˜ ∈ 𝐴, 𝐡, 1) = if(𝑗 ∈ 𝐴, ⦋𝑗 / π‘˜β¦Œπ΅, 1))
174166, 170, 173cbvmpt 4110 . . . . . . . . . . . . 13 (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1)) = (𝑗 ∈ β„€ ↦ if(𝑗 ∈ 𝐴, ⦋𝑗 / π‘˜β¦Œπ΅, 1))
175168nfel1 2340 . . . . . . . . . . . . . . 15 β„²π‘˜β¦‹π‘— / π‘˜β¦Œπ΅ ∈ β„‚
176172eleq1d 2256 . . . . . . . . . . . . . . 15 (π‘˜ = 𝑗 β†’ (𝐡 ∈ β„‚ ↔ ⦋𝑗 / π‘˜β¦Œπ΅ ∈ β„‚))
177175, 176rspc 2847 . . . . . . . . . . . . . 14 (𝑗 ∈ 𝐴 β†’ (βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚ β†’ ⦋𝑗 / π‘˜β¦Œπ΅ ∈ β„‚))
178125, 177mpan9 281 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ 𝐴) β†’ ⦋𝑗 / π‘˜β¦Œπ΅ ∈ β„‚)
179 breq1 4018 . . . . . . . . . . . . . . 15 (𝑛 = 𝑖 β†’ (𝑛 ≀ (β™―β€˜π΄) ↔ 𝑖 ≀ (β™―β€˜π΄)))
180 fveq2 5527 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 β†’ (π‘“β€˜π‘›) = (π‘“β€˜π‘–))
181180csbeq1d 3076 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑖 β†’ ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(π‘“β€˜π‘–) / π‘˜β¦Œπ΅)
182 csbcow 3080 . . . . . . . . . . . . . . . 16 ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅ = ⦋(π‘“β€˜π‘–) / π‘˜β¦Œπ΅
183181, 182eqtr4di 2238 . . . . . . . . . . . . . . 15 (𝑛 = 𝑖 β†’ ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅)
184179, 183ifbieq1d 3568 . . . . . . . . . . . . . 14 (𝑛 = 𝑖 β†’ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1) = if(𝑖 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅, 1))
185184cbvmptv 4111 . . . . . . . . . . . . 13 (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)) = (𝑖 ∈ β„• ↦ if(𝑖 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅, 1))
186174, 178, 185prodmodc 11599 . . . . . . . . . . . 12 (πœ‘ β†’ βˆƒ*π‘₯(βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))
18736, 186jca 306 . . . . . . . . . . 11 (πœ‘ β†’ ((seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) ∈ β„‚ ∧ βˆƒ*π‘₯(βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)))))
188 breq2 4019 . . . . . . . . . . . . . . . 16 (π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) β†’ (seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯ ↔ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€)))
189188anbi2d 464 . . . . . . . . . . . . . . 15 (π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) β†’ ((βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯) ↔ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))))
190189anbi2d 464 . . . . . . . . . . . . . 14 (π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) β†’ (((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ↔ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€)))))
191190rexbidv 2488 . . . . . . . . . . . . 13 (π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) β†’ (βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ↔ βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€)))))
192 eqeq1 2194 . . . . . . . . . . . . . . . 16 (π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) β†’ (π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š) ↔ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)))
193192anbi2d 464 . . . . . . . . . . . . . . 15 (π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) β†’ ((𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)) ↔ (𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))
194193exbidv 1835 . . . . . . . . . . . . . 14 (π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) β†’ (βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)) ↔ βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))
195194rexbidv 2488 . . . . . . . . . . . . 13 (π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) β†’ (βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)) ↔ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))
196191, 195orbi12d 794 . . . . . . . . . . . 12 (π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) β†’ ((βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))) ↔ (βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)))))
197196moi2 2930 . . . . . . . . . . 11 ((((seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) ∈ β„‚ ∧ βˆƒ*π‘₯(βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)))) ∧ ((βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))) ∧ (βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))) β†’ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))
198187, 197sylan 283 . . . . . . . . . 10 ((πœ‘ ∧ ((βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))) ∧ (βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))) β†’ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))
199198ancom2s 566 . . . . . . . . 9 ((πœ‘ ∧ ((βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))) ∧ (βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))) β†’ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))
200199expr 375 . . . . . . . 8 ((πœ‘ ∧ (βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)))) β†’ ((βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))) β†’ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€)))
201165, 200mpdan 421 . . . . . . 7 (πœ‘ β†’ ((βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))) β†’ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€)))
20264, 201biimtrrid 153 . . . . . 6 (πœ‘ β†’ ((βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))) β†’ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€)))
20364, 196bitr3id 194 . . . . . . 7 (π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) β†’ ((βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))) ↔ (βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)))))
204165, 203syl5ibrcom 157 . . . . . 6 (πœ‘ β†’ (π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) β†’ (βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)))))
205202, 204impbid 129 . . . . 5 (πœ‘ β†’ ((βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))) ↔ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€)))
206205adantr 276 . . . 4 ((πœ‘ ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) ∈ β„‚) β†’ ((βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))) ↔ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€)))
207206iota5 5210 . . 3 ((πœ‘ ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) ∈ β„‚) β†’ (β„©π‘₯(βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)))) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))
20836, 207mpdan 421 . 2 (πœ‘ β†’ (β„©π‘₯(βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š)))) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))
2091, 208eqtrid 2232 1 (πœ‘ β†’ βˆπ‘˜ ∈ 𝐴 𝐡 = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€))
Colors of variables: wff set class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 709  DECID wdc 835   = wceq 1363  βˆƒwex 1502  βˆƒ*wmo 2037   ∈ wcel 2158  βˆ€wral 2465  βˆƒwrex 2466  Vcvv 2749  β¦‹csb 3069   βŠ† wss 3141  ifcif 3546   class class class wbr 4015   ↦ cmpt 4076  β„©cio 5188  βŸΆwf 5224  β€“1-1-ontoβ†’wf1o 5227  β€˜cfv 5228  (class class class)co 5888  Fincfn 6753  β„‚cc 7822  0cc0 7824  1c1 7825   Β· cmul 7829   ≀ cle 8006   # cap 8551  β„•cn 8932  β„•0cn0 9189  β„€cz 9266  β„€β‰₯cuz 9541  ...cfz 10021  seqcseq 10458  β™―chash 10768   ⇝ cli 11299  βˆcprod 11571
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 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7915  ax-resscn 7916  ax-1cn 7917  ax-1re 7918  ax-icn 7919  ax-addcl 7920  ax-addrcl 7921  ax-mulcl 7922  ax-mulrcl 7923  ax-addcom 7924  ax-mulcom 7925  ax-addass 7926  ax-mulass 7927  ax-distr 7928  ax-i2m1 7929  ax-0lt1 7930  ax-1rid 7931  ax-0id 7932  ax-rnegex 7933  ax-precex 7934  ax-cnre 7935  ax-pre-ltirr 7936  ax-pre-ltwlin 7937  ax-pre-lttrn 7938  ax-pre-apti 7939  ax-pre-ltadd 7940  ax-pre-mulgt0 7941  ax-pre-mulext 7942  ax-arch 7943  ax-caucvg 7944
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-isom 5237  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6154  df-2nd 6155  df-recs 6319  df-irdg 6384  df-frec 6405  df-1o 6430  df-oadd 6434  df-er 6548  df-en 6754  df-dom 6755  df-fin 6756  df-pnf 8007  df-mnf 8008  df-xr 8009  df-ltxr 8010  df-le 8011  df-sub 8143  df-neg 8144  df-reap 8545  df-ap 8552  df-div 8643  df-inn 8933  df-2 8991  df-3 8992  df-4 8993  df-n0 9190  df-z 9267  df-uz 9542  df-q 9633  df-rp 9667  df-fz 10022  df-fzo 10156  df-seqfrec 10459  df-exp 10533  df-ihash 10769  df-cj 10864  df-re 10865  df-im 10866  df-rsqrt 11020  df-abs 11021  df-clim 11300  df-proddc 11572
This theorem is referenced by:  prod1dc  11607  fprodf1o  11609  fprodmul  11612  prodsnf  11613
  Copyright terms: Public domain W3C validator