Theorem prodmolem2a

Description: Lemma for prodmo . (Contributed by Scott Fenton, 4-Dec-2017)

	Ref	Expression
Hypotheses	prodmo.1	⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
	prodmo.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	prodmo.3	⊢ 𝐺 = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
	prodmolem2.4	⊢ 𝐻 = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝐾 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
	prodmolem2.5	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	prodmolem2.6	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	prodmolem2.7	⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
	prodmolem2.8	⊢ ( 𝜑 → 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 )
	prodmolem2.9	⊢ ( 𝜑 → 𝐾 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
Assertion	prodmolem2a	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		prodmo.1	⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
2		prodmo.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3		prodmo.3	⊢ 𝐺 = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
4		prodmolem2.4	⊢ 𝐻 = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝐾 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
5		prodmolem2.5	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6		prodmolem2.6	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
7		prodmolem2.7	⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
8		prodmolem2.8	⊢ ( 𝜑 → 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 )
9		prodmolem2.9	⊢ ( 𝜑 → 𝐾 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
10		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
11	10 8	hasheqf1od	⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = ( ♯ ‘ 𝐴 ) )
12	5	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
13		hashfz1	⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
14	12 13	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
15	11 14	eqtr3d	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = 𝑁 )
16	15	oveq2d	⊢ ( 𝜑 → ( 1 ... ( ♯ ‘ 𝐴 ) ) = ( 1 ... 𝑁 ) )
17		isoeq4	⊢ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) = ( 1 ... 𝑁 ) → ( 𝐾 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ↔ 𝐾 Isom < , < ( ( 1 ... 𝑁 ) , 𝐴 ) ) )
18	16 17	syl	⊢ ( 𝜑 → ( 𝐾 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ↔ 𝐾 Isom < , < ( ( 1 ... 𝑁 ) , 𝐴 ) ) )
19	9 18	mpbid	⊢ ( 𝜑 → 𝐾 Isom < , < ( ( 1 ... 𝑁 ) , 𝐴 ) )
20		isof1o	⊢ ( 𝐾 Isom < , < ( ( 1 ... 𝑁 ) , 𝐴 ) → 𝐾 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 )
21		f1of	⊢ ( 𝐾 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 → 𝐾 : ( 1 ... 𝑁 ) ⟶ 𝐴 )
22	19 20 21	3syl	⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑁 ) ⟶ 𝐴 )
23		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
24	5 23	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
25		eluzfz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
26	24 25	syl	⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... 𝑁 ) )
27	22 26	ffvelcdmd	⊢ ( 𝜑 → ( 𝐾 ‘ 𝑁 ) ∈ 𝐴 )
28	7 27	sseldd	⊢ ( 𝜑 → ( 𝐾 ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
29	7	sselda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
30	19 20	syl	⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 )
31		f1ocnvfv2	⊢ ( ( 𝐾 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐾 ‘ ( ◡ 𝐾 ‘ 𝑗 ) ) = 𝑗 )
32	30 31	sylan	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐾 ‘ ( ◡ 𝐾 ‘ 𝑗 ) ) = 𝑗 )
33		f1ocnv	⊢ ( 𝐾 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 → ◡ 𝐾 : 𝐴 –1-1-onto→ ( 1 ... 𝑁 ) )
34		f1of	⊢ ( ◡ 𝐾 : 𝐴 –1-1-onto→ ( 1 ... 𝑁 ) → ◡ 𝐾 : 𝐴 ⟶ ( 1 ... 𝑁 ) )
35	30 33 34	3syl	⊢ ( 𝜑 → ◡ 𝐾 : 𝐴 ⟶ ( 1 ... 𝑁 ) )
36	35	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ◡ 𝐾 ‘ 𝑗 ) ∈ ( 1 ... 𝑁 ) )
37		elfzle2	⊢ ( ( ◡ 𝐾 ‘ 𝑗 ) ∈ ( 1 ... 𝑁 ) → ( ◡ 𝐾 ‘ 𝑗 ) ≤ 𝑁 )
38	36 37	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ◡ 𝐾 ‘ 𝑗 ) ≤ 𝑁 )
39	19	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐾 Isom < , < ( ( 1 ... 𝑁 ) , 𝐴 ) )
40		fzssuz	⊢ ( 1 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 1 )
41		uzssz	⊢ ( ℤ≥ ‘ 1 ) ⊆ ℤ
42		zssre	⊢ ℤ ⊆ ℝ
43	41 42	sstri	⊢ ( ℤ≥ ‘ 1 ) ⊆ ℝ
44	40 43	sstri	⊢ ( 1 ... 𝑁 ) ⊆ ℝ
45		ressxr	⊢ ℝ ⊆ ℝ*
46	44 45	sstri	⊢ ( 1 ... 𝑁 ) ⊆ ℝ*
47	46	a1i	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 1 ... 𝑁 ) ⊆ ℝ* )
48		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
49	48 42	sstri	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ
50	49 45	sstri	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ*
51	7 50	sstrdi	⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
52	51	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐴 ⊆ ℝ* )
53	26	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
54		leisorel	⊢ ( ( 𝐾 Isom < , < ( ( 1 ... 𝑁 ) , 𝐴 ) ∧ ( ( 1 ... 𝑁 ) ⊆ ℝ* ∧ 𝐴 ⊆ ℝ* ) ∧ ( ( ◡ 𝐾 ‘ 𝑗 ) ∈ ( 1 ... 𝑁 ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) ) → ( ( ◡ 𝐾 ‘ 𝑗 ) ≤ 𝑁 ↔ ( 𝐾 ‘ ( ◡ 𝐾 ‘ 𝑗 ) ) ≤ ( 𝐾 ‘ 𝑁 ) ) )
55	39 47 52 36 53 54	syl122anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( ◡ 𝐾 ‘ 𝑗 ) ≤ 𝑁 ↔ ( 𝐾 ‘ ( ◡ 𝐾 ‘ 𝑗 ) ) ≤ ( 𝐾 ‘ 𝑁 ) ) )
56	38 55	mpbid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐾 ‘ ( ◡ 𝐾 ‘ 𝑗 ) ) ≤ ( 𝐾 ‘ 𝑁 ) )
57	32 56	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ≤ ( 𝐾 ‘ 𝑁 ) )
58	7 48	sstrdi	⊢ ( 𝜑 → 𝐴 ⊆ ℤ )
59	58	sselda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ ℤ )
60		eluzelz	⊢ ( ( 𝐾 ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ‘ 𝑁 ) ∈ ℤ )
61	28 60	syl	⊢ ( 𝜑 → ( 𝐾 ‘ 𝑁 ) ∈ ℤ )
62	61	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐾 ‘ 𝑁 ) ∈ ℤ )
63		eluz	⊢ ( ( 𝑗 ∈ ℤ ∧ ( 𝐾 ‘ 𝑁 ) ∈ ℤ ) → ( ( 𝐾 ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 𝑗 ) ↔ 𝑗 ≤ ( 𝐾 ‘ 𝑁 ) ) )
64	59 62 63	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐾 ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 𝑗 ) ↔ 𝑗 ≤ ( 𝐾 ‘ 𝑁 ) ) )
65	57 64	mpbird	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐾 ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
66		elfzuzb	⊢ ( 𝑗 ∈ ( 𝑀 ... ( 𝐾 ‘ 𝑁 ) ) ↔ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 𝑗 ) ) )
67	29 65 66	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ ( 𝑀 ... ( 𝐾 ‘ 𝑁 ) ) )
68	67	ex	⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 → 𝑗 ∈ ( 𝑀 ... ( 𝐾 ‘ 𝑁 ) ) ) )
69	68	ssrdv	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑀 ... ( 𝐾 ‘ 𝑁 ) ) )
70	1 2 28 69	fprodcvg	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝐾 ‘ 𝑁 ) ) )
71		mullid	⊢ ( 𝑚 ∈ ℂ → ( 1 · 𝑚 ) = 𝑚 )
72	71	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℂ ) → ( 1 · 𝑚 ) = 𝑚 )
73		mulrid	⊢ ( 𝑚 ∈ ℂ → ( 𝑚 · 1 ) = 𝑚 )
74	73	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℂ ) → ( 𝑚 · 1 ) = 𝑚 )
75		mulcl	⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑚 · 𝑥 ) ∈ ℂ )
76	75	adantl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑚 · 𝑥 ) ∈ ℂ )
77		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
78	26 16	eleqtrrd	⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
79		iftrue	⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = 𝐵 )
80	79	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = 𝐵 )
81	80 2	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ )
82	81	ex	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ ) )
83		iffalse	⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = 1 )
84		ax-1cn	⊢ 1 ∈ ℂ
85	83 84	eqeltrdi	⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ )
86	82 85	pm2.61d1	⊢ ( 𝜑 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ )
87	86	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ )
88	87 1	fmptd	⊢ ( 𝜑 → 𝐹 : ℤ ⟶ ℂ )
89		elfzelz	⊢ ( 𝑚 ∈ ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) → 𝑚 ∈ ℤ )
90		ffvelcdm	⊢ ( ( 𝐹 : ℤ ⟶ ℂ ∧ 𝑚 ∈ ℤ ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
91	88 89 90	syl2an	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
92		fveqeq2	⊢ ( 𝑘 = 𝑚 → ( ( 𝐹 ‘ 𝑘 ) = 1 ↔ ( 𝐹 ‘ 𝑚 ) = 1 ) )
93		eldifi	⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → 𝑘 ∈ ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) )
94	93	elfzelzd	⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → 𝑘 ∈ ℤ )
95		eldifn	⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → ¬ 𝑘 ∈ 𝐴 )
96	95 83	syl	⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = 1 )
97	96 84	eqeltrdi	⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ )
98	1	fvmpt2	⊢ ( ( 𝑘 ∈ ℤ ∧ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
99	94 97 98	syl2anc	⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
100	99 96	eqtrd	⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = 1 )
101	92 100	vtoclga	⊢ ( 𝑚 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → ( 𝐹 ‘ 𝑚 ) = 1 )
102	101	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑚 ) = 1 )
103		isof1o	⊢ ( 𝐾 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) → 𝐾 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
104		f1of	⊢ ( 𝐾 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝐾 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
105	9 103 104	3syl	⊢ ( 𝜑 → 𝐾 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
106	105	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 )
107	106	iftrued	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 1 ) = ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 )
108	58	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝐴 ⊆ ℤ )
109	108 106	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐾 ‘ 𝑥 ) ∈ ℤ )
110		nfv	⊢ Ⅎ 𝑘 𝜑
111		nfv	⊢ Ⅎ 𝑘 ( 𝐾 ‘ 𝑥 ) ∈ 𝐴
112		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵
113		nfcv	⊢ Ⅎ 𝑘 1
114	111 112 113	nfif	⊢ Ⅎ 𝑘 if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 1 )
115	114	nfel1	⊢ Ⅎ 𝑘 if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 1 ) ∈ ℂ
116	110 115	nfim	⊢ Ⅎ 𝑘 ( 𝜑 → if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 1 ) ∈ ℂ )
117		fvex	⊢ ( 𝐾 ‘ 𝑥 ) ∈ V
118		eleq1	⊢ ( 𝑘 = ( 𝐾 ‘ 𝑥 ) → ( 𝑘 ∈ 𝐴 ↔ ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 ) )
119		csbeq1a	⊢ ( 𝑘 = ( 𝐾 ‘ 𝑥 ) → 𝐵 = ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 )
120	118 119	ifbieq1d	⊢ ( 𝑘 = ( 𝐾 ‘ 𝑥 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 1 ) )
121	120	eleq1d	⊢ ( 𝑘 = ( 𝐾 ‘ 𝑥 ) → ( if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ ↔ if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 1 ) ∈ ℂ ) )
122	121	imbi2d	⊢ ( 𝑘 = ( 𝐾 ‘ 𝑥 ) → ( ( 𝜑 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ ) ↔ ( 𝜑 → if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 1 ) ∈ ℂ ) ) )
123	116 117 122 86	vtoclf	⊢ ( 𝜑 → if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 1 ) ∈ ℂ )
124	123	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 1 ) ∈ ℂ )
125		eleq1	⊢ ( 𝑛 = ( 𝐾 ‘ 𝑥 ) → ( 𝑛 ∈ 𝐴 ↔ ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 ) )
126		csbeq1	⊢ ( 𝑛 = ( 𝐾 ‘ 𝑥 ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐵 = ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 )
127	125 126	ifbieq1d	⊢ ( 𝑛 = ( 𝐾 ‘ 𝑥 ) → if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 1 ) = if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 1 ) )
128		nfcv	⊢ Ⅎ 𝑛 if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 )
129		nfv	⊢ Ⅎ 𝑘 𝑛 ∈ 𝐴
130		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ 𝐵
131	129 130 113	nfif	⊢ Ⅎ 𝑘 if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 1 )
132		eleq1	⊢ ( 𝑘 = 𝑛 → ( 𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴 ) )
133		csbeq1a	⊢ ( 𝑘 = 𝑛 → 𝐵 = ⦋ 𝑛 / 𝑘 ⦌ 𝐵 )
134	132 133	ifbieq1d	⊢ ( 𝑘 = 𝑛 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 1 ) )
135	128 131 134	cbvmpt	⊢ ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) = ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 1 ) )
136	1 135	eqtri	⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 1 ) )
137	127 136	fvmptg	⊢ ( ( ( 𝐾 ‘ 𝑥 ) ∈ ℤ ∧ if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 1 ) ∈ ℂ ) → ( 𝐹 ‘ ( 𝐾 ‘ 𝑥 ) ) = if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 1 ) )
138	109 124 137	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐹 ‘ ( 𝐾 ‘ 𝑥 ) ) = if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 1 ) )
139		elfznn	⊢ ( 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → 𝑥 ∈ ℕ )
140	107 124	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ∈ ℂ )
141		fveq2	⊢ ( 𝑗 = 𝑥 → ( 𝐾 ‘ 𝑗 ) = ( 𝐾 ‘ 𝑥 ) )
142	141	csbeq1d	⊢ ( 𝑗 = 𝑥 → ⦋ ( 𝐾 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 )
143	142 4	fvmptg	⊢ ( ( 𝑥 ∈ ℕ ∧ ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ∈ ℂ ) → ( 𝐻 ‘ 𝑥 ) = ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 )
144	139 140 143	syl2an2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐻 ‘ 𝑥 ) = ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 )
145	107 138 144	3eqtr4rd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐾 ‘ 𝑥 ) ) )
146	72 74 76 77 9 78 7 91 102 145	seqcoll	⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝐾 ‘ 𝑁 ) ) = ( seq 1 ( · , 𝐻 ) ‘ 𝑁 ) )
147	5 5	jca	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ ) )
148	1 2 3 4 147 8 30	prodmolem3	⊢ ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) = ( seq 1 ( · , 𝐻 ) ‘ 𝑁 ) )
149	146 148	eqtr4d	⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝐾 ‘ 𝑁 ) ) = ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) )
150	70 149	breqtrd	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) )