Metamath Proof Explorer

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