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	bilanri	$⊢ (y \subseteq ℕ \land \{z\} \subseteq ℕ) \to z \in ℕ$
61	57 60	sylbir	$⊢ y \cup \{z\} \subseteq ℕ \to z \in ℕ$
62	61	3ad2ant1	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to z \in ℕ$
63	62	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to z \in ℕ$
64		simprr	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to \neg z \in y$
65		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 : ℕ ⟶ ℕ$
66		simpl	$⊢ (y \subseteq ℕ \land \{z\} \subseteq ℕ) \to y \subseteq ℕ$
67	57 66	sylbir	$⊢ y \cup \{z\} \subseteq ℕ \to y \subseteq ℕ$
68	67	3ad2ant1	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to y \subseteq ℕ$
69	68	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to y \subseteq ℕ$
70	69	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 ℕ$
71	65 70	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 ℕ$
72	71	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 ℂ$
73		fveq2	$⊢ m = z \to F (m) = F (z)$
74		simpr	$⊢ (y \cup \{z\} \subseteq ℕ \land F : ℕ ⟶ ℕ) \to F : ℕ ⟶ ℕ$
75	61	adantr	$⊢ (y \cup \{z\} \subseteq ℕ \land F : ℕ ⟶ ℕ) \to z \in ℕ$
76	74 75	ffvelcdmd	$⊢ (y \cup \{z\} \subseteq ℕ \land F : ℕ ⟶ ℕ) \to F (z) \in ℕ$
77	76	3adant2	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to F (z) \in ℕ$
78	77	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to F (z) \in ℕ$
79	78	nncnd	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to F (z) \in ℂ$
80	54 55 56 63 64 72 73 79	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)$
81	80	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$
82	56 71	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 ℕ$
83	82	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 ℤ$
84	78	nnzd	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to F (z) \in ℤ$
85	83 84	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 ℤ$
86	48	3ad2ant2	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to N \in ℤ$
87	86	adantr	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to N \in ℤ$
88	85 87	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)$
89	81 88	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)$
90	89	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))$
91	90	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))$
92	91	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))$
93	92	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))$
94	93	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)$
95		simpl2	$⊢ ((y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \land (y \in Fin \land \neg z \in y)) \to N \in ℕ$
96	95 82 78	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 ℕ)$
97	96	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 ℕ))$
98	97	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 ℕ))$
99	98	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 ℕ))$
100	99	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 ℕ))$
101	100	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 ℕ)$
102	87 83	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$
103	102	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)$
104	103	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)$
105	104	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)$
106	105	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)$
107	106	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$
108	67	a1i	$⊢ (y \in Fin \land \neg z \in y) \to (y \cup \{z\} \subseteq ℕ \to y \subseteq ℕ)$
109		idd	$⊢ (y \in Fin \land \neg z \in y) \to (N \in ℕ \to N \in ℕ)$
110		idd	$⊢ (y \in Fin \land \neg z \in y) \to (F : ℕ ⟶ ℕ \to F : ℕ ⟶ ℕ)$
111	108 109 110	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 : ℕ ⟶ ℕ))$
112		ssun1	$⊢ y \subseteq y \cup \{z\}$
113		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)$
114	112 113	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)$
115		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)$
116	112 115	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)$
117	112	a1i	$⊢ ((y \in Fin \land \neg z \in y) \land m \in y) \to y \subseteq y \cup \{z\}$
118	117	ssdifd	$⊢ ((y \in Fin \land \neg z \in y) \land m \in y) \to y ∖ \{m\} \subseteq (y \cup \{z\}) ∖ \{m\}$
119		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)$
120	118 119	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)$
121	120	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)$
122	116 121	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)$
123	111 114 122	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))$
124	123	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))$
125	124	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$
126	107 125	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$
127		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)$
128	101 126 127	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)$
129		vsnid	$⊢ z \in \{z\}$
130	129	olci	$⊢ (z \in y \lor z \in \{z\})$
131		elun	$⊢ z \in (y \cup \{z\}) \leftrightarrow (z \in y \lor z \in \{z\})$
132	130 131	mpbir	$⊢ z \in (y \cup \{z\})$
133	73	oveq1d	$⊢ m = z \to F (m) \gcd N = F (z) \gcd N$
134	133	eqeq1d	$⊢ m = z \to (F (m) \gcd N = 1 \leftrightarrow F (z) \gcd N = 1)$
135	134	rspcv	$⊢ z \in (y \cup \{z\}) \to (\forall m \in (y \cup \{z\}) F (m) \gcd N = 1 \to F (z) \gcd N = 1)$
136	132 135	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)$
137	136	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$
138	77	nnzd	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to F (z) \in ℤ$
139	86 138	gcdcomd	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to N \gcd F (z) = F (z) \gcd N$
140	139	eqeq1d	$⊢ (y \cup \{z\} \subseteq ℕ \land N \in ℕ \land F : ℕ ⟶ ℕ) \to (N \gcd F (z) = 1 \leftrightarrow F (z) \gcd N = 1)$
141	140	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)$
142	137 141	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$
143	142	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$
144	143	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$
145	94 128 144	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$
146	145	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))$
147	11 22 33 44 53 146	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)$
148	147	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)))$
149	148	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)))))$
150	149	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)))$
151	150	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