Metamath Proof Explorer

Theorem 4sqlem18

Description: Lemma for 4sq . Inductive step, odd prime case. (Contributed by Mario Carneiro, 16-Jul-2014) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses 4sq.1 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
4sq.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4sq.3 ⊢ ( 𝜑 → 𝑃 = ( ( 2 · 𝑁 ) + 1 ) )
4sq.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
4sq.5 ⊢ ( 𝜑 → ( 0 ... ( 2 · 𝑁 ) ) ⊆ 𝑆 )
4sq.6 ⊢ 𝑇 = { 𝑖 ∈ ℕ ∣ ( 𝑖 · 𝑃 ) ∈ 𝑆 }
4sq.7 ⊢ 𝑀 = inf ( 𝑇 , ℝ , < )
Assertion 4sqlem18 ( 𝜑 → 𝑃 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 4sq.1 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
2 4sq.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 4sq.3 ⊢ ( 𝜑 → 𝑃 = ( ( 2 · 𝑁 ) + 1 ) )
4 4sq.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 4sq.5 ⊢ ( 𝜑 → ( 0 ... ( 2 · 𝑁 ) ) ⊆ 𝑆 )
6 4sq.6 ⊢ 𝑇 = { 𝑖 ∈ ℕ ∣ ( 𝑖 · 𝑃 ) ∈ 𝑆 }
7 4sq.7 ⊢ 𝑀 = inf ( 𝑇 , ℝ , < )
8 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
9 4 8 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
10 9 nncnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
11 10 mulid2d ⊢ ( 𝜑 → ( 1 · 𝑃 ) = 𝑃 )
12 6 ssrab3 ⊢ 𝑇 ⊆ ℕ
13 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
14 12 13 sseqtri ⊢ 𝑇 ⊆ ( ℤ≥ ‘ 1 )
15 1 2 3 4 5 6 7 4sqlem13 ⊢ ( 𝜑 → ( 𝑇 ≠ ∅ ∧ 𝑀 < 𝑃 ) )
16 15 simpld ⊢ ( 𝜑 → 𝑇 ≠ ∅ )
17 infssuzcl ⊢ ( ( 𝑇 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 )
18 14 16 17 sylancr ⊢ ( 𝜑 → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 )
19 7 18 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ 𝑇 )
20 oveq1 ⊢ ( 𝑖 = 𝑀 → ( 𝑖 · 𝑃 ) = ( 𝑀 · 𝑃 ) )
21 20 eleq1d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑖 · 𝑃 ) ∈ 𝑆 ↔ ( 𝑀 · 𝑃 ) ∈ 𝑆 ) )
22 21 6 elrab2 ⊢ ( 𝑀 ∈ 𝑇 ↔ ( 𝑀 ∈ ℕ ∧ ( 𝑀 · 𝑃 ) ∈ 𝑆 ) )
23 19 22 sylib ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ ( 𝑀 · 𝑃 ) ∈ 𝑆 ) )
24 23 simprd ⊢ ( 𝜑 → ( 𝑀 · 𝑃 ) ∈ 𝑆 )
25 1 4sqlem2 ⊢ ( ( 𝑀 · 𝑃 ) ∈ 𝑆 ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
26 24 25 sylib ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
28 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → 𝜑 )
29 28 2 syl ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → 𝑁 ∈ ℕ )
30 28 3 syl ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → 𝑃 = ( ( 2 · 𝑁 ) + 1 ) )
31 28 4 syl ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → 𝑃 ∈ ℙ )
32 28 5 syl ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → ( 0 ... ( 2 · 𝑁 ) ) ⊆ 𝑆 )
33 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
34 simp2ll ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → 𝑎 ∈ ℤ )
35 simp2lr ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → 𝑏 ∈ ℤ )
36 simp2rl ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → 𝑐 ∈ ℤ )
37 simp2rr ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → 𝑑 ∈ ℤ )
38 eqid ⊢ ( ( ( 𝑎 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) = ( ( ( 𝑎 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
39 eqid ⊢ ( ( ( 𝑏 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) = ( ( ( 𝑏 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
40 eqid ⊢ ( ( ( 𝑐 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) = ( ( ( 𝑐 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
41 eqid ⊢ ( ( ( 𝑑 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) = ( ( ( 𝑑 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
42 eqid ⊢ ( ( ( ( ( ( ( 𝑎 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) ↑ 2 ) + ( ( ( ( 𝑏 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) ↑ 2 ) ) + ( ( ( ( ( 𝑐 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) ↑ 2 ) + ( ( ( ( 𝑑 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) ↑ 2 ) ) ) / 𝑀 ) = ( ( ( ( ( ( ( 𝑎 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) ↑ 2 ) + ( ( ( ( 𝑏 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) ↑ 2 ) ) + ( ( ( ( ( 𝑐 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) ↑ 2 ) + ( ( ( ( 𝑑 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) ↑ 2 ) ) ) / 𝑀 )
43 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
44 1 29 30 31 32 6 7 33 34 35 36 37 38 39 40 41 42 43 4sqlem17 ⊢ ¬ ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
45 44 pm2.21i ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → ¬ 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
46 45 3expia ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ) → ( ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) → ¬ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) )
47 46 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) → ¬ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) )
48 47 rexlimdvva ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) → ¬ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) )
49 48 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝑀 · 𝑃 ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) → ¬ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) )
50 27 49 mpd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
51 50 pm2.01da ⊢ ( 𝜑 → ¬ 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
52 23 simpld ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
53 elnn1uz2 ⊢ ( 𝑀 ∈ ℕ ↔ ( 𝑀 = 1 ∨ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) )
54 52 53 sylib ⊢ ( 𝜑 → ( 𝑀 = 1 ∨ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) )
55 54 ord ⊢ ( 𝜑 → ( ¬ 𝑀 = 1 → 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) )
56 51 55 mt3d ⊢ ( 𝜑 → 𝑀 = 1 )
57 56 19 eqeltrrd ⊢ ( 𝜑 → 1 ∈ 𝑇 )
58 oveq1 ⊢ ( 𝑖 = 1 → ( 𝑖 · 𝑃 ) = ( 1 · 𝑃 ) )
59 58 eleq1d ⊢ ( 𝑖 = 1 → ( ( 𝑖 · 𝑃 ) ∈ 𝑆 ↔ ( 1 · 𝑃 ) ∈ 𝑆 ) )
60 59 6 elrab2 ⊢ ( 1 ∈ 𝑇 ↔ ( 1 ∈ ℕ ∧ ( 1 · 𝑃 ) ∈ 𝑆 ) )
61 60 simprbi ⊢ ( 1 ∈ 𝑇 → ( 1 · 𝑃 ) ∈ 𝑆 )
62 57 61 syl ⊢ ( 𝜑 → ( 1 · 𝑃 ) ∈ 𝑆 )
63 11 62 eqeltrrd ⊢ ( 𝜑 → 𝑃 ∈ 𝑆 )