Metamath Proof Explorer

Theorem 2sqlem6

Description: Lemma for 2sq . If a number that is a sum of two squares is divisible by a number whose prime divisors are all sums of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2sqlem6.1 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2sqlem6.2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
2sqlem6.3 ⊢ ( 𝜑 → ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆 ) )
2sqlem6.4 ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ 𝑆 )
Assertion 2sqlem6 ( 𝜑 → 𝐴 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2 2sqlem6.1 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
3 2sqlem6.2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
4 2sqlem6.3 ⊢ ( 𝜑 → ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆 ) )
5 2sqlem6.4 ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ 𝑆 )
6 breq2 ⊢ ( 𝑥 = 1 → ( 𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 1 ) )
7 6 imbi1d ⊢ ( 𝑥 = 1 → ( ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) ↔ ( 𝑝 ∥ 1 → 𝑝 ∈ 𝑆 ) ) )
8 7 ralbidv ⊢ ( 𝑥 = 1 → ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 1 → 𝑝 ∈ 𝑆 ) ) )
9 oveq2 ⊢ ( 𝑥 = 1 → ( 𝑚 · 𝑥 ) = ( 𝑚 · 1 ) )
10 9 eleq1d ⊢ ( 𝑥 = 1 → ( ( 𝑚 · 𝑥 ) ∈ 𝑆 ↔ ( 𝑚 · 1 ) ∈ 𝑆 ) )
11 10 imbi1d ⊢ ( 𝑥 = 1 → ( ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ↔ ( ( 𝑚 · 1 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
12 11 ralbidv ⊢ ( 𝑥 = 1 → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 1 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
13 8 12 imbi12d ⊢ ( 𝑥 = 1 → ( ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ↔ ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 1 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 1 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ) )
14 breq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑦 ) )
15 14 imbi1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) ↔ ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) ) )
16 15 ralbidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) ) )
17 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑚 · 𝑥 ) = ( 𝑚 · 𝑦 ) )
18 17 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑚 · 𝑥 ) ∈ 𝑆 ↔ ( 𝑚 · 𝑦 ) ∈ 𝑆 ) )
19 18 imbi1d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ↔ ( ( 𝑚 · 𝑦 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
20 19 ralbidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑦 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
21 16 20 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ↔ ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑦 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ) )
22 breq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑧 ) )
23 22 imbi1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) ↔ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) ) )
24 23 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) ) )
25 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑚 · 𝑥 ) = ( 𝑚 · 𝑧 ) )
26 25 eleq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑚 · 𝑥 ) ∈ 𝑆 ↔ ( 𝑚 · 𝑧 ) ∈ 𝑆 ) )
27 26 imbi1d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ↔ ( ( 𝑚 · 𝑧 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
28 27 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑧 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
29 24 28 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ↔ ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑧 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ) )
30 breq2 ⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( 𝑝 ∥ 𝑥 ↔ 𝑝 ∥ ( 𝑦 · 𝑧 ) ) )
31 30 imbi1d ⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) ↔ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) )
32 31 ralbidv ⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) )
33 oveq2 ⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( 𝑚 · 𝑥 ) = ( 𝑚 · ( 𝑦 · 𝑧 ) ) )
34 33 eleq1d ⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( ( 𝑚 · 𝑥 ) ∈ 𝑆 ↔ ( 𝑚 · ( 𝑦 · 𝑧 ) ) ∈ 𝑆 ) )
35 34 imbi1d ⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ↔ ( ( 𝑚 · ( 𝑦 · 𝑧 ) ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
36 35 ralbidv ⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑚 · ( 𝑦 · 𝑧 ) ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
37 32 36 imbi12d ⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ↔ ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · ( 𝑦 · 𝑧 ) ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ) )
38 breq2 ⊢ ( 𝑥 = 𝐵 → ( 𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝐵 ) )
39 38 imbi1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) ↔ ( 𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆 ) ) )
40 39 ralbidv ⊢ ( 𝑥 = 𝐵 → ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆 ) ) )
41 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝑚 · 𝑥 ) = ( 𝑚 · 𝐵 ) )
42 41 eleq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑚 · 𝑥 ) ∈ 𝑆 ↔ ( 𝑚 · 𝐵 ) ∈ 𝑆 ) )
43 42 imbi1d ⊢ ( 𝑥 = 𝐵 → ( ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ↔ ( ( 𝑚 · 𝐵 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
44 43 ralbidv ⊢ ( 𝑥 = 𝐵 → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝐵 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
45 40 44 imbi12d ⊢ ( 𝑥 = 𝐵 → ( ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ↔ ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝐵 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ) )
46 nncn ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
47 46 mulridd ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 · 1 ) = 𝑚 )
48 47 eleq1d ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑚 · 1 ) ∈ 𝑆 ↔ 𝑚 ∈ 𝑆 ) )
49 48 biimpd ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑚 · 1 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) )
50 49 rgen ⊢ ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 1 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 )
51 50 a1i ⊢ ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 1 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 1 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) )
52 breq1 ⊢ ( 𝑝 = 𝑥 → ( 𝑝 ∥ 𝑥 ↔ 𝑥 ∥ 𝑥 ) )
53 eleq1 ⊢ ( 𝑝 = 𝑥 → ( 𝑝 ∈ 𝑆 ↔ 𝑥 ∈ 𝑆 ) )
54 52 53 imbi12d ⊢ ( 𝑝 = 𝑥 → ( ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) ↔ ( 𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆 ) ) )
55 54 rspcv ⊢ ( 𝑥 ∈ ℙ → ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) → ( 𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆 ) ) )
56 prmz ⊢ ( 𝑥 ∈ ℙ → 𝑥 ∈ ℤ )
57 iddvds ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∥ 𝑥 )
58 56 57 syl ⊢ ( 𝑥 ∈ ℙ → 𝑥 ∥ 𝑥 )
59 simprl ⊢ ( ( ( 𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑚 · 𝑥 ) ∈ 𝑆 ) ) → 𝑚 ∈ ℕ )
60 simpll ⊢ ( ( ( 𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑚 · 𝑥 ) ∈ 𝑆 ) ) → 𝑥 ∈ ℙ )
61 simprr ⊢ ( ( ( 𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑚 · 𝑥 ) ∈ 𝑆 ) ) → ( 𝑚 · 𝑥 ) ∈ 𝑆 )
62 simplr ⊢ ( ( ( 𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑚 · 𝑥 ) ∈ 𝑆 ) ) → 𝑥 ∈ 𝑆 )
63 1 59 60 61 62 2sqlem5 ⊢ ( ( ( 𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑚 · 𝑥 ) ∈ 𝑆 ) ) → 𝑚 ∈ 𝑆 )
64 63 expr ⊢ ( ( ( 𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) )
65 64 ralrimiva ⊢ ( ( 𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) )
66 65 ex ⊢ ( 𝑥 ∈ ℙ → ( 𝑥 ∈ 𝑆 → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
67 58 66 embantd ⊢ ( 𝑥 ∈ ℙ → ( ( 𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
68 55 67 syld ⊢ ( 𝑥 ∈ ℙ → ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑥 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
69 anim12 ⊢ ( ( ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑦 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ∧ ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑧 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ) → ( ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) ) → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑦 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑧 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ) )
70 simpr ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
71 eluzelz ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) → 𝑦 ∈ ℤ )
72 71 ad2antrr ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑦 ∈ ℤ )
73 eluzelz ⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → 𝑧 ∈ ℤ )
74 73 ad2antlr ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑧 ∈ ℤ )
75 euclemma ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( 𝑝 ∥ ( 𝑦 · 𝑧 ) ↔ ( 𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧 ) ) )
76 70 72 74 75 syl3anc ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 𝑦 · 𝑧 ) ↔ ( 𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧 ) ) )
77 76 imbi1d ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ↔ ( ( 𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧 ) → 𝑝 ∈ 𝑆 ) ) )
78 jaob ⊢ ( ( ( 𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧 ) → 𝑝 ∈ 𝑆 ) ↔ ( ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) ∧ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) ) )
79 77 78 bitrdi ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ↔ ( ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) ∧ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) ) ) )
80 79 ralbidva ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ↔ ∀ 𝑝 ∈ ℙ ( ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) ∧ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) ) ) )
81 r19.26 ⊢ ( ∀ 𝑝 ∈ ℙ ( ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) ∧ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) ) ↔ ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) ) )
82 80 81 bitrdi ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ↔ ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) ) ) )
83 82 biimpa ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) → ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) ) )
84 oveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 · 𝑦 ) = ( 𝑛 · 𝑦 ) )
85 84 eleq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 · 𝑦 ) ∈ 𝑆 ↔ ( 𝑛 · 𝑦 ) ∈ 𝑆 ) )
86 eleq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 ∈ 𝑆 ↔ 𝑛 ∈ 𝑆 ) )
87 85 86 imbi12d ⊢ ( 𝑚 = 𝑛 → ( ( ( 𝑚 · 𝑦 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ↔ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) )
88 87 cbvralvw ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑦 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ↔ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) )
89 46 adantl ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℂ )
90 uzssz ⊢ ( ℤ≥ ‘ 2 ) ⊆ ℤ
91 zsscn ⊢ ℤ ⊆ ℂ
92 90 91 sstri ⊢ ( ℤ≥ ‘ 2 ) ⊆ ℂ
93 simpll ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) → 𝑦 ∈ ( ℤ≥ ‘ 2 ) )
94 93 ad2antrr ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) ∧ 𝑚 ∈ ℕ ) → 𝑦 ∈ ( ℤ≥ ‘ 2 ) )
95 92 94 sselid ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) ∧ 𝑚 ∈ ℕ ) → 𝑦 ∈ ℂ )
96 simplr ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) → 𝑧 ∈ ( ℤ≥ ‘ 2 ) )
97 96 ad2antrr ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) ∧ 𝑚 ∈ ℕ ) → 𝑧 ∈ ( ℤ≥ ‘ 2 ) )
98 92 97 sselid ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) ∧ 𝑚 ∈ ℕ ) → 𝑧 ∈ ℂ )
99 mul32 ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑚 · 𝑦 ) · 𝑧 ) = ( ( 𝑚 · 𝑧 ) · 𝑦 ) )
100 mulass ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑚 · 𝑦 ) · 𝑧 ) = ( 𝑚 · ( 𝑦 · 𝑧 ) ) )
101 99 100 eqtr3d ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑚 · 𝑧 ) · 𝑦 ) = ( 𝑚 · ( 𝑦 · 𝑧 ) ) )
102 89 95 98 101 syl3anc ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 · 𝑧 ) · 𝑦 ) = ( 𝑚 · ( 𝑦 · 𝑧 ) ) )
103 102 eleq1d ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝑚 · 𝑧 ) · 𝑦 ) ∈ 𝑆 ↔ ( 𝑚 · ( 𝑦 · 𝑧 ) ) ∈ 𝑆 ) )
104 simpr ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
105 eluz2nn ⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → 𝑧 ∈ ℕ )
106 97 105 syl ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) ∧ 𝑚 ∈ ℕ ) → 𝑧 ∈ ℕ )
107 104 106 nnmulcld ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 · 𝑧 ) ∈ ℕ )
108 simplr ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) ∧ 𝑚 ∈ ℕ ) → ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) )
109 oveq1 ⊢ ( 𝑛 = ( 𝑚 · 𝑧 ) → ( 𝑛 · 𝑦 ) = ( ( 𝑚 · 𝑧 ) · 𝑦 ) )
110 109 eleq1d ⊢ ( 𝑛 = ( 𝑚 · 𝑧 ) → ( ( 𝑛 · 𝑦 ) ∈ 𝑆 ↔ ( ( 𝑚 · 𝑧 ) · 𝑦 ) ∈ 𝑆 ) )
111 eleq1 ⊢ ( 𝑛 = ( 𝑚 · 𝑧 ) → ( 𝑛 ∈ 𝑆 ↔ ( 𝑚 · 𝑧 ) ∈ 𝑆 ) )
112 110 111 imbi12d ⊢ ( 𝑛 = ( 𝑚 · 𝑧 ) → ( ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ↔ ( ( ( 𝑚 · 𝑧 ) · 𝑦 ) ∈ 𝑆 → ( 𝑚 · 𝑧 ) ∈ 𝑆 ) ) )
113 112 rspcv ⊢ ( ( 𝑚 · 𝑧 ) ∈ ℕ → ( ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) → ( ( ( 𝑚 · 𝑧 ) · 𝑦 ) ∈ 𝑆 → ( 𝑚 · 𝑧 ) ∈ 𝑆 ) ) )
114 107 108 113 sylc ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝑚 · 𝑧 ) · 𝑦 ) ∈ 𝑆 → ( 𝑚 · 𝑧 ) ∈ 𝑆 ) )
115 103 114 sylbird ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 · ( 𝑦 · 𝑧 ) ) ∈ 𝑆 → ( 𝑚 · 𝑧 ) ∈ 𝑆 ) )
116 115 imim1d ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝑚 · 𝑧 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) → ( ( 𝑚 · ( 𝑦 · 𝑧 ) ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
117 116 ralimdva ⊢ ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 · 𝑦 ) ∈ 𝑆 → 𝑛 ∈ 𝑆 ) ) → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑧 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · ( 𝑦 · 𝑧 ) ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
118 88 117 sylan2b ⊢ ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑦 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑧 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · ( 𝑦 · 𝑧 ) ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
119 118 expimpd ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) → ( ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑦 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑧 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · ( 𝑦 · 𝑧 ) ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
120 83 119 embantd ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) ) → ( ( ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) ) → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑦 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑧 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · ( 𝑦 · 𝑧 ) ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
121 120 ex ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) → ( ( ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) ) → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑦 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑧 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · ( 𝑦 · 𝑧 ) ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ) )
122 121 com23 ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) ) → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑦 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑧 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ) → ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · ( 𝑦 · 𝑧 ) ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ) )
123 69 122 syl5 ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑦 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ∧ ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝑧 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ) → ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 𝑦 · 𝑧 ) → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · ( 𝑦 · 𝑧 ) ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) ) )
124 13 21 29 37 45 51 68 123 prmind ⊢ ( 𝐵 ∈ ℕ → ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆 ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝐵 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ) )
125 3 4 124 sylc ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝐵 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) )
126 oveq1 ⊢ ( 𝑚 = 𝐴 → ( 𝑚 · 𝐵 ) = ( 𝐴 · 𝐵 ) )
127 126 eleq1d ⊢ ( 𝑚 = 𝐴 → ( ( 𝑚 · 𝐵 ) ∈ 𝑆 ↔ ( 𝐴 · 𝐵 ) ∈ 𝑆 ) )
128 eleq1 ⊢ ( 𝑚 = 𝐴 → ( 𝑚 ∈ 𝑆 ↔ 𝐴 ∈ 𝑆 ) )
129 127 128 imbi12d ⊢ ( 𝑚 = 𝐴 → ( ( ( 𝑚 · 𝐵 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) ↔ ( ( 𝐴 · 𝐵 ) ∈ 𝑆 → 𝐴 ∈ 𝑆 ) ) )
130 129 rspcv ⊢ ( 𝐴 ∈ ℕ → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 · 𝐵 ) ∈ 𝑆 → 𝑚 ∈ 𝑆 ) → ( ( 𝐴 · 𝐵 ) ∈ 𝑆 → 𝐴 ∈ 𝑆 ) ) )
131 2 125 5 130 syl3c ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )