Metamath Proof Explorer

Theorem 4sqlem13

Description: Lemma for 4sq . (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 4sqlem13 ( 𝜑 → ( 𝑇 ≠ ∅ ∧ 𝑀 < 𝑃 ) )

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 eqid ⊢ { 𝑢 ∣ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) } = { 𝑢 ∣ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) }
9 eqid ⊢ ( 𝑣 ∈ { 𝑢 ∣ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) } ↦ ( ( 𝑃 − 1 ) − 𝑣 ) ) = ( 𝑣 ∈ { 𝑢 ∣ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) } ↦ ( ( 𝑃 − 1 ) − 𝑣 ) )
10 1 2 3 4 8 9 4sqlem12 ⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) )
11 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) )
12 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑘 ∈ ℕ )
13 11 12 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑘 ∈ ℕ )
14 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) )
15 abs1 ⊢ ( abs ‘ 1 ) = 1
16 15 oveq1i ⊢ ( ( abs ‘ 1 ) ↑ 2 ) = ( 1 ↑ 2 )
17 sq1 ⊢ ( 1 ↑ 2 ) = 1
18 16 17 eqtri ⊢ ( ( abs ‘ 1 ) ↑ 2 ) = 1
19 18 oveq2i ⊢ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 1 ) ↑ 2 ) ) = ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 )
20 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑢 ∈ ℤ[i] )
21 1z ⊢ 1 ∈ ℤ
22 zgz ⊢ ( 1 ∈ ℤ → 1 ∈ ℤ[i] )
23 21 22 ax-mp ⊢ 1 ∈ ℤ[i]
24 1 4sqlem4a ⊢ ( ( 𝑢 ∈ ℤ[i] ∧ 1 ∈ ℤ[i] ) → ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 1 ) ↑ 2 ) ) ∈ 𝑆 )
25 20 23 24 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + ( ( abs ‘ 1 ) ↑ 2 ) ) ∈ 𝑆 )
26 19 25 eqeltrrid ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) ∈ 𝑆 )
27 14 26 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → ( 𝑘 · 𝑃 ) ∈ 𝑆 )
28 oveq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 · 𝑃 ) = ( 𝑘 · 𝑃 ) )
29 28 eleq1d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑖 · 𝑃 ) ∈ 𝑆 ↔ ( 𝑘 · 𝑃 ) ∈ 𝑆 ) )
30 29 6 elrab2 ⊢ ( 𝑘 ∈ 𝑇 ↔ ( 𝑘 ∈ ℕ ∧ ( 𝑘 · 𝑃 ) ∈ 𝑆 ) )
31 13 27 30 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑘 ∈ 𝑇 )
32 31 ne0d ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑇 ≠ ∅ )
33 6 ssrab3 ⊢ 𝑇 ⊆ ℕ
34 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
35 33 34 sseqtri ⊢ 𝑇 ⊆ ( ℤ≥ ‘ 1 )
36 infssuzcl ⊢ ( ( 𝑇 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 )
37 35 32 36 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 )
38 7 37 eqeltrid ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑀 ∈ 𝑇 )
39 33 38 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑀 ∈ ℕ )
40 39 nnred ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑀 ∈ ℝ )
41 13 nnred ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑘 ∈ ℝ )
42 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑃 ∈ ℙ )
43 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
44 42 43 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑃 ∈ ℕ )
45 44 nnred ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑃 ∈ ℝ )
46 infssuzle ⊢ ( ( 𝑇 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑘 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ≤ 𝑘 )
47 35 31 46 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → inf ( 𝑇 , ℝ , < ) ≤ 𝑘 )
48 7 47 eqbrtrid ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑀 ≤ 𝑘 )
49 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
50 42 49 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑃 ∈ ℤ )
51 elfzm11 ⊢ ( ( 1 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ∧ 𝑘 < 𝑃 ) ) )
52 21 50 51 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ∧ 𝑘 < 𝑃 ) ) )
53 11 52 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ∧ 𝑘 < 𝑃 ) )
54 53 simp3d ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑘 < 𝑃 )
55 40 41 45 48 54 lelttrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → 𝑀 < 𝑃 )
56 32 55 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) ∧ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) → ( 𝑇 ≠ ∅ ∧ 𝑀 < 𝑃 ) )
57 56 ex ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑢 ∈ ℤ[i] ) ) → ( ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) → ( 𝑇 ≠ ∅ ∧ 𝑀 < 𝑃 ) ) )
58 57 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) → ( 𝑇 ≠ ∅ ∧ 𝑀 < 𝑃 ) ) )
59 10 58 mpd ⊢ ( 𝜑 → ( 𝑇 ≠ ∅ ∧ 𝑀 < 𝑃 ) )