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	mullidd	⊢ ( 𝜑 → ( 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	⊢ ( 𝜑 → 𝑃 ∈ 𝑆 )