Metamath Proof Explorer

Theorem 2sqlem10

Description: Lemma for 2sq . Every factor of a "proper" sum of two squares (where the summands are coprime) is a sum of two squares. (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Hypotheses 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2sqlem7.2 ⊢ 𝑌 = { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) }
Assertion 2sqlem10 ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∥ 𝐴 ) → 𝐵 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2 2sqlem7.2 ⊢ 𝑌 = { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) }
3 breq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∥ 𝑎 ↔ 𝐵 ∥ 𝑎 ) )
4 eleq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∈ 𝑆 ↔ 𝐵 ∈ 𝑆 ) )
5 3 4 imbi12d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ( 𝐵 ∥ 𝑎 → 𝐵 ∈ 𝑆 ) ) )
6 5 ralbidv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ∀ 𝑎 ∈ 𝑌 ( 𝐵 ∥ 𝑎 → 𝐵 ∈ 𝑆 ) ) )
7 oveq2 ⊢ ( 𝑚 = 1 → ( 1 ... 𝑚 ) = ( 1 ... 1 ) )
8 7 raleqdv ⊢ ( 𝑚 = 1 → ( ∀ 𝑏 ∈ ( 1 ... 𝑚 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ∀ 𝑏 ∈ ( 1 ... 1 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) )
9 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 1 ... 𝑚 ) = ( 1 ... 𝑛 ) )
10 9 raleqdv ⊢ ( 𝑚 = 𝑛 → ( ∀ 𝑏 ∈ ( 1 ... 𝑚 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) )
11 oveq2 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 1 ... 𝑚 ) = ( 1 ... ( 𝑛 + 1 ) ) )
12 11 raleqdv ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ∀ 𝑏 ∈ ( 1 ... 𝑚 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 + 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) )
13 oveq2 ⊢ ( 𝑚 = 𝐵 → ( 1 ... 𝑚 ) = ( 1 ... 𝐵 ) )
14 13 raleqdv ⊢ ( 𝑚 = 𝐵 → ( ∀ 𝑏 ∈ ( 1 ... 𝑚 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ∀ 𝑏 ∈ ( 1 ... 𝐵 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) )
15 elfz1eq ⊢ ( 𝑏 ∈ ( 1 ... 1 ) → 𝑏 = 1 )
16 1z ⊢ 1 ∈ ℤ
17 zgz ⊢ ( 1 ∈ ℤ → 1 ∈ ℤ[i] )
18 16 17 ax-mp ⊢ 1 ∈ ℤ[i]
19 sq1 ⊢ ( 1 ↑ 2 ) = 1
20 19 eqcomi ⊢ 1 = ( 1 ↑ 2 )
21 fveq2 ⊢ ( 𝑥 = 1 → ( abs ‘ 𝑥 ) = ( abs ‘ 1 ) )
22 abs1 ⊢ ( abs ‘ 1 ) = 1
23 21 22 eqtrdi ⊢ ( 𝑥 = 1 → ( abs ‘ 𝑥 ) = 1 )
24 23 oveq1d ⊢ ( 𝑥 = 1 → ( ( abs ‘ 𝑥 ) ↑ 2 ) = ( 1 ↑ 2 ) )
25 24 rspceeqv ⊢ ( ( 1 ∈ ℤ[i] ∧ 1 = ( 1 ↑ 2 ) ) → ∃ 𝑥 ∈ ℤ[i] 1 = ( ( abs ‘ 𝑥 ) ↑ 2 ) )
26 18 20 25 mp2an ⊢ ∃ 𝑥 ∈ ℤ[i] 1 = ( ( abs ‘ 𝑥 ) ↑ 2 )
27 1 2sqlem1 ⊢ ( 1 ∈ 𝑆 ↔ ∃ 𝑥 ∈ ℤ[i] 1 = ( ( abs ‘ 𝑥 ) ↑ 2 ) )
28 26 27 mpbir ⊢ 1 ∈ 𝑆
29 15 28 eqeltrdi ⊢ ( 𝑏 ∈ ( 1 ... 1 ) → 𝑏 ∈ 𝑆 )
30 29 a1d ⊢ ( 𝑏 ∈ ( 1 ... 1 ) → ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) )
31 30 ralrimivw ⊢ ( 𝑏 ∈ ( 1 ... 1 ) → ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) )
32 31 rgen ⊢ ∀ 𝑏 ∈ ( 1 ... 1 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 )
33 simplr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) )
34 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
35 34 ad2antrr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → 𝑛 ∈ ℂ )
36 ax-1cn ⊢ 1 ∈ ℂ
37 pncan ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
38 35 36 37 sylancl ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
39 38 oveq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) = ( 1 ... 𝑛 ) )
40 39 raleqdv ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → ( ∀ 𝑏 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) )
41 33 40 mpbird ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → ∀ 𝑏 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) )
42 simprr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → ( 𝑛 + 1 ) ∥ 𝑚 )
43 peano2nn ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ )
44 43 ad2antrr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → ( 𝑛 + 1 ) ∈ ℕ )
45 simprl ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → 𝑚 ∈ 𝑌 )
46 1 2 41 42 44 45 2sqlem9 ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → ( 𝑛 + 1 ) ∈ 𝑆 )
47 46 expr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ 𝑚 ∈ 𝑌 ) → ( ( 𝑛 + 1 ) ∥ 𝑚 → ( 𝑛 + 1 ) ∈ 𝑆 ) )
48 47 ralrimiva ⊢ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) → ∀ 𝑚 ∈ 𝑌 ( ( 𝑛 + 1 ) ∥ 𝑚 → ( 𝑛 + 1 ) ∈ 𝑆 ) )
49 48 ex ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) → ∀ 𝑚 ∈ 𝑌 ( ( 𝑛 + 1 ) ∥ 𝑚 → ( 𝑛 + 1 ) ∈ 𝑆 ) ) )
50 breq2 ⊢ ( 𝑎 = 𝑚 → ( ( 𝑛 + 1 ) ∥ 𝑎 ↔ ( 𝑛 + 1 ) ∥ 𝑚 ) )
51 50 imbi1d ⊢ ( 𝑎 = 𝑚 → ( ( ( 𝑛 + 1 ) ∥ 𝑎 → ( 𝑛 + 1 ) ∈ 𝑆 ) ↔ ( ( 𝑛 + 1 ) ∥ 𝑚 → ( 𝑛 + 1 ) ∈ 𝑆 ) ) )
52 51 cbvralvw ⊢ ( ∀ 𝑎 ∈ 𝑌 ( ( 𝑛 + 1 ) ∥ 𝑎 → ( 𝑛 + 1 ) ∈ 𝑆 ) ↔ ∀ 𝑚 ∈ 𝑌 ( ( 𝑛 + 1 ) ∥ 𝑚 → ( 𝑛 + 1 ) ∈ 𝑆 ) )
53 49 52 syl6ibr ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) → ∀ 𝑎 ∈ 𝑌 ( ( 𝑛 + 1 ) ∥ 𝑎 → ( 𝑛 + 1 ) ∈ 𝑆 ) ) )
54 ovex ⊢ ( 𝑛 + 1 ) ∈ V
55 breq1 ⊢ ( 𝑏 = ( 𝑛 + 1 ) → ( 𝑏 ∥ 𝑎 ↔ ( 𝑛 + 1 ) ∥ 𝑎 ) )
56 eleq1 ⊢ ( 𝑏 = ( 𝑛 + 1 ) → ( 𝑏 ∈ 𝑆 ↔ ( 𝑛 + 1 ) ∈ 𝑆 ) )
57 55 56 imbi12d ⊢ ( 𝑏 = ( 𝑛 + 1 ) → ( ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ( ( 𝑛 + 1 ) ∥ 𝑎 → ( 𝑛 + 1 ) ∈ 𝑆 ) ) )
58 57 ralbidv ⊢ ( 𝑏 = ( 𝑛 + 1 ) → ( ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ∀ 𝑎 ∈ 𝑌 ( ( 𝑛 + 1 ) ∥ 𝑎 → ( 𝑛 + 1 ) ∈ 𝑆 ) ) )
59 54 58 ralsn ⊢ ( ∀ 𝑏 ∈ { ( 𝑛 + 1 ) } ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ∀ 𝑎 ∈ 𝑌 ( ( 𝑛 + 1 ) ∥ 𝑎 → ( 𝑛 + 1 ) ∈ 𝑆 ) )
60 53 59 syl6ibr ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) → ∀ 𝑏 ∈ { ( 𝑛 + 1 ) } ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) )
61 60 ancld ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) → ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ∧ ∀ 𝑏 ∈ { ( 𝑛 + 1 ) } ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ) )
62 elnnuz ⊢ ( 𝑛 ∈ ℕ ↔ 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
63 fzsuc ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → ( 1 ... ( 𝑛 + 1 ) ) = ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) )
64 62 63 sylbi ⊢ ( 𝑛 ∈ ℕ → ( 1 ... ( 𝑛 + 1 ) ) = ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) )
65 64 raleqdv ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑏 ∈ ( 1 ... ( 𝑛 + 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ∀ 𝑏 ∈ ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) )
66 ralunb ⊢ ( ∀ 𝑏 ∈ ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ∧ ∀ 𝑏 ∈ { ( 𝑛 + 1 ) } ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) )
67 65 66 bitrdi ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑏 ∈ ( 1 ... ( 𝑛 + 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ∧ ∀ 𝑏 ∈ { ( 𝑛 + 1 ) } ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ) )
68 61 67 sylibrd ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) → ∀ 𝑏 ∈ ( 1 ... ( 𝑛 + 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) )
69 8 10 12 14 32 68 nnind ⊢ ( 𝐵 ∈ ℕ → ∀ 𝑏 ∈ ( 1 ... 𝐵 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) )
70 elfz1end ⊢ ( 𝐵 ∈ ℕ ↔ 𝐵 ∈ ( 1 ... 𝐵 ) )
71 70 biimpi ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ( 1 ... 𝐵 ) )
72 6 69 71 rspcdva ⊢ ( 𝐵 ∈ ℕ → ∀ 𝑎 ∈ 𝑌 ( 𝐵 ∥ 𝑎 → 𝐵 ∈ 𝑆 ) )
73 breq2 ⊢ ( 𝑎 = 𝐴 → ( 𝐵 ∥ 𝑎 ↔ 𝐵 ∥ 𝐴 ) )
74 73 imbi1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝐵 ∥ 𝑎 → 𝐵 ∈ 𝑆 ) ↔ ( 𝐵 ∥ 𝐴 → 𝐵 ∈ 𝑆 ) ) )
75 74 rspcv ⊢ ( 𝐴 ∈ 𝑌 → ( ∀ 𝑎 ∈ 𝑌 ( 𝐵 ∥ 𝑎 → 𝐵 ∈ 𝑆 ) → ( 𝐵 ∥ 𝐴 → 𝐵 ∈ 𝑆 ) ) )
76 72 75 syl5 ⊢ ( 𝐴 ∈ 𝑌 → ( 𝐵 ∈ ℕ → ( 𝐵 ∥ 𝐴 → 𝐵 ∈ 𝑆 ) ) )
77 76 3imp ⊢ ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∥ 𝐴 ) → 𝐵 ∈ 𝑆 )