Metamath Proof Explorer

Theorem 2sqlem9

Description: Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Hypotheses 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2sqlem7.2 ⊢ 𝑌 = { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) }
2sqlem9.5 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... ( 𝑀 − 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) )
2sqlem9.7 ⊢ ( 𝜑 → 𝑀 ∥ 𝑁 )
2sqlem9.6 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2sqlem9.4 ⊢ ( 𝜑 → 𝑁 ∈ 𝑌 )
Assertion 2sqlem9 ( 𝜑 → 𝑀 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2 2sqlem7.2 ⊢ 𝑌 = { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) }
3 2sqlem9.5 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... ( 𝑀 − 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) )
4 2sqlem9.7 ⊢ ( 𝜑 → 𝑀 ∥ 𝑁 )
5 2sqlem9.6 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
6 2sqlem9.4 ⊢ ( 𝜑 → 𝑁 ∈ 𝑌 )
7 eqeq1 ⊢ ( 𝑧 = 𝑁 → ( 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ 𝑁 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
8 7 anbi2d ⊢ ( 𝑧 = 𝑁 → ( ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑁 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
9 8 2rexbidv ⊢ ( 𝑧 = 𝑁 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑁 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
10 oveq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 gcd 𝑦 ) = ( 𝑢 gcd 𝑦 ) )
11 10 eqeq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 gcd 𝑦 ) = 1 ↔ ( 𝑢 gcd 𝑦 ) = 1 ) )
12 oveq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 ↑ 2 ) = ( 𝑢 ↑ 2 ) )
13 12 oveq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( 𝑢 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
14 13 eqeq2d ⊢ ( 𝑥 = 𝑢 → ( 𝑁 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
15 11 14 anbi12d ⊢ ( 𝑥 = 𝑢 → ( ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑁 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ( ( 𝑢 gcd 𝑦 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
16 oveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝑢 gcd 𝑦 ) = ( 𝑢 gcd 𝑣 ) )
17 16 eqeq1d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑢 gcd 𝑦 ) = 1 ↔ ( 𝑢 gcd 𝑣 ) = 1 ) )
18 oveq1 ⊢ ( 𝑦 = 𝑣 → ( 𝑦 ↑ 2 ) = ( 𝑣 ↑ 2 ) )
19 18 oveq2d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑢 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) )
20 19 eqeq2d ⊢ ( 𝑦 = 𝑣 → ( 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) )
21 17 20 anbi12d ⊢ ( 𝑦 = 𝑣 → ( ( ( 𝑢 gcd 𝑦 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ) )
22 15 21 cbvrex2vw ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑁 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) )
23 9 22 bitrdi ⊢ ( 𝑧 = 𝑁 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ) )
24 23 2 elab2g ⊢ ( 𝑁 ∈ 𝑌 → ( 𝑁 ∈ 𝑌 ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ) )
25 24 ibi ⊢ ( 𝑁 ∈ 𝑌 → ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) )
26 6 25 syl ⊢ ( 𝜑 → ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) )
27 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ) ∧ 𝑀 = 1 ) → 𝑀 = 1 )
28 1z ⊢ 1 ∈ ℤ
29 zgz ⊢ ( 1 ∈ ℤ → 1 ∈ ℤ[i] )
30 28 29 ax-mp ⊢ 1 ∈ ℤ[i]
31 sq1 ⊢ ( 1 ↑ 2 ) = 1
32 31 eqcomi ⊢ 1 = ( 1 ↑ 2 )
33 fveq2 ⊢ ( 𝑥 = 1 → ( abs ‘ 𝑥 ) = ( abs ‘ 1 ) )
34 abs1 ⊢ ( abs ‘ 1 ) = 1
35 33 34 eqtrdi ⊢ ( 𝑥 = 1 → ( abs ‘ 𝑥 ) = 1 )
36 35 oveq1d ⊢ ( 𝑥 = 1 → ( ( abs ‘ 𝑥 ) ↑ 2 ) = ( 1 ↑ 2 ) )
37 36 rspceeqv ⊢ ( ( 1 ∈ ℤ[i] ∧ 1 = ( 1 ↑ 2 ) ) → ∃ 𝑥 ∈ ℤ[i] 1 = ( ( abs ‘ 𝑥 ) ↑ 2 ) )
38 30 32 37 mp2an ⊢ ∃ 𝑥 ∈ ℤ[i] 1 = ( ( abs ‘ 𝑥 ) ↑ 2 )
39 1 2sqlem1 ⊢ ( 1 ∈ 𝑆 ↔ ∃ 𝑥 ∈ ℤ[i] 1 = ( ( abs ‘ 𝑥 ) ↑ 2 ) )
40 38 39 mpbir ⊢ 1 ∈ 𝑆
41 27 40 eqeltrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ) ∧ 𝑀 = 1 ) → 𝑀 ∈ 𝑆 )
42 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ∧ 𝑀 ≠ 1 ) ) → ∀ 𝑏 ∈ ( 1 ... ( 𝑀 − 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) )
43 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ∧ 𝑀 ≠ 1 ) ) → 𝑀 ∥ 𝑁 )
44 1 2 2sqlem7 ⊢ 𝑌 ⊆ ( 𝑆 ∩ ℕ )
45 inss2 ⊢ ( 𝑆 ∩ ℕ ) ⊆ ℕ
46 44 45 sstri ⊢ 𝑌 ⊆ ℕ
47 46 6 sselid ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
48 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ∧ 𝑀 ≠ 1 ) ) → 𝑁 ∈ ℕ )
49 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ∧ 𝑀 ≠ 1 ) ) → 𝑀 ∈ ℕ )
50 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ∧ 𝑀 ≠ 1 ) ) → 𝑀 ≠ 1 )
51 eluz2b3 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑀 ∈ ℕ ∧ 𝑀 ≠ 1 ) )
52 49 50 51 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ∧ 𝑀 ≠ 1 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
53 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ∧ 𝑀 ≠ 1 ) ) → 𝑢 ∈ ℤ )
54 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ∧ 𝑀 ≠ 1 ) ) → 𝑣 ∈ ℤ )
55 simprll ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ∧ 𝑀 ≠ 1 ) ) → ( 𝑢 gcd 𝑣 ) = 1 )
56 simprlr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ∧ 𝑀 ≠ 1 ) ) → 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) )
57 eqid ⊢ ( ( ( 𝑢 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) = ( ( ( 𝑢 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
58 eqid ⊢ ( ( ( 𝑣 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) = ( ( ( 𝑣 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
59 eqid ⊢ ( ( ( ( 𝑢 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) / ( ( ( ( 𝑢 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) gcd ( ( ( 𝑣 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) ) ) = ( ( ( ( 𝑢 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) / ( ( ( ( 𝑢 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) gcd ( ( ( 𝑣 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) ) )
60 eqid ⊢ ( ( ( ( 𝑣 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) / ( ( ( ( 𝑢 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) gcd ( ( ( 𝑣 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) ) ) = ( ( ( ( 𝑣 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) / ( ( ( ( 𝑢 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) gcd ( ( ( 𝑣 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) ) )
61 1 2 42 43 48 52 53 54 55 56 57 58 59 60 2sqlem8 ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ∧ 𝑀 ≠ 1 ) ) → 𝑀 ∈ 𝑆 )
62 61 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ) ∧ 𝑀 ≠ 1 ) → 𝑀 ∈ 𝑆 )
63 41 62 pm2.61dane ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ∧ ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) ) → 𝑀 ∈ 𝑆 )
64 63 ex ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) → ( ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) → 𝑀 ∈ 𝑆 ) )
65 64 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ ( ( 𝑢 gcd 𝑣 ) = 1 ∧ 𝑁 = ( ( 𝑢 ↑ 2 ) + ( 𝑣 ↑ 2 ) ) ) → 𝑀 ∈ 𝑆 ) )
66 26 65 mpd ⊢ ( 𝜑 → 𝑀 ∈ 𝑆 )