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 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 ) )