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	bilanri	$⊢ (y \subseteq ℕ \land \{z\} \subseteq ℕ) \to z \in ℕ$
8	4 7	sylbir	$⊢ y \cup \{z\} \subseteq ℕ \to z \in ℕ$
9	8	adantr	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to z \in ℕ$
10	9	adantl	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to z \in ℕ$
11		simplr	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to \neg z \in y$
12		simprrr	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to F : ℕ ⟶ ℕ$
13	12	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 : ℕ ⟶ ℕ$
14		simpl	$⊢ (y \subseteq ℕ \land \{z\} \subseteq ℕ) \to y \subseteq ℕ$
15	4 14	sylbir	$⊢ y \cup \{z\} \subseteq ℕ \to y \subseteq ℕ$
16	15	adantr	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to y \subseteq ℕ$
17	16	adantl	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to y \subseteq ℕ$
18	17	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 ℕ$
19	13 18	ffvelcdmd	$⊢ (((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 ℕ$
20	19	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 ℂ$
21		fveq2	$⊢ m = z \to F (m) = F (z)$
22	12 10	ffvelcdmd	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to F (z) \in ℕ$
23	22	nncnd	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to F (z) \in ℂ$
24	1 2 3 10 11 20 21 23	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)$
25	24	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)$
26		simprl	$⊢ ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (y \in Fin \land \neg z \in y)) \to y \in Fin$
27		simprr	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to F : ℕ ⟶ ℕ$
28	27	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (y \in Fin \land \neg z \in y)) \to F : ℕ ⟶ ℕ$
29	28	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 : ℕ ⟶ ℕ$
30	16	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \land (y \in Fin \land \neg z \in y)) \to y \subseteq ℕ$
31	30	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 ℕ$
32	29 31	ffvelcdmd	$⊢ (((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 ℕ$
33	26 32	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 ℕ$
34	33	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 ℕ)$
35	34	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 ℕ)$
36	35	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 ℕ)$
37	36	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 ℕ)$
38	37	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 ℕ$
39	38	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 ℤ$
40	27 9	ffvelcdmd	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to F (z) \in ℕ$
41	40	nnzd	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to F (z) \in ℤ$
42	41	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 ℤ$
43	42	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 ℤ$
44		nnz	$⊢ K \in ℕ \to K \in ℤ$
45	44	adantr	$⊢ (K \in ℕ \land F : ℕ ⟶ ℕ) \to K \in ℤ$
46	45	adantl	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to K \in ℤ$
47	46	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 ℤ$
48	47	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 ℤ$
49	39 43 48	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 ℤ)$
50		simpl	$⊢ (F : ℕ ⟶ ℕ \land y \cup \{z\} \subseteq ℕ) \to F : ℕ ⟶ ℕ$
51	8	adantl	$⊢ (F : ℕ ⟶ ℕ \land y \cup \{z\} \subseteq ℕ) \to z \in ℕ$
52	50 51	ffvelcdmd	$⊢ (F : ℕ ⟶ ℕ \land y \cup \{z\} \subseteq ℕ) \to F (z) \in ℕ$
53	52	ex	$⊢ F : ℕ ⟶ ℕ \to (y \cup \{z\} \subseteq ℕ \to F (z) \in ℕ)$
54	53	adantl	$⊢ (K \in ℕ \land F : ℕ ⟶ ℕ) \to (y \cup \{z\} \subseteq ℕ \to F (z) \in ℕ)$
55	54	impcom	$⊢ (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ)) \to F (z) \in ℕ$
56	55	adantl	$⊢ ((y \in Fin \land \neg z \in y) \land (y \cup \{z\} \subseteq ℕ \land (K \in ℕ \land F : ℕ ⟶ ℕ))) \to F (z) \in ℕ$
57	3 17 56	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 ℕ)$
58	57	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 ℕ)$
59	12	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 : ℕ ⟶ ℕ$
60		vsnid	$⊢ z \in \{z\}$
61	60	olci	$⊢ (z \in y \lor z \in \{z\})$
62		elun	$⊢ z \in (y \cup \{z\}) \leftrightarrow (z \in y \lor z \in \{z\})$
63	61 62	mpbir	$⊢ z \in (y \cup \{z\})$
64	63	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\})$
65		snssi	$⊢ m \in y \to \{m\} \subseteq y$
66	65	ssneld	$⊢ m \in y \to (\neg z \in y \to \neg z \in \{m\})$
67	66	com12	$⊢ \neg z \in y \to (m \in y \to \neg z \in \{m\})$
68	67	adantl	$⊢ (y \in Fin \land \neg z \in y) \to (m \in y \to \neg z \in \{m\})$
69	68	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\})$
70	69	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\}$
71	64 70	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\})$
72		fveq2	$⊢ n = z \to F (n) = F (z)$
73	72	oveq2d	$⊢ n = z \to F (m) \gcd F (n) = F (m) \gcd F (z)$
74	73	eqeq1d	$⊢ n = z \to (F (m) \gcd F (n) = 1 \leftrightarrow F (m) \gcd F (z) = 1)$
75	74	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)$
76	71 75	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)$
77	76	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)$
78		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)$
79	78	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$
80	77 79	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$
81		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$
82		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))$
83		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$
84	83	birani	$⊢ (\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$
85	82 84	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$
86	81 85	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$
87	86	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$
88	87	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$
89	78 88	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$
90	89	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$
91		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)$
92	91	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$
93	58 59 80 90 92	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$
94	93	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)$
95	94	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)$
96	95	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)$
97	96	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)$
98	97	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$
99	82	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)$
100	81 99	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)$
101	100	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)$
102	101	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)$
103	78 102	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)$
104		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)$
105	104	simplbi	$⊢ \forall m \in (y \cup \{z\}) F (m) ∥ K \to \forall m \in y F (m) ∥ K$
106	83	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$
107	106	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)$
108	16	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 ℕ$
109		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 ℕ$
110		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 : ℕ ⟶ ℕ$
111	108 109 110	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 : ℕ ⟶ ℕ))$
112		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)$
113		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)$
114	111 112 113	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)$
115	114	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)))$
116	115	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)))$
117	116	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))$
118	117	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)$
119	107 118	biimtrid	$⊢ (((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)$
120	103 105 119	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)$
121	120	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$
122	21	breq1d	$⊢ m = z \to (F (m) ∥ K \leftrightarrow F (z) ∥ K)$
123	122	rspcv	$⊢ z \in (y \cup \{z\}) \to (\forall m \in (y \cup \{z\}) F (m) ∥ K \to F (z) ∥ K)$
124	63 123	ax-mp	$⊢ \forall m \in (y \cup \{z\}) F (m) ∥ K \to F (z) ∥ K$
125	124	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$
126	125	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$
127	126	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$
128		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)$
129	128	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$
130	49 98 121 127 129	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$
131	25 130	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$
132	131	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