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

Theorem zproddc 11529
Description: Series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 5-Dec-2017.)
Hypotheses
Ref Expression
zprod.1 𝑍 = (ℤ𝑀)
zprod.2 (𝜑𝑀 ∈ ℤ)
zproddc.3 (𝜑 → ∃𝑛𝑍𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
zprod.4 (𝜑𝐴𝑍)
zproddc.dc (𝜑 → ∀𝑗𝑍 DECID 𝑗𝐴)
zprod.5 ((𝜑𝑘𝑍) → (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
zprod.6 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
Assertion
Ref Expression
zproddc (𝜑 → ∏𝑘𝐴 𝐵 = ( ⇝ ‘seq𝑀( · , 𝐹)))
Distinct variable groups:   𝐴,𝑗,𝑘,𝑛,𝑦   𝐵,𝑗,𝑛,𝑦   𝑘,𝐹   𝑗,𝑀,𝑘,𝑛,𝑦   𝑗,𝑍,𝑘,𝑛   𝜑,𝑗,𝑘,𝑛,𝑦
Allowed substitution hints:   𝐵(𝑘)   𝐹(𝑦,𝑗,𝑛)   𝑍(𝑦)

Proof of Theorem zproddc
Dummy variables 𝑓 𝑔 𝑖 𝑚 𝑝 𝑟 𝑞 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 524 . . . . . . . . 9 (((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) → 𝐴 ⊆ (ℤ𝑚))
2 simprr 527 . . . . . . . . 9 (((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)
31, 2jca 304 . . . . . . . 8 (((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) → (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
4 nfcv 2312 . . . . . . . . . . . 12 𝑖if(𝑘𝐴, 𝐵, 1)
5 nfv 1521 . . . . . . . . . . . . 13 𝑘 𝑖𝐴
6 nfcsb1v 3082 . . . . . . . . . . . . 13 𝑘𝑖 / 𝑘𝐵
7 nfcv 2312 . . . . . . . . . . . . 13 𝑘1
85, 6, 7nfif 3553 . . . . . . . . . . . 12 𝑘if(𝑖𝐴, 𝑖 / 𝑘𝐵, 1)
9 eleq1w 2231 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (𝑘𝐴𝑖𝐴))
10 csbeq1a 3058 . . . . . . . . . . . . 13 (𝑘 = 𝑖𝐵 = 𝑖 / 𝑘𝐵)
119, 10ifbieq1d 3547 . . . . . . . . . . . 12 (𝑘 = 𝑖 → if(𝑘𝐴, 𝐵, 1) = if(𝑖𝐴, 𝑖 / 𝑘𝐵, 1))
124, 8, 11cbvmpt 4082 . . . . . . . . . . 11 (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)) = (𝑖 ∈ ℤ ↦ if(𝑖𝐴, 𝑖 / 𝑘𝐵, 1))
13 simpll 524 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) → 𝜑)
14 zprod.6 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
1514ralrimiva 2543 . . . . . . . . . . . . 13 (𝜑 → ∀𝑘𝐴 𝐵 ∈ ℂ)
166nfel1 2323 . . . . . . . . . . . . . 14 𝑘𝑖 / 𝑘𝐵 ∈ ℂ
1710eleq1d 2239 . . . . . . . . . . . . . 14 (𝑘 = 𝑖 → (𝐵 ∈ ℂ ↔ 𝑖 / 𝑘𝐵 ∈ ℂ))
1816, 17rspc 2828 . . . . . . . . . . . . 13 (𝑖𝐴 → (∀𝑘𝐴 𝐵 ∈ ℂ → 𝑖 / 𝑘𝐵 ∈ ℂ))
1915, 18syl5 32 . . . . . . . . . . . 12 (𝑖𝐴 → (𝜑𝑖 / 𝑘𝐵 ∈ ℂ))
2013, 19mpan9 279 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖𝐴) → 𝑖 / 𝑘𝐵 ∈ ℂ)
21 simplr 525 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) → 𝑚 ∈ ℤ)
22 zprod.2 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℤ)
2322ad2antrr 485 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) → 𝑀 ∈ ℤ)
24 simpr 109 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) → 𝐴 ⊆ (ℤ𝑚))
25 zprod.4 . . . . . . . . . . . . 13 (𝜑𝐴𝑍)
26 zprod.1 . . . . . . . . . . . . 13 𝑍 = (ℤ𝑀)
2725, 26sseqtrdi 3195 . . . . . . . . . . . 12 (𝜑𝐴 ⊆ (ℤ𝑀))
2827ad2antrr 485 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) → 𝐴 ⊆ (ℤ𝑀))
29 zproddc.dc . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑗𝑍 DECID 𝑗𝐴)
3026raleqi 2669 . . . . . . . . . . . . . . . . . 18 (∀𝑗𝑍 DECID 𝑗𝐴 ↔ ∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴)
3129, 30sylib 121 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴)
32 eleq1w 2231 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝑗𝐴𝑖𝐴))
3332dcbid 833 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → (DECID 𝑗𝐴DECID 𝑖𝐴))
3433cbvralv 2696 . . . . . . . . . . . . . . . . 17 (∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴 ↔ ∀𝑖 ∈ (ℤ𝑀)DECID 𝑖𝐴)
3531, 34sylib 121 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑖 ∈ (ℤ𝑀)DECID 𝑖𝐴)
3635r19.21bi 2558 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → DECID 𝑖𝐴)
3736adantlr 474 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℤ) ∧ 𝑖 ∈ (ℤ𝑀)) → DECID 𝑖𝐴)
3837adantlr 474 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑀)) → DECID 𝑖𝐴)
3938adantlr 474 . . . . . . . . . . . 12 (((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑀)) → DECID 𝑖𝐴)
40 simp-4l 536 . . . . . . . . . . . . . . 15 (((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) ∧ ¬ 𝑖 ∈ (ℤ𝑀)) → 𝜑)
41 simpr 109 . . . . . . . . . . . . . . 15 (((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) ∧ ¬ 𝑖 ∈ (ℤ𝑀)) → ¬ 𝑖 ∈ (ℤ𝑀))
4227ssneld 3149 . . . . . . . . . . . . . . 15 (𝜑 → (¬ 𝑖 ∈ (ℤ𝑀) → ¬ 𝑖𝐴))
4340, 41, 42sylc 62 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) ∧ ¬ 𝑖 ∈ (ℤ𝑀)) → ¬ 𝑖𝐴)
4443olcd 729 . . . . . . . . . . . . 13 (((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) ∧ ¬ 𝑖 ∈ (ℤ𝑀)) → (𝑖𝐴 ∨ ¬ 𝑖𝐴))
45 df-dc 830 . . . . . . . . . . . . 13 (DECID 𝑖𝐴 ↔ (𝑖𝐴 ∨ ¬ 𝑖𝐴))
4644, 45sylibr 133 . . . . . . . . . . . 12 (((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) ∧ ¬ 𝑖 ∈ (ℤ𝑀)) → DECID 𝑖𝐴)
47 eluzelz 9483 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ𝑚) → 𝑖 ∈ ℤ)
48 eluzdc 9556 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → DECID 𝑖 ∈ (ℤ𝑀))
4923, 47, 48syl2an 287 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) → DECID 𝑖 ∈ (ℤ𝑀))
50 exmiddc 831 . . . . . . . . . . . . 13 (DECID 𝑖 ∈ (ℤ𝑀) → (𝑖 ∈ (ℤ𝑀) ∨ ¬ 𝑖 ∈ (ℤ𝑀)))
5149, 50syl 14 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) → (𝑖 ∈ (ℤ𝑀) ∨ ¬ 𝑖 ∈ (ℤ𝑀)))
5239, 46, 51mpjaodan 793 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) → DECID 𝑖𝐴)
5312, 20, 21, 23, 24, 28, 52, 38prodrbdc 11524 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
5453biimpd 143 . . . . . . . . 9 (((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥 → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
5554expimpd 361 . . . . . . . 8 ((𝜑𝑚 ∈ ℤ) → ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
563, 55syl5 32 . . . . . . 7 ((𝜑𝑚 ∈ ℤ) → (((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
5756rexlimdva 2587 . . . . . 6 (𝜑 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
58 uzssz 9493 . . . . . . . . . . . . . 14 (ℤ𝑀) ⊆ ℤ
5927, 58sstrdi 3159 . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ ℤ)
6059ad2antrr 485 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → 𝐴 ⊆ ℤ)
61 1zzd 9226 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → 1 ∈ ℤ)
62 nnz 9218 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
6362adantl 275 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℤ)
6463adantr 274 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → 𝑚 ∈ ℤ)
6561, 64fzfigd 10374 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → (1...𝑚) ∈ Fin)
66 simpr 109 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → 𝑓:(1...𝑚)–1-1-onto𝐴)
67 f1oeng 6731 . . . . . . . . . . . . . . 15 (((1...𝑚) ∈ Fin ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → (1...𝑚) ≈ 𝐴)
6865, 66, 67syl2anc 409 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → (1...𝑚) ≈ 𝐴)
6968ensymd 6757 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → 𝐴 ≈ (1...𝑚))
70 enfii 6848 . . . . . . . . . . . . 13 (((1...𝑚) ∈ Fin ∧ 𝐴 ≈ (1...𝑚)) → 𝐴 ∈ Fin)
7165, 69, 70syl2anc 409 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → 𝐴 ∈ Fin)
72 zfz1iso 10763 . . . . . . . . . . . 12 ((𝐴 ⊆ ℤ ∧ 𝐴 ∈ Fin) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
7360, 71, 72syl2anc 409 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
74 simpll 524 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝜑)
7574, 19mpan9 279 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖𝐴) → 𝑖 / 𝑘𝐵 ∈ ℂ)
76 breq1 3990 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑗 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑗 ≤ (♯‘𝐴)))
77 fveq2 5494 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑗 → (𝑓𝑛) = (𝑓𝑗))
7877csbeq1d 3056 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑗(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑗) / 𝑘𝐵)
7976, 78ifbieq1d 3547 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑘𝐵, 1))
80 csbcow 3060 . . . . . . . . . . . . . . . . . 18 (𝑓𝑗) / 𝑖𝑖 / 𝑘𝐵 = (𝑓𝑗) / 𝑘𝐵
81 ifeq1 3528 . . . . . . . . . . . . . . . . . 18 ((𝑓𝑗) / 𝑖𝑖 / 𝑘𝐵 = (𝑓𝑗) / 𝑘𝐵 → if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑖𝑖 / 𝑘𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑘𝐵, 1))
8280, 81ax-mp 5 . . . . . . . . . . . . . . . . 17 if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑖𝑖 / 𝑘𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑘𝐵, 1)
8379, 82eqtr4di 2221 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑖𝑖 / 𝑘𝐵, 1))
8483cbvmptv 4083 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑖𝑖 / 𝑘𝐵, 1))
85 eqid 2170 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (𝑔𝑗) / 𝑖𝑖 / 𝑘𝐵, 1)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (𝑔𝑗) / 𝑖𝑖 / 𝑘𝐵, 1))
8636ad4ant14 511 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ (ℤ𝑀)) → DECID 𝑖𝐴)
87 simplr 525 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ)
8822ad2antrr 485 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑀 ∈ ℤ)
8927ad2antrr 485 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝐴 ⊆ (ℤ𝑀))
90 simprl 526 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑓:(1...𝑚)–1-1-onto𝐴)
91 simprr 527 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
9212, 75, 84, 85, 86, 87, 88, 89, 90, 91prodmodclem2a 11526 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))
9365adantrr 476 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (1...𝑚) ∈ Fin)
9493, 90fihasheqf1od 10711 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘(1...𝑚)) = (♯‘𝐴))
9587nnnn0d 9175 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ0)
96 hashfz1 10704 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ0 → (♯‘(1...𝑚)) = 𝑚)
9795, 96syl 14 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘(1...𝑚)) = 𝑚)
9894, 97eqtr3d 2205 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘𝐴) = 𝑚)
9998breq2d 3999 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (𝑛 ≤ (♯‘𝐴) ↔ 𝑛𝑚))
10099ifbid 3546 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1) = if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1))
101100mpteq2dv 4078 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))
102101seqeq3d 10396 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1))))
103102fveq1d 5496 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))
10492, 103breqtrd 4013 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))
105104expr 373 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → (𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)))
106105exlimdv 1812 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → (∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)))
10773, 106mpd 13 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))
108 breq2 3991 . . . . . . . . . 10 (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚) → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)))
109107, 108syl5ibrcom 156 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
110109expimpd 361 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
111110exlimdv 1812 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
112111rexlimdva 2587 . . . . . 6 (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
11357, 112jaod 712 . . . . 5 (𝜑 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
11422adantr 274 . . . . . . . 8 ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) → 𝑀 ∈ ℤ)
11527adantr 274 . . . . . . . . 9 ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) → 𝐴 ⊆ (ℤ𝑀))
11631adantr 274 . . . . . . . . 9 ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) → ∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴)
117115, 116jca 304 . . . . . . . 8 ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) → (𝐴 ⊆ (ℤ𝑀) ∧ ∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴))
118 zproddc.3 . . . . . . . . . . 11 (𝜑 → ∃𝑛𝑍𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
11926eleq2i 2237 . . . . . . . . . . . . 13 (𝑛𝑍𝑛 ∈ (ℤ𝑀))
120 eluzelz 9483 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ𝑀) → 𝑛 ∈ ℤ)
121120adantl 275 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (ℤ𝑀)) → 𝑛 ∈ ℤ)
122 simpr 109 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → 𝑝 ∈ (ℤ𝑛))
123 simplr 525 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → 𝑛 ∈ (ℤ𝑀))
124 uztrn 9490 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ∈ (ℤ𝑛) ∧ 𝑛 ∈ (ℤ𝑀)) → 𝑝 ∈ (ℤ𝑀))
125122, 123, 124syl2anc 409 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → 𝑝 ∈ (ℤ𝑀))
126125, 26eleqtrrdi 2264 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → 𝑝𝑍)
127 zprod.5 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘𝑍) → (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
128127ralrimiva 2543 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
129128ad2antrr 485 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → ∀𝑘𝑍 (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
130 nfv 1521 . . . . . . . . . . . . . . . . . . . . . 22 𝑘 𝑝𝐴
131 nfcsb1v 3082 . . . . . . . . . . . . . . . . . . . . . 22 𝑘𝑝 / 𝑘𝐵
132130, 131, 7nfif 3553 . . . . . . . . . . . . . . . . . . . . 21 𝑘if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1)
133132nfeq2 2324 . . . . . . . . . . . . . . . . . . . 20 𝑘(𝐹𝑝) = if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1)
134 fveq2 5494 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → (𝐹𝑘) = (𝐹𝑝))
135 eleq1w 2231 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑝 → (𝑘𝐴𝑝𝐴))
136 csbeq1a 3058 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑝𝐵 = 𝑝 / 𝑘𝐵)
137135, 136ifbieq1d 3547 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → if(𝑘𝐴, 𝐵, 1) = if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1))
138134, 137eqeq12d 2185 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑝 → ((𝐹𝑘) = if(𝑘𝐴, 𝐵, 1) ↔ (𝐹𝑝) = if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1)))
139133, 138rspc 2828 . . . . . . . . . . . . . . . . . . 19 (𝑝𝑍 → (∀𝑘𝑍 (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1) → (𝐹𝑝) = if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1)))
140126, 129, 139sylc 62 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → (𝐹𝑝) = if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1))
141 simpr 109 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) ∧ 𝑝𝐴) → 𝑝𝐴)
14215ad3antrrr 489 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) ∧ 𝑝𝐴) → ∀𝑘𝐴 𝐵 ∈ ℂ)
143131nfel1 2323 . . . . . . . . . . . . . . . . . . . . 21 𝑘𝑝 / 𝑘𝐵 ∈ ℂ
144136eleq1d 2239 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → (𝐵 ∈ ℂ ↔ 𝑝 / 𝑘𝐵 ∈ ℂ))
145143, 144rspc 2828 . . . . . . . . . . . . . . . . . . . 20 (𝑝𝐴 → (∀𝑘𝐴 𝐵 ∈ ℂ → 𝑝 / 𝑘𝐵 ∈ ℂ))
146141, 142, 145sylc 62 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) ∧ 𝑝𝐴) → 𝑝 / 𝑘𝐵 ∈ ℂ)
147 1cnd 7923 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) ∧ ¬ 𝑝𝐴) → 1 ∈ ℂ)
148 eleq1w 2231 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑝 → (𝑗𝐴𝑝𝐴))
149148dcbid 833 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑝 → (DECID 𝑗𝐴DECID 𝑝𝐴))
15029ad2antrr 485 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → ∀𝑗𝑍 DECID 𝑗𝐴)
151149, 150, 126rspcdva 2839 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → DECID 𝑝𝐴)
152146, 147, 151ifcldadc 3554 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1) ∈ ℂ)
153140, 152eqeltrd 2247 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → (𝐹𝑝) ∈ ℂ)
154 simpr 109 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → 𝑟 ∈ (ℤ𝑛))
155 simplr 525 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → 𝑛 ∈ (ℤ𝑀))
156 uztrn 9490 . . . . . . . . . . . . . . . . . . . . 21 ((𝑟 ∈ (ℤ𝑛) ∧ 𝑛 ∈ (ℤ𝑀)) → 𝑟 ∈ (ℤ𝑀))
157154, 155, 156syl2anc 409 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → 𝑟 ∈ (ℤ𝑀))
158157, 26eleqtrrdi 2264 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → 𝑟𝑍)
159128ad2antrr 485 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → ∀𝑘𝑍 (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
160 nfv 1521 . . . . . . . . . . . . . . . . . . . . . 22 𝑘 𝑟𝐴
161 nfcsb1v 3082 . . . . . . . . . . . . . . . . . . . . . 22 𝑘𝑟 / 𝑘𝐵
162160, 161, 7nfif 3553 . . . . . . . . . . . . . . . . . . . . 21 𝑘if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1)
163162nfeq2 2324 . . . . . . . . . . . . . . . . . . . 20 𝑘(𝐹𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1)
164 fveq2 5494 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑟 → (𝐹𝑘) = (𝐹𝑟))
165 eleq1w 2231 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑟 → (𝑘𝐴𝑟𝐴))
166 csbeq1a 3058 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑟𝐵 = 𝑟 / 𝑘𝐵)
167165, 166ifbieq1d 3547 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑟 → if(𝑘𝐴, 𝐵, 1) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1))
168164, 167eqeq12d 2185 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑟 → ((𝐹𝑘) = if(𝑘𝐴, 𝐵, 1) ↔ (𝐹𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1)))
169163, 168rspc 2828 . . . . . . . . . . . . . . . . . . 19 (𝑟𝑍 → (∀𝑘𝑍 (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1) → (𝐹𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1)))
170158, 159, 169sylc 62 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → (𝐹𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1))
17158, 157sselid 3145 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → 𝑟 ∈ ℤ)
172 simpr 109 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) ∧ 𝑟𝐴) → 𝑟𝐴)
17315ad3antrrr 489 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) ∧ 𝑟𝐴) → ∀𝑘𝐴 𝐵 ∈ ℂ)
174161nfel1 2323 . . . . . . . . . . . . . . . . . . . . . 22 𝑘𝑟 / 𝑘𝐵 ∈ ℂ
175166eleq1d 2239 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑟 → (𝐵 ∈ ℂ ↔ 𝑟 / 𝑘𝐵 ∈ ℂ))
176174, 175rspc 2828 . . . . . . . . . . . . . . . . . . . . 21 (𝑟𝐴 → (∀𝑘𝐴 𝐵 ∈ ℂ → 𝑟 / 𝑘𝐵 ∈ ℂ))
177172, 173, 176sylc 62 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) ∧ 𝑟𝐴) → 𝑟 / 𝑘𝐵 ∈ ℂ)
178 1cnd 7923 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) ∧ ¬ 𝑟𝐴) → 1 ∈ ℂ)
179 eleq1w 2231 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑟 → (𝑗𝐴𝑟𝐴))
180179dcbid 833 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑟 → (DECID 𝑗𝐴DECID 𝑟𝐴))
18129ad2antrr 485 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → ∀𝑗𝑍 DECID 𝑗𝐴)
182180, 181, 158rspcdva 2839 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → DECID 𝑟𝐴)
183177, 178, 182ifcldadc 3554 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1) ∈ ℂ)
184 nfcv 2312 . . . . . . . . . . . . . . . . . . . 20 𝑘𝑟
185 eqid 2170 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
186184, 162, 167, 185fvmptf 5586 . . . . . . . . . . . . . . . . . . 19 ((𝑟 ∈ ℤ ∧ if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1))
187171, 183, 186syl2anc 409 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1))
188170, 187eqtr4d 2206 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → (𝐹𝑟) = ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑟))
189 mulcl 7888 . . . . . . . . . . . . . . . . . 18 ((𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ) → (𝑝 · 𝑞) ∈ ℂ)
190189adantl 275 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ (𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ)) → (𝑝 · 𝑞) ∈ ℂ)
191121, 153, 188, 190seq3feq 10415 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (ℤ𝑀)) → seq𝑛( · , 𝐹) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))))
192191breq1d 3997 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (ℤ𝑀)) → (seq𝑛( · , 𝐹) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦))
193192anbi2d 461 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (ℤ𝑀)) → ((𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ (𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)))
194193exbidv 1818 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑀)) → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)))
195119, 194sylan2b 285 . . . . . . . . . . . 12 ((𝜑𝑛𝑍) → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)))
196195rexbidva 2467 . . . . . . . . . . 11 (𝜑 → (∃𝑛𝑍𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑛𝑍𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)))
197118, 196mpbid 146 . . . . . . . . . 10 (𝜑 → ∃𝑛𝑍𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦))
19826rexeqi 2670 . . . . . . . . . 10 (∃𝑛𝑍𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦))
199197, 198sylib 121 . . . . . . . . 9 (𝜑 → ∃𝑛 ∈ (ℤ𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦))
200199anim1i 338 . . . . . . . 8 ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) → (∃𝑛 ∈ (ℤ𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
201 fveq2 5494 . . . . . . . . . . . 12 (𝑚 = 𝑀 → (ℤ𝑚) = (ℤ𝑀))
202201sseq2d 3177 . . . . . . . . . . 11 (𝑚 = 𝑀 → (𝐴 ⊆ (ℤ𝑚) ↔ 𝐴 ⊆ (ℤ𝑀)))
203201raleqdv 2671 . . . . . . . . . . 11 (𝑚 = 𝑀 → (∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ↔ ∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴))
204202, 203anbi12d 470 . . . . . . . . . 10 (𝑚 = 𝑀 → ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ↔ (𝐴 ⊆ (ℤ𝑀) ∧ ∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴)))
205201rexeqdv 2672 . . . . . . . . . . 11 (𝑚 = 𝑀 → (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)))
206 seqeq1 10391 . . . . . . . . . . . 12 (𝑚 = 𝑀 → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) = seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))))
207206breq1d 3997 . . . . . . . . . . 11 (𝑚 = 𝑀 → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
208205, 207anbi12d 470 . . . . . . . . . 10 (𝑚 = 𝑀 → ((∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ (∃𝑛 ∈ (ℤ𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)))
209204, 208anbi12d 470 . . . . . . . . 9 (𝑚 = 𝑀 → (((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ↔ ((𝐴 ⊆ (ℤ𝑀) ∧ ∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))))
210209rspcev 2834 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ ((𝐴 ⊆ (ℤ𝑀) ∧ ∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))) → ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)))
211114, 117, 200, 210syl12anc 1231 . . . . . . 7 ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) → ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)))
212211orcd 728 . . . . . 6 ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))))
213212ex 114 . . . . 5 (𝜑 → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)))))
214113, 213impbid 128 . . . 4 (𝜑 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))) ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
215 eluzelz 9483 . . . . . . . 8 (𝑝 ∈ (ℤ𝑀) → 𝑝 ∈ ℤ)
216 simpr 109 . . . . . . . . . 10 (((𝜑𝑝 ∈ (ℤ𝑀)) ∧ 𝑝𝐴) → 𝑝𝐴)
21715ad2antrr 485 . . . . . . . . . 10 (((𝜑𝑝 ∈ (ℤ𝑀)) ∧ 𝑝𝐴) → ∀𝑘𝐴 𝐵 ∈ ℂ)
218216, 217, 145sylc 62 . . . . . . . . 9 (((𝜑𝑝 ∈ (ℤ𝑀)) ∧ 𝑝𝐴) → 𝑝 / 𝑘𝐵 ∈ ℂ)
219 1cnd 7923 . . . . . . . . 9 (((𝜑𝑝 ∈ (ℤ𝑀)) ∧ ¬ 𝑝𝐴) → 1 ∈ ℂ)
22029adantr 274 . . . . . . . . . 10 ((𝜑𝑝 ∈ (ℤ𝑀)) → ∀𝑗𝑍 DECID 𝑗𝐴)
22126eleq2i 2237 . . . . . . . . . . . 12 (𝑝𝑍𝑝 ∈ (ℤ𝑀))
222221biimpri 132 . . . . . . . . . . 11 (𝑝 ∈ (ℤ𝑀) → 𝑝𝑍)
223222adantl 275 . . . . . . . . . 10 ((𝜑𝑝 ∈ (ℤ𝑀)) → 𝑝𝑍)
224149, 220, 223rspcdva 2839 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℤ𝑀)) → DECID 𝑝𝐴)
225218, 219, 224ifcldadc 3554 . . . . . . . 8 ((𝜑𝑝 ∈ (ℤ𝑀)) → if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1) ∈ ℂ)
226 nfcv 2312 . . . . . . . . 9 𝑘𝑝
227226, 132, 137, 185fvmptf 5586 . . . . . . . 8 ((𝑝 ∈ ℤ ∧ if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑝) = if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1))
228215, 225, 227syl2an2 589 . . . . . . 7 ((𝜑𝑝 ∈ (ℤ𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑝) = if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1))
229228, 225eqeltrd 2247 . . . . . 6 ((𝜑𝑝 ∈ (ℤ𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑝) ∈ ℂ)
230 eluzelz 9483 . . . . . . . 8 (𝑟 ∈ (ℤ𝑀) → 𝑟 ∈ ℤ)
231 simpr 109 . . . . . . . . . 10 (((𝜑𝑟 ∈ (ℤ𝑀)) ∧ 𝑟𝐴) → 𝑟𝐴)
23215ad2antrr 485 . . . . . . . . . 10 (((𝜑𝑟 ∈ (ℤ𝑀)) ∧ 𝑟𝐴) → ∀𝑘𝐴 𝐵 ∈ ℂ)
233231, 232, 176sylc 62 . . . . . . . . 9 (((𝜑𝑟 ∈ (ℤ𝑀)) ∧ 𝑟𝐴) → 𝑟 / 𝑘𝐵 ∈ ℂ)
234 1cnd 7923 . . . . . . . . 9 (((𝜑𝑟 ∈ (ℤ𝑀)) ∧ ¬ 𝑟𝐴) → 1 ∈ ℂ)
23529adantr 274 . . . . . . . . . 10 ((𝜑𝑟 ∈ (ℤ𝑀)) → ∀𝑗𝑍 DECID 𝑗𝐴)
23626eleq2i 2237 . . . . . . . . . . . 12 (𝑟𝑍𝑟 ∈ (ℤ𝑀))
237236biimpri 132 . . . . . . . . . . 11 (𝑟 ∈ (ℤ𝑀) → 𝑟𝑍)
238237adantl 275 . . . . . . . . . 10 ((𝜑𝑟 ∈ (ℤ𝑀)) → 𝑟𝑍)
239180, 235, 238rspcdva 2839 . . . . . . . . 9 ((𝜑𝑟 ∈ (ℤ𝑀)) → DECID 𝑟𝐴)
240233, 234, 239ifcldadc 3554 . . . . . . . 8 ((𝜑𝑟 ∈ (ℤ𝑀)) → if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1) ∈ ℂ)
241230, 240, 186syl2an2 589 . . . . . . 7 ((𝜑𝑟 ∈ (ℤ𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1))
242128adantr 274 . . . . . . . 8 ((𝜑𝑟 ∈ (ℤ𝑀)) → ∀𝑘𝑍 (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
243238, 242, 169sylc 62 . . . . . . 7 ((𝜑𝑟 ∈ (ℤ𝑀)) → (𝐹𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1))
244241, 243eqtr4d 2206 . . . . . 6 ((𝜑𝑟 ∈ (ℤ𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑟) = (𝐹𝑟))
245189adantl 275 . . . . . 6 ((𝜑 ∧ (𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ)) → (𝑝 · 𝑞) ∈ ℂ)
24622, 229, 244, 245seq3feq 10415 . . . . 5 (𝜑 → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) = seq𝑀( · , 𝐹))
247246breq1d 3997 . . . 4 (𝜑 → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , 𝐹) ⇝ 𝑥))
248214, 247bitrd 187 . . 3 (𝜑 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))) ↔ seq𝑀( · , 𝐹) ⇝ 𝑥))
249248iotabidv 5179 . 2 (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)))) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥))
250 df-proddc 11501 . 2 𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))))
251 df-fv 5204 . 2 ( ⇝ ‘seq𝑀( · , 𝐹)) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥)
252249, 250, 2513eqtr4g 2228 1 (𝜑 → ∏𝑘𝐴 𝐵 = ( ⇝ ‘seq𝑀( · , 𝐹)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 703  DECID wdc 829   = wceq 1348  wex 1485  wcel 2141  wral 2448  wrex 2449  csb 3049  wss 3121  ifcif 3525   class class class wbr 3987  cmpt 4048  cio 5156  1-1-ontowf1o 5195  cfv 5196   Isom wiso 5197  (class class class)co 5850  cen 6712  Fincfn 6714  cc 7759  0cc0 7761  1c1 7762   · cmul 7766   < clt 7941  cle 7942   # cap 8487  cn 8865  0cn0 9122  cz 9199  cuz 9474  ...cfz 9952  seqcseq 10388  chash 10696  cli 11228  cprod 11500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4102  ax-sep 4105  ax-nul 4113  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-iinf 4570  ax-cnex 7852  ax-resscn 7853  ax-1cn 7854  ax-1re 7855  ax-icn 7856  ax-addcl 7857  ax-addrcl 7858  ax-mulcl 7859  ax-mulrcl 7860  ax-addcom 7861  ax-mulcom 7862  ax-addass 7863  ax-mulass 7864  ax-distr 7865  ax-i2m1 7866  ax-0lt1 7867  ax-1rid 7868  ax-0id 7869  ax-rnegex 7870  ax-precex 7871  ax-cnre 7872  ax-pre-ltirr 7873  ax-pre-ltwlin 7874  ax-pre-lttrn 7875  ax-pre-apti 7876  ax-pre-ltadd 7877  ax-pre-mulgt0 7878  ax-pre-mulext 7879
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3526  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-tr 4086  df-id 4276  df-po 4279  df-iso 4280  df-iord 4349  df-on 4351  df-ilim 4352  df-suc 4354  df-iom 4573  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-isom 5205  df-riota 5806  df-ov 5853  df-oprab 5854  df-mpo 5855  df-1st 6116  df-2nd 6117  df-recs 6281  df-irdg 6346  df-frec 6367  df-1o 6392  df-oadd 6396  df-er 6509  df-en 6715  df-dom 6716  df-fin 6717  df-pnf 7943  df-mnf 7944  df-xr 7945  df-ltxr 7946  df-le 7947  df-sub 8079  df-neg 8080  df-reap 8481  df-ap 8488  df-div 8577  df-inn 8866  df-2 8924  df-n0 9123  df-z 9200  df-uz 9475  df-q 9566  df-rp 9598  df-fz 9953  df-fzo 10086  df-seqfrec 10389  df-exp 10463  df-ihash 10697  df-cj 10793  df-rsqrt 10949  df-abs 10950  df-clim 11229  df-proddc 11501
This theorem is referenced by:  iprodap  11530  zprodap0  11531  prodssdc  11539
  Copyright terms: Public domain W3C validator