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 33 39 raleqtrrdv ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → ∀ 𝑏 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) )
41 simprr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → ( 𝑛 + 1 ) ∥ 𝑚 )
42 peano2nn ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ )
43 42 ad2antrr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → ( 𝑛 + 1 ) ∈ ℕ )
44 simprl ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → 𝑚 ∈ 𝑌 )
45 1 2 40 41 43 44 2sqlem9 ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ 𝑌 ∧ ( 𝑛 + 1 ) ∥ 𝑚 ) ) → ( 𝑛 + 1 ) ∈ 𝑆 )
46 45 expr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ∧ 𝑚 ∈ 𝑌 ) → ( ( 𝑛 + 1 ) ∥ 𝑚 → ( 𝑛 + 1 ) ∈ 𝑆 ) )
47 46 ralrimiva ⊢ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) → ∀ 𝑚 ∈ 𝑌 ( ( 𝑛 + 1 ) ∥ 𝑚 → ( 𝑛 + 1 ) ∈ 𝑆 ) )
48 47 ex ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) → ∀ 𝑚 ∈ 𝑌 ( ( 𝑛 + 1 ) ∥ 𝑚 → ( 𝑛 + 1 ) ∈ 𝑆 ) ) )
49 breq2 ⊢ ( 𝑎 = 𝑚 → ( ( 𝑛 + 1 ) ∥ 𝑎 ↔ ( 𝑛 + 1 ) ∥ 𝑚 ) )
50 49 imbi1d ⊢ ( 𝑎 = 𝑚 → ( ( ( 𝑛 + 1 ) ∥ 𝑎 → ( 𝑛 + 1 ) ∈ 𝑆 ) ↔ ( ( 𝑛 + 1 ) ∥ 𝑚 → ( 𝑛 + 1 ) ∈ 𝑆 ) ) )
51 50 cbvralvw ⊢ ( ∀ 𝑎 ∈ 𝑌 ( ( 𝑛 + 1 ) ∥ 𝑎 → ( 𝑛 + 1 ) ∈ 𝑆 ) ↔ ∀ 𝑚 ∈ 𝑌 ( ( 𝑛 + 1 ) ∥ 𝑚 → ( 𝑛 + 1 ) ∈ 𝑆 ) )
52 48 51 imbitrrdi ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) → ∀ 𝑎 ∈ 𝑌 ( ( 𝑛 + 1 ) ∥ 𝑎 → ( 𝑛 + 1 ) ∈ 𝑆 ) ) )
53 ovex ⊢ ( 𝑛 + 1 ) ∈ V
54 breq1 ⊢ ( 𝑏 = ( 𝑛 + 1 ) → ( 𝑏 ∥ 𝑎 ↔ ( 𝑛 + 1 ) ∥ 𝑎 ) )
55 eleq1 ⊢ ( 𝑏 = ( 𝑛 + 1 ) → ( 𝑏 ∈ 𝑆 ↔ ( 𝑛 + 1 ) ∈ 𝑆 ) )
56 54 55 imbi12d ⊢ ( 𝑏 = ( 𝑛 + 1 ) → ( ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ( ( 𝑛 + 1 ) ∥ 𝑎 → ( 𝑛 + 1 ) ∈ 𝑆 ) ) )
57 56 ralbidv ⊢ ( 𝑏 = ( 𝑛 + 1 ) → ( ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ∀ 𝑎 ∈ 𝑌 ( ( 𝑛 + 1 ) ∥ 𝑎 → ( 𝑛 + 1 ) ∈ 𝑆 ) ) )
58 53 57 ralsn ⊢ ( ∀ 𝑏 ∈ { ( 𝑛 + 1 ) } ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ∀ 𝑎 ∈ 𝑌 ( ( 𝑛 + 1 ) ∥ 𝑎 → ( 𝑛 + 1 ) ∈ 𝑆 ) )
59 52 58 imbitrrdi ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) → ∀ 𝑏 ∈ { ( 𝑛 + 1 ) } ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) )
60 59 ancld ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) → ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ∧ ∀ 𝑏 ∈ { ( 𝑛 + 1 ) } ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ) )
61 elnnuz ⊢ ( 𝑛 ∈ ℕ ↔ 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
62 fzsuc ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → ( 1 ... ( 𝑛 + 1 ) ) = ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) )
63 61 62 sylbi ⊢ ( 𝑛 ∈ ℕ → ( 1 ... ( 𝑛 + 1 ) ) = ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) )
64 63 raleqdv ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑏 ∈ ( 1 ... ( 𝑛 + 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ∀ 𝑏 ∈ ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) )
65 ralunb ⊢ ( ∀ 𝑏 ∈ ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ∧ ∀ 𝑏 ∈ { ( 𝑛 + 1 ) } ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) )
66 64 65 bitrdi ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑏 ∈ ( 1 ... ( 𝑛 + 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ∧ ∀ 𝑏 ∈ { ( 𝑛 + 1 ) } ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) ) )
67 60 66 sylibrd ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) → ∀ 𝑏 ∈ ( 1 ... ( 𝑛 + 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ) )
68 8 10 12 14 32 67 nnind ⊢ ( 𝐵 ∈ ℕ → ∀ 𝑏 ∈ ( 1 ... 𝐵 ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) )
69 elfz1end ⊢ ( 𝐵 ∈ ℕ ↔ 𝐵 ∈ ( 1 ... 𝐵 ) )
70 69 biimpi ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ( 1 ... 𝐵 ) )
71 6 68 70 rspcdva ⊢ ( 𝐵 ∈ ℕ → ∀ 𝑎 ∈ 𝑌 ( 𝐵 ∥ 𝑎 → 𝐵 ∈ 𝑆 ) )
72 breq2 ⊢ ( 𝑎 = 𝐴 → ( 𝐵 ∥ 𝑎 ↔ 𝐵 ∥ 𝐴 ) )
73 72 imbi1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝐵 ∥ 𝑎 → 𝐵 ∈ 𝑆 ) ↔ ( 𝐵 ∥ 𝐴 → 𝐵 ∈ 𝑆 ) ) )
74 73 rspcv ⊢ ( 𝐴 ∈ 𝑌 → ( ∀ 𝑎 ∈ 𝑌 ( 𝐵 ∥ 𝑎 → 𝐵 ∈ 𝑆 ) → ( 𝐵 ∥ 𝐴 → 𝐵 ∈ 𝑆 ) ) )
75 71 74 syl5 ⊢ ( 𝐴 ∈ 𝑌 → ( 𝐵 ∈ ℕ → ( 𝐵 ∥ 𝐴 → 𝐵 ∈ 𝑆 ) ) )
76 75 3imp ⊢ ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∥ 𝐴 ) → 𝐵 ∈ 𝑆 )