MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  coprmproddvdslem Structured version   Visualization version   GIF version

Theorem coprmproddvdslem 16363
Description: Lemma for coprmproddvds 16364: Induction step. (Contributed by AV, 19-Aug-2020.)
Assertion
Ref Expression
coprmproddvdslem ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → ∏𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)))
Distinct variable groups:   𝑚,𝐹,𝑛   𝑚,𝐾,𝑦,𝑧   𝑦,𝑛,𝑧
Allowed substitution hints:   𝐹(𝑦,𝑧)   𝐾(𝑛)

Proof of Theorem coprmproddvdslem
StepHypRef 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
65snss 4725 . . . . . . . . . 10 (𝑧 ∈ ℕ ↔ {𝑧} ⊆ ℕ)
76biimpri 227 . . . . . . . . 9 ({𝑧} ⊆ ℕ → 𝑧 ∈ ℕ)
87adantl 482 . . . . . . . 8 ((𝑦 ⊆ ℕ ∧ {𝑧} ⊆ ℕ) → 𝑧 ∈ ℕ)
94, 8sylbir 234 . . . . . . 7 ((𝑦 ∪ {𝑧}) ⊆ ℕ → 𝑧 ∈ ℕ)
109adantr 481 . . . . . 6 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → 𝑧 ∈ ℕ)
1110adantl 482 . . . . 5 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝑧 ∈ ℕ)
12 simplr 766 . . . . 5 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ¬ 𝑧𝑦)
13 simprrr 779 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝐹:ℕ⟶ℕ)
1413adantr 481 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → 𝐹:ℕ⟶ℕ)
15 simpl 483 . . . . . . . . . . 11 ((𝑦 ⊆ ℕ ∧ {𝑧} ⊆ ℕ) → 𝑦 ⊆ ℕ)
164, 15sylbir 234 . . . . . . . . . 10 ((𝑦 ∪ {𝑧}) ⊆ ℕ → 𝑦 ⊆ ℕ)
1716adantr 481 . . . . . . . . 9 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → 𝑦 ⊆ ℕ)
1817adantl 482 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝑦 ⊆ ℕ)
1918sselda 3926 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → 𝑚 ∈ ℕ)
2014, 19ffvelrnd 6957 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → (𝐹𝑚) ∈ ℕ)
2120nncnd 11987 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → (𝐹𝑚) ∈ ℂ)
22 fveq2 6769 . . . . 5 (𝑚 = 𝑧 → (𝐹𝑚) = (𝐹𝑧))
2313, 11ffvelrnd 6957 . . . . . 6 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝐹𝑧) ∈ ℕ)
2423nncnd 11987 . . . . 5 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝐹𝑧) ∈ ℂ)
251, 2, 3, 11, 12, 21, 22, 24fprodsplitsn 15695 . . . 4 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ∏𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) = (∏𝑚𝑦 (𝐹𝑚) · (𝐹𝑧)))
2625ad2ant2r 744 . . 3 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → ∏𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) = (∏𝑚𝑦 (𝐹𝑚) · (𝐹𝑧)))
27 simprl 768 . . . . . . . . . . . 12 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝑦 ∈ Fin)
28 simprr 770 . . . . . . . . . . . . . . 15 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → 𝐹:ℕ⟶ℕ)
2928adantr 481 . . . . . . . . . . . . . 14 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝐹:ℕ⟶ℕ)
3029adantr 481 . . . . . . . . . . . . 13 (((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ 𝑚𝑦) → 𝐹:ℕ⟶ℕ)
3117adantr 481 . . . . . . . . . . . . . 14 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝑦 ⊆ ℕ)
3231sselda 3926 . . . . . . . . . . . . 13 (((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ 𝑚𝑦) → 𝑚 ∈ ℕ)
3330, 32ffvelrnd 6957 . . . . . . . . . . . 12 (((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ 𝑚𝑦) → (𝐹𝑚) ∈ ℕ)
3427, 33fprodnncl 15661 . . . . . . . . . . 11 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ∏𝑚𝑦 (𝐹𝑚) ∈ ℕ)
3534ex 413 . . . . . . . . . 10 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ∏𝑚𝑦 (𝐹𝑚) ∈ ℕ))
3635adantr 481 . . . . . . . . 9 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ∏𝑚𝑦 (𝐹𝑚) ∈ ℕ))
3736com12 32 . . . . . . . 8 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∈ ℕ))
3837adantr 481 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∈ ℕ))
3938imp 407 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → ∏𝑚𝑦 (𝐹𝑚) ∈ ℕ)
4039nnzd 12422 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → ∏𝑚𝑦 (𝐹𝑚) ∈ ℤ)
4128, 10ffvelrnd 6957 . . . . . . . 8 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → (𝐹𝑧) ∈ ℕ)
4241nnzd 12422 . . . . . . 7 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → (𝐹𝑧) ∈ ℤ)
4342adantr 481 . . . . . 6 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → (𝐹𝑧) ∈ ℤ)
4443adantl 482 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → (𝐹𝑧) ∈ ℤ)
45 nnz 12340 . . . . . . . . 9 (𝐾 ∈ ℕ → 𝐾 ∈ ℤ)
4645adantr 481 . . . . . . . 8 ((𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ) → 𝐾 ∈ ℤ)
4746adantl 482 . . . . . . 7 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → 𝐾 ∈ ℤ)
4847adantr 481 . . . . . 6 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → 𝐾 ∈ ℤ)
4948adantl 482 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → 𝐾 ∈ ℤ)
5040, 44, 493jca 1127 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → (∏𝑚𝑦 (𝐹𝑚) ∈ ℤ ∧ (𝐹𝑧) ∈ ℤ ∧ 𝐾 ∈ ℤ))
51 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝐹:ℕ⟶ℕ ∧ (𝑦 ∪ {𝑧}) ⊆ ℕ) → 𝐹:ℕ⟶ℕ)
529adantl 482 . . . . . . . . . . . . . . . . 17 ((𝐹:ℕ⟶ℕ ∧ (𝑦 ∪ {𝑧}) ⊆ ℕ) → 𝑧 ∈ ℕ)
5351, 52ffvelrnd 6957 . . . . . . . . . . . . . . . 16 ((𝐹:ℕ⟶ℕ ∧ (𝑦 ∪ {𝑧}) ⊆ ℕ) → (𝐹𝑧) ∈ ℕ)
5453ex 413 . . . . . . . . . . . . . . 15 (𝐹:ℕ⟶ℕ → ((𝑦 ∪ {𝑧}) ⊆ ℕ → (𝐹𝑧) ∈ ℕ))
5554adantl 482 . . . . . . . . . . . . . 14 ((𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ) → ((𝑦 ∪ {𝑧}) ⊆ ℕ → (𝐹𝑧) ∈ ℕ))
5655impcom 408 . . . . . . . . . . . . 13 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → (𝐹𝑧) ∈ ℕ)
5756adantl 482 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝐹𝑧) ∈ ℕ)
583, 18, 573jca 1127 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ (𝐹𝑧) ∈ ℕ))
5958adantr 481 . . . . . . . . . 10 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → (𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ (𝐹𝑧) ∈ ℕ))
6013adantr 481 . . . . . . . . . 10 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → 𝐹:ℕ⟶ℕ)
61 vsnid 4604 . . . . . . . . . . . . . . . . 17 𝑧 ∈ {𝑧}
6261olci 863 . . . . . . . . . . . . . . . 16 (𝑧𝑦𝑧 ∈ {𝑧})
63 elun 4088 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑧𝑦𝑧 ∈ {𝑧}))
6462, 63mpbir 230 . . . . . . . . . . . . . . 15 𝑧 ∈ (𝑦 ∪ {𝑧})
6564a1i 11 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → 𝑧 ∈ (𝑦 ∪ {𝑧}))
66 snssi 4747 . . . . . . . . . . . . . . . . . . 19 (𝑚𝑦 → {𝑚} ⊆ 𝑦)
6766ssneld 3928 . . . . . . . . . . . . . . . . . 18 (𝑚𝑦 → (¬ 𝑧𝑦 → ¬ 𝑧 ∈ {𝑚}))
6867com12 32 . . . . . . . . . . . . . . . . 17 𝑧𝑦 → (𝑚𝑦 → ¬ 𝑧 ∈ {𝑚}))
6968adantl 482 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝑚𝑦 → ¬ 𝑧 ∈ {𝑚}))
7069adantr 481 . . . . . . . . . . . . . . 15 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝑚𝑦 → ¬ 𝑧 ∈ {𝑚}))
7170imp 407 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → ¬ 𝑧 ∈ {𝑚})
7265, 71eldifd 3903 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → 𝑧 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚}))
73 fveq2 6769 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑧 → (𝐹𝑛) = (𝐹𝑧))
7473oveq2d 7285 . . . . . . . . . . . . . . 15 (𝑛 = 𝑧 → ((𝐹𝑚) gcd (𝐹𝑛)) = ((𝐹𝑚) gcd (𝐹𝑧)))
7574eqeq1d 2742 . . . . . . . . . . . . . 14 (𝑛 = 𝑧 → (((𝐹𝑚) gcd (𝐹𝑛)) = 1 ↔ ((𝐹𝑚) gcd (𝐹𝑧)) = 1))
7675rspcv 3556 . . . . . . . . . . . . 13 (𝑧 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚}) → (∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ((𝐹𝑚) gcd (𝐹𝑧)) = 1))
7772, 76syl 17 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → (∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ((𝐹𝑚) gcd (𝐹𝑧)) = 1))
7877ralimdva 3105 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (∀𝑚𝑦𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑚𝑦 ((𝐹𝑚) gcd (𝐹𝑧)) = 1))
79 ralunb 4130 . . . . . . . . . . . 12 (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ↔ (∀𝑚𝑦𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ {𝑧}∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1))
8079simplbi 498 . . . . . . . . . . 11 (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑚𝑦𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
8178, 80impel 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)
8584biimpi 215 . . . . . . . . . . . . . . . . 17 (∀𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) → ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
8685adantr 481 . . . . . . . . . . . . . . . 16 ((∀𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) ∧ ∀𝑛 ∈ {𝑧} (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1)) → ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
8783, 86sylbi 216 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ (𝑦 ∪ {𝑧})(𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) → ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
8882, 87sylbir 234 . . . . . . . . . . . . . 14 (∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
8988ralimi 3089 . . . . . . . . . . . . 13 (∀𝑚𝑦𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
9089adantr 481 . . . . . . . . . . . 12 ((∀𝑚𝑦𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ {𝑧}∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → ∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
9179, 90sylbi 216 . . . . . . . . . . 11 (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
9291adantl 482 . . . . . . . . . 10 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → ∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
93 coprmprod 16362 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ (𝐹𝑧) ∈ ℕ) ∧ 𝐹:ℕ⟶ℕ ∧ ∀𝑚𝑦 ((𝐹𝑚) gcd (𝐹𝑧)) = 1) → (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1))
9493imp 407 . . . . . . . . . 10 ((((𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ (𝐹𝑧) ∈ ℕ) ∧ 𝐹:ℕ⟶ℕ ∧ ∀𝑚𝑦 ((𝐹𝑚) gcd (𝐹𝑧)) = 1) ∧ ∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1)
9559, 60, 81, 92, 94syl31anc 1372 . . . . . . . . 9 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1)
9695ex 413 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1))
9796adantrd 492 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ((∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾) → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1))
9897expimpd 454 . . . . . 6 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1))
9998adantr 481 . . . . 5 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1))
10099imp 407 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1)
10183simplbi 498 . . . . . . . . . 10 (∀𝑛 ∈ (𝑦 ∪ {𝑧})(𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) → ∀𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1))
10282, 101sylbir 234 . . . . . . . . 9 (∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1))
103102ralimi 3089 . . . . . . . 8 (∀𝑚𝑦𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑚𝑦𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1))
104103adantr 481 . . . . . . 7 ((∀𝑚𝑦𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ {𝑧}∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → ∀𝑚𝑦𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1))
10579, 104sylbi 216 . . . . . 6 (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑚𝑦𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1))
106 ralunb 4130 . . . . . . 7 (∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾 ↔ (∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾 ∧ ∀𝑚 ∈ {𝑧} (𝐹𝑚) ∥ 𝐾))
107106simplbi 498 . . . . . 6 (∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾 → ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)
10884ralbii 3093 . . . . . . . 8 (∀𝑚𝑦𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) ↔ ∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
109108anbi1i 624 . . . . . . 7 ((∀𝑚𝑦𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾) ↔ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾))
11017adantl 482 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝑦 ⊆ ℕ)
111 simprrl 778 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝐾 ∈ ℕ)
112 simprrr 779 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝐹:ℕ⟶ℕ)
113110, 111, 112jca32 516 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)))
114 simplr 766 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾))
115 pm2.27 42 . . . . . . . . . . . 12 (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾))
116113, 114, 115syl2anc 584 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾))
117116exp31 420 . . . . . . . . . 10 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾))))
118117com24 95 . . . . . . . . 9 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → ((∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾))))
119118imp 407 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → ((∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)))
120119imp 407 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ((∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾))
121109, 120syl5bi 241 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ((∀𝑚𝑦𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾))
122105, 107, 121syl2ani 607 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ((∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾))
123122impr 455 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)
12422breq1d 5089 . . . . . . . . 9 (𝑚 = 𝑧 → ((𝐹𝑚) ∥ 𝐾 ↔ (𝐹𝑧) ∥ 𝐾))
125124rspcv 3556 . . . . . . . 8 (𝑧 ∈ (𝑦 ∪ {𝑧}) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾 → (𝐹𝑧) ∥ 𝐾))
12664, 125ax-mp 5 . . . . . . 7 (∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾 → (𝐹𝑧) ∥ 𝐾)
127126adantl 482 . . . . . 6 ((∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾) → (𝐹𝑧) ∥ 𝐾)
128127adantl 482 . . . . 5 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → (𝐹𝑧) ∥ 𝐾)
129128adantl 482 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → (𝐹𝑧) ∥ 𝐾)
130 coprmdvds2 16355 . . . . 5 (((∏𝑚𝑦 (𝐹𝑚) ∈ ℤ ∧ (𝐹𝑧) ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1) → ((∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾 ∧ (𝐹𝑧) ∥ 𝐾) → (∏𝑚𝑦 (𝐹𝑚) · (𝐹𝑧)) ∥ 𝐾))
131130imp 407 . . . 4 ((((∏𝑚𝑦 (𝐹𝑚) ∈ ℤ ∧ (𝐹𝑧) ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1) ∧ (∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾 ∧ (𝐹𝑧) ∥ 𝐾)) → (∏𝑚𝑦 (𝐹𝑚) · (𝐹𝑧)) ∥ 𝐾)
13250, 100, 123, 129, 131syl22anc 836 . . 3 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → (∏𝑚𝑦 (𝐹𝑚) · (𝐹𝑧)) ∥ 𝐾)
13326, 132eqbrtrd 5101 . 2 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → ∏𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)
134133exp31 420 1 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → ∏𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 844  w3a 1086   = wceq 1542  wcel 2110  wnel 3051  wral 3066  cdif 3889  cun 3890  wss 3892  {csn 4567   class class class wbr 5079  wf 6427  cfv 6431  (class class class)co 7269  Fincfn 8714  1c1 10871   · cmul 10875  cn 11971  cz 12317  cprod 15611  cdvds 15959   gcd cgcd 16197
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580  ax-inf2 9375  ax-cnex 10926  ax-resscn 10927  ax-1cn 10928  ax-icn 10929  ax-addcl 10930  ax-addrcl 10931  ax-mulcl 10932  ax-mulrcl 10933  ax-mulcom 10934  ax-addass 10935  ax-mulass 10936  ax-distr 10937  ax-i2m1 10938  ax-1ne0 10939  ax-1rid 10940  ax-rnegex 10941  ax-rrecex 10942  ax-cnre 10943  ax-pre-lttri 10944  ax-pre-lttrn 10945  ax-pre-ltadd 10946  ax-pre-mulgt0 10947  ax-pre-sup 10948
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-int 4886  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6200  df-ord 6267  df-on 6268  df-lim 6269  df-suc 6270  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-f1 6436  df-fo 6437  df-f1o 6438  df-fv 6439  df-isom 6440  df-riota 7226  df-ov 7272  df-oprab 7273  df-mpo 7274  df-om 7705  df-1st 7822  df-2nd 7823  df-frecs 8086  df-wrecs 8117  df-recs 8191  df-rdg 8230  df-1o 8286  df-er 8479  df-en 8715  df-dom 8716  df-sdom 8717  df-fin 8718  df-sup 9177  df-inf 9178  df-oi 9245  df-card 9696  df-pnf 11010  df-mnf 11011  df-xr 11012  df-ltxr 11013  df-le 11014  df-sub 11205  df-neg 11206  df-div 11631  df-nn 11972  df-2 12034  df-3 12035  df-n0 12232  df-z 12318  df-uz 12580  df-rp 12728  df-fz 13237  df-fzo 13380  df-fl 13508  df-mod 13586  df-seq 13718  df-exp 13779  df-hash 14041  df-cj 14806  df-re 14807  df-im 14808  df-sqrt 14942  df-abs 14943  df-clim 15193  df-prod 15612  df-dvds 15960  df-gcd 16198
This theorem is referenced by:  coprmproddvds  16364
  Copyright terms: Public domain W3C validator