Theorem 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	⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑀 ⊆ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ 𝑀 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) → ( ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ( ∏ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) )

Proof

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