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

Theorem zproddc 11409
 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 519 . . . . . . . . 9 (((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) → 𝐴 ⊆ (ℤ𝑚))
2 simprr 522 . . . . . . . . 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 2283 . . . . . . . . . . . 12 𝑖if(𝑘𝐴, 𝐵, 1)
5 nfv 1509 . . . . . . . . . . . . 13 𝑘 𝑖𝐴
6 nfcsb1v 3042 . . . . . . . . . . . . 13 𝑘𝑖 / 𝑘𝐵
7 nfcv 2283 . . . . . . . . . . . . 13 𝑘1
85, 6, 7nfif 3507 . . . . . . . . . . . 12 𝑘if(𝑖𝐴, 𝑖 / 𝑘𝐵, 1)
9 eleq1w 2202 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (𝑘𝐴𝑖𝐴))
10 csbeq1a 3018 . . . . . . . . . . . . 13 (𝑘 = 𝑖𝐵 = 𝑖 / 𝑘𝐵)
119, 10ifbieq1d 3501 . . . . . . . . . . . 12 (𝑘 = 𝑖 → if(𝑘𝐴, 𝐵, 1) = if(𝑖𝐴, 𝑖 / 𝑘𝐵, 1))
124, 8, 11cbvmpt 4033 . . . . . . . . . . 11 (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)) = (𝑖 ∈ ℤ ↦ if(𝑖𝐴, 𝑖 / 𝑘𝐵, 1))
13 simpll 519 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) → 𝜑)
14 zprod.6 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
1514ralrimiva 2510 . . . . . . . . . . . . 13 (𝜑 → ∀𝑘𝐴 𝐵 ∈ ℂ)
166nfel1 2294 . . . . . . . . . . . . . 14 𝑘𝑖 / 𝑘𝐵 ∈ ℂ
1710eleq1d 2210 . . . . . . . . . . . . . 14 (𝑘 = 𝑖 → (𝐵 ∈ ℂ ↔ 𝑖 / 𝑘𝐵 ∈ ℂ))
1816, 17rspc 2789 . . . . . . . . . . . . 13 (𝑖𝐴 → (∀𝑘𝐴 𝐵 ∈ ℂ → 𝑖 / 𝑘𝐵 ∈ ℂ))
1915, 18syl5 32 . . . . . . . . . . . 12 (𝑖𝐴 → (𝜑𝑖 / 𝑘𝐵 ∈ ℂ))
2013, 19mpan9 279 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖𝐴) → 𝑖 / 𝑘𝐵 ∈ ℂ)
21 simplr 520 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) → 𝑚 ∈ ℤ)
22 zprod.2 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℤ)
2322ad2antrr 480 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) → 𝑀 ∈ ℤ)
24 simpr 109 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) → 𝐴 ⊆ (ℤ𝑚))
25 zprod.4 . . . . . . . . . . . . 13 (𝜑𝐴𝑍)
26 zprod.1 . . . . . . . . . . . . 13 𝑍 = (ℤ𝑀)
2725, 26sseqtrdi 3152 . . . . . . . . . . . 12 (𝜑𝐴 ⊆ (ℤ𝑀))
2827ad2antrr 480 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) → 𝐴 ⊆ (ℤ𝑀))
29 zproddc.dc . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑗𝑍 DECID 𝑗𝐴)
3026raleqi 2635 . . . . . . . . . . . . . . . . . 18 (∀𝑗𝑍 DECID 𝑗𝐴 ↔ ∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴)
3129, 30sylib 121 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴)
32 eleq1w 2202 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝑗𝐴𝑖𝐴))
3332dcbid 824 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → (DECID 𝑗𝐴DECID 𝑖𝐴))
3433cbvralv 2659 . . . . . . . . . . . . . . . . 17 (∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴 ↔ ∀𝑖 ∈ (ℤ𝑀)DECID 𝑖𝐴)
3531, 34sylib 121 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑖 ∈ (ℤ𝑀)DECID 𝑖𝐴)
3635r19.21bi 2525 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → DECID 𝑖𝐴)
3736adantlr 469 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℤ) ∧ 𝑖 ∈ (ℤ𝑀)) → DECID 𝑖𝐴)
3837adantlr 469 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑀)) → DECID 𝑖𝐴)
3938adantlr 469 . . . . . . . . . . . 12 (((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑀)) → DECID 𝑖𝐴)
40 simp-4l 531 . . . . . . . . . . . . . . 15 (((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) ∧ ¬ 𝑖 ∈ (ℤ𝑀)) → 𝜑)
41 simpr 109 . . . . . . . . . . . . . . 15 (((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) ∧ ¬ 𝑖 ∈ (ℤ𝑀)) → ¬ 𝑖 ∈ (ℤ𝑀))
4227ssneld 3106 . . . . . . . . . . . . . . 15 (𝜑 → (¬ 𝑖 ∈ (ℤ𝑀) → ¬ 𝑖𝐴))
4340, 41, 42sylc 62 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) ∧ ¬ 𝑖 ∈ (ℤ𝑀)) → ¬ 𝑖𝐴)
4443olcd 724 . . . . . . . . . . . . 13 (((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) ∧ ¬ 𝑖 ∈ (ℤ𝑀)) → (𝑖𝐴 ∨ ¬ 𝑖𝐴))
45 df-dc 821 . . . . . . . . . . . . 13 (DECID 𝑖𝐴 ↔ (𝑖𝐴 ∨ ¬ 𝑖𝐴))
4644, 45sylibr 133 . . . . . . . . . . . 12 (((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) ∧ ¬ 𝑖 ∈ (ℤ𝑀)) → DECID 𝑖𝐴)
47 eluzelz 9388 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ𝑚) → 𝑖 ∈ ℤ)
48 eluzdc 9460 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → DECID 𝑖 ∈ (ℤ𝑀))
4923, 47, 48syl2an 287 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) → DECID 𝑖 ∈ (ℤ𝑀))
50 exmiddc 822 . . . . . . . . . . . . 13 (DECID 𝑖 ∈ (ℤ𝑀) → (𝑖 ∈ (ℤ𝑀) ∨ ¬ 𝑖 ∈ (ℤ𝑀)))
5149, 50syl 14 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) → (𝑖 ∈ (ℤ𝑀) ∨ ¬ 𝑖 ∈ (ℤ𝑀)))
5239, 46, 51mpjaodan 788 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ𝑚)) ∧ 𝑖 ∈ (ℤ𝑚)) → DECID 𝑖𝐴)
5312, 20, 21, 23, 24, 28, 52, 38prodrbdc 11404 . . . . . . . . . 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 2554 . . . . . 6 (𝜑 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
58 uzssz 9398 . . . . . . . . . . . . . 14 (ℤ𝑀) ⊆ ℤ
5927, 58sstrdi 3116 . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ ℤ)
6059ad2antrr 480 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → 𝐴 ⊆ ℤ)
61 1zzd 9134 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → 1 ∈ ℤ)
62 nnz 9126 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
6362adantl 275 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℤ)
6463adantr 274 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → 𝑚 ∈ ℤ)
6561, 64fzfigd 10264 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → (1...𝑚) ∈ Fin)
66 simpr 109 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → 𝑓:(1...𝑚)–1-1-onto𝐴)
67 f1oeng 6663 . . . . . . . . . . . . . . 15 (((1...𝑚) ∈ Fin ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → (1...𝑚) ≈ 𝐴)
6865, 66, 67syl2anc 409 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → (1...𝑚) ≈ 𝐴)
6968ensymd 6689 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → 𝐴 ≈ (1...𝑚))
70 enfii 6780 . . . . . . . . . . . . 13 (((1...𝑚) ∈ Fin ∧ 𝐴 ≈ (1...𝑚)) → 𝐴 ∈ Fin)
7165, 69, 70syl2anc 409 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → 𝐴 ∈ Fin)
72 zfz1iso 10645 . . . . . . . . . . . 12 ((𝐴 ⊆ ℤ ∧ 𝐴 ∈ Fin) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
7360, 71, 72syl2anc 409 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
74 simpll 519 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝜑)
7574, 19mpan9 279 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖𝐴) → 𝑖 / 𝑘𝐵 ∈ ℂ)
76 breq1 3942 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑗 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑗 ≤ (♯‘𝐴)))
77 fveq2 5433 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑗 → (𝑓𝑛) = (𝑓𝑗))
7877csbeq1d 3016 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑗(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑗) / 𝑘𝐵)
7976, 78ifbieq1d 3501 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑘𝐵, 1))
80 csbcow 3020 . . . . . . . . . . . . . . . . . 18 (𝑓𝑗) / 𝑖𝑖 / 𝑘𝐵 = (𝑓𝑗) / 𝑘𝐵
81 ifeq1 3484 . . . . . . . . . . . . . . . . . 18 ((𝑓𝑗) / 𝑖𝑖 / 𝑘𝐵 = (𝑓𝑗) / 𝑘𝐵 → if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑖𝑖 / 𝑘𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑘𝐵, 1))
8280, 81ax-mp 5 . . . . . . . . . . . . . . . . 17 if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑖𝑖 / 𝑘𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑘𝐵, 1)
8379, 82eqtr4di 2192 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑖𝑖 / 𝑘𝐵, 1))
8483cbvmptv 4034 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑖𝑖 / 𝑘𝐵, 1))
85 eqid 2141 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (𝑔𝑗) / 𝑖𝑖 / 𝑘𝐵, 1)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (𝑔𝑗) / 𝑖𝑖 / 𝑘𝐵, 1))
8636ad4ant14 506 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ (ℤ𝑀)) → DECID 𝑖𝐴)
87 simplr 520 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ)
8822ad2antrr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑀 ∈ ℤ)
8927ad2antrr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝐴 ⊆ (ℤ𝑀))
90 simprl 521 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑓:(1...𝑚)–1-1-onto𝐴)
91 simprr 522 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
9212, 75, 84, 85, 86, 87, 88, 89, 90, 91prodmodclem2a 11406 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))
9365adantrr 471 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (1...𝑚) ∈ Fin)
9493, 90fihasheqf1od 10597 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘(1...𝑚)) = (♯‘𝐴))
9587nnnn0d 9083 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ0)
96 hashfz1 10590 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ0 → (♯‘(1...𝑚)) = 𝑚)
9795, 96syl 14 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘(1...𝑚)) = 𝑚)
9894, 97eqtr3d 2176 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘𝐴) = 𝑚)
9998breq2d 3951 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (𝑛 ≤ (♯‘𝐴) ↔ 𝑛𝑚))
10099ifbid 3500 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1) = if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1))
101100mpteq2dv 4029 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))
102101seqeq3d 10286 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1))))
103102fveq1d 5435 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))
10492, 103breqtrd 3964 . . . . . . . . . . . . 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 1793 . . . . . . . . . . 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 3943 . . . . . . . . . 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 1793 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
112111rexlimdva 2554 . . . . . 6 (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
11357, 112jaod 707 . . . . 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 2208 . . . . . . . . . . . . 13 (𝑛𝑍𝑛 ∈ (ℤ𝑀))
120 eluzelz 9388 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ𝑀) → 𝑛 ∈ ℤ)
121120adantl 275 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (ℤ𝑀)) → 𝑛 ∈ ℤ)
122 simpr 109 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → 𝑝 ∈ (ℤ𝑛))
123 simplr 520 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → 𝑛 ∈ (ℤ𝑀))
124 uztrn 9395 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ∈ (ℤ𝑛) ∧ 𝑛 ∈ (ℤ𝑀)) → 𝑝 ∈ (ℤ𝑀))
125122, 123, 124syl2anc 409 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → 𝑝 ∈ (ℤ𝑀))
126125, 26eleqtrrdi 2235 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → 𝑝𝑍)
127 zprod.5 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘𝑍) → (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
128127ralrimiva 2510 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
129128ad2antrr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → ∀𝑘𝑍 (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
130 nfv 1509 . . . . . . . . . . . . . . . . . . . . . 22 𝑘 𝑝𝐴
131 nfcsb1v 3042 . . . . . . . . . . . . . . . . . . . . . 22 𝑘𝑝 / 𝑘𝐵
132130, 131, 7nfif 3507 . . . . . . . . . . . . . . . . . . . . 21 𝑘if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1)
133132nfeq2 2295 . . . . . . . . . . . . . . . . . . . 20 𝑘(𝐹𝑝) = if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1)
134 fveq2 5433 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → (𝐹𝑘) = (𝐹𝑝))
135 eleq1w 2202 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑝 → (𝑘𝐴𝑝𝐴))
136 csbeq1a 3018 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑝𝐵 = 𝑝 / 𝑘𝐵)
137135, 136ifbieq1d 3501 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → if(𝑘𝐴, 𝐵, 1) = if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1))
138134, 137eqeq12d 2156 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑝 → ((𝐹𝑘) = if(𝑘𝐴, 𝐵, 1) ↔ (𝐹𝑝) = if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1)))
139133, 138rspc 2789 . . . . . . . . . . . . . . . . . . 19 (𝑝𝑍 → (∀𝑘𝑍 (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1) → (𝐹𝑝) = if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1)))
140126, 129, 139sylc 62 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → (𝐹𝑝) = if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1))
141 simpr 109 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) ∧ 𝑝𝐴) → 𝑝𝐴)
14215ad3antrrr 484 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) ∧ 𝑝𝐴) → ∀𝑘𝐴 𝐵 ∈ ℂ)
143131nfel1 2294 . . . . . . . . . . . . . . . . . . . . 21 𝑘𝑝 / 𝑘𝐵 ∈ ℂ
144136eleq1d 2210 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → (𝐵 ∈ ℂ ↔ 𝑝 / 𝑘𝐵 ∈ ℂ))
145143, 144rspc 2789 . . . . . . . . . . . . . . . . . . . 20 (𝑝𝐴 → (∀𝑘𝐴 𝐵 ∈ ℂ → 𝑝 / 𝑘𝐵 ∈ ℂ))
146141, 142, 145sylc 62 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) ∧ 𝑝𝐴) → 𝑝 / 𝑘𝐵 ∈ ℂ)
147 1cnd 7835 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) ∧ ¬ 𝑝𝐴) → 1 ∈ ℂ)
148 eleq1w 2202 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑝 → (𝑗𝐴𝑝𝐴))
149148dcbid 824 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑝 → (DECID 𝑗𝐴DECID 𝑝𝐴))
15029ad2antrr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → ∀𝑗𝑍 DECID 𝑗𝐴)
151149, 150, 126rspcdva 2800 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → DECID 𝑝𝐴)
152146, 147, 151ifcldadc 3508 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1) ∈ ℂ)
153140, 152eqeltrd 2218 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑝 ∈ (ℤ𝑛)) → (𝐹𝑝) ∈ ℂ)
154 simpr 109 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → 𝑟 ∈ (ℤ𝑛))
155 simplr 520 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → 𝑛 ∈ (ℤ𝑀))
156 uztrn 9395 . . . . . . . . . . . . . . . . . . . . 21 ((𝑟 ∈ (ℤ𝑛) ∧ 𝑛 ∈ (ℤ𝑀)) → 𝑟 ∈ (ℤ𝑀))
157154, 155, 156syl2anc 409 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → 𝑟 ∈ (ℤ𝑀))
158157, 26eleqtrrdi 2235 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → 𝑟𝑍)
159128ad2antrr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → ∀𝑘𝑍 (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
160 nfv 1509 . . . . . . . . . . . . . . . . . . . . . 22 𝑘 𝑟𝐴
161 nfcsb1v 3042 . . . . . . . . . . . . . . . . . . . . . 22 𝑘𝑟 / 𝑘𝐵
162160, 161, 7nfif 3507 . . . . . . . . . . . . . . . . . . . . 21 𝑘if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1)
163162nfeq2 2295 . . . . . . . . . . . . . . . . . . . 20 𝑘(𝐹𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1)
164 fveq2 5433 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑟 → (𝐹𝑘) = (𝐹𝑟))
165 eleq1w 2202 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑟 → (𝑘𝐴𝑟𝐴))
166 csbeq1a 3018 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑟𝐵 = 𝑟 / 𝑘𝐵)
167165, 166ifbieq1d 3501 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑟 → if(𝑘𝐴, 𝐵, 1) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1))
168164, 167eqeq12d 2156 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑟 → ((𝐹𝑘) = if(𝑘𝐴, 𝐵, 1) ↔ (𝐹𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1)))
169163, 168rspc 2789 . . . . . . . . . . . . . . . . . . 19 (𝑟𝑍 → (∀𝑘𝑍 (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1) → (𝐹𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1)))
170158, 159, 169sylc 62 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → (𝐹𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1))
17158, 157sseldi 3102 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → 𝑟 ∈ ℤ)
172 simpr 109 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) ∧ 𝑟𝐴) → 𝑟𝐴)
17315ad3antrrr 484 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) ∧ 𝑟𝐴) → ∀𝑘𝐴 𝐵 ∈ ℂ)
174161nfel1 2294 . . . . . . . . . . . . . . . . . . . . . 22 𝑘𝑟 / 𝑘𝐵 ∈ ℂ
175166eleq1d 2210 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑟 → (𝐵 ∈ ℂ ↔ 𝑟 / 𝑘𝐵 ∈ ℂ))
176174, 175rspc 2789 . . . . . . . . . . . . . . . . . . . . 21 (𝑟𝐴 → (∀𝑘𝐴 𝐵 ∈ ℂ → 𝑟 / 𝑘𝐵 ∈ ℂ))
177172, 173, 176sylc 62 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) ∧ 𝑟𝐴) → 𝑟 / 𝑘𝐵 ∈ ℂ)
178 1cnd 7835 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) ∧ ¬ 𝑟𝐴) → 1 ∈ ℂ)
179 eleq1w 2202 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑟 → (𝑗𝐴𝑟𝐴))
180179dcbid 824 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑟 → (DECID 𝑗𝐴DECID 𝑟𝐴))
18129ad2antrr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → ∀𝑗𝑍 DECID 𝑗𝐴)
182180, 181, 158rspcdva 2800 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → DECID 𝑟𝐴)
183177, 178, 182ifcldadc 3508 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1) ∈ ℂ)
184 nfcv 2283 . . . . . . . . . . . . . . . . . . . 20 𝑘𝑟
185 eqid 2141 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
186184, 162, 167, 185fvmptf 5525 . . . . . . . . . . . . . . . . . . 19 ((𝑟 ∈ ℤ ∧ if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1))
187171, 183, 186syl2anc 409 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1))
188170, 187eqtr4d 2177 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ 𝑟 ∈ (ℤ𝑛)) → (𝐹𝑟) = ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑟))
189 mulcl 7800 . . . . . . . . . . . . . . . . . 18 ((𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ) → (𝑝 · 𝑞) ∈ ℂ)
190189adantl 275 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (ℤ𝑀)) ∧ (𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ)) → (𝑝 · 𝑞) ∈ ℂ)
191121, 153, 188, 190seq3feq 10305 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (ℤ𝑀)) → seq𝑛( · , 𝐹) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))))
192191breq1d 3949 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (ℤ𝑀)) → (seq𝑛( · , 𝐹) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦))
193192anbi2d 460 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (ℤ𝑀)) → ((𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ (𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)))
194193exbidv 1799 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑀)) → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)))
195119, 194sylan2b 285 . . . . . . . . . . . 12 ((𝜑𝑛𝑍) → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)))
196195rexbidva 2437 . . . . . . . . . . 11 (𝜑 → (∃𝑛𝑍𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑛𝑍𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)))
197118, 196mpbid 146 . . . . . . . . . 10 (𝜑 → ∃𝑛𝑍𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦))
19826rexeqi 2636 . . . . . . . . . 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 5433 . . . . . . . . . . . 12 (𝑚 = 𝑀 → (ℤ𝑚) = (ℤ𝑀))
202201sseq2d 3134 . . . . . . . . . . 11 (𝑚 = 𝑀 → (𝐴 ⊆ (ℤ𝑚) ↔ 𝐴 ⊆ (ℤ𝑀)))
203201raleqdv 2637 . . . . . . . . . . 11 (𝑚 = 𝑀 → (∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ↔ ∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴))
204202, 203anbi12d 465 . . . . . . . . . 10 (𝑚 = 𝑀 → ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ↔ (𝐴 ⊆ (ℤ𝑀) ∧ ∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴)))
205201rexeqdv 2638 . . . . . . . . . . 11 (𝑚 = 𝑀 → (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)))
206 seqeq1 10281 . . . . . . . . . . . 12 (𝑚 = 𝑀 → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) = seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))))
207206breq1d 3949 . . . . . . . . . . 11 (𝑚 = 𝑀 → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
208205, 207anbi12d 465 . . . . . . . . . 10 (𝑚 = 𝑀 → ((∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ (∃𝑛 ∈ (ℤ𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)))
209204, 208anbi12d 465 . . . . . . . . 9 (𝑚 = 𝑀 → (((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ↔ ((𝐴 ⊆ (ℤ𝑀) ∧ ∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))))
210209rspcev 2795 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ ((𝐴 ⊆ (ℤ𝑀) ∧ ∀𝑗 ∈ (ℤ𝑀)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))) → ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)))
211114, 117, 200, 210syl12anc 1215 . . . . . . 7 ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) → ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)))
212211orcd 723 . . . . . 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 9388 . . . . . . . 8 (𝑝 ∈ (ℤ𝑀) → 𝑝 ∈ ℤ)
216 simpr 109 . . . . . . . . . 10 (((𝜑𝑝 ∈ (ℤ𝑀)) ∧ 𝑝𝐴) → 𝑝𝐴)
21715ad2antrr 480 . . . . . . . . . 10 (((𝜑𝑝 ∈ (ℤ𝑀)) ∧ 𝑝𝐴) → ∀𝑘𝐴 𝐵 ∈ ℂ)
218216, 217, 145sylc 62 . . . . . . . . 9 (((𝜑𝑝 ∈ (ℤ𝑀)) ∧ 𝑝𝐴) → 𝑝 / 𝑘𝐵 ∈ ℂ)
219 1cnd 7835 . . . . . . . . 9 (((𝜑𝑝 ∈ (ℤ𝑀)) ∧ ¬ 𝑝𝐴) → 1 ∈ ℂ)
22029adantr 274 . . . . . . . . . 10 ((𝜑𝑝 ∈ (ℤ𝑀)) → ∀𝑗𝑍 DECID 𝑗𝐴)
22126eleq2i 2208 . . . . . . . . . . . 12 (𝑝𝑍𝑝 ∈ (ℤ𝑀))
222221biimpri 132 . . . . . . . . . . 11 (𝑝 ∈ (ℤ𝑀) → 𝑝𝑍)
223222adantl 275 . . . . . . . . . 10 ((𝜑𝑝 ∈ (ℤ𝑀)) → 𝑝𝑍)
224149, 220, 223rspcdva 2800 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℤ𝑀)) → DECID 𝑝𝐴)
225218, 219, 224ifcldadc 3508 . . . . . . . 8 ((𝜑𝑝 ∈ (ℤ𝑀)) → if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1) ∈ ℂ)
226 nfcv 2283 . . . . . . . . 9 𝑘𝑝
227226, 132, 137, 185fvmptf 5525 . . . . . . . 8 ((𝑝 ∈ ℤ ∧ if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑝) = if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1))
228215, 225, 227syl2an2 584 . . . . . . 7 ((𝜑𝑝 ∈ (ℤ𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑝) = if(𝑝𝐴, 𝑝 / 𝑘𝐵, 1))
229228, 225eqeltrd 2218 . . . . . 6 ((𝜑𝑝 ∈ (ℤ𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑝) ∈ ℂ)
230 eluzelz 9388 . . . . . . . 8 (𝑟 ∈ (ℤ𝑀) → 𝑟 ∈ ℤ)
231 simpr 109 . . . . . . . . . 10 (((𝜑𝑟 ∈ (ℤ𝑀)) ∧ 𝑟𝐴) → 𝑟𝐴)
23215ad2antrr 480 . . . . . . . . . 10 (((𝜑𝑟 ∈ (ℤ𝑀)) ∧ 𝑟𝐴) → ∀𝑘𝐴 𝐵 ∈ ℂ)
233231, 232, 176sylc 62 . . . . . . . . 9 (((𝜑𝑟 ∈ (ℤ𝑀)) ∧ 𝑟𝐴) → 𝑟 / 𝑘𝐵 ∈ ℂ)
234 1cnd 7835 . . . . . . . . 9 (((𝜑𝑟 ∈ (ℤ𝑀)) ∧ ¬ 𝑟𝐴) → 1 ∈ ℂ)
23529adantr 274 . . . . . . . . . 10 ((𝜑𝑟 ∈ (ℤ𝑀)) → ∀𝑗𝑍 DECID 𝑗𝐴)
23626eleq2i 2208 . . . . . . . . . . . 12 (𝑟𝑍𝑟 ∈ (ℤ𝑀))
237236biimpri 132 . . . . . . . . . . 11 (𝑟 ∈ (ℤ𝑀) → 𝑟𝑍)
238237adantl 275 . . . . . . . . . 10 ((𝜑𝑟 ∈ (ℤ𝑀)) → 𝑟𝑍)
239180, 235, 238rspcdva 2800 . . . . . . . . 9 ((𝜑𝑟 ∈ (ℤ𝑀)) → DECID 𝑟𝐴)
240233, 234, 239ifcldadc 3508 . . . . . . . 8 ((𝜑𝑟 ∈ (ℤ𝑀)) → if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1) ∈ ℂ)
241230, 240, 186syl2an2 584 . . . . . . 7 ((𝜑𝑟 ∈ (ℤ𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1))
242128adantr 274 . . . . . . . 8 ((𝜑𝑟 ∈ (ℤ𝑀)) → ∀𝑘𝑍 (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
243238, 242, 169sylc 62 . . . . . . 7 ((𝜑𝑟 ∈ (ℤ𝑀)) → (𝐹𝑟) = if(𝑟𝐴, 𝑟 / 𝑘𝐵, 1))
244241, 243eqtr4d 2177 . . . . . 6 ((𝜑𝑟 ∈ (ℤ𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))‘𝑟) = (𝐹𝑟))
245189adantl 275 . . . . . 6 ((𝜑 ∧ (𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ)) → (𝑝 · 𝑞) ∈ ℂ)
24622, 229, 244, 245seq3feq 10305 . . . . 5 (𝜑 → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) = seq𝑀( · , 𝐹))
247246breq1d 3949 . . . 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 5121 . 2 (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)))) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥))
250 df-proddc 11381 . 2 𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))))
251 df-fv 5143 . 2 ( ⇝ ‘seq𝑀( · , 𝐹)) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥)
252249, 250, 2513eqtr4g 2199 1 (𝜑 → ∏𝑘𝐴 𝐵 = ( ⇝ ‘seq𝑀( · , 𝐹)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 820   = wceq 1332  ∃wex 1469   ∈ wcel 1481  ∀wral 2418  ∃wrex 2419  ⦋csb 3009   ⊆ wss 3078  ifcif 3481   class class class wbr 3939   ↦ cmpt 3999  ℩cio 5098  –1-1-onto→wf1o 5134  ‘cfv 5135   Isom wiso 5136  (class class class)co 5786   ≈ cen 6644  Fincfn 6646  ℂcc 7671  0cc0 7673  1c1 7674   · cmul 7678   < clt 7853   ≤ cle 7854   # cap 8396  ℕcn 8773  ℕ0cn0 9030  ℤcz 9107  ℤ≥cuz 9379  ...cfz 9850  seqcseq 10278  ♯chash 10582   ⇝ cli 11108  ∏cprod 11380 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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2123  ax-coll 4053  ax-sep 4056  ax-nul 4064  ax-pow 4108  ax-pr 4142  ax-un 4366  ax-setind 4463  ax-iinf 4513  ax-cnex 7764  ax-resscn 7765  ax-1cn 7766  ax-1re 7767  ax-icn 7768  ax-addcl 7769  ax-addrcl 7770  ax-mulcl 7771  ax-mulrcl 7772  ax-addcom 7773  ax-mulcom 7774  ax-addass 7775  ax-mulass 7776  ax-distr 7777  ax-i2m1 7778  ax-0lt1 7779  ax-1rid 7780  ax-0id 7781  ax-rnegex 7782  ax-precex 7783  ax-cnre 7784  ax-pre-ltirr 7785  ax-pre-ltwlin 7786  ax-pre-lttrn 7787  ax-pre-apti 7788  ax-pre-ltadd 7789  ax-pre-mulgt0 7790  ax-pre-mulext 7791 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1738  df-eu 2004  df-mo 2005  df-clab 2128  df-cleq 2134  df-clel 2137  df-nfc 2272  df-ne 2311  df-nel 2406  df-ral 2423  df-rex 2424  df-reu 2425  df-rmo 2426  df-rab 2427  df-v 2693  df-sbc 2916  df-csb 3010  df-dif 3080  df-un 3082  df-in 3084  df-ss 3091  df-nul 3371  df-if 3482  df-pw 3519  df-sn 3540  df-pr 3541  df-op 3543  df-uni 3747  df-int 3782  df-iun 3825  df-br 3940  df-opab 4000  df-mpt 4001  df-tr 4037  df-id 4226  df-po 4229  df-iso 4230  df-iord 4299  df-on 4301  df-ilim 4302  df-suc 4304  df-iom 4516  df-xp 4557  df-rel 4558  df-cnv 4559  df-co 4560  df-dm 4561  df-rn 4562  df-res 4563  df-ima 4564  df-iota 5100  df-fun 5137  df-fn 5138  df-f 5139  df-f1 5140  df-fo 5141  df-f1o 5142  df-fv 5143  df-isom 5144  df-riota 5742  df-ov 5789  df-oprab 5790  df-mpo 5791  df-1st 6050  df-2nd 6051  df-recs 6214  df-irdg 6279  df-frec 6300  df-1o 6325  df-oadd 6329  df-er 6441  df-en 6647  df-dom 6648  df-fin 6649  df-pnf 7855  df-mnf 7856  df-xr 7857  df-ltxr 7858  df-le 7859  df-sub 7988  df-neg 7989  df-reap 8390  df-ap 8397  df-div 8486  df-inn 8774  df-2 8832  df-n0 9031  df-z 9108  df-uz 9380  df-q 9468  df-rp 9500  df-fz 9851  df-fzo 9980  df-seqfrec 10279  df-exp 10353  df-ihash 10583  df-cj 10675  df-rsqrt 10831  df-abs 10832  df-clim 11109  df-proddc 11381 This theorem is referenced by:  iprodap  11410  zprodap0  11411  prodssdc  11419
 Copyright terms: Public domain W3C validator