This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 bilanri ⊢ ( ( 𝑦 ⊆ ℕ ∧ { 𝑧 } ⊆ ℕ ) → 𝑧 ∈ ℕ )
61 57 60 sylbir ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ → 𝑧 ∈ ℕ )
62 61 3ad2ant1 ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → 𝑧 ∈ ℕ )
63 62 adantr ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → 𝑧 ∈ ℕ )
64 simprr ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ¬ 𝑧 ∈ 𝑦 )
65 simpll3 ⊢ ( ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ 𝑚 ∈ 𝑦 ) → 𝐹 : ℕ ⟶ ℕ )
66 simpl ⊢ ( ( 𝑦 ⊆ ℕ ∧ { 𝑧 } ⊆ ℕ ) → 𝑦 ⊆ ℕ )
67 57 66 sylbir ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ → 𝑦 ⊆ ℕ )
68 67 3ad2ant1 ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → 𝑦 ⊆ ℕ )
69 68 adantr ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → 𝑦 ⊆ ℕ )
70 69 sselda ⊢ ( ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ 𝑚 ∈ 𝑦 ) → 𝑚 ∈ ℕ )
71 65 70 ffvelcdmd ⊢ ( ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ 𝑚 ∈ 𝑦 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℕ )
72 71 nncnd ⊢ ( ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ 𝑚 ∈ 𝑦 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
73 fveq2 ⊢ ( 𝑚 = 𝑧 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑧 ) )
74 simpr ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → 𝐹 : ℕ ⟶ ℕ )
75 61 adantr ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → 𝑧 ∈ ℕ )
76 74 75 ffvelcdmd ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℕ )
77 76 3adant2 ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℕ )
78 77 adantr ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℕ )
79 78 nncnd ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
80 54 55 56 63 64 72 73 79 fprodsplitsn ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) = ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) )
81 80 oveq1d ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = ( ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) gcd 𝑁 ) )
82 56 71 fprodnncl ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℕ )
83 82 nnzd ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℤ )
84 78 nnzd ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℤ )
85 83 84 zmulcld ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) ∈ ℤ )
86 48 3ad2ant2 ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → 𝑁 ∈ ℤ )
87 86 adantr ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → 𝑁 ∈ ℤ )
88 85 87 gcdcomd ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) gcd 𝑁 ) = ( 𝑁 gcd ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) ) )
89 81 88 eqtrd ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = ( 𝑁 gcd ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) ) )
90 89 ex ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = ( 𝑁 gcd ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) ) ) )
91 90 3ad2ant1 ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = ( 𝑁 gcd ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) ) ) )
92 91 com12 ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = ( 𝑁 gcd ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) ) ) )
93 92 adantr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = ( 𝑁 gcd ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) ) ) )
94 93 imp ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ) → ( ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = ( 𝑁 gcd ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) ) )
95 simpl2 ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → 𝑁 ∈ ℕ )
96 95 82 78 3jca ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝑁 ∈ ℕ ∧ ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℕ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℕ ) )
97 96 ex ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( 𝑁 ∈ ℕ ∧ ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℕ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℕ ) ) )
98 97 3ad2ant1 ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( 𝑁 ∈ ℕ ∧ ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℕ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℕ ) ) )
99 98 com12 ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( 𝑁 ∈ ℕ ∧ ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℕ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℕ ) ) )
100 99 adantr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( 𝑁 ∈ ℕ ∧ ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℕ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℕ ) ) )
101 100 imp ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ) → ( 𝑁 ∈ ℕ ∧ ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℕ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℕ ) )
102 87 83 gcdcomd ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝑁 gcd ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ) = ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) )
103 102 ex ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( 𝑁 gcd ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ) = ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) ) )
104 103 3ad2ant1 ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( 𝑁 gcd ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ) = ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) ) )
105 104 com12 ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( 𝑁 gcd ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ) = ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) ) )
106 105 adantr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( 𝑁 gcd ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ) = ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) ) )
107 106 imp ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ) → ( 𝑁 gcd ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ) = ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) )
108 67 a1i ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ → 𝑦 ⊆ ℕ ) )
109 idd ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ ) )
110 idd ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( 𝐹 : ℕ ⟶ ℕ → 𝐹 : ℕ ⟶ ℕ ) )
111 108 109 110 3anim123d ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) )
112 ssun1 ⊢ 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } )
113 ssralv ⊢ ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 → ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) )
114 112 113 mp1i ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 → ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) )
115 ssralv ⊢ ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
116 112 115 mp1i ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
117 112 a1i ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑚 ∈ 𝑦 ) → 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) )
118 117 ssdifd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑚 ∈ 𝑦 ) → ( 𝑦 ∖ { 𝑚 } ) ⊆ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) )
119 ssralv ⊢ ( ( 𝑦 ∖ { 𝑚 } ) ⊆ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) → ( ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
120 118 119 syl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑚 ∈ 𝑦 ) → ( ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
121 120 ralimdva ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
122 116 121 syld ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
123 111 114 122 3anim123d ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ) )
124 123 imim1d ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) )
125 124 imp31 ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 )
126 107 125 eqtrd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ) → ( 𝑁 gcd ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ) = 1 )
127 rpmulgcd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℕ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℕ ) ∧ ( 𝑁 gcd ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ) = 1 ) → ( 𝑁 gcd ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑁 gcd ( 𝐹 ‘ 𝑧 ) ) )
128 101 126 127 syl2anc ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ) → ( 𝑁 gcd ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑁 gcd ( 𝐹 ‘ 𝑧 ) ) )
129 vsnid ⊢ 𝑧 ∈ { 𝑧 }
130 129 olci ⊢ ( 𝑧 ∈ 𝑦 ∨ 𝑧 ∈ { 𝑧 } )
131 elun ⊢ ( 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑧 ∈ 𝑦 ∨ 𝑧 ∈ { 𝑧 } ) )
132 130 131 mpbir ⊢ 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } )
133 73 oveq1d ⊢ ( 𝑚 = 𝑧 → ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = ( ( 𝐹 ‘ 𝑧 ) gcd 𝑁 ) )
134 133 eqeq1d ⊢ ( 𝑚 = 𝑧 → ( ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ↔ ( ( 𝐹 ‘ 𝑧 ) gcd 𝑁 ) = 1 ) )
135 134 rspcv ⊢ ( 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 → ( ( 𝐹 ‘ 𝑧 ) gcd 𝑁 ) = 1 ) )
136 132 135 mp1i ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 → ( ( 𝐹 ‘ 𝑧 ) gcd 𝑁 ) = 1 ) )
137 136 imp ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) → ( ( 𝐹 ‘ 𝑧 ) gcd 𝑁 ) = 1 )
138 77 nnzd ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℤ )
139 86 138 gcdcomd ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( 𝑁 gcd ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ 𝑧 ) gcd 𝑁 ) )
140 139 eqeq1d ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( ( 𝑁 gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ↔ ( ( 𝐹 ‘ 𝑧 ) gcd 𝑁 ) = 1 ) )
141 140 adantr ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) → ( ( 𝑁 gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ↔ ( ( 𝐹 ‘ 𝑧 ) gcd 𝑁 ) = 1 ) )
142 137 141 mpbird ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) → ( 𝑁 gcd ( 𝐹 ‘ 𝑧 ) ) = 1 )
143 142 3adant3 ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( 𝑁 gcd ( 𝐹 ‘ 𝑧 ) ) = 1 )
144 143 adantl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ) → ( 𝑁 gcd ( 𝐹 ‘ 𝑧 ) ) = 1 )
145 94 128 144 3eqtrd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ) → ( ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 )
146 145 exp31 ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ( 𝑦 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) )
147 11 22 33 44 53 146 findcard2s ⊢ ( 𝑀 ∈ Fin → ( ( ( 𝑀 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ∀ 𝑚 ∈ 𝑀 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ∧ ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) )
148 147 3expd ⊢ ( 𝑀 ∈ Fin → ( ( 𝑀 ⊆ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( ∀ 𝑚 ∈ 𝑀 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 → ( ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ( ∏ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) ) )
149 148 3expd ⊢ ( 𝑀 ∈ Fin → ( 𝑀 ⊆ ℕ → ( 𝑁 ∈ ℕ → ( 𝐹 : ℕ ⟶ ℕ → ( ∀ 𝑚 ∈ 𝑀 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 → ( ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ( ∏ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) ) ) ) )
150 149 3imp ⊢ ( ( 𝑀 ∈ Fin ∧ 𝑀 ⊆ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐹 : ℕ ⟶ ℕ → ( ∀ 𝑚 ∈ 𝑀 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 → ( ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ( ∏ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) ) ) )
151 150 3imp ⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑀 ⊆ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ 𝑀 ( ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) → ( ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ( ∏ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) gcd 𝑁 ) = 1 ) )