Theorem coprmproddvdslem

Description: Lemma for coprmproddvds : Induction step. (Contributed by AV, 19-Aug-2020)

	Ref	Expression
Assertion	coprmproddvdslem	⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑚 ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) )
2		nfcv	⊢ Ⅎ 𝑚 ( 𝐹 ‘ 𝑧 )
3		simpll	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → 𝑦 ∈ Fin )
4		unss	⊢ ( ( 𝑦 ⊆ ℕ ∧ { 𝑧 } ⊆ ℕ ) ↔ ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ )
5		vex	⊢ 𝑧 ∈ V
6	5	snss	⊢ ( 𝑧 ∈ ℕ ↔ { 𝑧 } ⊆ ℕ )
7	6	biimpri	⊢ ( { 𝑧 } ⊆ ℕ → 𝑧 ∈ ℕ )
8	7	adantl	⊢ ( ( 𝑦 ⊆ ℕ ∧ { 𝑧 } ⊆ ℕ ) → 𝑧 ∈ ℕ )
9	4 8	sylbir	⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ → 𝑧 ∈ ℕ )
10	9	adantr	⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) → 𝑧 ∈ ℕ )
11	10	adantl	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → 𝑧 ∈ ℕ )
12		simplr	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ¬ 𝑧 ∈ 𝑦 )
13		simprrr	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → 𝐹 : ℕ ⟶ ℕ )
14	13	adantr	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) ∧ 𝑚 ∈ 𝑦 ) → 𝐹 : ℕ ⟶ ℕ )
15		simpl	⊢ ( ( 𝑦 ⊆ ℕ ∧ { 𝑧 } ⊆ ℕ ) → 𝑦 ⊆ ℕ )
16	4 15	sylbir	⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ → 𝑦 ⊆ ℕ )
17	16	adantr	⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) → 𝑦 ⊆ ℕ )
18	17	adantl	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → 𝑦 ⊆ ℕ )
19	18	sselda	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) ∧ 𝑚 ∈ 𝑦 ) → 𝑚 ∈ ℕ )
20	14 19	ffvelcdmd	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) ∧ 𝑚 ∈ 𝑦 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℕ )
21	20	nncnd	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) ∧ 𝑚 ∈ 𝑦 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
22		fveq2	⊢ ( 𝑚 = 𝑧 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑧 ) )
23	13 11	ffvelcdmd	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℕ )
24	23	nncnd	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
25	1 2 3 11 12 21 22 24	fprodsplitsn	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) = ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) )
26	25	ad2ant2r	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) → ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) = ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) )
27		simprl	⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → 𝑦 ∈ Fin )
28		simprr	⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) → 𝐹 : ℕ ⟶ ℕ )
29	28	adantr	⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → 𝐹 : ℕ ⟶ ℕ )
30	29	adantr	⊢ ( ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ 𝑚 ∈ 𝑦 ) → 𝐹 : ℕ ⟶ ℕ )
31	17	adantr	⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → 𝑦 ⊆ ℕ )
32	31	sselda	⊢ ( ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ 𝑚 ∈ 𝑦 ) → 𝑚 ∈ ℕ )
33	30 32	ffvelcdmd	⊢ ( ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ 𝑚 ∈ 𝑦 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℕ )
34	27 33	fprodnncl	⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℕ )
35	34	ex	⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) → ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℕ ) )
36	35	adantr	⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℕ ) )
37	36	com12	⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℕ ) )
38	37	adantr	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℕ ) )
39	38	imp	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℕ )
40	39	nnzd	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℤ )
41	28 10	ffvelcdmd	⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℕ )
42	41	nnzd	⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℤ )
43	42	adantr	⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℤ )
44	43	adantl	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℤ )
45		nnz	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
46	45	adantr	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → 𝐾 ∈ ℤ )
47	46	adantl	⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) → 𝐾 ∈ ℤ )
48	47	adantr	⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → 𝐾 ∈ ℤ )
49	48	adantl	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) → 𝐾 ∈ ℤ )
50	40 44 49	3jca	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℤ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) )
51		simpl	⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ) → 𝐹 : ℕ ⟶ ℕ )
52	9	adantl	⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ) → 𝑧 ∈ ℕ )
53	51 52	ffvelcdmd	⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℕ )
54	53	ex	⊢ ( 𝐹 : ℕ ⟶ ℕ → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ → ( 𝐹 ‘ 𝑧 ) ∈ ℕ ) )
55	54	adantl	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ → ( 𝐹 ‘ 𝑧 ) ∈ ℕ ) )
56	55	impcom	⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℕ )
57	56	adantl	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℕ )
58	3 18 57	3jca	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ( 𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℕ ) )
59	58	adantr	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( 𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℕ ) )
60	13	adantr	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → 𝐹 : ℕ ⟶ ℕ )
61		vsnid	⊢ 𝑧 ∈ { 𝑧 }
62	61	olci	⊢ ( 𝑧 ∈ 𝑦 ∨ 𝑧 ∈ { 𝑧 } )
63		elun	⊢ ( 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑧 ∈ 𝑦 ∨ 𝑧 ∈ { 𝑧 } ) )
64	62 63	mpbir	⊢ 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } )
65	64	a1i	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) ∧ 𝑚 ∈ 𝑦 ) → 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) )
66		snssi	⊢ ( 𝑚 ∈ 𝑦 → { 𝑚 } ⊆ 𝑦 )
67	66	ssneld	⊢ ( 𝑚 ∈ 𝑦 → ( ¬ 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ { 𝑚 } ) )
68	67	com12	⊢ ( ¬ 𝑧 ∈ 𝑦 → ( 𝑚 ∈ 𝑦 → ¬ 𝑧 ∈ { 𝑚 } ) )
69	68	adantl	⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( 𝑚 ∈ 𝑦 → ¬ 𝑧 ∈ { 𝑚 } ) )
70	69	adantr	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ( 𝑚 ∈ 𝑦 → ¬ 𝑧 ∈ { 𝑚 } ) )
71	70	imp	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) ∧ 𝑚 ∈ 𝑦 ) → ¬ 𝑧 ∈ { 𝑚 } )
72	65 71	eldifd	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) ∧ 𝑚 ∈ 𝑦 ) → 𝑧 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) )
73		fveq2	⊢ ( 𝑛 = 𝑧 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑧 ) )
74	73	oveq2d	⊢ ( 𝑛 = 𝑧 → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) )
75	74	eqeq1d	⊢ ( 𝑛 = 𝑧 → ( ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ↔ ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ) )
76	75	rspcv	⊢ ( 𝑧 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) → ( ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ) )
77	72 76	syl	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) ∧ 𝑚 ∈ 𝑦 ) → ( ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ) )
78	77	ralimdva	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ) )
79		ralunb	⊢ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ↔ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ { 𝑧 } ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
80	79	simplbi	⊢ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 )
81	78 80	impel	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 )
82		raldifb	⊢ ( ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ↔ ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 )
83		ralunb	⊢ ( ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ↔ ( ∀ 𝑛 ∈ 𝑦 ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ∧ ∀ 𝑛 ∈ { 𝑧 } ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ) )
84		raldifb	⊢ ( ∀ 𝑛 ∈ 𝑦 ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ↔ ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 )
85	84	biimpi	⊢ ( ∀ 𝑛 ∈ 𝑦 ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 )
86	85	adantr	⊢ ( ( ∀ 𝑛 ∈ 𝑦 ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ∧ ∀ 𝑛 ∈ { 𝑧 } ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ) → ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 )
87	83 86	sylbi	⊢ ( ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 )
88	82 87	sylbir	⊢ ( ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 )
89	88	ralimi	⊢ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 )
90	89	adantr	⊢ ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ { 𝑧 } ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 )
91	79 90	sylbi	⊢ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 )
92	91	adantl	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 )
93		coprmprod	⊢ ( ( ( 𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℕ ) ∧ 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ) → ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ) )
94	93	imp	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℕ ) ∧ 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ 𝑦 ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ) ∧ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 )
95	59 60 81 92 94	syl31anc	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 )
96	95	ex	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ) )
97	96	adantrd	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ( ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ) )
98	97	expimpd	⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ) )
99	98	adantr	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ) )
100	99	imp	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 )
101	83	simplbi	⊢ ( ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ∀ 𝑛 ∈ 𝑦 ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
102	82 101	sylbir	⊢ ( ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ∀ 𝑛 ∈ 𝑦 ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
103	102	ralimi	⊢ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ 𝑦 ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
104	103	adantr	⊢ ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ { 𝑧 } ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) → ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ 𝑦 ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
105	79 104	sylbi	⊢ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 → ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ 𝑦 ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
106		ralunb	⊢ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ↔ ( ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ∧ ∀ 𝑚 ∈ { 𝑧 } ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
107	106	simplbi	⊢ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 → ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 )
108	84	ralbii	⊢ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ 𝑦 ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ↔ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 )
109	108	anbi1i	⊢ ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ 𝑦 ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ↔ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
110	17	adantl	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → 𝑦 ⊆ ℕ )
111		simprrl	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → 𝐾 ∈ ℕ )
112		simprrr	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → 𝐹 : ℕ ⟶ ℕ )
113	110 111 112	jca32	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) )
114		simplr	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
115		pm2.27	⊢ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ( ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
116	113 114 115	syl2anc	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ( ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
117	116	exp31	⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) → ( ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) )
118	117	com24	⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) → ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) )
119	118	imp	⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) → ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) )
120	119	imp	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
121	109 120	biimtrid	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ 𝑦 ( 𝑛 ∉ { 𝑚 } → ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
122	105 107 121	syl2ani	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) → ( ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
123	122	impr	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 )
124	22	breq1d	⊢ ( 𝑚 = 𝑧 → ( ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ↔ ( 𝐹 ‘ 𝑧 ) ∥ 𝐾 ) )
125	124	rspcv	⊢ ( 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 → ( 𝐹 ‘ 𝑧 ) ∥ 𝐾 ) )
126	64 125	ax-mp	⊢ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 → ( 𝐹 ‘ 𝑧 ) ∥ 𝐾 )
127	126	adantl	⊢ ( ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ( 𝐹 ‘ 𝑧 ) ∥ 𝐾 )
128	127	adantl	⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ( 𝐹 ‘ 𝑧 ) ∥ 𝐾 )
129	128	adantl	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) → ( 𝐹 ‘ 𝑧 ) ∥ 𝐾 )
130		coprmdvds2	⊢ ( ( ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℤ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ) → ( ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ∧ ( 𝐹 ‘ 𝑧 ) ∥ 𝐾 ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) ∥ 𝐾 ) )
131	130	imp	⊢ ( ( ( ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∈ ℤ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑧 ) ) = 1 ) ∧ ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ∧ ( 𝐹 ‘ 𝑧 ) ∥ 𝐾 ) ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) ∥ 𝐾 )
132	50 100 123 129 131	syl22anc	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) → ( ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) · ( 𝐹 ‘ 𝑧 ) ) ∥ 𝐾 )
133	26 132	eqbrtrd	⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) → ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 )
134	133	exp31	⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) )