MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4sqlem18 Structured version   Visualization version   GIF version

Theorem 4sqlem18 16934
Description: Lemma for 4sq 16936. Inductive step, odd prime case. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
Hypotheses
Ref Expression
4sq.1 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
4sq.2 (𝜑𝑁 ∈ ℕ)
4sq.3 (𝜑𝑃 = ((2 · 𝑁) + 1))
4sq.4 (𝜑𝑃 ∈ ℙ)
4sq.5 (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)
4sq.6 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}
4sq.7 𝑀 = inf(𝑇, ℝ, < )
Assertion
Ref Expression
4sqlem18 (𝜑𝑃𝑆)
Distinct variable groups:   𝑤,𝑛,𝑥,𝑦,𝑧   𝑖,𝑛,𝑀   𝑛,𝑁   𝑃,𝑖,𝑛   𝜑,𝑛   𝑆,𝑖,𝑛
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑖)   𝑃(𝑥,𝑦,𝑧,𝑤)   𝑆(𝑥,𝑦,𝑧,𝑤)   𝑇(𝑥,𝑦,𝑧,𝑤,𝑖,𝑛)   𝑀(𝑥,𝑦,𝑧,𝑤)   𝑁(𝑥,𝑦,𝑧,𝑤,𝑖)

Proof of Theorem 4sqlem18
Dummy variables 𝑎 𝑏 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 4sq.4 . . . . 5 (𝜑𝑃 ∈ ℙ)
2 prmnn 16648 . . . . 5 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
31, 2syl 17 . . . 4 (𝜑𝑃 ∈ ℕ)
43nncnd 12261 . . 3 (𝜑𝑃 ∈ ℂ)
54mullidd 11264 . 2 (𝜑 → (1 · 𝑃) = 𝑃)
6 4sq.7 . . . . . . . . . . . 12 𝑀 = inf(𝑇, ℝ, < )
7 4sq.6 . . . . . . . . . . . . . . 15 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}
87ssrab3 4076 . . . . . . . . . . . . . 14 𝑇 ⊆ ℕ
9 nnuz 12898 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
108, 9sseqtri 4013 . . . . . . . . . . . . 13 𝑇 ⊆ (ℤ‘1)
11 4sq.1 . . . . . . . . . . . . . . 15 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
12 4sq.2 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℕ)
13 4sq.3 . . . . . . . . . . . . . . 15 (𝜑𝑃 = ((2 · 𝑁) + 1))
14 4sq.5 . . . . . . . . . . . . . . 15 (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)
1511, 12, 13, 1, 14, 7, 64sqlem13 16929 . . . . . . . . . . . . . 14 (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃))
1615simpld 493 . . . . . . . . . . . . 13 (𝜑𝑇 ≠ ∅)
17 infssuzcl 12949 . . . . . . . . . . . . 13 ((𝑇 ⊆ (ℤ‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇)
1810, 16, 17sylancr 585 . . . . . . . . . . . 12 (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇)
196, 18eqeltrid 2829 . . . . . . . . . . 11 (𝜑𝑀𝑇)
20 oveq1 7426 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → (𝑖 · 𝑃) = (𝑀 · 𝑃))
2120eleq1d 2810 . . . . . . . . . . . 12 (𝑖 = 𝑀 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑀 · 𝑃) ∈ 𝑆))
2221, 7elrab2 3682 . . . . . . . . . . 11 (𝑀𝑇 ↔ (𝑀 ∈ ℕ ∧ (𝑀 · 𝑃) ∈ 𝑆))
2319, 22sylib 217 . . . . . . . . . 10 (𝜑 → (𝑀 ∈ ℕ ∧ (𝑀 · 𝑃) ∈ 𝑆))
2423simprd 494 . . . . . . . . 9 (𝜑 → (𝑀 · 𝑃) ∈ 𝑆)
25114sqlem2 16921 . . . . . . . . 9 ((𝑀 · 𝑃) ∈ 𝑆 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
2624, 25sylib 217 . . . . . . . 8 (𝜑 → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
2726adantr 479 . . . . . . 7 ((𝜑𝑀 ∈ (ℤ‘2)) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
28 simp1l 1194 . . . . . . . . . . . . . 14 (((𝜑𝑀 ∈ (ℤ‘2)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝜑)
2928, 12syl 17 . . . . . . . . . . . . 13 (((𝜑𝑀 ∈ (ℤ‘2)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑁 ∈ ℕ)
3028, 13syl 17 . . . . . . . . . . . . 13 (((𝜑𝑀 ∈ (ℤ‘2)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑃 = ((2 · 𝑁) + 1))
3128, 1syl 17 . . . . . . . . . . . . 13 (((𝜑𝑀 ∈ (ℤ‘2)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑃 ∈ ℙ)
3228, 14syl 17 . . . . . . . . . . . . 13 (((𝜑𝑀 ∈ (ℤ‘2)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → (0...(2 · 𝑁)) ⊆ 𝑆)
33 simp1r 1195 . . . . . . . . . . . . 13 (((𝜑𝑀 ∈ (ℤ‘2)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑀 ∈ (ℤ‘2))
34 simp2ll 1237 . . . . . . . . . . . . 13 (((𝜑𝑀 ∈ (ℤ‘2)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑎 ∈ ℤ)
35 simp2lr 1238 . . . . . . . . . . . . 13 (((𝜑𝑀 ∈ (ℤ‘2)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑏 ∈ ℤ)
36 simp2rl 1239 . . . . . . . . . . . . 13 (((𝜑𝑀 ∈ (ℤ‘2)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑐 ∈ ℤ)
37 simp2rr 1240 . . . . . . . . . . . . 13 (((𝜑𝑀 ∈ (ℤ‘2)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑑 ∈ ℤ)
38 eqid 2725 . . . . . . . . . . . . 13 (((𝑎 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑎 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
39 eqid 2725 . . . . . . . . . . . . 13 (((𝑏 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑏 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
40 eqid 2725 . . . . . . . . . . . . 13 (((𝑐 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑐 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
41 eqid 2725 . . . . . . . . . . . . 13 (((𝑑 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑑 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
42 eqid 2725 . . . . . . . . . . . . 13 (((((((𝑎 + (𝑀 / 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 1135 . . . . . . . . . . . . 13 (((𝜑𝑀 ∈ (ℤ‘2)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
4411, 29, 30, 31, 32, 7, 6, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 434sqlem17 16933 . . . . . . . . . . . 12 ¬ ((𝜑𝑀 ∈ (ℤ‘2)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
4544pm2.21i 119 . . . . . . . . . . 11 (((𝜑𝑀 ∈ (ℤ‘2)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → ¬ 𝑀 ∈ (ℤ‘2))
46453expia 1118 . . . . . . . . . 10 (((𝜑𝑀 ∈ (ℤ‘2)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ))) → ((𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ¬ 𝑀 ∈ (ℤ‘2)))
4746anassrs 466 . . . . . . . . 9 ((((𝜑𝑀 ∈ (ℤ‘2)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) → ((𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ¬ 𝑀 ∈ (ℤ‘2)))
4847rexlimdvva 3201 . . . . . . . 8 (((𝜑𝑀 ∈ (ℤ‘2)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ¬ 𝑀 ∈ (ℤ‘2)))
4948rexlimdvva 3201 . . . . . . 7 ((𝜑𝑀 ∈ (ℤ‘2)) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ¬ 𝑀 ∈ (ℤ‘2)))
5027, 49mpd 15 . . . . . 6 ((𝜑𝑀 ∈ (ℤ‘2)) → ¬ 𝑀 ∈ (ℤ‘2))
5150pm2.01da 797 . . . . 5 (𝜑 → ¬ 𝑀 ∈ (ℤ‘2))
5223simpld 493 . . . . . . 7 (𝜑𝑀 ∈ ℕ)
53 elnn1uz2 12942 . . . . . . 7 (𝑀 ∈ ℕ ↔ (𝑀 = 1 ∨ 𝑀 ∈ (ℤ‘2)))
5452, 53sylib 217 . . . . . 6 (𝜑 → (𝑀 = 1 ∨ 𝑀 ∈ (ℤ‘2)))
5554ord 862 . . . . 5 (𝜑 → (¬ 𝑀 = 1 → 𝑀 ∈ (ℤ‘2)))
5651, 55mt3d 148 . . . 4 (𝜑𝑀 = 1)
5756, 19eqeltrrd 2826 . . 3 (𝜑 → 1 ∈ 𝑇)
58 oveq1 7426 . . . . . 6 (𝑖 = 1 → (𝑖 · 𝑃) = (1 · 𝑃))
5958eleq1d 2810 . . . . 5 (𝑖 = 1 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (1 · 𝑃) ∈ 𝑆))
6059, 7elrab2 3682 . . . 4 (1 ∈ 𝑇 ↔ (1 ∈ ℕ ∧ (1 · 𝑃) ∈ 𝑆))
6160simprbi 495 . . 3 (1 ∈ 𝑇 → (1 · 𝑃) ∈ 𝑆)
6257, 61syl 17 . 2 (𝜑 → (1 · 𝑃) ∈ 𝑆)
635, 62eqeltrrd 2826 1 (𝜑𝑃𝑆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  wo 845  w3a 1084   = wceq 1533  wcel 2098  {cab 2702  wne 2929  wrex 3059  {crab 3418  wss 3944  c0 4322   class class class wbr 5149  cfv 6549  (class class class)co 7419  infcinf 9466  cr 11139  0cc0 11140  1c1 11141   + caddc 11143   · cmul 11145   < clt 11280  cmin 11476   / cdiv 11903  cn 12245  2c2 12300  cz 12591  cuz 12855  ...cfz 13519   mod cmo 13870  cexp 14062  cprime 16645
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217  ax-pre-sup 11218
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-oadd 8491  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-sup 9467  df-inf 9468  df-dju 9926  df-card 9964  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-div 11904  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-n0 12506  df-xnn0 12578  df-z 12592  df-uz 12856  df-rp 13010  df-fz 13520  df-fl 13793  df-mod 13871  df-seq 14003  df-exp 14063  df-hash 14326  df-cj 15082  df-re 15083  df-im 15084  df-sqrt 15218  df-abs 15219  df-dvds 16235  df-gcd 16473  df-prm 16646  df-gz 16902
This theorem is referenced by:  4sqlem19  16935
  Copyright terms: Public domain W3C validator