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

Theorem coprmproddvdslem 15423
Description: Lemma for coprmproddvds 15424: 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 1883 . . . . 5 𝑚((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)))
2 nfcv 2793 . . . . 5 𝑚(𝐹𝑧)
3 simpll 805 . . . . 5 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝑦 ∈ Fin)
4 unss 3820 . . . . . . . 8 ((𝑦 ⊆ ℕ ∧ {𝑧} ⊆ ℕ) ↔ (𝑦 ∪ {𝑧}) ⊆ ℕ)
5 vex 3234 . . . . . . . . . . 11 𝑧 ∈ V
65snss 4348 . . . . . . . . . 10 (𝑧 ∈ ℕ ↔ {𝑧} ⊆ ℕ)
76biimpri 218 . . . . . . . . 9 ({𝑧} ⊆ ℕ → 𝑧 ∈ ℕ)
87adantl 481 . . . . . . . 8 ((𝑦 ⊆ ℕ ∧ {𝑧} ⊆ ℕ) → 𝑧 ∈ ℕ)
94, 8sylbir 225 . . . . . . 7 ((𝑦 ∪ {𝑧}) ⊆ ℕ → 𝑧 ∈ ℕ)
109adantr 480 . . . . . 6 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → 𝑧 ∈ ℕ)
1110adantl 481 . . . . 5 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝑧 ∈ ℕ)
12 simplr 807 . . . . 5 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ¬ 𝑧𝑦)
13 simprrr 822 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝐹:ℕ⟶ℕ)
1413adantr 480 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → 𝐹:ℕ⟶ℕ)
15 simpl 472 . . . . . . . . . . 11 ((𝑦 ⊆ ℕ ∧ {𝑧} ⊆ ℕ) → 𝑦 ⊆ ℕ)
164, 15sylbir 225 . . . . . . . . . 10 ((𝑦 ∪ {𝑧}) ⊆ ℕ → 𝑦 ⊆ ℕ)
1716adantr 480 . . . . . . . . 9 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → 𝑦 ⊆ ℕ)
1817adantl 481 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝑦 ⊆ ℕ)
1918sselda 3636 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → 𝑚 ∈ ℕ)
2014, 19ffvelrnd 6400 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → (𝐹𝑚) ∈ ℕ)
2120nncnd 11074 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → (𝐹𝑚) ∈ ℂ)
22 fveq2 6229 . . . . 5 (𝑚 = 𝑧 → (𝐹𝑚) = (𝐹𝑧))
2313, 11ffvelrnd 6400 . . . . . 6 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝐹𝑧) ∈ ℕ)
2423nncnd 11074 . . . . 5 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝐹𝑧) ∈ ℂ)
251, 2, 3, 11, 12, 21, 22, 24fprodsplitsn 14764 . . . 4 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ∏𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) = (∏𝑚𝑦 (𝐹𝑚) · (𝐹𝑧)))
2625ad2ant2r 798 . . 3 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → ∏𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) = (∏𝑚𝑦 (𝐹𝑚) · (𝐹𝑧)))
27 simprl 809 . . . . . . . . . . . 12 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝑦 ∈ Fin)
28 simprr 811 . . . . . . . . . . . . . . 15 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → 𝐹:ℕ⟶ℕ)
2928adantr 480 . . . . . . . . . . . . . 14 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝐹:ℕ⟶ℕ)
3029adantr 480 . . . . . . . . . . . . 13 (((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ 𝑚𝑦) → 𝐹:ℕ⟶ℕ)
3117adantr 480 . . . . . . . . . . . . . 14 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝑦 ⊆ ℕ)
3231sselda 3636 . . . . . . . . . . . . 13 (((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ 𝑚𝑦) → 𝑚 ∈ ℕ)
3330, 32ffvelrnd 6400 . . . . . . . . . . . 12 (((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ 𝑚𝑦) → (𝐹𝑚) ∈ ℕ)
3427, 33fprodnncl 14729 . . . . . . . . . . 11 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ∏𝑚𝑦 (𝐹𝑚) ∈ ℕ)
3534ex 449 . . . . . . . . . 10 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ∏𝑚𝑦 (𝐹𝑚) ∈ ℕ))
3635adantr 480 . . . . . . . . 9 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ∏𝑚𝑦 (𝐹𝑚) ∈ ℕ))
3736com12 32 . . . . . . . 8 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∈ ℕ))
3837adantr 480 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∈ ℕ))
3938imp 444 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → ∏𝑚𝑦 (𝐹𝑚) ∈ ℕ)
4039nnzd 11519 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → ∏𝑚𝑦 (𝐹𝑚) ∈ ℤ)
4128, 10ffvelrnd 6400 . . . . . . . 8 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → (𝐹𝑧) ∈ ℕ)
4241nnzd 11519 . . . . . . 7 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → (𝐹𝑧) ∈ ℤ)
4342adantr 480 . . . . . 6 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → (𝐹𝑧) ∈ ℤ)
4443adantl 481 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → (𝐹𝑧) ∈ ℤ)
45 nnz 11437 . . . . . . . . 9 (𝐾 ∈ ℕ → 𝐾 ∈ ℤ)
4645adantr 480 . . . . . . . 8 ((𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ) → 𝐾 ∈ ℤ)
4746adantl 481 . . . . . . 7 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → 𝐾 ∈ ℤ)
4847adantr 480 . . . . . 6 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → 𝐾 ∈ ℤ)
4948adantl 481 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → 𝐾 ∈ ℤ)
5040, 44, 493jca 1261 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → (∏𝑚𝑦 (𝐹𝑚) ∈ ℤ ∧ (𝐹𝑧) ∈ ℤ ∧ 𝐾 ∈ ℤ))
51 simpl 472 . . . . . . . . . . . . . . . . 17 ((𝐹:ℕ⟶ℕ ∧ (𝑦 ∪ {𝑧}) ⊆ ℕ) → 𝐹:ℕ⟶ℕ)
529adantl 481 . . . . . . . . . . . . . . . . 17 ((𝐹:ℕ⟶ℕ ∧ (𝑦 ∪ {𝑧}) ⊆ ℕ) → 𝑧 ∈ ℕ)
5351, 52ffvelrnd 6400 . . . . . . . . . . . . . . . 16 ((𝐹:ℕ⟶ℕ ∧ (𝑦 ∪ {𝑧}) ⊆ ℕ) → (𝐹𝑧) ∈ ℕ)
5453ex 449 . . . . . . . . . . . . . . 15 (𝐹:ℕ⟶ℕ → ((𝑦 ∪ {𝑧}) ⊆ ℕ → (𝐹𝑧) ∈ ℕ))
5554adantl 481 . . . . . . . . . . . . . 14 ((𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ) → ((𝑦 ∪ {𝑧}) ⊆ ℕ → (𝐹𝑧) ∈ ℕ))
5655impcom 445 . . . . . . . . . . . . 13 (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → (𝐹𝑧) ∈ ℕ)
5756adantl 481 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝐹𝑧) ∈ ℕ)
583, 18, 573jca 1261 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ (𝐹𝑧) ∈ ℕ))
5958adantr 480 . . . . . . . . . 10 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → (𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ (𝐹𝑧) ∈ ℕ))
6013adantr 480 . . . . . . . . . 10 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → 𝐹:ℕ⟶ℕ)
61 ralunb 3827 . . . . . . . . . . . . 13 (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ↔ (∀𝑚𝑦𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ {𝑧}∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1))
6261simplbi 475 . . . . . . . . . . . 12 (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑚𝑦𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
63 vsnid 4242 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ {𝑧}
6463olci 405 . . . . . . . . . . . . . . . . 17 (𝑧𝑦𝑧 ∈ {𝑧})
65 elun 3786 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑧𝑦𝑧 ∈ {𝑧}))
6664, 65mpbir 221 . . . . . . . . . . . . . . . 16 𝑧 ∈ (𝑦 ∪ {𝑧})
6766a1i 11 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → 𝑧 ∈ (𝑦 ∪ {𝑧}))
68 snssi 4371 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑦 → {𝑚} ⊆ 𝑦)
6968ssneld 3638 . . . . . . . . . . . . . . . . . . 19 (𝑚𝑦 → (¬ 𝑧𝑦 → ¬ 𝑧 ∈ {𝑚}))
7069com12 32 . . . . . . . . . . . . . . . . . 18 𝑧𝑦 → (𝑚𝑦 → ¬ 𝑧 ∈ {𝑚}))
7170adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝑚𝑦 → ¬ 𝑧 ∈ {𝑚}))
7271adantr 480 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝑚𝑦 → ¬ 𝑧 ∈ {𝑚}))
7372imp 444 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → ¬ 𝑧 ∈ {𝑚})
7467, 73eldifd 3618 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → 𝑧 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚}))
75 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑧 → (𝐹𝑛) = (𝐹𝑧))
7675oveq2d 6706 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑧 → ((𝐹𝑚) gcd (𝐹𝑛)) = ((𝐹𝑚) gcd (𝐹𝑧)))
7776eqeq1d 2653 . . . . . . . . . . . . . . 15 (𝑛 = 𝑧 → (((𝐹𝑚) gcd (𝐹𝑛)) = 1 ↔ ((𝐹𝑚) gcd (𝐹𝑧)) = 1))
7877rspcv 3336 . . . . . . . . . . . . . 14 (𝑧 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚}) → (∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ((𝐹𝑚) gcd (𝐹𝑧)) = 1))
7974, 78syl 17 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ 𝑚𝑦) → (∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ((𝐹𝑚) gcd (𝐹𝑧)) = 1))
8079ralimdva 2991 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (∀𝑚𝑦𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑚𝑦 ((𝐹𝑚) gcd (𝐹𝑧)) = 1))
8162, 80syl5 34 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑚𝑦 ((𝐹𝑚) gcd (𝐹𝑧)) = 1))
8281imp 444 . . . . . . . . . 10 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → ∀𝑚𝑦 ((𝐹𝑚) gcd (𝐹𝑧)) = 1)
83 raldifb 3783 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ (𝑦 ∪ {𝑧})(𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) ↔ ∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
84 ralunb 3827 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝑦 ∪ {𝑧})(𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) ↔ (∀𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) ∧ ∀𝑛 ∈ {𝑧} (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1)))
85 raldifb 3783 . . . . . . . . . . . . . . . . . 18 (∀𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) ↔ ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
8685biimpi 206 . . . . . . . . . . . . . . . . 17 (∀𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) → ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
8786adantr 480 . . . . . . . . . . . . . . . 16 ((∀𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) ∧ ∀𝑛 ∈ {𝑧} (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1)) → ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
8884, 87sylbi 207 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ (𝑦 ∪ {𝑧})(𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) → ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
8983, 88sylbir 225 . . . . . . . . . . . . . 14 (∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
9089ralimi 2981 . . . . . . . . . . . . 13 (∀𝑚𝑦𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
9190adantr 480 . . . . . . . . . . . 12 ((∀𝑚𝑦𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ {𝑧}∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → ∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
9261, 91sylbi 207 . . . . . . . . . . 11 (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
9392adantl 481 . . . . . . . . . 10 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → ∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
94 coprmprod 15422 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ (𝐹𝑧) ∈ ℕ) ∧ 𝐹:ℕ⟶ℕ ∧ ∀𝑚𝑦 ((𝐹𝑚) gcd (𝐹𝑧)) = 1) → (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1))
9594imp 444 . . . . . . . . . 10 ((((𝑦 ∈ Fin ∧ 𝑦 ⊆ ℕ ∧ (𝐹𝑧) ∈ ℕ) ∧ 𝐹:ℕ⟶ℕ ∧ ∀𝑚𝑦 ((𝐹𝑚) gcd (𝐹𝑧)) = 1) ∧ ∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1)
9659, 60, 82, 93, 95syl31anc 1369 . . . . . . . . 9 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1)
9796ex 449 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1))
9897adantrd 483 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ((∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾) → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1))
9998expimpd 628 . . . . . 6 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1))
10099adantr 480 . . . . 5 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1))
101100imp 444 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1)
10284simplbi 475 . . . . . . . . . 10 (∀𝑛 ∈ (𝑦 ∪ {𝑧})(𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) → ∀𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1))
10383, 102sylbir 225 . . . . . . . . 9 (∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1))
104103ralimi 2981 . . . . . . . 8 (∀𝑚𝑦𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑚𝑦𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1))
105104adantr 480 . . . . . . 7 ((∀𝑚𝑦𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ {𝑧}∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1) → ∀𝑚𝑦𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1))
10661, 105sylbi 207 . . . . . 6 (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 → ∀𝑚𝑦𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1))
107 ralunb 3827 . . . . . . 7 (∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾 ↔ (∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾 ∧ ∀𝑚 ∈ {𝑧} (𝐹𝑚) ∥ 𝐾))
108107simplbi 475 . . . . . 6 (∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾 → ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)
10985ralbii 3009 . . . . . . . 8 (∀𝑚𝑦𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) ↔ ∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1)
110109anbi1i 731 . . . . . . 7 ((∀𝑚𝑦𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾) ↔ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾))
11117adantl 481 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝑦 ⊆ ℕ)
112 simprrl 821 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝐾 ∈ ℕ)
113 simprrr 822 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → 𝐹:ℕ⟶ℕ)
114111, 112, 113jca32 557 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)))
115 simplr 807 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾))
116 pm2.27 42 . . . . . . . . . . . 12 (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾))
117114, 115, 116syl2anc 694 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾))
118117exp31 629 . . . . . . . . . 10 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾))))
119118com24 95 . . . . . . . . 9 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → ((∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾))))
120119imp 444 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) → ((∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)))
121120imp 444 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ((∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾))
122110, 121syl5bi 232 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ((∀𝑚𝑦𝑛𝑦 (𝑛 ∉ {𝑚} → ((𝐹𝑚) gcd (𝐹𝑛)) = 1) ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾))
123106, 108, 122syl2ani 689 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ ((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ))) → ((∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾))
124123impr 648 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)
12522breq1d 4695 . . . . . . . . 9 (𝑚 = 𝑧 → ((𝐹𝑚) ∥ 𝐾 ↔ (𝐹𝑧) ∥ 𝐾))
126125rspcv 3336 . . . . . . . 8 (𝑧 ∈ (𝑦 ∪ {𝑧}) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾 → (𝐹𝑧) ∥ 𝐾))
12766, 126ax-mp 5 . . . . . . 7 (∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾 → (𝐹𝑧) ∥ 𝐾)
128127adantl 481 . . . . . 6 ((∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾) → (𝐹𝑧) ∥ 𝐾)
129128adantl 481 . . . . 5 ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → (𝐹𝑧) ∥ 𝐾)
130129adantl 481 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → (𝐹𝑧) ∥ 𝐾)
131 coprmdvds2 15415 . . . . 5 (((∏𝑚𝑦 (𝐹𝑚) ∈ ℤ ∧ (𝐹𝑧) ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1) → ((∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾 ∧ (𝐹𝑧) ∥ 𝐾) → (∏𝑚𝑦 (𝐹𝑚) · (𝐹𝑧)) ∥ 𝐾))
132131imp 444 . . . 4 ((((∏𝑚𝑦 (𝐹𝑚) ∈ ℤ ∧ (𝐹𝑧) ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (∏𝑚𝑦 (𝐹𝑚) gcd (𝐹𝑧)) = 1) ∧ (∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾 ∧ (𝐹𝑧) ∥ 𝐾)) → (∏𝑚𝑦 (𝐹𝑚) · (𝐹𝑧)) ∥ 𝐾)
13350, 101, 124, 130, 132syl22anc 1367 . . 3 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → (∏𝑚𝑦 (𝐹𝑚) · (𝐹𝑧)) ∥ 𝐾)
13426, 133eqbrtrd 4707 . 2 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) ∧ (((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾))) → ∏𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)
135134exp31 629 1 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚𝑦𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚𝑦 (𝐹𝑚) ∥ 𝐾)) → ∏𝑚𝑦 (𝐹𝑚) ∥ 𝐾) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹𝑚) gcd (𝐹𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)) → ∏𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹𝑚) ∥ 𝐾)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382  wa 383  w3a 1054   = wceq 1523  wcel 2030  wnel 2926  wral 2941  cdif 3604  cun 3605  wss 3607  {csn 4210   class class class wbr 4685  wf 5922  cfv 5926  (class class class)co 6690  Fincfn 7997  1c1 9975   · cmul 9979  cn 11058  cz 11415  cprod 14679  cdvds 15027   gcd cgcd 15263
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-prod 14680  df-dvds 15028  df-gcd 15264
This theorem is referenced by:  coprmproddvds  15424
  Copyright terms: Public domain W3C validator