prodmodclem2a - Intuitionistic Logic Explorer

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

Theorem prodmodclem2a 11962

Description: Lemma for prodmodc 11964. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.)

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

**Assertion**
Ref	Expression
prodmodclem2a	⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁))

Distinct variable groups: 𝐴,𝑗,𝑘 𝐵,𝑗 𝑘,𝐹 𝑗,𝐺 𝑗,𝐾,𝑘 𝑗,𝑀,𝑘 𝑗,𝑁,𝑘 𝑓,𝑗,𝑘 𝜑,𝑘 Allowed substitution hints: 𝜑(𝑓,𝑗) 𝐴(𝑓) 𝐵(𝑓,𝑘) 𝐹(𝑓,𝑗) 𝐺(𝑓,𝑘) 𝐻(𝑓,𝑗,𝑘) 𝐾(𝑓) 𝑀(𝑓) 𝑁(𝑓)

Proof of Theorem prodmodclem2a Dummy variables 𝑝 𝑚 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prodmo.1	. . 3 ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
2		prodmo.2	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
3		prodmodclem2a.dc	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)
4		prodmolem2.7	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ (ℤ_≥‘𝑀))
5		prodmolem2.9	. . . . . . 7 ⊢ (𝜑 → 𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴))
6		1zzd 9419	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
7		prodmolem2.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
8	7	nnzd 9514	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9	6, 8	fzfigd 10598	. . . . . . . . . . 11 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
10		prodmolem2.8	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)
11	9, 10	fihasheqf1od 10956	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴))
12	7	nnnn0d 9368	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
13		hashfz1 10950	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
14	12, 13	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
15	11, 14	eqtr3d 2241	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐴) = 𝑁)
16	15	oveq2d 5973	. . . . . . . 8 ⊢ (𝜑 → (1...(♯‘𝐴)) = (1...𝑁))
17		isoeq4 5886	. . . . . . . 8 ⊢ ((1...(♯‘𝐴)) = (1...𝑁) → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
18	16, 17	syl 14	. . . . . . 7 ⊢ (𝜑 → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
19	5, 18	mpbid 147	. . . . . 6 ⊢ (𝜑 → 𝐾 Isom < , < ((1...𝑁), 𝐴))
20		isof1o 5889	. . . . . 6 ⊢ (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto→𝐴)
21		f1of 5534	. . . . . 6 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴)
22	19, 20, 21	3syl 17	. . . . 5 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴)
23		nnuz 9704	. . . . . . 7 ⊢ ℕ = (ℤ_≥‘1)
24	7, 23	eleqtrdi 2299	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
25		eluzfz2 10174	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 𝑁 ∈ (1...𝑁))
26	24, 25	syl 14	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
27	22, 26	ffvelcdmd 5729	. . . 4 ⊢ (𝜑 → (𝐾‘𝑁) ∈ 𝐴)
28	4, 27	sseldd 3198	. . 3 ⊢ (𝜑 → (𝐾‘𝑁) ∈ (ℤ_≥‘𝑀))
29	4	sselda 3197	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (ℤ_≥‘𝑀))
30	19, 20	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)
31		f1ocnvfv2 5860	. . . . . . . . 9 ⊢ ((𝐾:(1...𝑁)–1-1-onto→𝐴 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) = 𝑝)
32	30, 31	sylan 283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) = 𝑝)
33		f1ocnv 5547	. . . . . . . . . . . 12 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → ^◡𝐾:𝐴–1-1-onto→(1...𝑁))
34		f1of 5534	. . . . . . . . . . . 12 ⊢ (^◡𝐾:𝐴–1-1-onto→(1...𝑁) → ^◡𝐾:𝐴⟶(1...𝑁))
35	30, 33, 34	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐾:𝐴⟶(1...𝑁))
36	35	ffvelcdmda 5728	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (^◡𝐾‘𝑝) ∈ (1...𝑁))
37		elfzle2 10170	. . . . . . . . . 10 ⊢ ((^◡𝐾‘𝑝) ∈ (1...𝑁) → (^◡𝐾‘𝑝) ≤ 𝑁)
38	36, 37	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (^◡𝐾‘𝑝) ≤ 𝑁)
39	19	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴))
40		fzssuz 10207	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
41		uzssz 9688	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘1) ⊆ ℤ
42		zssre 9399	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
43	41, 42	sstri 3206	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘1) ⊆ ℝ
44	40, 43	sstri 3206	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ ℝ
45		ressxr 8136	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ^*
46	44, 45	sstri 3206	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℝ^*
47	46	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (1...𝑁) ⊆ ℝ^*)
48		uzssz 9688	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
49	48, 42	sstri 3206	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
50	49, 45	sstri 3206	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ^*
51	4, 50	sstrdi 3209	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
52	51	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐴 ⊆ ℝ^*)
53	26	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑁 ∈ (1...𝑁))
54		leisorel 11004	. . . . . . . . . 10 ⊢ ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ ((^◡𝐾‘𝑝) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((^◡𝐾‘𝑝) ≤ 𝑁 ↔ (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁)))
55	39, 47, 52, 36, 53, 54	syl122anc 1259	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → ((^◡𝐾‘𝑝) ≤ 𝑁 ↔ (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁)))
56	38, 55	mpbid 147	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁))
57	32, 56	eqbrtrrd 4075	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ≤ (𝐾‘𝑁))
58	4, 48	sstrdi 3209	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
59	58	sselda 3197	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℤ)
60	48, 28	sselid 3195	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑁) ∈ ℤ)
61	60	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘𝑁) ∈ ℤ)
62		eluz 9681	. . . . . . . 8 ⊢ ((𝑝 ∈ ℤ ∧ (𝐾‘𝑁) ∈ ℤ) → ((𝐾‘𝑁) ∈ (ℤ_≥‘𝑝) ↔ 𝑝 ≤ (𝐾‘𝑁)))
63	59, 61, 62	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → ((𝐾‘𝑁) ∈ (ℤ_≥‘𝑝) ↔ 𝑝 ≤ (𝐾‘𝑁)))
64	57, 63	mpbird 167	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘𝑁) ∈ (ℤ_≥‘𝑝))
65		elfzuzb 10161	. . . . . 6 ⊢ (𝑝 ∈ (𝑀...(𝐾‘𝑁)) ↔ (𝑝 ∈ (ℤ_≥‘𝑀) ∧ (𝐾‘𝑁) ∈ (ℤ_≥‘𝑝)))
66	29, 64, 65	sylanbrc 417	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (𝑀...(𝐾‘𝑁)))
67	66	ex 115	. . . 4 ⊢ (𝜑 → (𝑝 ∈ 𝐴 → 𝑝 ∈ (𝑀...(𝐾‘𝑁))))
68	67	ssrdv 3203	. . 3 ⊢ (𝜑 → 𝐴 ⊆ (𝑀...(𝐾‘𝑁)))
69	1, 2, 3, 28, 68	fproddccvg 11958	. 2 ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)))
70		mullid 8090	. . . . 5 ⊢ (𝑚 ∈ ℂ → (1 · 𝑚) = 𝑚)
71	70	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (1 · 𝑚) = 𝑚)
72		mulrid 8089	. . . . 5 ⊢ (𝑚 ∈ ℂ → (𝑚 · 1) = 𝑚)
73	72	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (𝑚 · 1) = 𝑚)
74		mulcl 8072	. . . . 5 ⊢ ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 · 𝑥) ∈ ℂ)
75	74	adantl 277	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 · 𝑥) ∈ ℂ)
76		1cnd 8108	. . . 4 ⊢ (𝜑 → 1 ∈ ℂ)
77	26, 16	eleqtrrd 2286	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))
78		eluzelz 9677	. . . . . 6 ⊢ (𝑚 ∈ (ℤ_≥‘𝑀) → 𝑚 ∈ ℤ)
79		simpr 110	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → 𝑚 ∈ 𝐴)
80	2	ralrimiva 2580	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
81	80	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
82		nfcsb1v 3130	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵
83	82	nfel1 2360	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ
84		csbeq1a 3106	. . . . . . . . . 10 ⊢ (𝑘 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑘⦌𝐵)
85	84	eleq1d 2275	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → (𝐵 ∈ ℂ ↔ ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ))
86	83, 85	rspc 2875	. . . . . . . 8 ⊢ (𝑚 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ))
87	79, 81, 86	sylc 62	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ)
88		1cnd 8108	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ ¬ 𝑚 ∈ 𝐴) → 1 ∈ ℂ)
89		eleq1 2269	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → (𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴))
90	89	dcbid 840	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → (DECID 𝑘 ∈ 𝐴 ↔ DECID 𝑚 ∈ 𝐴))
91	3	ralrimiva 2580	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ_≥‘𝑀)DECID 𝑘 ∈ 𝐴)
92	91	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → ∀𝑘 ∈ (ℤ_≥‘𝑀)DECID 𝑘 ∈ 𝐴)
93		simpr 110	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝑚 ∈ (ℤ_≥‘𝑀))
94	90, 92, 93	rspcdva 2886	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → DECID 𝑚 ∈ 𝐴)
95	87, 88, 94	ifcldadc 3605	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ)
96		nfcv 2349	. . . . . . 7 ⊢ Ⅎ𝑘𝑚
97		nfv 1552	. . . . . . . 8 ⊢ Ⅎ𝑘 𝑚 ∈ 𝐴
98		nfcv 2349	. . . . . . . 8 ⊢ Ⅎ𝑘1
99	97, 82, 98	nfif 3604	. . . . . . 7 ⊢ Ⅎ𝑘if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1)
100	89, 84	ifbieq1d 3598	. . . . . . 7 ⊢ (𝑘 = 𝑚 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
101	96, 99, 100, 1	fvmptf 5685	. . . . . 6 ⊢ ((𝑚 ∈ ℤ ∧ if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ) → (𝐹‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
102	78, 95, 101	syl2an2 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
103	102, 95	eqeltrd 2283	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑚) ∈ ℂ)
104		prodmodclem2.4	. . . . . 6 ⊢ 𝐻 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1))
105		breq1 4054	. . . . . . 7 ⊢ (𝑗 = 𝑚 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑚 ≤ (♯‘𝐴)))
106		fveq2 5589	. . . . . . . 8 ⊢ (𝑗 = 𝑚 → (𝐾‘𝑗) = (𝐾‘𝑚))
107	106	csbeq1d 3104	. . . . . . 7 ⊢ (𝑗 = 𝑚 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
108	105, 107	ifbieq1d 3598	. . . . . 6 ⊢ (𝑗 = 𝑚 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1))
109		elnnuz 9705	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↔ 𝑚 ∈ (ℤ_≥‘1))
110	109	biimpri 133	. . . . . . 7 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 𝑚 ∈ ℕ)
111	110	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → 𝑚 ∈ ℕ)
112	22	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝐾:(1...𝑁)⟶𝐴)
113		1zzd 9419	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 1 ∈ ℤ)
114	8	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑁 ∈ ℤ)
115		eluzelz 9677	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 𝑚 ∈ ℤ)
116	115	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ∈ ℤ)
117	113, 114, 116	3jca 1180	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ))
118		eluzle 9680	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 1 ≤ 𝑚)
119	118	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 1 ≤ 𝑚)
120		simpr 110	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ≤ (♯‘𝐴))
121	15	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (♯‘𝐴) = 𝑁)
122	120, 121	breqtrd 4077	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ≤ 𝑁)
123	119, 122	jca 306	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (1 ≤ 𝑚 ∧ 𝑚 ≤ 𝑁))
124		elfz2 10157	. . . . . . . . . 10 ⊢ (𝑚 ∈ (1...𝑁) ↔ ((1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (1 ≤ 𝑚 ∧ 𝑚 ≤ 𝑁)))
125	117, 123, 124	sylanbrc 417	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ∈ (1...𝑁))
126	112, 125	ffvelcdmd 5729	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (𝐾‘𝑚) ∈ 𝐴)
127	80	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
128		nfcsb1v 3130	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵
129	128	nfel1 2360	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ
130		csbeq1a 3106	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑚) → 𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
131	130	eleq1d 2275	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
132	129, 131	rspc 2875	. . . . . . . 8 ⊢ ((𝐾‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
133	126, 127, 132	sylc 62	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
134		1cnd 8108	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑚 ≤ (♯‘𝐴)) → 1 ∈ ℂ)
135	111	nnzd 9514	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → 𝑚 ∈ ℤ)
136	15, 8	eqeltrd 2283	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
137	136	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (♯‘𝐴) ∈ ℤ)
138		zdcle 9469	. . . . . . . 8 ⊢ ((𝑚 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → DECID 𝑚 ≤ (♯‘𝐴))
139	135, 137, 138	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → DECID 𝑚 ≤ (♯‘𝐴))
140	133, 134, 139	ifcldadc 3605	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1) ∈ ℂ)
141	104, 108, 111, 140	fvmptd3 5686	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (𝐻‘𝑚) = if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1))
142	141, 140	eqeltrd 2283	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (𝐻‘𝑚) ∈ ℂ)
143		eldifi 3299	. . . . . . 7 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))))
144		elfzelz 10167	. . . . . . 7 ⊢ (𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑚 ∈ ℤ)
145	143, 144	syl 14	. . . . . 6 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑚 ∈ ℤ)
146		eldifn 3300	. . . . . . . . 9 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑚 ∈ 𝐴)
147	146	iffalsed 3585	. . . . . . . 8 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) = 1)
148		ax-1cn 8038	. . . . . . . 8 ⊢ 1 ∈ ℂ
149	147, 148	eqeltrdi 2297	. . . . . . 7 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ)
150	149	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ)
151	145, 150, 101	syl2an2 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
152	147	adantl 277	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) = 1)
153	151, 152	eqtrd 2239	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = 1)
154		elfzle2 10170	. . . . . . 7 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ≤ (♯‘𝐴))
155	154	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ (♯‘𝐴))
156	155	iftrued 3582	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
157		breq1 4054	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑥 ≤ (♯‘𝐴)))
158		fveq2 5589	. . . . . . . 8 ⊢ (𝑗 = 𝑥 → (𝐾‘𝑗) = (𝐾‘𝑥))
159	158	csbeq1d 3104	. . . . . . 7 ⊢ (𝑗 = 𝑥 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
160	157, 159	ifbieq1d 3598	. . . . . 6 ⊢ (𝑗 = 𝑥 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
161		elfznn 10196	. . . . . . 7 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ∈ ℕ)
162	161	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ ℕ)
163	22	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐾:(1...𝑁)⟶𝐴)
164		simpr 110	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ (1...(♯‘𝐴)))
165	15	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (♯‘𝐴) = 𝑁)
166	165	oveq2d 5973	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (1...(♯‘𝐴)) = (1...𝑁))
167	164, 166	eleqtrd 2285	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ (1...𝑁))
168	163, 167	ffvelcdmd 5729	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ 𝐴)
169	80	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
170		nfcsb1v 3130	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵
171	170	nfel1 2360	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ
172		csbeq1a 3106	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → 𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
173	172	eleq1d 2275	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ))
174	171, 173	rspc 2875	. . . . . . . 8 ⊢ ((𝐾‘𝑥) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ))
175	168, 169, 174	sylc 62	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ)
176	156, 175	eqeltrd 2283	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ)
177	104, 160, 162, 176	fvmptd3 5686	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
178	4	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
179	178, 48	sstrdi 3209	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ ℤ)
180	179, 168	sseldd 3198	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ ℤ)
181	168	iftrued 3582	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
182	181, 175	eqeltrd 2283	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ)
183		nfcv 2349	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐾‘𝑥)
184		nfv 1552	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝐾‘𝑥) ∈ 𝐴
185	184, 170, 98	nfif 3604	. . . . . . . 8 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1)
186		eleq1 2269	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
187	186, 172	ifbieq1d 3598	. . . . . . . 8 ⊢ (𝑘 = (𝐾‘𝑥) → if(𝑘 ∈ 𝐴, 𝐵, 1) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
188	183, 185, 187, 1	fvmptf 5685	. . . . . . 7 ⊢ (((𝐾‘𝑥) ∈ ℤ ∧ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
189	180, 182, 188	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
190	189, 181	eqtrd 2239	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
191	156, 177, 190	3eqtr4d 2249	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = (𝐹‘(𝐾‘𝑥)))
192	71, 73, 75, 76, 5, 77, 4, 103, 142, 153, 191	seq3coll 11009	. . 3 ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)) = (seq1( · , 𝐻)‘𝑁))
193		prodmodc.3	. . . 4 ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))
194	7, 7	jca 306	. . . 4 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ))
195	1, 2, 193, 104, 194, 10, 30	prodmodclem3 11961	. . 3 ⊢ (𝜑 → (seq1( · , 𝐺)‘𝑁) = (seq1( · , 𝐻)‘𝑁))
196	192, 195	eqtr4d 2242	. 2 ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)) = (seq1( · , 𝐺)‘𝑁))
197	69, 196	breqtrd 4077	1 ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 DECID wdc 836 ∧ w3a 981 = wceq 1373 ∈ wcel 2177 ∀wral 2485 ⦋csb 3097 ∖ cdif 3167 ⊆ wss 3170 ifcif 3575 class class class wbr 4051 ↦ cmpt 4113 ^◡ccnv 4682 ⟶wf 5276 –1-1-onto→wf1o 5279 ‘cfv 5280 Isom wiso 5281 (class class class)co 5957 ℂcc 7943 ℝcr 7944 1c1 7946 · cmul 7950 ℝ^*cxr 8126 < clt 8127 ≤ cle 8128 ℕcn 9056 ℕ₀cn0 9315 ℤcz 9392 ℤ_≥cuz 9668 ...cfz 10150 seqcseq 10614 ♯chash 10942 ⇝ cli 11664

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4167 ax-sep 4170 ax-nul 4178 ax-pow 4226 ax-pr 4261 ax-un 4488 ax-setind 4593 ax-iinf 4644 ax-cnex 8036 ax-resscn 8037 ax-1cn 8038 ax-1re 8039 ax-icn 8040 ax-addcl 8041 ax-addrcl 8042 ax-mulcl 8043 ax-mulrcl 8044 ax-addcom 8045 ax-mulcom 8046 ax-addass 8047 ax-mulass 8048 ax-distr 8049 ax-i2m1 8050 ax-0lt1 8051 ax-1rid 8052 ax-0id 8053 ax-rnegex 8054 ax-precex 8055 ax-cnre 8056 ax-pre-ltirr 8057 ax-pre-ltwlin 8058 ax-pre-lttrn 8059 ax-pre-apti 8060 ax-pre-ltadd 8061 ax-pre-mulgt0 8062 ax-pre-mulext 8063

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-nul 3465 df-if 3576 df-pw 3623 df-sn 3644 df-pr 3645 df-op 3647 df-uni 3857 df-int 3892 df-iun 3935 df-br 4052 df-opab 4114 df-mpt 4115 df-tr 4151 df-id 4348 df-po 4351 df-iso 4352 df-iord 4421 df-on 4423 df-ilim 4424 df-suc 4426 df-iom 4647 df-xp 4689 df-rel 4690 df-cnv 4691 df-co 4692 df-dm 4693 df-rn 4694 df-res 4695 df-ima 4696 df-iota 5241 df-fun 5282 df-fn 5283 df-f 5284 df-f1 5285 df-fo 5286 df-f1o 5287 df-fv 5288 df-isom 5289 df-riota 5912 df-ov 5960 df-oprab 5961 df-mpo 5962 df-1st 6239 df-2nd 6240 df-recs 6404 df-frec 6490 df-1o 6515 df-er 6633 df-en 6841 df-dom 6842 df-fin 6843 df-pnf 8129 df-mnf 8130 df-xr 8131 df-ltxr 8132 df-le 8133 df-sub 8265 df-neg 8266 df-reap 8668 df-ap 8675 df-div 8766 df-inn 9057 df-2 9115 df-n0 9316 df-z 9393 df-uz 9669 df-rp 9796 df-fz 10151 df-fzo 10285 df-seqfrec 10615 df-exp 10706 df-ihash 10943 df-cj 11228 df-rsqrt 11384 df-abs 11385 df-clim 11665

This theorem is referenced by: prodmodclem2 11963 zproddc 11965

W3C validator