coprmprod

Description: The product of the elements of a sequence of pairwise coprime positive integers is coprime to a positive integer which is coprime to all integers of the sequence. (Contributed by AV, 18-Aug-2020)

		Ref	Expression
	Assertion	coprmprod	$⊢ ((M \in Fin \land M \subseteq ℕ \land N \in ℕ) \land F : ℕ ⟶ ℕ \land \forall m \in M F (m) \gcd N = 1) \to (\forall m \in M \forall n \in (M ∖ \{m\}) F (m) \gcd F (n) = 1 \to \prod_{m \in M} F (m) \gcd N = 1)$

Proof

Step	Hyp	Ref	Expression
1		sseq1	$⊢ x = \emptyset \to (x \subseteq ℕ \leftrightarrow \emptyset \subseteq ℕ)$
2	1	3anbi1d	$⊢ x = \emptyset \to ((x \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \leftrightarrow (\emptyset \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ))$
3		raleq	$⊢ x = \emptyset \to (\forall m \in x F (m) \gcd N = 1 \leftrightarrow \forall m \in \emptyset F (m) \gcd N = 1)$
4		difeq1	$⊢ x = \emptyset \to x ∖ \{m\} = \emptyset ∖ \{m\}$
5	4	raleqdv	$⊢ x = \emptyset \to (\forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1 \leftrightarrow \forall n \in (\emptyset ∖ \{m\}) F (m) \gcd F (n) = 1)$
6	5	raleqbi1dv	$⊢ x = \emptyset \to (\forall m \in x \forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1 \leftrightarrow \forall m \in \emptyset \forall n \in (\emptyset ∖ \{m\}) F (m) \gcd F (n) = 1)$
7	2 3 6	3anbi123d	$⊢ x = \emptyset \to (((x \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in x F (m) \gcd N = 1 \land \forall m \in x \forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1) \leftrightarrow ((\emptyset \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in \emptyset F (m) \gcd N = 1 \land \forall m \in \emptyset \forall n \in (\emptyset ∖ \{m\}) F (m) \gcd F (n) = 1))$
8		prodeq1	$⊢ x = \emptyset \to \prod_{m \in x} F (m) = \prod_{m \in \emptyset} F (m)$
9	8	oveq1d	$⊢ x = \emptyset \to \prod_{m \in x} F (m) \gcd N = \prod_{m \in \emptyset} F (m) \gcd N$
10	9	eqeq1d	$⊢ x = \emptyset \to (\prod_{m \in x} F (m) \gcd N = 1 \leftrightarrow \prod_{m \in \emptyset} F (m) \gcd N = 1)$
11	7 10	imbi12d	$⊢ x = \emptyset \to ((((x \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in x F (m) \gcd N = 1 \land \forall m \in x \forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1) \to \prod_{m \in x} F (m) \gcd N = 1) \leftrightarrow (((\emptyset \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in \emptyset F (m) \gcd N = 1 \land \forall m \in \emptyset \forall n \in (\emptyset ∖ \{m\}) F (m) \gcd F (n) = 1) \to \prod_{m \in \emptyset} F (m) \gcd N = 1))$
12		sseq1	$⊢ x = y \to (x \subseteq ℕ \leftrightarrow y \subseteq ℕ)$
13	12	3anbi1d	$⊢ x = y \to ((x \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \leftrightarrow (y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ))$
14		raleq	$⊢ x = y \to (\forall m \in x F (m) \gcd N = 1 \leftrightarrow \forall m \in y F (m) \gcd N = 1)$
15		difeq1	$⊢ x = y \to x ∖ \{m\} = y ∖ \{m\}$
16	15	raleqdv	$⊢ x = y \to (\forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1 \leftrightarrow \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1)$
17	16	raleqbi1dv	$⊢ x = y \to (\forall m \in x \forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1 \leftrightarrow \forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1)$
18	13 14 17	3anbi123d	$⊢ x = y \to (((x \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in x F (m) \gcd N = 1 \land \forall m \in x \forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1) \leftrightarrow ((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 1 \land \forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1))$
19		prodeq1	$⊢ x = y \to \prod_{m \in x} F (m) = \prod_{m \in y} F (m)$
20	19	oveq1d	$⊢ x = y \to \prod_{m \in x} F (m) \gcd N = \prod_{m \in y} F (m) \gcd N$
21	20	eqeq1d	$⊢ x = y \to (\prod_{m \in x} F (m) \gcd N = 1 \leftrightarrow \prod_{m \in y} F (m) \gcd N = 1)$
22	18 21	imbi12d	$⊢ x = y \to ((((x \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in x F (m) \gcd N = 1 \land \forall m \in x \forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1) \to \prod_{m \in x} F (m) \gcd N = 1) \leftrightarrow (((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 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 N = 1))$
23		sseq1	$⊢ x = y \cup \{z\} \to (x \subseteq ℕ \leftrightarrow y \cup \{z\} \subseteq ℕ)$
24	23	3anbi1d	$⊢ x = y \cup \{z\} \to ((x \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \leftrightarrow (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ))$
25		raleq	$⊢ x = y \cup \{z\} \to (\forall m \in x F (m) \gcd N = 1 \leftrightarrow \forall m \in (y \cup \{z\}) F (m) \gcd N = 1)$
26		difeq1	$⊢ x = y \cup \{z\} \to x ∖ \{m\} = (y \cup \{z\}) ∖ \{m\}$
27	26	raleqdv	$⊢ x = y \cup \{z\} \to (\forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1 \leftrightarrow \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1)$
28	27	raleqbi1dv	$⊢ x = y \cup \{z\} \to (\forall m \in x \forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1 \leftrightarrow \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1)$
29	24 25 28	3anbi123d	$⊢ x = y \cup \{z\} \to (((x \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in x F (m) \gcd N = 1 \land \forall m \in x \forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1) \leftrightarrow ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1))$
30		prodeq1	$⊢ x = y \cup \{z\} \to \prod_{m \in x} F (m) = \prod_{m \in y \cup \{z\}} F (m)$
31	30	oveq1d	$⊢ x = y \cup \{z\} \to \prod_{m \in x} F (m) \gcd N = \prod_{m \in y \cup \{z\}} F (m) \gcd N$
32	31	eqeq1d	$⊢ x = y \cup \{z\} \to (\prod_{m \in x} F (m) \gcd N = 1 \leftrightarrow \prod_{m \in y \cup \{z\}} F (m) \gcd N = 1)$
33	29 32	imbi12d	$⊢ x = y \cup \{z\} \to ((((x \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in x F (m) \gcd N = 1 \land \forall m \in x \forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1) \to \prod_{m \in x} F (m) \gcd N = 1) \leftrightarrow (((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \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 \cup \{z\}} F (m) \gcd N = 1))$
34		sseq1	$⊢ x = M \to (x \subseteq ℕ \leftrightarrow M \subseteq ℕ)$
35	34	3anbi1d	$⊢ x = M \to ((x \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \leftrightarrow (M \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ))$
36		raleq	$⊢ x = M \to (\forall m \in x F (m) \gcd N = 1 \leftrightarrow \forall m \in M F (m) \gcd N = 1)$
37		difeq1	$⊢ x = M \to x ∖ \{m\} = M ∖ \{m\}$
38	37	raleqdv	$⊢ x = M \to (\forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1 \leftrightarrow \forall n \in (M ∖ \{m\}) F (m) \gcd F (n) = 1)$
39	38	raleqbi1dv	$⊢ x = M \to (\forall m \in x \forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1 \leftrightarrow \forall m \in M \forall n \in (M ∖ \{m\}) F (m) \gcd F (n) = 1)$
40	35 36 39	3anbi123d	$⊢ x = M \to (((x \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in x F (m) \gcd N = 1 \land \forall m \in x \forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1) \leftrightarrow ((M \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in M F (m) \gcd N = 1 \land \forall m \in M \forall n \in (M ∖ \{m\}) F (m) \gcd F (n) = 1))$
41		prodeq1	$⊢ x = M \to \prod_{m \in x} F (m) = \prod_{m \in M} F (m)$
42	41	oveq1d	$⊢ x = M \to \prod_{m \in x} F (m) \gcd N = \prod_{m \in M} F (m) \gcd N$
43	42	eqeq1d	$⊢ x = M \to (\prod_{m \in x} F (m) \gcd N = 1 \leftrightarrow \prod_{m \in M} F (m) \gcd N = 1)$
44	40 43	imbi12d	$⊢ x = M \to ((((x \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in x F (m) \gcd N = 1 \land \forall m \in x \forall n \in (x ∖ \{m\}) F (m) \gcd F (n) = 1) \to \prod_{m \in x} F (m) \gcd N = 1) \leftrightarrow (((M \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in M F (m) \gcd N = 1 \land \forall m \in M \forall n \in (M ∖ \{m\}) F (m) \gcd F (n) = 1) \to \prod_{m \in M} F (m) \gcd N = 1))$
45		prod0	$⊢ \prod_{m \in \emptyset} F (m) = 1$
46	45	a1i	$⊢ N \in ℕ \to \prod_{m \in \emptyset} F (m) = 1$
47	46	oveq1d	$⊢ N \in ℕ \to \prod_{m \in \emptyset} F (m) \gcd N = 1 \gcd N$
48		nnz	$⊢ N \in ℕ \to N \in ℤ$
49		1gcd	$⊢ N \in ℤ \to 1 \gcd N = 1$
50	48 49	syl	$⊢ N \in ℕ \to 1 \gcd N = 1$
51	47 50	eqtrd	$⊢ N \in ℕ \to \prod_{m \in \emptyset} F (m) \gcd N = 1$
52	51	3ad2ant2	$⊢ (\emptyset \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to \prod_{m \in \emptyset} F (m) \gcd N = 1$
53	52	3ad2ant1	$⊢ ((\emptyset \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in \emptyset F (m) \gcd N = 1 \land \forall m \in \emptyset \forall n \in (\emptyset ∖ \{m\}) F (m) \gcd F (n) = 1) \to \prod_{m \in \emptyset} F (m) \gcd N = 1$
54		nfv	$⊢ Ⅎ m ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y))$
55		nfcv	$⊢ \underline{Ⅎ} m F (z)$
56		simprl	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to y \in Fin$
57		unss	$⊢ (y \subseteq ℕ \land \{z\} \subseteq ℕ) \leftrightarrow y \cup \{z\} \subseteq ℕ$
58		vex	$⊢ z \in V$
59	58	snss	$⊢ z \in ℕ \leftrightarrow \{z\} \subseteq ℕ$
60	59	biimpri	$⊢ \{z\} \subseteq ℕ \to z \in ℕ$
61	60	adantl	$⊢ (y \subseteq ℕ \land \{z\} \subseteq ℕ) \to z \in ℕ$
62	57 61	sylbir	$⊢ y \cup \{z\} \subseteq ℕ \to z \in ℕ$
63	62	3ad2ant1	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to z \in ℕ$
64	63	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to z \in ℕ$
65		simprr	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to \neg z \in y$
66		simpll3	$⊢ (((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \land m \in y) \to F : ℕ ⟶ ℕ$
67		simpl	$⊢ (y \subseteq ℕ \land \{z\} \subseteq ℕ) \to y \subseteq ℕ$
68	57 67	sylbir	$⊢ y \cup \{z\} \subseteq ℕ \to y \subseteq ℕ$
69	68	3ad2ant1	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to y \subseteq ℕ$
70	69	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to y \subseteq ℕ$
71	70	sselda	$⊢ (((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \land m \in y) \to m \in ℕ$
72	66 71	ffvelcdmd	$⊢ (((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \land m \in y) \to F (m) \in ℕ$
73	72	nncnd	$⊢ (((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \land m \in y) \to F (m) \in ℂ$
74		fveq2	$⊢ m = z \to F (m) = F (z)$
75		simpr	$⊢ (y \cup \{z\} \subseteq ℕ \land F : ℕ ⟶ ℕ) \to F : ℕ ⟶ ℕ$
76	62	adantr	$⊢ (y \cup \{z\} \subseteq ℕ \land F : ℕ ⟶ ℕ) \to z \in ℕ$
77	75 76	ffvelcdmd	$⊢ (y \cup \{z\} \subseteq ℕ \land F : ℕ ⟶ ℕ) \to F (z) \in ℕ$
78	77	3adant2	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to F (z) \in ℕ$
79	78	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to F (z) \in ℕ$
80	79	nncnd	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to F (z) \in ℂ$
81	54 55 56 64 65 73 74 80	fprodsplitsn	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to \prod_{m \in y \cup \{z\}} F (m) = \prod_{m \in y} F (m) F (z)$
82	81	oveq1d	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to \prod_{m \in y \cup \{z\}} F (m) \gcd N = \prod_{m \in y} F (m) F (z) \gcd N$
83	56 72	fprodnncl	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to \prod_{m \in y} F (m) \in ℕ$
84	83	nnzd	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to \prod_{m \in y} F (m) \in ℤ$
85	79	nnzd	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to F (z) \in ℤ$
86	84 85	zmulcld	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to \prod_{m \in y} F (m) F (z) \in ℤ$
87	48	3ad2ant2	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to N \in ℤ$
88	87	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to N \in ℤ$
89	86 88	gcdcomd	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to \prod_{m \in y} F (m) F (z) \gcd N = N \gcd \prod_{m \in y} F (m) F (z)$
90	82 89	eqtrd	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to \prod_{m \in y \cup \{z\}} F (m) \gcd N = N \gcd \prod_{m \in y} F (m) F (z)$
91	90	ex	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to ((y \in Fin \land \neg z \in y) \to \prod_{m \in y \cup \{z\}} F (m) \gcd N = N \gcd \prod_{m \in y} F (m) F (z))$
92	91	3ad2ant1	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \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 \neg z \in y) \to \prod_{m \in y \cup \{z\}} F (m) \gcd N = N \gcd \prod_{m \in y} F (m) F (z))$
93	92	com12	$⊢ (y \in Fin \land \neg z \in y) \to (((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \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 \cup \{z\}} F (m) \gcd N = N \gcd \prod_{m \in y} F (m) F (z))$
94	93	adantr	$⊢ ((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 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 N = 1)) \to (((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \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 \cup \{z\}} F (m) \gcd N = N \gcd \prod_{m \in y} F (m) F (z))$
95	94	imp	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 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 N = 1)) \land ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \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 \cup \{z\}} F (m) \gcd N = N \gcd \prod_{m \in y} F (m) F (z)$
96		simpl2	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to N \in ℕ$
97	96 83 79	3jca	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to (N \in ℕ \land \prod_{m \in y} F (m) \in ℕ \land F (z) \in ℕ)$
98	97	ex	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to ((y \in Fin \land \neg z \in y) \to (N \in ℕ \land \prod_{m \in y} F (m) \in ℕ \land F (z) \in ℕ))$
99	98	3ad2ant1	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \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 \neg z \in y) \to (N \in ℕ \land \prod_{m \in y} F (m) \in ℕ \land F (z) \in ℕ))$
100	99	com12	$⊢ (y \in Fin \land \neg z \in y) \to (((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1) \to (N \in ℕ \land \prod_{m \in y} F (m) \in ℕ \land F (z) \in ℕ))$
101	100	adantr	$⊢ ((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 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 N = 1)) \to (((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1) \to (N \in ℕ \land \prod_{m \in y} F (m) \in ℕ \land F (z) \in ℕ))$
102	101	imp	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 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 N = 1)) \land ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1)) \to (N \in ℕ \land \prod_{m \in y} F (m) \in ℕ \land F (z) \in ℕ)$
103	88 84	gcdcomd	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to N \gcd \prod_{m \in y} F (m) = \prod_{m \in y} F (m) \gcd N$
104	103	ex	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to ((y \in Fin \land \neg z \in y) \to N \gcd \prod_{m \in y} F (m) = \prod_{m \in y} F (m) \gcd N)$
105	104	3ad2ant1	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \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 \neg z \in y) \to N \gcd \prod_{m \in y} F (m) = \prod_{m \in y} F (m) \gcd N)$
106	105	com12	$⊢ (y \in Fin \land \neg z \in y) \to (((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1) \to N \gcd \prod_{m \in y} F (m) = \prod_{m \in y} F (m) \gcd N)$
107	106	adantr	$⊢ ((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 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 N = 1)) \to (((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1) \to N \gcd \prod_{m \in y} F (m) = \prod_{m \in y} F (m) \gcd N)$
108	107	imp	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 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 N = 1)) \land ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1)) \to N \gcd \prod_{m \in y} F (m) = \prod_{m \in y} F (m) \gcd N$
109	68	a1i	$⊢ (y \in Fin \land \neg z \in y) \to (y \cup \{z\} \subseteq ℕ \to y \subseteq ℕ)$
110		idd	$⊢ (y \in Fin \land \neg z \in y) \to (N \in ℕ \to N \in ℕ)$
111		idd	$⊢ (y \in Fin \land \neg z \in y) \to (F : ℕ ⟶ ℕ \to F : ℕ ⟶ ℕ)$
112	109 110 111	3anim123d	$⊢ (y \in Fin \land \neg z \in y) \to ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to (y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ))$
113		ssun1	$⊢ y \subseteq y \cup \{z\}$
114		ssralv	$⊢ y \subseteq y \cup \{z\} \to (\forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \to \forall m \in y F (m) \gcd N = 1)$
115	113 114	mp1i	$⊢ (y \in Fin \land \neg z \in y) \to (\forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \to \forall m \in y F (m) \gcd N = 1)$
116		ssralv	$⊢ y \subseteq y \cup \{z\} \to (\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)$
117	113 116	mp1i	$⊢ (y \in Fin \land \neg z \in y) \to (\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)$
118	113	a1i	$⊢ ((y \in Fin \land \neg z \in y) \land m \in y) \to y \subseteq y \cup \{z\}$
119	118	ssdifd	$⊢ ((y \in Fin \land \neg z \in y) \land m \in y) \to y ∖ \{m\} \subseteq (y \cup \{z\}) ∖ \{m\}$
120		ssralv	$⊢ y ∖ \{m\} \subseteq (y \cup \{z\}) ∖ \{m\} \to (\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)$
121	119 120	syl	$⊢ ((y \in Fin \land \neg z \in y) \land m \in y) \to (\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)$
122	121	ralimdva	$⊢ (y \in Fin \land \neg z \in y) \to (\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)$
123	117 122	syld	$⊢ (y \in Fin \land \neg z \in y) \to (\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)$
124	112 115 123	3anim123d	$⊢ (y \in Fin \land \neg z \in y) \to (((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1) \to ((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 1 \land \forall m \in y \forall n \in (y ∖ \{m\}) F (m) \gcd F (n) = 1))$
125	124	imim1d	$⊢ (y \in Fin \land \neg z \in y) \to ((((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 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 N = 1) \to (((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \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 N = 1))$
126	125	imp31	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 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 N = 1)) \land ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \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 N = 1$
127	108 126	eqtrd	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 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 N = 1)) \land ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1)) \to N \gcd \prod_{m \in y} F (m) = 1$
128		rpmulgcd	$⊢ ((N \in ℕ \land \prod_{m \in y} F (m) \in ℕ \land F (z) \in ℕ) \land N \gcd \prod_{m \in y} F (m) = 1) \to N \gcd \prod_{m \in y} F (m) F (z) = N \gcd F (z)$
129	102 127 128	syl2anc	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 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 N = 1)) \land ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1)) \to N \gcd \prod_{m \in y} F (m) F (z) = N \gcd F (z)$
130		vsnid	$⊢ z \in \{z\}$
131	130	olci	$⊢ (z \in y \lor z \in \{z\})$
132		elun	$⊢ z \in (y \cup \{z\}) \leftrightarrow (z \in y \lor z \in \{z\})$
133	131 132	mpbir	$⊢ z \in (y \cup \{z\})$
134	74	oveq1d	$⊢ m = z \to F (m) \gcd N = F (z) \gcd N$
135	134	eqeq1d	$⊢ m = z \to (F (m) \gcd N = 1 \leftrightarrow F (z) \gcd N = 1)$
136	135	rspcv	$⊢ z \in (y \cup \{z\}) \to (\forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \to F (z) \gcd N = 1)$
137	133 136	mp1i	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to (\forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \to F (z) \gcd N = 1)$
138	137	imp	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1) \to F (z) \gcd N = 1$
139	78	nnzd	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to F (z) \in ℤ$
140	87 139	gcdcomd	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to N \gcd F (z) = F (z) \gcd N$
141	140	eqeq1d	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to (N \gcd F (z) = 1 \leftrightarrow F (z) \gcd N = 1)$
142	141	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1) \to (N \gcd F (z) = 1 \leftrightarrow F (z) \gcd N = 1)$
143	138 142	mpbird	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1) \to N \gcd F (z) = 1$
144	143	3adant3	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1) \to N \gcd F (z) = 1$
145	144	adantl	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 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 N = 1)) \land ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \land \forall m \in (y \cup \{z\}) \forall n \in ((y \cup \{z\}) ∖ \{m\}) F (m) \gcd F (n) = 1)) \to N \gcd F (z) = 1$
146	95 129 145	3eqtrd	$⊢ (((y \in Fin \land \neg z \in y) \land (((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 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 N = 1)) \land ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \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 \cup \{z\}} F (m) \gcd N = 1$
147	146	exp31	$⊢ (y \in Fin \land \neg z \in y) \to ((((y \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in y F (m) \gcd N = 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 N = 1) \to (((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \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 \cup \{z\}} F (m) \gcd N = 1))$
148	11 22 33 44 53 147	findcard2s	$⊢ M \in Fin \to (((M \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land \forall m \in M F (m) \gcd N = 1 \land \forall m \in M \forall n \in (M ∖ \{m\}) F (m) \gcd F (n) = 1) \to \prod_{m \in M} F (m) \gcd N = 1)$
149	148	3expd	$⊢ M \in Fin \to ((M \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to (\forall m \in M F (m) \gcd N = 1 \to (\forall m \in M \forall n \in (M ∖ \{m\}) F (m) \gcd F (n) = 1 \to \prod_{m \in M} F (m) \gcd N = 1)))$
150	149	3expd	$⊢ M \in Fin \to (M \subseteq ℕ \to (N \in ℕ \to (F : ℕ ⟶ ℕ \to (\forall m \in M F (m) \gcd N = 1 \to (\forall m \in M \forall n \in (M ∖ \{m\}) F (m) \gcd F (n) = 1 \to \prod_{m \in M} F (m) \gcd N = 1)))))$
151	150	3imp	$⊢ (M \in Fin \land M \subseteq ℕ \land N \in ℕ) \to (F : ℕ ⟶ ℕ \to (\forall m \in M F (m) \gcd N = 1 \to (\forall m \in M \forall n \in (M ∖ \{m\}) F (m) \gcd F (n) = 1 \to \prod_{m \in M} F (m) \gcd N = 1)))$
152	151	3imp	$⊢ ((M \in Fin \land M \subseteq ℕ \land N \in ℕ) \land F : ℕ ⟶ ℕ \land \forall m \in M F (m) \gcd N = 1) \to (\forall m \in M \forall n \in (M ∖ \{m\}) F (m) \gcd F (n) = 1 \to \prod_{m \in M} F (m) \gcd N = 1)$

Metamath Proof Explorer

Theorem coprmprod

Proof