Proof of Theorem coprmproddvdslem
Step | Hyp | Ref
| Expression |
1 | | nfv 1921 |
. . . . 5
⊢
Ⅎ𝑚((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) |
2 | | nfcv 2909 |
. . . . 5
⊢
Ⅎ𝑚(𝐹‘𝑧) |
3 | | simpll 764 |
. . . . 5
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝑦 ∈ Fin) |
4 | | unss 4123 |
. . . . . . . 8
⊢ ((𝑦 ⊆ ℕ ∧ {𝑧} ⊆ ℕ) ↔ (𝑦 ∪ {𝑧}) ⊆ ℕ) |
5 | | vex 3435 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
6 | 5 | snss 4725 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℕ ↔ {𝑧} ⊆
ℕ) |
7 | 6 | biimpri 227 |
. . . . . . . . 9
⊢ ({𝑧} ⊆ ℕ → 𝑧 ∈
ℕ) |
8 | 7 | adantl 482 |
. . . . . . . 8
⊢ ((𝑦 ⊆ ℕ ∧ {𝑧} ⊆ ℕ) → 𝑧 ∈
ℕ) |
9 | 4, 8 | sylbir 234 |
. . . . . . 7
⊢ ((𝑦 ∪ {𝑧}) ⊆ ℕ → 𝑧 ∈ ℕ) |
10 | 9 | adantr 481 |
. . . . . 6
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → 𝑧 ∈
ℕ) |
11 | 10 | adantl 482 |
. . . . 5
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝑧 ∈
ℕ) |
12 | | simplr 766 |
. . . . 5
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ¬
𝑧 ∈ 𝑦) |
13 | | simprrr 779 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝐹:ℕ⟶ℕ) |
14 | 13 | adantr 481 |
. . . . . . 7
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚 ∈ 𝑦) → 𝐹:ℕ⟶ℕ) |
15 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ ℕ ∧ {𝑧} ⊆ ℕ) → 𝑦 ⊆
ℕ) |
16 | 4, 15 | sylbir 234 |
. . . . . . . . . 10
⊢ ((𝑦 ∪ {𝑧}) ⊆ ℕ → 𝑦 ⊆ ℕ) |
17 | 16 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → 𝑦 ⊆
ℕ) |
18 | 17 | adantl 482 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝑦 ⊆
ℕ) |
19 | 18 | sselda 3926 |
. . . . . . 7
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚 ∈ 𝑦) → 𝑚 ∈ ℕ) |
20 | 14, 19 | ffvelrnd 6957 |
. . . . . 6
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚 ∈ 𝑦) → (𝐹‘𝑚) ∈ ℕ) |
21 | 20 | nncnd 11987 |
. . . . 5
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚 ∈ 𝑦) → (𝐹‘𝑚) ∈ ℂ) |
22 | | fveq2 6769 |
. . . . 5
⊢ (𝑚 = 𝑧 → (𝐹‘𝑚) = (𝐹‘𝑧)) |
23 | 13, 11 | ffvelrnd 6957 |
. . . . . 6
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝐹‘𝑧) ∈ ℕ) |
24 | 23 | nncnd 11987 |
. . . . 5
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝐹‘𝑧) ∈ ℂ) |
25 | 1, 2, 3, 11, 12, 21, 22, 24 | fprodsplitsn 15695 |
. . . 4
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) →
∏𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) = (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) · (𝐹‘𝑧))) |
26 | 25 | ad2ant2r 744 |
. . 3
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾))) → ∏𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) = (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) · (𝐹‘𝑧))) |
27 | | simprl 768 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑦 ∈ Fin) |
28 | | simprr 770 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → 𝐹:ℕ⟶ℕ) |
29 | 28 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝐹:ℕ⟶ℕ) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(𝑦 ∈ Fin ∧ ¬
𝑧 ∈ 𝑦)) ∧ 𝑚 ∈ 𝑦) → 𝐹:ℕ⟶ℕ) |
31 | 17 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑦 ⊆ ℕ) |
32 | 31 | sselda 3926 |
. . . . . . . . . . . . 13
⊢
(((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(𝑦 ∈ Fin ∧ ¬
𝑧 ∈ 𝑦)) ∧ 𝑚 ∈ 𝑦) → 𝑚 ∈ ℕ) |
33 | 30, 32 | ffvelrnd 6957 |
. . . . . . . . . . . 12
⊢
(((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(𝑦 ∈ Fin ∧ ¬
𝑧 ∈ 𝑦)) ∧ 𝑚 ∈ 𝑦) → (𝐹‘𝑚) ∈ ℕ) |
34 | 27, 33 | fprodnncl 15661 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∈ ℕ) |
35 | 34 | ex 413 |
. . . . . . . . . 10
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∈ ℕ)) |
36 | 35 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾)) → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∈ ℕ)) |
37 | 36 | com12 32 |
. . . . . . . 8
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∈ ℕ)) |
38 | 37 | adantr 481 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∈ ℕ)) |
39 | 38 | imp 407 |
. . . . . 6
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾))) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∈ ℕ) |
40 | 39 | nnzd 12422 |
. . . . 5
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾))) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∈ ℤ) |
41 | 28, 10 | ffvelrnd 6957 |
. . . . . . . 8
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → (𝐹‘𝑧) ∈ ℕ) |
42 | 41 | nnzd 12422 |
. . . . . . 7
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → (𝐹‘𝑧) ∈ ℤ) |
43 | 42 | adantr 481 |
. . . . . 6
⊢ ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾)) → (𝐹‘𝑧) ∈ ℤ) |
44 | 43 | adantl 482 |
. . . . 5
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾))) → (𝐹‘𝑧) ∈ ℤ) |
45 | | nnz 12340 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℤ) |
46 | 45 | adantr 481 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ) →
𝐾 ∈
ℤ) |
47 | 46 | adantl 482 |
. . . . . . 7
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → 𝐾 ∈
ℤ) |
48 | 47 | adantr 481 |
. . . . . 6
⊢ ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾)) → 𝐾 ∈ ℤ) |
49 | 48 | adantl 482 |
. . . . 5
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾))) → 𝐾 ∈ ℤ) |
50 | 40, 44, 49 | 3jca 1127 |
. . . 4
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾))) → (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∈ ℤ ∧ (𝐹‘𝑧) ∈ ℤ ∧ 𝐾 ∈ ℤ)) |
51 | | simpl 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:ℕ⟶ℕ ∧
(𝑦 ∪ {𝑧}) ⊆ ℕ) → 𝐹:ℕ⟶ℕ) |
52 | 9 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:ℕ⟶ℕ ∧
(𝑦 ∪ {𝑧}) ⊆ ℕ) → 𝑧 ∈
ℕ) |
53 | 51, 52 | ffvelrnd 6957 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:ℕ⟶ℕ ∧
(𝑦 ∪ {𝑧}) ⊆ ℕ) →
(𝐹‘𝑧) ∈ ℕ) |
54 | 53 | ex 413 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:ℕ⟶ℕ →
((𝑦 ∪ {𝑧}) ⊆ ℕ → (𝐹‘𝑧) ∈ ℕ)) |
55 | 54 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ) →
((𝑦 ∪ {𝑧}) ⊆ ℕ → (𝐹‘𝑧) ∈ ℕ)) |
56 | 55 | impcom 408 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → (𝐹‘𝑧) ∈ ℕ) |
57 | 56 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝐹‘𝑧) ∈ ℕ) |
58 | 3, 18, 57 | 3jca 1127 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ (𝐹‘𝑧) ∈ ℕ)) |
59 | 58 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧
∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) → (𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ (𝐹‘𝑧) ∈ ℕ)) |
60 | 13 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧
∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) → 𝐹:ℕ⟶ℕ) |
61 | | vsnid 4604 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ {𝑧} |
62 | 61 | olci 863 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑦 ∨ 𝑧 ∈ {𝑧}) |
63 | | elun 4088 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑧 ∈ 𝑦 ∨ 𝑧 ∈ {𝑧})) |
64 | 62, 63 | mpbir 230 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ (𝑦 ∪ {𝑧}) |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚 ∈ 𝑦) → 𝑧 ∈ (𝑦 ∪ {𝑧})) |
66 | | snssi 4747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ 𝑦 → {𝑚} ⊆ 𝑦) |
67 | 66 | ssneld 3928 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ 𝑦 → (¬ 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ {𝑚})) |
68 | 67 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ 𝑦 → (𝑚 ∈ 𝑦 → ¬ 𝑧 ∈ {𝑚})) |
69 | 68 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝑚 ∈ 𝑦 → ¬ 𝑧 ∈ {𝑚})) |
70 | 69 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝑚 ∈ 𝑦 → ¬ 𝑧 ∈ {𝑚})) |
71 | 70 | imp 407 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚 ∈ 𝑦) → ¬ 𝑧 ∈ {𝑚}) |
72 | 65, 71 | eldifd 3903 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚 ∈ 𝑦) → 𝑧 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})) |
73 | | fveq2 6769 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑧 → (𝐹‘𝑛) = (𝐹‘𝑧)) |
74 | 73 | oveq2d 7285 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑧 → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = ((𝐹‘𝑚) gcd (𝐹‘𝑧))) |
75 | 74 | eqeq1d 2742 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑧 → (((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ↔ ((𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1)) |
76 | 75 | rspcv 3556 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚}) → (∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 → ((𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1)) |
77 | 72, 76 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚 ∈ 𝑦) → (∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 → ((𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1)) |
78 | 77 | ralimdva 3105 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) →
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 → ∀𝑚 ∈ 𝑦 ((𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1)) |
79 | | ralunb 4130 |
. . . . . . . . . . . 12
⊢
(∀𝑚 ∈
(𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ↔ (∀𝑚 ∈ 𝑦 ∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ {𝑧}∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1)) |
80 | 79 | simplbi 498 |
. . . . . . . . . . 11
⊢
(∀𝑚 ∈
(𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 → ∀𝑚 ∈ 𝑦 ∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) |
81 | 78, 80 | impel 506 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧
∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) → ∀𝑚 ∈ 𝑦 ((𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1) |
82 | | raldifb 4084 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
(𝑦 ∪ {𝑧})(𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) ↔ ∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) |
83 | | ralunb 4130 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
(𝑦 ∪ {𝑧})(𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) ↔ (∀𝑛 ∈ 𝑦 (𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) ∧ ∀𝑛 ∈ {𝑧} (𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1))) |
84 | | raldifb 4084 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
𝑦 (𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) ↔ ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) |
85 | 84 | biimpi 215 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑛 ∈
𝑦 (𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) → ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) |
86 | 85 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑛 ∈
𝑦 (𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) ∧ ∀𝑛 ∈ {𝑧} (𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1)) → ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) |
87 | 83, 86 | sylbi 216 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
(𝑦 ∪ {𝑧})(𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) → ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) |
88 | 82, 87 | sylbir 234 |
. . . . . . . . . . . . . 14
⊢
(∀𝑛 ∈
((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 → ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) |
89 | 88 | ralimi 3089 |
. . . . . . . . . . . . 13
⊢
(∀𝑚 ∈
𝑦 ∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 → ∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) |
90 | 89 | adantr 481 |
. . . . . . . . . . . 12
⊢
((∀𝑚 ∈
𝑦 ∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ {𝑧}∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) → ∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) |
91 | 79, 90 | sylbi 216 |
. . . . . . . . . . 11
⊢
(∀𝑚 ∈
(𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 → ∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) |
92 | 91 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧
∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) → ∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) |
93 | | coprmprod 16362 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ (𝐹‘𝑧) ∈ ℕ) ∧ 𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ 𝑦 ((𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1) → (∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 → (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1)) |
94 | 93 | imp 407 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ (𝐹‘𝑧) ∈ ℕ) ∧ 𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ 𝑦 ((𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1) ∧ ∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) → (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1) |
95 | 59, 60, 81, 92, 94 | syl31anc 1372 |
. . . . . . . . 9
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧
∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) → (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1) |
96 | 95 | ex 413 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) →
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 → (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1)) |
97 | 96 | adantrd 492 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) →
((∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾) → (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1)) |
98 | 97 | expimpd 454 |
. . . . . 6
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾)) → (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1)) |
99 | 98 | adantr 481 |
. . . . 5
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾)) → (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1)) |
100 | 99 | imp 407 |
. . . 4
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾))) → (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1) |
101 | 83 | simplbi 498 |
. . . . . . . . . 10
⊢
(∀𝑛 ∈
(𝑦 ∪ {𝑧})(𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) → ∀𝑛 ∈ 𝑦 (𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1)) |
102 | 82, 101 | sylbir 234 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 → ∀𝑛 ∈ 𝑦 (𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1)) |
103 | 102 | ralimi 3089 |
. . . . . . . 8
⊢
(∀𝑚 ∈
𝑦 ∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 → ∀𝑚 ∈ 𝑦 ∀𝑛 ∈ 𝑦 (𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1)) |
104 | 103 | adantr 481 |
. . . . . . 7
⊢
((∀𝑚 ∈
𝑦 ∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ {𝑧}∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) → ∀𝑚 ∈ 𝑦 ∀𝑛 ∈ 𝑦 (𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1)) |
105 | 79, 104 | sylbi 216 |
. . . . . 6
⊢
(∀𝑚 ∈
(𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 → ∀𝑚 ∈ 𝑦 ∀𝑛 ∈ 𝑦 (𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1)) |
106 | | ralunb 4130 |
. . . . . . 7
⊢
(∀𝑚 ∈
(𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾 ↔ (∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾 ∧ ∀𝑚 ∈ {𝑧} (𝐹‘𝑚) ∥ 𝐾)) |
107 | 106 | simplbi 498 |
. . . . . 6
⊢
(∀𝑚 ∈
(𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾 → ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾) |
108 | 84 | ralbii 3093 |
. . . . . . . 8
⊢
(∀𝑚 ∈
𝑦 ∀𝑛 ∈ 𝑦 (𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) ↔ ∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) |
109 | 108 | anbi1i 624 |
. . . . . . 7
⊢
((∀𝑚 ∈
𝑦 ∀𝑛 ∈ 𝑦 (𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾) ↔ (∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) |
110 | 17 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝑦 ⊆
ℕ) |
111 | | simprrl 778 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝐾 ∈
ℕ) |
112 | | simprrr 779 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝐹:ℕ⟶ℕ) |
113 | 110, 111,
112 | jca32 516 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) |
114 | | simplr 766 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) →
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) |
115 | | pm2.27 42 |
. . . . . . . . . . . 12
⊢ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) |
116 | 113, 114,
115 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) |
117 | 116 | exp31 420 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾) → (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)))) |
118 | 117 | com24 95 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾) → (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) →
((∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)))) |
119 | 118 | imp 407 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) →
((∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾))) |
120 | 119 | imp 407 |
. . . . . . 7
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) →
((∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) |
121 | 109, 120 | syl5bi 241 |
. . . . . 6
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) →
((∀𝑚 ∈ 𝑦 ∀𝑛 ∈ 𝑦 (𝑛 ∉ {𝑚} → ((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1) ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) |
122 | 105, 107,
121 | syl2ani 607 |
. . . . 5
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) →
((∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) |
123 | 122 | impr 455 |
. . . 4
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾))) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾) |
124 | 22 | breq1d 5089 |
. . . . . . . . 9
⊢ (𝑚 = 𝑧 → ((𝐹‘𝑚) ∥ 𝐾 ↔ (𝐹‘𝑧) ∥ 𝐾)) |
125 | 124 | rspcv 3556 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝑦 ∪ {𝑧}) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾 → (𝐹‘𝑧) ∥ 𝐾)) |
126 | 64, 125 | ax-mp 5 |
. . . . . . 7
⊢
(∀𝑚 ∈
(𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾 → (𝐹‘𝑧) ∥ 𝐾) |
127 | 126 | adantl 482 |
. . . . . 6
⊢
((∀𝑚 ∈
(𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾) → (𝐹‘𝑧) ∥ 𝐾) |
128 | 127 | adantl 482 |
. . . . 5
⊢ ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾)) → (𝐹‘𝑧) ∥ 𝐾) |
129 | 128 | adantl 482 |
. . . 4
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾))) → (𝐹‘𝑧) ∥ 𝐾) |
130 | | coprmdvds2 16355 |
. . . . 5
⊢
(((∏𝑚 ∈
𝑦 (𝐹‘𝑚) ∈ ℤ ∧ (𝐹‘𝑧) ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1) → ((∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾 ∧ (𝐹‘𝑧) ∥ 𝐾) → (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) · (𝐹‘𝑧)) ∥ 𝐾)) |
131 | 130 | imp 407 |
. . . 4
⊢
((((∏𝑚 ∈
𝑦 (𝐹‘𝑚) ∈ ℤ ∧ (𝐹‘𝑧) ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) gcd (𝐹‘𝑧)) = 1) ∧ (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾 ∧ (𝐹‘𝑧) ∥ 𝐾)) → (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) · (𝐹‘𝑧)) ∥ 𝐾) |
132 | 50, 100, 123, 129, 131 | syl22anc 836 |
. . 3
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾))) → (∏𝑚 ∈ 𝑦 (𝐹‘𝑚) · (𝐹‘𝑧)) ∥ 𝐾) |
133 | 26, 132 | eqbrtrd 5101 |
. 2
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾))) → ∏𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾) |
134 | 133 | exp31 420 |
1
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧
(∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾))) |