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

Theorem fprodseq 11608
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 11576 . 2 βˆπ‘˜ ∈ 𝐴 𝐡 = (β„©π‘₯(βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))
2 nnuz 9580 . . . . 5 β„• = (β„€β‰₯β€˜1)
3 1zzd 9297 . . . . 5 (πœ‘ β†’ 1 ∈ β„€)
4 eqid 2188 . . . . . . 7 (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))
5 breq1 4020 . . . . . . . 8 (𝑛 = 𝑝 β†’ (𝑛 ≀ 𝑀 ↔ 𝑝 ≀ 𝑀))
6 fveq2 5529 . . . . . . . 8 (𝑛 = 𝑝 β†’ (πΊβ€˜π‘›) = (πΊβ€˜π‘))
75, 6ifbieq1d 3570 . . . . . . 7 (𝑛 = 𝑝 β†’ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1) = if(𝑝 ≀ 𝑀, (πΊβ€˜π‘), 1))
8 simpr 110 . . . . . . 7 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ 𝑝 ∈ β„•)
9 simpll 527 . . . . . . . . 9 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ 𝑀) β†’ πœ‘)
108anim1i 340 . . . . . . . . . 10 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ 𝑀) β†’ (𝑝 ∈ β„• ∧ 𝑝 ≀ 𝑀))
11 fprod.2 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀 ∈ β„•)
1211nnzd 9391 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑀 ∈ β„€)
13 fznn 10106 . . . . . . . . . . . 12 (𝑀 ∈ β„€ β†’ (𝑝 ∈ (1...𝑀) ↔ (𝑝 ∈ β„• ∧ 𝑝 ≀ 𝑀)))
1412, 13syl 14 . . . . . . . . . . 11 (πœ‘ β†’ (𝑝 ∈ (1...𝑀) ↔ (𝑝 ∈ β„• ∧ 𝑝 ≀ 𝑀)))
1514ad2antrr 488 . . . . . . . . . 10 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ 𝑀) β†’ (𝑝 ∈ (1...𝑀) ↔ (𝑝 ∈ β„• ∧ 𝑝 ≀ 𝑀)))
1610, 15mpbird 167 . . . . . . . . 9 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ 𝑀) β†’ 𝑝 ∈ (1...𝑀))
176eleq1d 2257 . . . . . . . . . 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 11411 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) ∈ β„‚)
2322adantr 276 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ (1...𝑀)) β†’ βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) ∈ β„‚)
24 simpr 110 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ (1...𝑀)) β†’ 𝑝 ∈ (1...𝑀))
2517, 23, 24rspcdva 2860 . . . . . . . . 9 ((πœ‘ ∧ 𝑝 ∈ (1...𝑀)) β†’ (πΊβ€˜π‘) ∈ β„‚)
269, 16, 25syl2anc 411 . . . . . . . 8 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ 𝑀) β†’ (πΊβ€˜π‘) ∈ β„‚)
27 1cnd 7990 . . . . . . . 8 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ Β¬ 𝑝 ≀ 𝑀) β†’ 1 ∈ β„‚)
288nnzd 9391 . . . . . . . . 9 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ 𝑝 ∈ β„€)
2912adantr 276 . . . . . . . . 9 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ 𝑀 ∈ β„€)
30 zdcle 9346 . . . . . . . . 9 ((𝑝 ∈ β„€ ∧ 𝑀 ∈ β„€) β†’ DECID 𝑝 ≀ 𝑀)
3128, 29, 30syl2anc 411 . . . . . . . 8 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ DECID 𝑝 ≀ 𝑀)
3226, 27, 31ifcldadc 3577 . . . . . . 7 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ if(𝑝 ≀ 𝑀, (πΊβ€˜π‘), 1) ∈ β„‚)
334, 7, 8, 32fvmptd3 5624 . . . . . 6 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))β€˜π‘) = if(𝑝 ≀ 𝑀, (πΊβ€˜π‘), 1))
3433, 32eqeltrd 2265 . . . . 5 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))β€˜π‘) ∈ β„‚)
352, 3, 34prodf 11563 . . . 4 (πœ‘ β†’ seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))):β„•βŸΆβ„‚)
3635, 11ffvelcdmd 5667 . . 3 (πœ‘ β†’ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) ∈ β„‚)
37 eleq1w 2249 . . . . . . . . . . . . 13 (𝑖 = 𝑗 β†’ (𝑖 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
3837dcbid 839 . . . . . . . . . . . 12 (𝑖 = 𝑗 β†’ (DECID 𝑖 ∈ 𝐴 ↔ DECID 𝑗 ∈ 𝐴))
3938cbvralv 2717 . . . . . . . . . . 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 2496 . . . . . . . 8 (βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘š)DECID 𝑖 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ↔ βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)))
43 nnnn0 9200 . . . . . . . . . . . . . . . . . . . . 21 (π‘š ∈ β„• β†’ π‘š ∈ β„•0)
44 hashfz1 10780 . . . . . . . . . . . . . . . . . . . . 21 (π‘š ∈ β„•0 β†’ (β™―β€˜(1...π‘š)) = π‘š)
4543, 44syl 14 . . . . . . . . . . . . . . . . . . . 20 (π‘š ∈ β„• β†’ (β™―β€˜(1...π‘š)) = π‘š)
4645adantr 276 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (β™―β€˜(1...π‘š)) = π‘š)
47 1zzd 9297 . . . . . . . . . . . . . . . . . . . . 21 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ 1 ∈ β„€)
48 nnz 9289 . . . . . . . . . . . . . . . . . . . . . 22 (π‘š ∈ β„• β†’ π‘š ∈ β„€)
4948adantr 276 . . . . . . . . . . . . . . . . . . . . 21 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ π‘š ∈ β„€)
5047, 49fzfigd 10448 . . . . . . . . . . . . . . . . . . . 20 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (1...π‘š) ∈ Fin)
51 simpr 110 . . . . . . . . . . . . . . . . . . . 20 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ 𝑓:(1...π‘š)–1-1-onto→𝐴)
5250, 51fihasheqf1od 10786 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (β™―β€˜(1...π‘š)) = (β™―β€˜π΄))
5346, 52eqtr3d 2223 . . . . . . . . . . . . . . . . . 18 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ π‘š = (β™―β€˜π΄))
5453breq2d 4029 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (𝑛 ≀ π‘š ↔ 𝑛 ≀ (β™―β€˜π΄)))
5554ifbid 3569 . . . . . . . . . . . . . . . 16 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1) = if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1))
5655mpteq2dv 4108 . . . . . . . . . . . . . . 15 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))
5756seqeq3d 10470 . . . . . . . . . . . . . 14 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1))) = seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1))))
5857fveq1d 5531 . . . . . . . . . . . . 13 ((π‘š ∈ β„• ∧ 𝑓:(1...π‘š)–1-1-onto→𝐴) β†’ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))
5958eqeq2d 2200 . . . . . . . . . . . 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 2504 . . . . . . . . 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 5475 . . . . . . . . . . . . 13 (𝐹:(1...𝑀)–1-1-onto→𝐴 β†’ 𝐹:(1...𝑀)⟢𝐴)
6619, 65syl 14 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹:(1...𝑀)⟢𝐴)
673, 12fzfigd 10448 . . . . . . . . . . . 12 (πœ‘ β†’ (1...𝑀) ∈ Fin)
68 fex 5760 . . . . . . . . . . . 12 ((𝐹:(1...𝑀)⟢𝐴 ∧ (1...𝑀) ∈ Fin) β†’ 𝐹 ∈ V)
6966, 67, 68syl2anc 411 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹 ∈ V)
7011, 2eleqtrdi 2281 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀 ∈ (β„€β‰₯β€˜1))
71 fveq2 5529 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑒 β†’ (πΉβ€˜π‘›) = (πΉβ€˜π‘’))
7271csbeq1d 3078 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑒 β†’ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅)
73 fveq2 5529 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑒 β†’ (πΊβ€˜π‘›) = (πΊβ€˜π‘’))
7472, 73eqeq12d 2203 . . . . . . . . . . . . . . 15 (𝑛 = 𝑒 β†’ (⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = (πΊβ€˜π‘›) ↔ ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅ = (πΊβ€˜π‘’)))
7566ffvelcdmda 5666 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ (πΉβ€˜π‘›) ∈ 𝐴)
7618adantl 277 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) ∧ π‘˜ = (πΉβ€˜π‘›)) β†’ 𝐡 = 𝐢)
7775, 76csbied 3117 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = 𝐢)
7877, 21eqtr4d 2224 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (1...𝑀)) β†’ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = (πΊβ€˜π‘›))
7978ralrimiva 2562 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ βˆ€π‘› ∈ (1...𝑀)⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = (πΊβ€˜π‘›))
8079adantr 276 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ βˆ€π‘› ∈ (1...𝑀)⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = (πΊβ€˜π‘›))
81 simpr 110 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ 𝑒 ∈ (1...𝑀))
8274, 80, 81rspcdva 2860 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅ = (πΊβ€˜π‘’))
83 eqid 2188 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))
84 breq1 4020 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑒 β†’ (𝑛 ≀ (β™―β€˜π΄) ↔ 𝑒 ≀ (β™―β€˜π΄)))
8584, 72ifbieq1d 3570 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑒 β†’ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1) = if(𝑒 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅, 1))
86 elfznn 10071 . . . . . . . . . . . . . . . . 17 (𝑒 ∈ (1...𝑀) β†’ 𝑒 ∈ β„•)
8786adantl 277 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ 𝑒 ∈ β„•)
88 elfzle2 10045 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ (1...𝑀) β†’ 𝑒 ≀ 𝑀)
8988adantl 277 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ 𝑒 ≀ 𝑀)
9011nnnn0d 9246 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 𝑀 ∈ β„•0)
91 hashfz1 10780 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ β„•0 β†’ (β™―β€˜(1...𝑀)) = 𝑀)
9290, 91syl 14 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (β™―β€˜(1...𝑀)) = 𝑀)
9367, 19fihasheqf1od 10786 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (β™―β€˜(1...𝑀)) = (β™―β€˜π΄))
9492, 93eqtr3d 2223 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝑀 = (β™―β€˜π΄))
9594adantr 276 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ 𝑀 = (β™―β€˜π΄))
9689, 95breqtrd 4043 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ 𝑒 ≀ (β™―β€˜π΄))
9796iftrued 3555 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ if(𝑒 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅, 1) = ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅)
9897, 82eqtrd 2221 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ if(𝑒 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅, 1) = (πΊβ€˜π‘’))
9973eleq1d 2257 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑒 β†’ ((πΊβ€˜π‘›) ∈ β„‚ ↔ (πΊβ€˜π‘’) ∈ β„‚))
10022adantr 276 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ βˆ€π‘› ∈ (1...𝑀)(πΊβ€˜π‘›) ∈ β„‚)
10199, 100, 81rspcdva 2860 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ (πΊβ€˜π‘’) ∈ β„‚)
10298, 101eqeltrd 2265 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ if(𝑒 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅, 1) ∈ β„‚)
10383, 85, 87, 102fvmptd3 5624 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))β€˜π‘’) = if(𝑒 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅, 1))
104103, 97eqtrd 2221 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))β€˜π‘’) = ⦋(πΉβ€˜π‘’) / π‘˜β¦Œπ΅)
105 breq1 4020 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑒 β†’ (𝑛 ≀ 𝑀 ↔ 𝑒 ≀ 𝑀))
106105, 73ifbieq1d 3570 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑒 β†’ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1) = if(𝑒 ≀ 𝑀, (πΊβ€˜π‘’), 1))
10789iftrued 3555 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ if(𝑒 ≀ 𝑀, (πΊβ€˜π‘’), 1) = (πΊβ€˜π‘’))
108107, 101eqeltrd 2265 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ if(𝑒 ≀ 𝑀, (πΊβ€˜π‘’), 1) ∈ β„‚)
1094, 106, 87, 108fvmptd3 5624 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))β€˜π‘’) = if(𝑒 ≀ 𝑀, (πΊβ€˜π‘’), 1))
110109, 107eqtrd 2221 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))β€˜π‘’) = (πΊβ€˜π‘’))
11182, 104, 1103eqtr4rd 2232 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (1...𝑀)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))β€˜π‘’) = ((𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))β€˜π‘’))
112 elnnuz 9581 . . . . . . . . . . . . . 14 (𝑝 ∈ β„• ↔ 𝑝 ∈ (β„€β‰₯β€˜1))
113112, 34sylan2br 288 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑝 ∈ (β„€β‰₯β€˜1)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1))β€˜π‘) ∈ β„‚)
114 breq1 4020 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑝 β†’ (𝑛 ≀ (β™―β€˜π΄) ↔ 𝑝 ≀ (β™―β€˜π΄)))
115 fveq2 5529 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑝 β†’ (πΉβ€˜π‘›) = (πΉβ€˜π‘))
116115csbeq1d 3078 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑝 β†’ ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅)
117114, 116ifbieq1d 3570 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑝 β†’ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1) = if(𝑝 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅, 1))
118 simpll 527 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ (β™―β€˜π΄)) β†’ πœ‘)
119 simpr 110 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ (β™―β€˜π΄)) β†’ 𝑝 ≀ (β™―β€˜π΄))
12094breq2d 4029 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑝 ≀ 𝑀 ↔ 𝑝 ≀ (β™―β€˜π΄)))
121120ad2antrr 488 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ (β™―β€˜π΄)) β†’ (𝑝 ≀ 𝑀 ↔ 𝑝 ≀ (β™―β€˜π΄)))
122119, 121mpbird 167 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ (β™―β€˜π΄)) β†’ 𝑝 ≀ 𝑀)
123122, 16syldan 282 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ (β™―β€˜π΄)) β†’ 𝑝 ∈ (1...𝑀))
12466ffvelcdmda 5666 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ (1...𝑀)) β†’ (πΉβ€˜π‘) ∈ 𝐴)
12520ralrimiva 2562 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚)
126125adantr 276 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ (1...𝑀)) β†’ βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚)
127 nfcsb1v 3104 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘˜β¦‹(πΉβ€˜π‘) / π‘˜β¦Œπ΅
128127nfel1 2342 . . . . . . . . . . . . . . . . . . . 20 β„²π‘˜β¦‹(πΉβ€˜π‘) / π‘˜β¦Œπ΅ ∈ β„‚
129 csbeq1a 3080 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ = (πΉβ€˜π‘) β†’ 𝐡 = ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅)
130129eleq1d 2257 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = (πΉβ€˜π‘) β†’ (𝐡 ∈ β„‚ ↔ ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅ ∈ β„‚))
131128, 130rspc 2849 . . . . . . . . . . . . . . . . . . 19 ((πΉβ€˜π‘) ∈ 𝐴 β†’ (βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚ β†’ ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅ ∈ β„‚))
132124, 126, 131sylc 62 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑝 ∈ (1...𝑀)) β†’ ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅ ∈ β„‚)
133118, 123, 132syl2anc 411 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ 𝑝 ≀ (β™―β€˜π΄)) β†’ ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅ ∈ β„‚)
134 1cnd 7990 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑝 ∈ β„•) ∧ Β¬ 𝑝 ≀ (β™―β€˜π΄)) β†’ 1 ∈ β„‚)
13594, 12eqeltrrd 2266 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (β™―β€˜π΄) ∈ β„€)
136135adantr 276 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ (β™―β€˜π΄) ∈ β„€)
137 zdcle 9346 . . . . . . . . . . . . . . . . . 18 ((𝑝 ∈ β„€ ∧ (β™―β€˜π΄) ∈ β„€) β†’ DECID 𝑝 ≀ (β™―β€˜π΄))
13828, 136, 137syl2anc 411 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ DECID 𝑝 ≀ (β™―β€˜π΄))
139133, 134, 138ifcldadc 3577 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ if(𝑝 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅, 1) ∈ β„‚)
14083, 117, 8, 139fvmptd3 5624 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))β€˜π‘) = if(𝑝 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘) / π‘˜β¦Œπ΅, 1))
141140, 139eqeltrd 2265 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑝 ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))β€˜π‘) ∈ β„‚)
142112, 141sylan2br 288 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑝 ∈ (β„€β‰₯β€˜1)) β†’ ((𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))β€˜π‘) ∈ β„‚)
143 mulcl 7955 . . . . . . . . . . . . . 14 ((𝑝 ∈ β„‚ ∧ π‘ž ∈ β„‚) β†’ (𝑝 Β· π‘ž) ∈ β„‚)
144143adantl 277 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑝 ∈ β„‚ ∧ π‘ž ∈ β„‚)) β†’ (𝑝 Β· π‘ž) ∈ β„‚)
14570, 111, 113, 142, 144seq3fveq 10488 . . . . . . . . . . . 12 (πœ‘ β†’ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€))
14619, 145jca 306 . . . . . . . . . . 11 (πœ‘ β†’ (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€)))
147 f1oeq1 5463 . . . . . . . . . . . 12 (𝑓 = 𝐹 β†’ (𝑓:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐹:(1...𝑀)–1-1-onto→𝐴))
148 fveq1 5528 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝐹 β†’ (π‘“β€˜π‘›) = (πΉβ€˜π‘›))
149148csbeq1d 3078 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝐹 β†’ ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅)
150149ifeq1d 3565 . . . . . . . . . . . . . . . 16 (𝑓 = 𝐹 β†’ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1) = if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))
151150mpteq2dv 4108 . . . . . . . . . . . . . . 15 (𝑓 = 𝐹 β†’ (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)) = (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1)))
152151seqeq3d 10470 . . . . . . . . . . . . . 14 (𝑓 = 𝐹 β†’ seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1))) = seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1))))
153152fveq1d 5531 . . . . . . . . . . . . 13 (𝑓 = 𝐹 β†’ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(πΉβ€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€))
154153eqeq2d 2200 . . . . . . . . . . . 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 2840 . . . . . . . . . 10 (πœ‘ β†’ βˆƒπ‘“(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ 𝑀, (πΊβ€˜π‘›), 1)))β€˜π‘€) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€)))
157 oveq2 5898 . . . . . . . . . . . . . 14 (π‘š = 𝑀 β†’ (1...π‘š) = (1...𝑀))
158157f1oeq2d 5471 . . . . . . . . . . . . 13 (π‘š = 𝑀 β†’ (𝑓:(1...π‘š)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑀)–1-1-onto→𝐴))
159 fveq2 5529 . . . . . . . . . . . . . 14 (π‘š = 𝑀 β†’ (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘€))
160159eqeq2d 2200 . . . . . . . . . . . . 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 2855 . . . . . . . . . 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 2331 . . . . . . . . . . . . . 14 Ⅎ𝑗if(π‘˜ ∈ 𝐴, 𝐡, 1)
167 nfv 1538 . . . . . . . . . . . . . . 15 β„²π‘˜ 𝑗 ∈ 𝐴
168 nfcsb1v 3104 . . . . . . . . . . . . . . 15 β„²π‘˜β¦‹π‘— / π‘˜β¦Œπ΅
169 nfcv 2331 . . . . . . . . . . . . . . 15 β„²π‘˜1
170167, 168, 169nfif 3576 . . . . . . . . . . . . . 14 β„²π‘˜if(𝑗 ∈ 𝐴, ⦋𝑗 / π‘˜β¦Œπ΅, 1)
171 eleq1w 2249 . . . . . . . . . . . . . . 15 (π‘˜ = 𝑗 β†’ (π‘˜ ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
172 csbeq1a 3080 . . . . . . . . . . . . . . 15 (π‘˜ = 𝑗 β†’ 𝐡 = ⦋𝑗 / π‘˜β¦Œπ΅)
173171, 172ifbieq1d 3570 . . . . . . . . . . . . . 14 (π‘˜ = 𝑗 β†’ if(π‘˜ ∈ 𝐴, 𝐡, 1) = if(𝑗 ∈ 𝐴, ⦋𝑗 / π‘˜β¦Œπ΅, 1))
174166, 170, 173cbvmpt 4112 . . . . . . . . . . . . 13 (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1)) = (𝑗 ∈ β„€ ↦ if(𝑗 ∈ 𝐴, ⦋𝑗 / π‘˜β¦Œπ΅, 1))
175168nfel1 2342 . . . . . . . . . . . . . . 15 β„²π‘˜β¦‹π‘— / π‘˜β¦Œπ΅ ∈ β„‚
176172eleq1d 2257 . . . . . . . . . . . . . . 15 (π‘˜ = 𝑗 β†’ (𝐡 ∈ β„‚ ↔ ⦋𝑗 / π‘˜β¦Œπ΅ ∈ β„‚))
177175, 176rspc 2849 . . . . . . . . . . . . . 14 (𝑗 ∈ 𝐴 β†’ (βˆ€π‘˜ ∈ 𝐴 𝐡 ∈ β„‚ β†’ ⦋𝑗 / π‘˜β¦Œπ΅ ∈ β„‚))
178125, 177mpan9 281 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ 𝐴) β†’ ⦋𝑗 / π‘˜β¦Œπ΅ ∈ β„‚)
179 breq1 4020 . . . . . . . . . . . . . . 15 (𝑛 = 𝑖 β†’ (𝑛 ≀ (β™―β€˜π΄) ↔ 𝑖 ≀ (β™―β€˜π΄)))
180 fveq2 5529 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 β†’ (π‘“β€˜π‘›) = (π‘“β€˜π‘–))
181180csbeq1d 3078 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑖 β†’ ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(π‘“β€˜π‘–) / π‘˜β¦Œπ΅)
182 csbcow 3082 . . . . . . . . . . . . . . . 16 ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅ = ⦋(π‘“β€˜π‘–) / π‘˜β¦Œπ΅
183181, 182eqtr4di 2239 . . . . . . . . . . . . . . 15 (𝑛 = 𝑖 β†’ ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅ = ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅)
184179, 183ifbieq1d 3570 . . . . . . . . . . . . . 14 (𝑛 = 𝑖 β†’ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1) = if(𝑖 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅, 1))
185184cbvmptv 4113 . . . . . . . . . . . . 13 (𝑛 ∈ β„• ↦ if(𝑛 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)) = (𝑖 ∈ β„• ↦ if(𝑖 ≀ (β™―β€˜π΄), ⦋(π‘“β€˜π‘–) / π‘—β¦Œβ¦‹π‘— / π‘˜β¦Œπ΅, 1))
186174, 178, 185prodmodc 11603 . . . . . . . . . . . 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 4021 . . . . . . . . . . . . . . . 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 2490 . . . . . . . . . . . . 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 2195 . . . . . . . . . . . . . . . 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 2490 . . . . . . . . . . . . 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 2932 . . . . . . . . . . 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 5212 . . 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 2233 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 2038   ∈ wcel 2159  βˆ€wral 2467  βˆƒwrex 2468  Vcvv 2751  β¦‹csb 3071   βŠ† wss 3143  ifcif 3548   class class class wbr 4017   ↦ cmpt 4078  β„©cio 5190  βŸΆwf 5226  β€“1-1-ontoβ†’wf1o 5229  β€˜cfv 5230  (class class class)co 5890  Fincfn 6757  β„‚cc 7826  0cc0 7828  1c1 7829   Β· cmul 7833   ≀ cle 8010   # cap 8555  β„•cn 8936  β„•0cn0 9193  β„€cz 9270  β„€β‰₯cuz 9545  ...cfz 10025  seqcseq 10462  β™―chash 10772   ⇝ cli 11303  βˆcprod 11575
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 2161  ax-14 2162  ax-ext 2170  ax-coll 4132  ax-sep 4135  ax-nul 4143  ax-pow 4188  ax-pr 4223  ax-un 4447  ax-setind 4550  ax-iinf 4601  ax-cnex 7919  ax-resscn 7920  ax-1cn 7921  ax-1re 7922  ax-icn 7923  ax-addcl 7924  ax-addrcl 7925  ax-mulcl 7926  ax-mulrcl 7927  ax-addcom 7928  ax-mulcom 7929  ax-addass 7930  ax-mulass 7931  ax-distr 7932  ax-i2m1 7933  ax-0lt1 7934  ax-1rid 7935  ax-0id 7936  ax-rnegex 7937  ax-precex 7938  ax-cnre 7939  ax-pre-ltirr 7940  ax-pre-ltwlin 7941  ax-pre-lttrn 7942  ax-pre-apti 7943  ax-pre-ltadd 7944  ax-pre-mulgt0 7945  ax-pre-mulext 7946  ax-arch 7947  ax-caucvg 7948
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 2040  df-mo 2041  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-ne 2360  df-nel 2455  df-ral 2472  df-rex 2473  df-reu 2474  df-rmo 2475  df-rab 2476  df-v 2753  df-sbc 2977  df-csb 3072  df-dif 3145  df-un 3147  df-in 3149  df-ss 3156  df-nul 3437  df-if 3549  df-pw 3591  df-sn 3612  df-pr 3613  df-op 3615  df-uni 3824  df-int 3859  df-iun 3902  df-br 4018  df-opab 4079  df-mpt 4080  df-tr 4116  df-id 4307  df-po 4310  df-iso 4311  df-iord 4380  df-on 4382  df-ilim 4383  df-suc 4385  df-iom 4604  df-xp 4646  df-rel 4647  df-cnv 4648  df-co 4649  df-dm 4650  df-rn 4651  df-res 4652  df-ima 4653  df-iota 5192  df-fun 5232  df-fn 5233  df-f 5234  df-f1 5235  df-fo 5236  df-f1o 5237  df-fv 5238  df-isom 5239  df-riota 5846  df-ov 5893  df-oprab 5894  df-mpo 5895  df-1st 6158  df-2nd 6159  df-recs 6323  df-irdg 6388  df-frec 6409  df-1o 6434  df-oadd 6438  df-er 6552  df-en 6758  df-dom 6759  df-fin 6760  df-pnf 8011  df-mnf 8012  df-xr 8013  df-ltxr 8014  df-le 8015  df-sub 8147  df-neg 8148  df-reap 8549  df-ap 8556  df-div 8647  df-inn 8937  df-2 8995  df-3 8996  df-4 8997  df-n0 9194  df-z 9271  df-uz 9546  df-q 9637  df-rp 9671  df-fz 10026  df-fzo 10160  df-seqfrec 10463  df-exp 10537  df-ihash 10773  df-cj 10868  df-re 10869  df-im 10870  df-rsqrt 11024  df-abs 11025  df-clim 11304  df-proddc 11576
This theorem is referenced by:  prod1dc  11611  fprodf1o  11613  fprodmul  11616  prodsnf  11617
  Copyright terms: Public domain W3C validator