coprmproddvdslem

Description: Lemma for coprmproddvds : Induction step. (Contributed by AV, 19-Aug-2020)

		Ref	Expression
	Assertion	coprmproddvdslem	$⊢ (y \in Fin \land \neg z \in y) \to ((((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K) \to (((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K)) \to \prod_{m \in y \cup \{z\}} F (m) ∥ K))$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ m ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)))$
2		nfcv	$⊢ \underline{Ⅎ} m F (z)$
3		simpll	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to y \in Fin$
4		unss	$⊢ (y \subseteq ℕ \land \{z\} \subseteq ℕ) \leftrightarrow y \cup \{z\} \subseteq ℕ$
5		vex	$⊢ z \in V$
6	5	snss	$⊢ z \in ℕ \leftrightarrow \{z\} \subseteq ℕ$
7	6	biimpri	$⊢ \{z\} \subseteq ℕ \to z \in ℕ$
8	7	adantl	$⊢ (y \subseteq ℕ \land \{z\} \subseteq ℕ) \to z \in ℕ$
9	4 8	sylbir	$⊢ y \cup \{z\} \subseteq ℕ \to z \in ℕ$
10	9	adantr	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to z \in ℕ$
11	10	adantl	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to z \in ℕ$
12		simplr	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to \neg z \in y$
13		simprrr	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to F : ℕ ⟶ ℕ$
14	13	adantr	$⊢ (((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \land m \in y) \to F : ℕ ⟶ ℕ$
15		simpl	$⊢ (y \subseteq ℕ \land \{z\} \subseteq ℕ) \to y \subseteq ℕ$
16	4 15	sylbir	$⊢ y \cup \{z\} \subseteq ℕ \to y \subseteq ℕ$
17	16	adantr	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to y \subseteq ℕ$
18	17	adantl	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to y \subseteq ℕ$
19	18	sselda	$⊢ (((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \land m \in y) \to m \in ℕ$
20	14 19	ffvelrnd	$⊢ (((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \land m \in y) \to F (m) \in ℕ$
21	20	nncnd	$⊢ (((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \land m \in y) \to F (m) \in ℂ$
22		fveq2	$⊢ m = z \to F (m) = F (z)$
23	13 11	ffvelrnd	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to F (z) \in ℕ$
24	23	nncnd	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to F (z) \in ℂ$
25	1 2 3 11 12 21 22 24	fprodsplitsn	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to \prod_{m \in y \cup \{z\}} F (m) = \prod_{m \in y} F (m) F (z)$
26	25	ad2ant2r	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \land ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K))) \to \prod_{m \in y \cup \{z\}} F (m) = \prod_{m \in y} F (m) F (z)$
27		simprl	$⊢ ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (y \in Fin \land \neg z \in y)) \to y \in Fin$
28		simprr	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to F : ℕ ⟶ ℕ$
29	28	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (y \in Fin \land \neg z \in y)) \to F : ℕ ⟶ ℕ$
30	29	adantr	$⊢ (((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (y \in Fin \land \neg z \in y)) \land m \in y) \to F : ℕ ⟶ ℕ$
31	17	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (y \in Fin \land \neg z \in y)) \to y \subseteq ℕ$
32	31	sselda	$⊢ (((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (y \in Fin \land \neg z \in y)) \land m \in y) \to m \in ℕ$
33	30 32	ffvelrnd	$⊢ (((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (y \in Fin \land \neg z \in y)) \land m \in y) \to F (m) \in ℕ$
34	27 33	fprodnncl	$⊢ ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (y \in Fin \land \neg z \in y)) \to \prod_{m \in y} F (m) \in ℕ$
35	34	ex	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to ((y \in Fin \land \neg z \in y) \to \prod_{m \in y} F (m) \in ℕ)$
36	35	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K)) \to ((y \in Fin \land \neg z \in y) \to \prod_{m \in y} F (m) \in ℕ)$
37	36	com12	$⊢ (y \in Fin \land \neg z \in y) \to (((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K)) \to \prod_{m \in y} F (m) \in ℕ)$
38	37	adantr	$⊢ ((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \to (((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K)) \to \prod_{m \in y} F (m) \in ℕ)$
39	38	imp	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \land ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K))) \to \prod_{m \in y} F (m) \in ℕ$
40	39	nnzd	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \land ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K))) \to \prod_{m \in y} F (m) \in ℤ$
41	28 10	ffvelrnd	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to F (z) \in ℕ$
42	41	nnzd	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to F (z) \in ℤ$
43	42	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K)) \to F (z) \in ℤ$
44	43	adantl	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \land ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K))) \to F (z) \in ℤ$
45		nnz	$⊢ K \in ℕ \to K \in ℤ$
46	45	adantr	$⊢ (K \in ℕ \land F : ℕ ⟶ ℕ) \to K \in ℤ$
47	46	adantl	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to K \in ℤ$
48	47	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K)) \to K \in ℤ$
49	48	adantl	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \land ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K))) \to K \in ℤ$
50	40 44 49	3jca	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \land ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K))) \to (\prod_{m \in y} F (m) \in ℤ \land F (z) \in ℤ \land K \in ℤ)$
51		simpl	$⊢ (F : ℕ ⟶ ℕ \land y \cup \{z\} \subseteq ℕ) \to F : ℕ ⟶ ℕ$
52	9	adantl	$⊢ (F : ℕ ⟶ ℕ \land y \cup \{z\} \subseteq ℕ) \to z \in ℕ$
53	51 52	ffvelrnd	$⊢ (F : ℕ ⟶ ℕ \land y \cup \{z\} \subseteq ℕ) \to F (z) \in ℕ$
54	53	ex	$⊢ F : ℕ ⟶ ℕ \to (y \cup \{z\} \subseteq ℕ \to F (z) \in ℕ)$
55	54	adantl	$⊢ (K \in ℕ \land F : ℕ ⟶ ℕ) \to (y \cup \{z\} \subseteq ℕ \to F (z) \in ℕ)$
56	55	impcom	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to F (z) \in ℕ$
57	56	adantl	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to F (z) \in ℕ$
58	3 18 57	3jca	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to (y \in Fin \land y \subseteq ℕ \land F (z) \in ℕ)$
59	58	adantr	$⊢ (((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1) \to (y \in Fin \land y \subseteq ℕ \land F (z) \in ℕ)$
60	13	adantr	$⊢ (((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1) \to F : ℕ ⟶ ℕ$
61		vsnid	$⊢ z \in \{z\}$
62	61	olci	$⊢ (z \in y \lor z \in \{z\})$
63		elun	$⊢ z \in (y \cup \{z\}) \leftrightarrow (z \in y \lor z \in \{z\})$
64	62 63	mpbir	$⊢ z \in (y \cup \{z\})$
65	64	a1i	$⊢ (((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \land m \in y) \to z \in (y \cup \{z\})$
66		snssi	$⊢ m \in y \to \{m\} \subseteq y$
67	66	ssneld	$⊢ m \in y \to (\neg z \in y \to \neg z \in \{m\})$
68	67	com12	$⊢ \neg z \in y \to (m \in y \to \neg z \in \{m\})$
69	68	adantl	$⊢ (y \in Fin \land \neg z \in y) \to (m \in y \to \neg z \in \{m\})$
70	69	adantr	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to (m \in y \to \neg z \in \{m\})$
71	70	imp	$⊢ (((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \land m \in y) \to \neg z \in \{m\}$
72	65 71	eldifd	$⊢ (((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \land m \in y) \to z \in ((y \cup \{z\}) ∖ \{m\})$
73		fveq2	$⊢ n = z \to F (n) = F (z)$
74	73	oveq2d	$⊢ n = z \to F (m) \gcd F (n) = F (m) \gcd F (z)$
75	74	eqeq1d	$⊢ n = z \to (F (m) \gcd F (n) = 1 \leftrightarrow F (m) \gcd F (z) = 1)$
76	75	rspcv	$⊢ z \in ((y \cup \{z\}) ∖ \{m\}) \to (\forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \to F (m) \gcd F (z) = 1)$
77	72 76	syl	$⊢ (((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \land m \in y) \to (\forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \to F (m) \gcd F (z) = 1)$
78	77	ralimdva	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to (\forall m \in y \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \to \forall m \in y F (m) \gcd F (z) = 1)$
79		ralunb	$⊢ \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \leftrightarrow (\forall m \in y \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in \{z\} \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1)$
80	79	simplbi	$⊢ \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \to \forall m \in y \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1$
81	78 80	impel	$⊢ (((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1) \to \forall m \in y F (m) \gcd F (z) = 1$
82		raldifb	$⊢ \forall n \in (y \cup \{z\}) (n \notin \{m\} \to F (m) \gcd F (n) = 1) \leftrightarrow \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1$
83		ralunb	$⊢ \forall n \in (y \cup \{z\}) (n \notin \{m\} \to F (m) \gcd F (n) = 1) \leftrightarrow (\forall n \in y (n \notin \{m\} \to F (m) \gcd F (n) = 1) \land \forall n \in \{z\} (n \notin \{m\} \to F (m) \gcd F (n) = 1))$
84		raldifb	$⊢ \forall n \in y (n \notin \{m\} \to F (m) \gcd F (n) = 1) \leftrightarrow \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1$
85	84	biimpi	$⊢ \forall n \in y (n \notin \{m\} \to F (m) \gcd F (n) = 1) \to \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1$
86	85	adantr	$⊢ (\forall n \in y (n \notin \{m\} \to F (m) \gcd F (n) = 1) \land \forall n \in \{z\} (n \notin \{m\} \to F (m) \gcd F (n) = 1)) \to \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1$
87	83 86	sylbi	$⊢ \forall n \in (y \cup \{z\}) (n \notin \{m\} \to F (m) \gcd F (n) = 1) \to \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1$
88	82 87	sylbir	$⊢ \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \to \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1$
89	88	ralimi	$⊢ \forall m \in y \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \to \forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1$
90	89	adantr	$⊢ (\forall m \in y \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in \{z\} \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1) \to \forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1$
91	79 90	sylbi	$⊢ \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \to \forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1$
92	91	adantl	$⊢ (((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1) \to \forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1$
93		coprmprod	$⊢ ((y \in Fin \land y \subseteq ℕ \land F (z) \in ℕ) \land F : ℕ ⟶ ℕ \land \forall m \in y F (m) \gcd F (z) = 1) \to (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \to \prod_{m \in y} F (m) \gcd F (z) = 1)$
94	93	imp	$⊢ (((y \in Fin \land y \subseteq ℕ \land F (z) \in ℕ) \land F : ℕ ⟶ ℕ \land \forall m \in y F (m) \gcd F (z) = 1) \land \forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1) \to \prod_{m \in y} F (m) \gcd F (z) = 1$
95	59 60 81 92 94	syl31anc	$⊢ (((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1) \to \prod_{m \in y} F (m) \gcd F (z) = 1$
96	95	ex	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \to \prod_{m \in y} F (m) \gcd F (z) = 1)$
97	96	adantrd	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to ((\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K) \to \prod_{m \in y} F (m) \gcd F (z) = 1)$
98	97	expimpd	$⊢ (y \in Fin \land \neg z \in y) \to (((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K)) \to \prod_{m \in y} F (m) \gcd F (z) = 1)$
99	98	adantr	$⊢ ((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \to (((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K)) \to \prod_{m \in y} F (m) \gcd F (z) = 1)$
100	99	imp	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \land ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K))) \to \prod_{m \in y} F (m) \gcd F (z) = 1$
101	83	simplbi	$⊢ \forall n \in (y \cup \{z\}) (n \notin \{m\} \to F (m) \gcd F (n) = 1) \to \forall n \in y (n \notin \{m\} \to F (m) \gcd F (n) = 1)$
102	82 101	sylbir	$⊢ \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \to \forall n \in y (n \notin \{m\} \to F (m) \gcd F (n) = 1)$
103	102	ralimi	$⊢ \forall m \in y \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \to \forall m \in y \forall n \in y (n \notin \{m\} \to F (m) \gcd F (n) = 1)$
104	103	adantr	$⊢ (\forall m \in y \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in \{z\} \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1) \to \forall m \in y \forall n \in y (n \notin \{m\} \to F (m) \gcd F (n) = 1)$
105	79 104	sylbi	$⊢ \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \to \forall m \in y \forall n \in y (n \notin \{m\} \to F (m) \gcd F (n) = 1)$
106		ralunb	$⊢ \forall m \in (y \cup \{z\}) F (m) ∥ K \leftrightarrow (\forall m \in y F (m) ∥ K \land \forall m \in \{z\} F (m) ∥ K)$
107	106	simplbi	$⊢ \forall m \in (y \cup \{z\}) F (m) ∥ K \to \forall m \in y F (m) ∥ K$
108	84	ralbii	$⊢ \forall m \in y \forall n \in y (n \notin \{m\} \to F (m) \gcd F (n) = 1) \leftrightarrow \forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1$
109	108	anbi1i	$⊢ (\forall m \in y \forall n \in y (n \notin \{m\} \to F (m) \gcd F (n) = 1) \land \forall m \in y F (m) ∥ K) \leftrightarrow (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)$
110	17	adantl	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to y \subseteq ℕ$
111		simprrl	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to K \in ℕ$
112		simprrr	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to F : ℕ ⟶ ℕ$
113	110 111 112	jca32	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to (y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))$
114		simplr	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)$
115		pm2.27	$⊢ ((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to ((((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K) \to \prod_{m \in y} F (m) ∥ K)$
116	113 114 115	syl2anc	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to ((((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K) \to \prod_{m \in y} F (m) ∥ K)$
117	116	exp31	$⊢ (y \in Fin \land \neg z \in y) \to ((\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K) \to ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to ((((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K) \to \prod_{m \in y} F (m) ∥ K)))$
118	117	com24	$⊢ (y \in Fin \land \neg z \in y) \to ((((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K) \to ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to ((\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K) \to \prod_{m \in y} F (m) ∥ K)))$
119	118	imp	$⊢ ((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \to ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to ((\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K) \to \prod_{m \in y} F (m) ∥ K))$
120	119	imp	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to ((\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K) \to \prod_{m \in y} F (m) ∥ K)$
121	109 120	syl5bi	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to ((\forall m \in y \forall n \in y (n \notin \{m\} \to F (m) \gcd F (n) = 1) \land \forall m \in y F (m) ∥ K) \to \prod_{m \in y} F (m) ∥ K)$
122	105 107 121	syl2ani	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to ((\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K) \to \prod_{m \in y} F (m) ∥ K)$
123	122	impr	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \land ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K))) \to \prod_{m \in y} F (m) ∥ K$
124	22	breq1d	$⊢ m = z \to (F (m) ∥ K \leftrightarrow F (z) ∥ K)$
125	124	rspcv	$⊢ z \in (y \cup \{z\}) \to (\forall m \in (y \cup \{z\}) F (m) ∥ K \to F (z) ∥ K)$
126	64 125	ax-mp	$⊢ \forall m \in (y \cup \{z\}) F (m) ∥ K \to F (z) ∥ K$
127	126	adantl	$⊢ (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K) \to F (z) ∥ K$
128	127	adantl	$⊢ ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K)) \to F (z) ∥ K$
129	128	adantl	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \land ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K))) \to F (z) ∥ K$
130		coprmdvds2	$⊢ ((\prod_{m \in y} F (m) \in ℤ \land F (z) \in ℤ \land K \in ℤ) \land \prod_{m \in y} F (m) \gcd F (z) = 1) \to ((\prod_{m \in y} F (m) ∥ K \land F (z) ∥ K) \to \prod_{m \in y} F (m) F (z) ∥ K)$
131	130	imp	$⊢ (((\prod_{m \in y} F (m) \in ℤ \land F (z) \in ℤ \land K \in ℤ) \land \prod_{m \in y} F (m) \gcd F (z) = 1) \land (\prod_{m \in y} F (m) ∥ K \land F (z) ∥ K)) \to \prod_{m \in y} F (m) F (z) ∥ K$
132	50 100 123 129 131	syl22anc	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \land ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K))) \to \prod_{m \in y} F (m) F (z) ∥ K$
133	26 132	eqbrtrd	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K)) \land ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K))) \to \prod_{m \in y \cup \{z\}} F (m) ∥ K$
134	133	exp31	$⊢ (y \in Fin \land \neg z \in y) \to ((((y \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in y F (m) ∥ K)) \to \prod_{m \in y} F (m) ∥ K) \to (((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (\forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1 \land \forall m \in (y \cup \{z\}) F (m) ∥ K)) \to \prod_{m \in y \cup \{z\}} F (m) ∥ K))$

Metamath Proof Explorer

Theorem coprmproddvdslem

Proof