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 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 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) )