Metamath Proof Explorer

Theorem 2sqlem8a

Description: Lemma for 2sqlem8 . (Contributed by Mario Carneiro, 4-Jun-2016)

Ref Expression
Hypotheses 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2sqlem7.2 ⊢ 𝑌 = { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) }
2sqlem9.5 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... ( 𝑀 − 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) )
2sqlem9.7 ⊢ ( 𝜑 → 𝑀 ∥ 𝑁 )
2sqlem8.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2sqlem8.m ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
2sqlem8.1 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
2sqlem8.2 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
2sqlem8.3 ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
2sqlem8.4 ⊢ ( 𝜑 → 𝑁 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
2sqlem8.c ⊢ 𝐶 = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
2sqlem8.d ⊢ 𝐷 = ( ( ( 𝐵 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
Assertion 2sqlem8a ( 𝜑 → ( 𝐶 gcd 𝐷 ) ∈ ℕ )

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 2sqlem8.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6 2sqlem8.m ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
7 2sqlem8.1 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
8 2sqlem8.2 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
9 2sqlem8.3 ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
10 2sqlem8.4 ⊢ ( 𝜑 → 𝑁 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
11 2sqlem8.c ⊢ 𝐶 = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
12 2sqlem8.d ⊢ 𝐷 = ( ( ( 𝐵 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
13 eluz2b3 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑀 ∈ ℕ ∧ 𝑀 ≠ 1 ) )
14 6 13 sylib ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑀 ≠ 1 ) )
15 14 simpld ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
16 7 15 11 4sqlem5 ⊢ ( 𝜑 → ( 𝐶 ∈ ℤ ∧ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ∈ ℤ ) )
17 16 simpld ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
18 8 15 12 4sqlem5 ⊢ ( 𝜑 → ( 𝐷 ∈ ℤ ∧ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ∈ ℤ ) )
19 18 simpld ⊢ ( 𝜑 → 𝐷 ∈ ℤ )
20 14 simprd ⊢ ( 𝜑 → 𝑀 ≠ 1 )
21 simpr ⊢ ( ( 𝜑 ∧ ( 𝐶 ↑ 2 ) = 0 ) → ( 𝐶 ↑ 2 ) = 0 )
22 7 15 11 21 4sqlem9 ⊢ ( ( 𝜑 ∧ ( 𝐶 ↑ 2 ) = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) )
23 22 ex ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) = 0 → ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ) )
24 eluzelz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℤ )
25 6 24 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
26 dvdssq ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝑀 ∥ 𝐴 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ) )
27 25 7 26 syl2anc ⊢ ( 𝜑 → ( 𝑀 ∥ 𝐴 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ) )
28 23 27 sylibrd ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) = 0 → 𝑀 ∥ 𝐴 ) )
29 simpr ⊢ ( ( 𝜑 ∧ ( 𝐷 ↑ 2 ) = 0 ) → ( 𝐷 ↑ 2 ) = 0 )
30 8 15 12 29 4sqlem9 ⊢ ( ( 𝜑 ∧ ( 𝐷 ↑ 2 ) = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) )
31 30 ex ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) = 0 → ( 𝑀 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) )
32 dvdssq ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑀 ∥ 𝐵 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) )
33 25 8 32 syl2anc ⊢ ( 𝜑 → ( 𝑀 ∥ 𝐵 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) )
34 31 33 sylibrd ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) = 0 → 𝑀 ∥ 𝐵 ) )
35 ax-1ne0 ⊢ 1 ≠ 0
36 35 a1i ⊢ ( 𝜑 → 1 ≠ 0 )
37 9 36 eqnetrd ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ≠ 0 )
38 37 neneqd ⊢ ( 𝜑 → ¬ ( 𝐴 gcd 𝐵 ) = 0 )
39 gcdeq0 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
40 7 8 39 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
41 38 40 mtbid ⊢ ( 𝜑 → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
42 dvdslegcd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( 𝑀 ∥ 𝐴 ∧ 𝑀 ∥ 𝐵 ) → 𝑀 ≤ ( 𝐴 gcd 𝐵 ) ) )
43 25 7 8 41 42 syl31anc ⊢ ( 𝜑 → ( ( 𝑀 ∥ 𝐴 ∧ 𝑀 ∥ 𝐵 ) → 𝑀 ≤ ( 𝐴 gcd 𝐵 ) ) )
44 28 34 43 syl2and ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) = 0 ∧ ( 𝐷 ↑ 2 ) = 0 ) → 𝑀 ≤ ( 𝐴 gcd 𝐵 ) ) )
45 9 breq2d ⊢ ( 𝜑 → ( 𝑀 ≤ ( 𝐴 gcd 𝐵 ) ↔ 𝑀 ≤ 1 ) )
46 nnle1eq1 ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ≤ 1 ↔ 𝑀 = 1 ) )
47 15 46 syl ⊢ ( 𝜑 → ( 𝑀 ≤ 1 ↔ 𝑀 = 1 ) )
48 45 47 bitrd ⊢ ( 𝜑 → ( 𝑀 ≤ ( 𝐴 gcd 𝐵 ) ↔ 𝑀 = 1 ) )
49 44 48 sylibd ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) = 0 ∧ ( 𝐷 ↑ 2 ) = 0 ) → 𝑀 = 1 ) )
50 49 necon3ad ⊢ ( 𝜑 → ( 𝑀 ≠ 1 → ¬ ( ( 𝐶 ↑ 2 ) = 0 ∧ ( 𝐷 ↑ 2 ) = 0 ) ) )
51 20 50 mpd ⊢ ( 𝜑 → ¬ ( ( 𝐶 ↑ 2 ) = 0 ∧ ( 𝐷 ↑ 2 ) = 0 ) )
52 17 zcnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
53 sqeq0 ⊢ ( 𝐶 ∈ ℂ → ( ( 𝐶 ↑ 2 ) = 0 ↔ 𝐶 = 0 ) )
54 52 53 syl ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) = 0 ↔ 𝐶 = 0 ) )
55 19 zcnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
56 sqeq0 ⊢ ( 𝐷 ∈ ℂ → ( ( 𝐷 ↑ 2 ) = 0 ↔ 𝐷 = 0 ) )
57 55 56 syl ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) = 0 ↔ 𝐷 = 0 ) )
58 54 57 anbi12d ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) = 0 ∧ ( 𝐷 ↑ 2 ) = 0 ) ↔ ( 𝐶 = 0 ∧ 𝐷 = 0 ) ) )
59 51 58 mtbid ⊢ ( 𝜑 → ¬ ( 𝐶 = 0 ∧ 𝐷 = 0 ) )
60 gcdn0cl ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ¬ ( 𝐶 = 0 ∧ 𝐷 = 0 ) ) → ( 𝐶 gcd 𝐷 ) ∈ ℕ )
61 17 19 59 60 syl21anc ⊢ ( 𝜑 → ( 𝐶 gcd 𝐷 ) ∈ ℕ )