Metamath Proof Explorer

Theorem coprmproddvds

Description: If a positive integer is divisible by each element of a set of pairwise coprime positive integers, then it is divisible by their product. (Contributed by AV, 19-Aug-2020)

Ref Expression
Assertion coprmproddvds ( ( ( 𝑀 ⊆ ℕ ∧ 𝑀 ∈ Fin ) ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 )

Proof

Step Hyp Ref Expression
1 cleq1lem ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ↔ ( ∅ ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) )
2 difeq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ∖ { 𝑚 } ) = ( ∅ ∖ { 𝑚 } ) )
3 2 raleqdv ⊢ ( 𝑥 = ∅ → ( ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ↔ ∀ 𝑛 ∈ ( ∅ ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
4 3 raleqbi1dv ⊢ ( 𝑥 = ∅ → ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ↔ ∀ 𝑚 ∈ ∅ ∀ 𝑛 ∈ ( ∅ ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
5 raleq ⊢ ( 𝑥 = ∅ → ( ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ↔ ∀ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
6 4 5 anbi12d ⊢ ( 𝑥 = ∅ → ( ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ↔ ( ∀ 𝑚 ∈ ∅ ∀ 𝑛 ∈ ( ∅ ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) )
7 1 6 anbi12d ⊢ ( 𝑥 = ∅ → ( ( ( 𝑥 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ↔ ( ( ∅ ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ∅ ∀ 𝑛 ∈ ( ∅ ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) )
8 prodeq1 ⊢ ( 𝑥 = ∅ → ∏ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) = ∏ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) )
9 8 breq1d ⊢ ( 𝑥 = ∅ → ( ∏ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ↔ ∏ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
10 7 9 imbi12d ⊢ ( 𝑥 = ∅ → ( ( ( ( 𝑥 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ↔ ( ( ( ∅ ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ∅ ∀ 𝑛 ∈ ( ∅ ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) )
11 cleq1lem ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ↔ ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) )
12 difeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∖ { 𝑚 } ) = ( 𝑦 ∖ { 𝑚 } ) )
13 12 raleqdv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ↔ ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
14 13 raleqbi1dv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ↔ ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
15 raleq ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ↔ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
16 14 15 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ↔ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) )
17 11 16 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ↔ ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) )
18 prodeq1 ⊢ ( 𝑥 = 𝑦 → ∏ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) = ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) )
19 18 breq1d ⊢ ( 𝑥 = 𝑦 → ( ∏ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ↔ ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
20 17 19 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( ( 𝑥 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ↔ ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) )
21 cleq1lem ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑥 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ↔ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) )
22 difeq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ∖ { 𝑚 } ) = ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) )
23 22 raleqdv ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ↔ ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
24 23 raleqbi1dv ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ↔ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
25 raleq ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ↔ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
26 24 25 anbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ↔ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) )
27 21 26 anbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ( 𝑥 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ↔ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) )
28 prodeq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ∏ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) = ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) )
29 28 breq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∏ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ↔ ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
30 27 29 imbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ( ( 𝑥 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ↔ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) )
31 cleq1lem ⊢ ( 𝑥 = 𝑀 → ( ( 𝑥 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ↔ ( 𝑀 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ) )
32 difeq1 ⊢ ( 𝑥 = 𝑀 → ( 𝑥 ∖ { 𝑚 } ) = ( 𝑀 ∖ { 𝑚 } ) )
33 32 raleqdv ⊢ ( 𝑥 = 𝑀 → ( ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ↔ ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
34 33 raleqbi1dv ⊢ ( 𝑥 = 𝑀 → ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ↔ ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ) )
35 raleq ⊢ ( 𝑥 = 𝑀 → ( ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ↔ ∀ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
36 34 35 anbi12d ⊢ ( 𝑥 = 𝑀 → ( ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ↔ ( ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) )
37 31 36 anbi12d ⊢ ( 𝑥 = 𝑀 → ( ( ( 𝑥 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ↔ ( ( 𝑀 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) )
38 prodeq1 ⊢ ( 𝑥 = 𝑀 → ∏ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) = ∏ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) )
39 38 breq1d ⊢ ( 𝑥 = 𝑀 → ( ∏ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ↔ ∏ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
40 37 39 imbi12d ⊢ ( 𝑥 = 𝑀 → ( ( ( ( 𝑥 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑥 ∀ 𝑛 ∈ ( 𝑥 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑥 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ↔ ( ( ( 𝑀 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) )
41 prod0 ⊢ ∏ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) = 1
42 nnz ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
43 1dvds ⊢ ( 𝐾 ∈ ℤ → 1 ∥ 𝐾 )
44 42 43 syl ⊢ ( 𝐾 ∈ ℕ → 1 ∥ 𝐾 )
45 41 44 eqbrtrid ⊢ ( 𝐾 ∈ ℕ → ∏ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 )
46 45 adantr ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ∏ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 )
47 46 ad2antlr ⊢ ( ( ( ∅ ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ∅ ∀ 𝑛 ∈ ( ∅ ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ ∅ ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 )
48 coprmproddvdslem ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ( 𝑦 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑛 ∈ ( 𝑦 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑦 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ( ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∀ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) )
49 10 20 30 40 47 48 findcard2s ⊢ ( 𝑀 ∈ Fin → ( ( ( 𝑀 ⊆ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ) ∧ ( ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) )
50 49 exp4c ⊢ ( 𝑀 ∈ Fin → ( 𝑀 ⊆ ℕ → ( ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( ( ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ∏ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) ) )
51 50 impcom ⊢ ( ( 𝑀 ⊆ ℕ ∧ 𝑀 ∈ Fin ) → ( ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( ( ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) → ∏ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) )
52 51 3imp ⊢ ( ( ( 𝑀 ⊆ ℕ ∧ 𝑀 ∈ Fin ) ∧ ( 𝐾 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ ( ∀ 𝑚 ∈ 𝑀 ∀ 𝑛 ∈ ( 𝑀 ∖ { 𝑚 } ) ( ( 𝐹 ‘ 𝑚 ) gcd ( 𝐹 ‘ 𝑛 ) ) = 1 ∧ ∀ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 ) ) → ∏ 𝑚 ∈ 𝑀 ( 𝐹 ‘ 𝑚 ) ∥ 𝐾 )