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 mulid1d ( 𝑚 ∈ ℕ → ( 𝑚 · 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 ( 𝜑𝐴𝑆 )