prodmodclem2a - Intuitionistic Logic Explorer

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

Theorem prodmodclem2a 12136

Description: Lemma for prodmodc 12138. (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 9505	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
7		prodmolem2.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
8	7	nnzd 9600	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9	6, 8	fzfigd 10692	. . . . . . . . . . 11 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
10		prodmolem2.8	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)
11	9, 10	fihasheqf1od 11050	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴))
12	7	nnnn0d 9454	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
13		hashfz1 11044	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
14	12, 13	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
15	11, 14	eqtr3d 2266	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐴) = 𝑁)
16	15	oveq2d 6033	. . . . . . . 8 ⊢ (𝜑 → (1...(♯‘𝐴)) = (1...𝑁))
17		isoeq4 5944	. . . . . . . 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 5947	. . . . . 6 ⊢ (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto→𝐴)
21		f1of 5583	. . . . . 6 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴)
22	19, 20, 21	3syl 17	. . . . 5 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴)
23		nnuz 9791	. . . . . . 7 ⊢ ℕ = (ℤ_≥‘1)
24	7, 23	eleqtrdi 2324	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
25		eluzfz2 10266	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 𝑁 ∈ (1...𝑁))
26	24, 25	syl 14	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
27	22, 26	ffvelcdmd 5783	. . . 4 ⊢ (𝜑 → (𝐾‘𝑁) ∈ 𝐴)
28	4, 27	sseldd 3228	. . 3 ⊢ (𝜑 → (𝐾‘𝑁) ∈ (ℤ_≥‘𝑀))
29	4	sselda 3227	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (ℤ_≥‘𝑀))
30	19, 20	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)
31		f1ocnvfv2 5918	. . . . . . . . 9 ⊢ ((𝐾:(1...𝑁)–1-1-onto→𝐴 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) = 𝑝)
32	30, 31	sylan 283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) = 𝑝)
33		f1ocnv 5596	. . . . . . . . . . . 12 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → ^◡𝐾:𝐴–1-1-onto→(1...𝑁))
34		f1of 5583	. . . . . . . . . . . 12 ⊢ (^◡𝐾:𝐴–1-1-onto→(1...𝑁) → ^◡𝐾:𝐴⟶(1...𝑁))
35	30, 33, 34	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐾:𝐴⟶(1...𝑁))
36	35	ffvelcdmda 5782	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (^◡𝐾‘𝑝) ∈ (1...𝑁))
37		elfzle2 10262	. . . . . . . . . 10 ⊢ ((^◡𝐾‘𝑝) ∈ (1...𝑁) → (^◡𝐾‘𝑝) ≤ 𝑁)
38	36, 37	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (^◡𝐾‘𝑝) ≤ 𝑁)
39	19	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴))
40		fzssuz 10299	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
41		uzssz 9775	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘1) ⊆ ℤ
42		zssre 9485	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
43	41, 42	sstri 3236	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘1) ⊆ ℝ
44	40, 43	sstri 3236	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ ℝ
45		ressxr 8222	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ^*
46	44, 45	sstri 3236	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℝ^*
47	46	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (1...𝑁) ⊆ ℝ^*)
48		uzssz 9775	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
49	48, 42	sstri 3236	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
50	49, 45	sstri 3236	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ^*
51	4, 50	sstrdi 3239	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
52	51	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐴 ⊆ ℝ^*)
53	26	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑁 ∈ (1...𝑁))
54		leisorel 11100	. . . . . . . . . 10 ⊢ ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ ((^◡𝐾‘𝑝) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((^◡𝐾‘𝑝) ≤ 𝑁 ↔ (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁)))
55	39, 47, 52, 36, 53, 54	syl122anc 1282	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → ((^◡𝐾‘𝑝) ≤ 𝑁 ↔ (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁)))
56	38, 55	mpbid 147	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁))
57	32, 56	eqbrtrrd 4112	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ≤ (𝐾‘𝑁))
58	4, 48	sstrdi 3239	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
59	58	sselda 3227	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℤ)
60	48, 28	sselid 3225	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑁) ∈ ℤ)
61	60	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘𝑁) ∈ ℤ)
62		eluz 9768	. . . . . . . 8 ⊢ ((𝑝 ∈ ℤ ∧ (𝐾‘𝑁) ∈ ℤ) → ((𝐾‘𝑁) ∈ (ℤ_≥‘𝑝) ↔ 𝑝 ≤ (𝐾‘𝑁)))
63	59, 61, 62	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → ((𝐾‘𝑁) ∈ (ℤ_≥‘𝑝) ↔ 𝑝 ≤ (𝐾‘𝑁)))
64	57, 63	mpbird 167	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘𝑁) ∈ (ℤ_≥‘𝑝))
65		elfzuzb 10253	. . . . . 6 ⊢ (𝑝 ∈ (𝑀...(𝐾‘𝑁)) ↔ (𝑝 ∈ (ℤ_≥‘𝑀) ∧ (𝐾‘𝑁) ∈ (ℤ_≥‘𝑝)))
66	29, 64, 65	sylanbrc 417	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (𝑀...(𝐾‘𝑁)))
67	66	ex 115	. . . 4 ⊢ (𝜑 → (𝑝 ∈ 𝐴 → 𝑝 ∈ (𝑀...(𝐾‘𝑁))))
68	67	ssrdv 3233	. . 3 ⊢ (𝜑 → 𝐴 ⊆ (𝑀...(𝐾‘𝑁)))
69	1, 2, 3, 28, 68	fproddccvg 12132	. 2 ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)))
70		mullid 8176	. . . . 5 ⊢ (𝑚 ∈ ℂ → (1 · 𝑚) = 𝑚)
71	70	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (1 · 𝑚) = 𝑚)
72		mulrid 8175	. . . . 5 ⊢ (𝑚 ∈ ℂ → (𝑚 · 1) = 𝑚)
73	72	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (𝑚 · 1) = 𝑚)
74		mulcl 8158	. . . . 5 ⊢ ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 · 𝑥) ∈ ℂ)
75	74	adantl 277	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 · 𝑥) ∈ ℂ)
76		1cnd 8194	. . . 4 ⊢ (𝜑 → 1 ∈ ℂ)
77	26, 16	eleqtrrd 2311	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))
78		eluzelz 9764	. . . . . 6 ⊢ (𝑚 ∈ (ℤ_≥‘𝑀) → 𝑚 ∈ ℤ)
79		simpr 110	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → 𝑚 ∈ 𝐴)
80	2	ralrimiva 2605	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
81	80	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
82		nfcsb1v 3160	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵
83	82	nfel1 2385	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ
84		csbeq1a 3136	. . . . . . . . . 10 ⊢ (𝑘 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑘⦌𝐵)
85	84	eleq1d 2300	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → (𝐵 ∈ ℂ ↔ ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ))
86	83, 85	rspc 2904	. . . . . . . 8 ⊢ (𝑚 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ))
87	79, 81, 86	sylc 62	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ)
88		1cnd 8194	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ ¬ 𝑚 ∈ 𝐴) → 1 ∈ ℂ)
89		eleq1 2294	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → (𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴))
90	89	dcbid 845	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → (DECID 𝑘 ∈ 𝐴 ↔ DECID 𝑚 ∈ 𝐴))
91	3	ralrimiva 2605	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ_≥‘𝑀)DECID 𝑘 ∈ 𝐴)
92	91	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → ∀𝑘 ∈ (ℤ_≥‘𝑀)DECID 𝑘 ∈ 𝐴)
93		simpr 110	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝑚 ∈ (ℤ_≥‘𝑀))
94	90, 92, 93	rspcdva 2915	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → DECID 𝑚 ∈ 𝐴)
95	87, 88, 94	ifcldadc 3635	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ)
96		nfcv 2374	. . . . . . 7 ⊢ Ⅎ𝑘𝑚
97		nfv 1576	. . . . . . . 8 ⊢ Ⅎ𝑘 𝑚 ∈ 𝐴
98		nfcv 2374	. . . . . . . 8 ⊢ Ⅎ𝑘1
99	97, 82, 98	nfif 3634	. . . . . . 7 ⊢ Ⅎ𝑘if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1)
100	89, 84	ifbieq1d 3628	. . . . . . 7 ⊢ (𝑘 = 𝑚 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
101	96, 99, 100, 1	fvmptf 5739	. . . . . 6 ⊢ ((𝑚 ∈ ℤ ∧ if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ) → (𝐹‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
102	78, 95, 101	syl2an2 598	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
103	102, 95	eqeltrd 2308	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑚) ∈ ℂ)
104		prodmodclem2.4	. . . . . 6 ⊢ 𝐻 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1))
105		breq1 4091	. . . . . . 7 ⊢ (𝑗 = 𝑚 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑚 ≤ (♯‘𝐴)))
106		fveq2 5639	. . . . . . . 8 ⊢ (𝑗 = 𝑚 → (𝐾‘𝑗) = (𝐾‘𝑚))
107	106	csbeq1d 3134	. . . . . . 7 ⊢ (𝑗 = 𝑚 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
108	105, 107	ifbieq1d 3628	. . . . . 6 ⊢ (𝑗 = 𝑚 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1))
109		elnnuz 9792	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↔ 𝑚 ∈ (ℤ_≥‘1))
110	109	biimpri 133	. . . . . . 7 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 𝑚 ∈ ℕ)
111	110	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → 𝑚 ∈ ℕ)
112	22	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝐾:(1...𝑁)⟶𝐴)
113		1zzd 9505	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 1 ∈ ℤ)
114	8	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑁 ∈ ℤ)
115		eluzelz 9764	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 𝑚 ∈ ℤ)
116	115	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ∈ ℤ)
117	113, 114, 116	3jca 1203	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ))
118		eluzle 9767	. . . . . . . . . . . 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 4114	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ≤ 𝑁)
123	119, 122	jca 306	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (1 ≤ 𝑚 ∧ 𝑚 ≤ 𝑁))
124		elfz2 10249	. . . . . . . . . 10 ⊢ (𝑚 ∈ (1...𝑁) ↔ ((1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (1 ≤ 𝑚 ∧ 𝑚 ≤ 𝑁)))
125	117, 123, 124	sylanbrc 417	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ∈ (1...𝑁))
126	112, 125	ffvelcdmd 5783	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (𝐾‘𝑚) ∈ 𝐴)
127	80	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
128		nfcsb1v 3160	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵
129	128	nfel1 2385	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ
130		csbeq1a 3136	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑚) → 𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
131	130	eleq1d 2300	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
132	129, 131	rspc 2904	. . . . . . . 8 ⊢ ((𝐾‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
133	126, 127, 132	sylc 62	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
134		1cnd 8194	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑚 ≤ (♯‘𝐴)) → 1 ∈ ℂ)
135	111	nnzd 9600	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → 𝑚 ∈ ℤ)
136	15, 8	eqeltrd 2308	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
137	136	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (♯‘𝐴) ∈ ℤ)
138		zdcle 9555	. . . . . . . 8 ⊢ ((𝑚 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → DECID 𝑚 ≤ (♯‘𝐴))
139	135, 137, 138	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → DECID 𝑚 ≤ (♯‘𝐴))
140	133, 134, 139	ifcldadc 3635	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1) ∈ ℂ)
141	104, 108, 111, 140	fvmptd3 5740	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (𝐻‘𝑚) = if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1))
142	141, 140	eqeltrd 2308	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (𝐻‘𝑚) ∈ ℂ)
143		eldifi 3329	. . . . . . 7 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))))
144		elfzelz 10259	. . . . . . 7 ⊢ (𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑚 ∈ ℤ)
145	143, 144	syl 14	. . . . . 6 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑚 ∈ ℤ)
146		eldifn 3330	. . . . . . . . 9 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑚 ∈ 𝐴)
147	146	iffalsed 3615	. . . . . . . 8 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) = 1)
148		ax-1cn 8124	. . . . . . . 8 ⊢ 1 ∈ ℂ
149	147, 148	eqeltrdi 2322	. . . . . . 7 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ)
150	149	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ)
151	145, 150, 101	syl2an2 598	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
152	147	adantl 277	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) = 1)
153	151, 152	eqtrd 2264	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = 1)
154		elfzle2 10262	. . . . . . 7 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ≤ (♯‘𝐴))
155	154	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ (♯‘𝐴))
156	155	iftrued 3612	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
157		breq1 4091	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑥 ≤ (♯‘𝐴)))
158		fveq2 5639	. . . . . . . 8 ⊢ (𝑗 = 𝑥 → (𝐾‘𝑗) = (𝐾‘𝑥))
159	158	csbeq1d 3134	. . . . . . 7 ⊢ (𝑗 = 𝑥 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
160	157, 159	ifbieq1d 3628	. . . . . 6 ⊢ (𝑗 = 𝑥 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
161		elfznn 10288	. . . . . . 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 6033	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (1...(♯‘𝐴)) = (1...𝑁))
167	164, 166	eleqtrd 2310	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ (1...𝑁))
168	163, 167	ffvelcdmd 5783	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ 𝐴)
169	80	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
170		nfcsb1v 3160	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵
171	170	nfel1 2385	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ
172		csbeq1a 3136	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → 𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
173	172	eleq1d 2300	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ))
174	171, 173	rspc 2904	. . . . . . . 8 ⊢ ((𝐾‘𝑥) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ))
175	168, 169, 174	sylc 62	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ)
176	156, 175	eqeltrd 2308	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ)
177	104, 160, 162, 176	fvmptd3 5740	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
178	4	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
179	178, 48	sstrdi 3239	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ ℤ)
180	179, 168	sseldd 3228	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ ℤ)
181	168	iftrued 3612	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
182	181, 175	eqeltrd 2308	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ)
183		nfcv 2374	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐾‘𝑥)
184		nfv 1576	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝐾‘𝑥) ∈ 𝐴
185	184, 170, 98	nfif 3634	. . . . . . . 8 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1)
186		eleq1 2294	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
187	186, 172	ifbieq1d 3628	. . . . . . . 8 ⊢ (𝑘 = (𝐾‘𝑥) → if(𝑘 ∈ 𝐴, 𝐵, 1) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
188	183, 185, 187, 1	fvmptf 5739	. . . . . . 7 ⊢ (((𝐾‘𝑥) ∈ ℤ ∧ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
189	180, 182, 188	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
190	189, 181	eqtrd 2264	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
191	156, 177, 190	3eqtr4d 2274	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = (𝐹‘(𝐾‘𝑥)))
192	71, 73, 75, 76, 5, 77, 4, 103, 142, 153, 191	seq3coll 11105	. . 3 ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)) = (seq1( · , 𝐻)‘𝑁))
193		prodmodc.3	. . . 4 ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))
194	7, 7	jca 306	. . . 4 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ))
195	1, 2, 193, 104, 194, 10, 30	prodmodclem3 12135	. . 3 ⊢ (𝜑 → (seq1( · , 𝐺)‘𝑁) = (seq1( · , 𝐻)‘𝑁))
196	192, 195	eqtr4d 2267	. 2 ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)) = (seq1( · , 𝐺)‘𝑁))
197	69, 196	breqtrd 4114	1 ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 DECID wdc 841 ∧ w3a 1004 = wceq 1397 ∈ wcel 2202 ∀wral 2510 ⦋csb 3127 ∖ cdif 3197 ⊆ wss 3200 ifcif 3605 class class class wbr 4088 ↦ cmpt 4150 ^◡ccnv 4724 ⟶wf 5322 –1-1-onto→wf1o 5325 ‘cfv 5326 Isom wiso 5327 (class class class)co 6017 ℂcc 8029 ℝcr 8030 1c1 8032 · cmul 8036 ℝ^*cxr 8212 < clt 8213 ≤ cle 8214 ℕcn 9142 ℕ₀cn0 9401 ℤcz 9478 ℤ_≥cuz 9754 ...cfz 10242 seqcseq 10708 ♯chash 11036 ⇝ cli 11838

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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 ax-cnex 8122 ax-resscn 8123 ax-1cn 8124 ax-1re 8125 ax-icn 8126 ax-addcl 8127 ax-addrcl 8128 ax-mulcl 8129 ax-mulrcl 8130 ax-addcom 8131 ax-mulcom 8132 ax-addass 8133 ax-mulass 8134 ax-distr 8135 ax-i2m1 8136 ax-0lt1 8137 ax-1rid 8138 ax-0id 8139 ax-rnegex 8140 ax-precex 8141 ax-cnre 8142 ax-pre-ltirr 8143 ax-pre-ltwlin 8144 ax-pre-lttrn 8145 ax-pre-apti 8146 ax-pre-ltadd 8147 ax-pre-mulgt0 8148 ax-pre-mulext 8149

This theorem depends on definitions: df-bi 117 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rmo 2518 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-po 4393 df-iso 4394 df-iord 4463 df-on 4465 df-ilim 4466 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-isom 5335 df-riota 5970 df-ov 6020 df-oprab 6021 df-mpo 6022 df-1st 6302 df-2nd 6303 df-recs 6470 df-frec 6556 df-1o 6581 df-er 6701 df-en 6909 df-dom 6910 df-fin 6911 df-pnf 8215 df-mnf 8216 df-xr 8217 df-ltxr 8218 df-le 8219 df-sub 8351 df-neg 8352 df-reap 8754 df-ap 8761 df-div 8852 df-inn 9143 df-2 9201 df-n0 9402 df-z 9479 df-uz 9755 df-rp 9888 df-fz 10243 df-fzo 10377 df-seqfrec 10709 df-exp 10800 df-ihash 11037 df-cj 11402 df-rsqrt 11558 df-abs 11559 df-clim 11839

This theorem is referenced by: prodmodclem2 12137 zproddc 12139

W3C validator