prodmodclem2a - Intuitionistic Logic Explorer

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

Theorem prodmodclem2a 11719

Description: Lemma for prodmodc 11721. (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 9344	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
7		prodmolem2.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
8	7	nnzd 9438	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9	6, 8	fzfigd 10502	. . . . . . . . . . 11 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
10		prodmolem2.8	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)
11	9, 10	fihasheqf1od 10860	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴))
12	7	nnnn0d 9293	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
13		hashfz1 10854	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
14	12, 13	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
15	11, 14	eqtr3d 2228	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐴) = 𝑁)
16	15	oveq2d 5934	. . . . . . . 8 ⊢ (𝜑 → (1...(♯‘𝐴)) = (1...𝑁))
17		isoeq4 5847	. . . . . . . 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 5850	. . . . . 6 ⊢ (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto→𝐴)
21		f1of 5500	. . . . . 6 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴)
22	19, 20, 21	3syl 17	. . . . 5 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴)
23		nnuz 9628	. . . . . . 7 ⊢ ℕ = (ℤ_≥‘1)
24	7, 23	eleqtrdi 2286	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
25		eluzfz2 10098	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 𝑁 ∈ (1...𝑁))
26	24, 25	syl 14	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
27	22, 26	ffvelcdmd 5694	. . . 4 ⊢ (𝜑 → (𝐾‘𝑁) ∈ 𝐴)
28	4, 27	sseldd 3180	. . 3 ⊢ (𝜑 → (𝐾‘𝑁) ∈ (ℤ_≥‘𝑀))
29	4	sselda 3179	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (ℤ_≥‘𝑀))
30	19, 20	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)
31		f1ocnvfv2 5821	. . . . . . . . 9 ⊢ ((𝐾:(1...𝑁)–1-1-onto→𝐴 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) = 𝑝)
32	30, 31	sylan 283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) = 𝑝)
33		f1ocnv 5513	. . . . . . . . . . . 12 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → ^◡𝐾:𝐴–1-1-onto→(1...𝑁))
34		f1of 5500	. . . . . . . . . . . 12 ⊢ (^◡𝐾:𝐴–1-1-onto→(1...𝑁) → ^◡𝐾:𝐴⟶(1...𝑁))
35	30, 33, 34	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐾:𝐴⟶(1...𝑁))
36	35	ffvelcdmda 5693	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (^◡𝐾‘𝑝) ∈ (1...𝑁))
37		elfzle2 10094	. . . . . . . . . 10 ⊢ ((^◡𝐾‘𝑝) ∈ (1...𝑁) → (^◡𝐾‘𝑝) ≤ 𝑁)
38	36, 37	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (^◡𝐾‘𝑝) ≤ 𝑁)
39	19	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴))
40		fzssuz 10131	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
41		uzssz 9612	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘1) ⊆ ℤ
42		zssre 9324	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
43	41, 42	sstri 3188	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘1) ⊆ ℝ
44	40, 43	sstri 3188	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ ℝ
45		ressxr 8063	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ^*
46	44, 45	sstri 3188	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℝ^*
47	46	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (1...𝑁) ⊆ ℝ^*)
48		uzssz 9612	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
49	48, 42	sstri 3188	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
50	49, 45	sstri 3188	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ^*
51	4, 50	sstrdi 3191	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
52	51	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐴 ⊆ ℝ^*)
53	26	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑁 ∈ (1...𝑁))
54		leisorel 10908	. . . . . . . . . 10 ⊢ ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ ((^◡𝐾‘𝑝) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((^◡𝐾‘𝑝) ≤ 𝑁 ↔ (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁)))
55	39, 47, 52, 36, 53, 54	syl122anc 1258	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → ((^◡𝐾‘𝑝) ≤ 𝑁 ↔ (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁)))
56	38, 55	mpbid 147	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁))
57	32, 56	eqbrtrrd 4053	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ≤ (𝐾‘𝑁))
58	4, 48	sstrdi 3191	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
59	58	sselda 3179	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℤ)
60	48, 28	sselid 3177	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑁) ∈ ℤ)
61	60	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘𝑁) ∈ ℤ)
62		eluz 9605	. . . . . . . 8 ⊢ ((𝑝 ∈ ℤ ∧ (𝐾‘𝑁) ∈ ℤ) → ((𝐾‘𝑁) ∈ (ℤ_≥‘𝑝) ↔ 𝑝 ≤ (𝐾‘𝑁)))
63	59, 61, 62	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → ((𝐾‘𝑁) ∈ (ℤ_≥‘𝑝) ↔ 𝑝 ≤ (𝐾‘𝑁)))
64	57, 63	mpbird 167	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘𝑁) ∈ (ℤ_≥‘𝑝))
65		elfzuzb 10085	. . . . . 6 ⊢ (𝑝 ∈ (𝑀...(𝐾‘𝑁)) ↔ (𝑝 ∈ (ℤ_≥‘𝑀) ∧ (𝐾‘𝑁) ∈ (ℤ_≥‘𝑝)))
66	29, 64, 65	sylanbrc 417	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (𝑀...(𝐾‘𝑁)))
67	66	ex 115	. . . 4 ⊢ (𝜑 → (𝑝 ∈ 𝐴 → 𝑝 ∈ (𝑀...(𝐾‘𝑁))))
68	67	ssrdv 3185	. . 3 ⊢ (𝜑 → 𝐴 ⊆ (𝑀...(𝐾‘𝑁)))
69	1, 2, 3, 28, 68	fproddccvg 11715	. 2 ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)))
70		mullid 8017	. . . . 5 ⊢ (𝑚 ∈ ℂ → (1 · 𝑚) = 𝑚)
71	70	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (1 · 𝑚) = 𝑚)
72		mulrid 8016	. . . . 5 ⊢ (𝑚 ∈ ℂ → (𝑚 · 1) = 𝑚)
73	72	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (𝑚 · 1) = 𝑚)
74		mulcl 7999	. . . . 5 ⊢ ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 · 𝑥) ∈ ℂ)
75	74	adantl 277	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 · 𝑥) ∈ ℂ)
76		1cnd 8035	. . . 4 ⊢ (𝜑 → 1 ∈ ℂ)
77	26, 16	eleqtrrd 2273	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))
78		eluzelz 9601	. . . . . 6 ⊢ (𝑚 ∈ (ℤ_≥‘𝑀) → 𝑚 ∈ ℤ)
79		simpr 110	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → 𝑚 ∈ 𝐴)
80	2	ralrimiva 2567	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
81	80	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
82		nfcsb1v 3113	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵
83	82	nfel1 2347	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ
84		csbeq1a 3089	. . . . . . . . . 10 ⊢ (𝑘 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑘⦌𝐵)
85	84	eleq1d 2262	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → (𝐵 ∈ ℂ ↔ ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ))
86	83, 85	rspc 2858	. . . . . . . 8 ⊢ (𝑚 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ))
87	79, 81, 86	sylc 62	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ)
88		1cnd 8035	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ ¬ 𝑚 ∈ 𝐴) → 1 ∈ ℂ)
89		eleq1 2256	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → (𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴))
90	89	dcbid 839	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → (DECID 𝑘 ∈ 𝐴 ↔ DECID 𝑚 ∈ 𝐴))
91	3	ralrimiva 2567	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ_≥‘𝑀)DECID 𝑘 ∈ 𝐴)
92	91	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → ∀𝑘 ∈ (ℤ_≥‘𝑀)DECID 𝑘 ∈ 𝐴)
93		simpr 110	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝑚 ∈ (ℤ_≥‘𝑀))
94	90, 92, 93	rspcdva 2869	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → DECID 𝑚 ∈ 𝐴)
95	87, 88, 94	ifcldadc 3586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ)
96		nfcv 2336	. . . . . . 7 ⊢ Ⅎ𝑘𝑚
97		nfv 1539	. . . . . . . 8 ⊢ Ⅎ𝑘 𝑚 ∈ 𝐴
98		nfcv 2336	. . . . . . . 8 ⊢ Ⅎ𝑘1
99	97, 82, 98	nfif 3585	. . . . . . 7 ⊢ Ⅎ𝑘if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1)
100	89, 84	ifbieq1d 3579	. . . . . . 7 ⊢ (𝑘 = 𝑚 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
101	96, 99, 100, 1	fvmptf 5650	. . . . . 6 ⊢ ((𝑚 ∈ ℤ ∧ if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ) → (𝐹‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
102	78, 95, 101	syl2an2 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
103	102, 95	eqeltrd 2270	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑚) ∈ ℂ)
104		prodmodclem2.4	. . . . . 6 ⊢ 𝐻 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1))
105		breq1 4032	. . . . . . 7 ⊢ (𝑗 = 𝑚 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑚 ≤ (♯‘𝐴)))
106		fveq2 5554	. . . . . . . 8 ⊢ (𝑗 = 𝑚 → (𝐾‘𝑗) = (𝐾‘𝑚))
107	106	csbeq1d 3087	. . . . . . 7 ⊢ (𝑗 = 𝑚 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
108	105, 107	ifbieq1d 3579	. . . . . 6 ⊢ (𝑗 = 𝑚 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1))
109		elnnuz 9629	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↔ 𝑚 ∈ (ℤ_≥‘1))
110	109	biimpri 133	. . . . . . 7 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 𝑚 ∈ ℕ)
111	110	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → 𝑚 ∈ ℕ)
112	22	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝐾:(1...𝑁)⟶𝐴)
113		1zzd 9344	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 1 ∈ ℤ)
114	8	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑁 ∈ ℤ)
115		eluzelz 9601	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 𝑚 ∈ ℤ)
116	115	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ∈ ℤ)
117	113, 114, 116	3jca 1179	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ))
118		eluzle 9604	. . . . . . . . . . . 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 4055	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ≤ 𝑁)
123	119, 122	jca 306	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (1 ≤ 𝑚 ∧ 𝑚 ≤ 𝑁))
124		elfz2 10081	. . . . . . . . . 10 ⊢ (𝑚 ∈ (1...𝑁) ↔ ((1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (1 ≤ 𝑚 ∧ 𝑚 ≤ 𝑁)))
125	117, 123, 124	sylanbrc 417	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ∈ (1...𝑁))
126	112, 125	ffvelcdmd 5694	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (𝐾‘𝑚) ∈ 𝐴)
127	80	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
128		nfcsb1v 3113	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵
129	128	nfel1 2347	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ
130		csbeq1a 3089	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑚) → 𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
131	130	eleq1d 2262	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
132	129, 131	rspc 2858	. . . . . . . 8 ⊢ ((𝐾‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
133	126, 127, 132	sylc 62	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
134		1cnd 8035	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑚 ≤ (♯‘𝐴)) → 1 ∈ ℂ)
135	111	nnzd 9438	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → 𝑚 ∈ ℤ)
136	15, 8	eqeltrd 2270	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
137	136	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (♯‘𝐴) ∈ ℤ)
138		zdcle 9393	. . . . . . . 8 ⊢ ((𝑚 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → DECID 𝑚 ≤ (♯‘𝐴))
139	135, 137, 138	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → DECID 𝑚 ≤ (♯‘𝐴))
140	133, 134, 139	ifcldadc 3586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1) ∈ ℂ)
141	104, 108, 111, 140	fvmptd3 5651	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (𝐻‘𝑚) = if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1))
142	141, 140	eqeltrd 2270	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (𝐻‘𝑚) ∈ ℂ)
143		eldifi 3281	. . . . . . 7 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))))
144		elfzelz 10091	. . . . . . 7 ⊢ (𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑚 ∈ ℤ)
145	143, 144	syl 14	. . . . . 6 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑚 ∈ ℤ)
146		eldifn 3282	. . . . . . . . 9 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑚 ∈ 𝐴)
147	146	iffalsed 3567	. . . . . . . 8 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) = 1)
148		ax-1cn 7965	. . . . . . . 8 ⊢ 1 ∈ ℂ
149	147, 148	eqeltrdi 2284	. . . . . . 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 2226	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = 1)
154		elfzle2 10094	. . . . . . 7 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ≤ (♯‘𝐴))
155	154	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ (♯‘𝐴))
156	155	iftrued 3564	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
157		breq1 4032	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑥 ≤ (♯‘𝐴)))
158		fveq2 5554	. . . . . . . 8 ⊢ (𝑗 = 𝑥 → (𝐾‘𝑗) = (𝐾‘𝑥))
159	158	csbeq1d 3087	. . . . . . 7 ⊢ (𝑗 = 𝑥 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
160	157, 159	ifbieq1d 3579	. . . . . 6 ⊢ (𝑗 = 𝑥 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
161		elfznn 10120	. . . . . . 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 5934	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (1...(♯‘𝐴)) = (1...𝑁))
167	164, 166	eleqtrd 2272	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ (1...𝑁))
168	163, 167	ffvelcdmd 5694	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ 𝐴)
169	80	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
170		nfcsb1v 3113	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵
171	170	nfel1 2347	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ
172		csbeq1a 3089	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → 𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
173	172	eleq1d 2262	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ))
174	171, 173	rspc 2858	. . . . . . . 8 ⊢ ((𝐾‘𝑥) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ))
175	168, 169, 174	sylc 62	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ)
176	156, 175	eqeltrd 2270	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ)
177	104, 160, 162, 176	fvmptd3 5651	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
178	4	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
179	178, 48	sstrdi 3191	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ ℤ)
180	179, 168	sseldd 3180	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ ℤ)
181	168	iftrued 3564	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
182	181, 175	eqeltrd 2270	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ)
183		nfcv 2336	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐾‘𝑥)
184		nfv 1539	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝐾‘𝑥) ∈ 𝐴
185	184, 170, 98	nfif 3585	. . . . . . . 8 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1)
186		eleq1 2256	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
187	186, 172	ifbieq1d 3579	. . . . . . . 8 ⊢ (𝑘 = (𝐾‘𝑥) → if(𝑘 ∈ 𝐴, 𝐵, 1) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
188	183, 185, 187, 1	fvmptf 5650	. . . . . . 7 ⊢ (((𝐾‘𝑥) ∈ ℤ ∧ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
189	180, 182, 188	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
190	189, 181	eqtrd 2226	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
191	156, 177, 190	3eqtr4d 2236	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = (𝐹‘(𝐾‘𝑥)))
192	71, 73, 75, 76, 5, 77, 4, 103, 142, 153, 191	seq3coll 10913	. . 3 ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)) = (seq1( · , 𝐻)‘𝑁))
193		prodmodc.3	. . . 4 ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))
194	7, 7	jca 306	. . . 4 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ))
195	1, 2, 193, 104, 194, 10, 30	prodmodclem3 11718	. . 3 ⊢ (𝜑 → (seq1( · , 𝐺)‘𝑁) = (seq1( · , 𝐻)‘𝑁))
196	192, 195	eqtr4d 2229	. 2 ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)) = (seq1( · , 𝐺)‘𝑁))
197	69, 196	breqtrd 4055	1 ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 DECID wdc 835 ∧ w3a 980 = wceq 1364 ∈ wcel 2164 ∀wral 2472 ⦋csb 3080 ∖ cdif 3150 ⊆ wss 3153 ifcif 3557 class class class wbr 4029 ↦ cmpt 4090 ^◡ccnv 4658 ⟶wf 5250 –1-1-onto→wf1o 5253 ‘cfv 5254 Isom wiso 5255 (class class class)co 5918 ℂcc 7870 ℝcr 7871 1c1 7873 · cmul 7877 ℝ^*cxr 8053 < clt 8054 ≤ cle 8055 ℕcn 8982 ℕ₀cn0 9240 ℤcz 9317 ℤ_≥cuz 9592 ...cfz 10074 seqcseq 10518 ♯chash 10846 ⇝ cli 11421

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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4144 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-iinf 4620 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-mulrcl 7971 ax-addcom 7972 ax-mulcom 7973 ax-addass 7974 ax-mulass 7975 ax-distr 7976 ax-i2m1 7977 ax-0lt1 7978 ax-1rid 7979 ax-0id 7980 ax-rnegex 7981 ax-precex 7982 ax-cnre 7983 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986 ax-pre-apti 7987 ax-pre-ltadd 7988 ax-pre-mulgt0 7989 ax-pre-mulext 7990

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4324 df-po 4327 df-iso 4328 df-iord 4397 df-on 4399 df-ilim 4400 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-f1 5259 df-fo 5260 df-f1o 5261 df-fv 5262 df-isom 5263 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-1st 6193 df-2nd 6194 df-recs 6358 df-frec 6444 df-1o 6469 df-er 6587 df-en 6795 df-dom 6796 df-fin 6797 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-le 8060 df-sub 8192 df-neg 8193 df-reap 8594 df-ap 8601 df-div 8692 df-inn 8983 df-2 9041 df-n0 9241 df-z 9318 df-uz 9593 df-rp 9720 df-fz 10075 df-fzo 10209 df-seqfrec 10519 df-exp 10610 df-ihash 10847 df-cj 10986 df-rsqrt 11142 df-abs 11143 df-clim 11422

This theorem is referenced by: prodmodclem2 11720 zproddc 11722

W3C validator