# Metamath Proof Explorer

## Theorem 4sqlem15

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

Ref Expression
Hypotheses 4sq.1 $⊢ S = n | ∃ x ∈ ℤ ∃ y ∈ ℤ ∃ z ∈ ℤ ∃ w ∈ ℤ n = x 2 + y 2 + z 2 + w 2$
4sq.2 $⊢ φ → N ∈ ℕ$
4sq.3 $⊢ φ → P = 2 ⋅ N + 1$
4sq.4 $⊢ φ → P ∈ ℙ$
4sq.5 $⊢ φ → 0 … 2 ⋅ N ⊆ S$
4sq.6 $⊢ T = i ∈ ℕ | i ⁢ P ∈ S$
4sq.7 $⊢ M = sup T ℝ <$
4sq.m $⊢ φ → M ∈ ℤ ≥ 2$
4sq.a $⊢ φ → A ∈ ℤ$
4sq.b $⊢ φ → B ∈ ℤ$
4sq.c $⊢ φ → C ∈ ℤ$
4sq.d $⊢ φ → D ∈ ℤ$
4sq.e $⊢ E = A + M 2 mod M − M 2$
4sq.f $⊢ F = B + M 2 mod M − M 2$
4sq.g $⊢ G = C + M 2 mod M − M 2$
4sq.h $⊢ H = D + M 2 mod M − M 2$
4sq.r $⊢ R = E 2 + F 2 + G 2 + H 2 M$
4sq.p $⊢ φ → M ⁢ P = A 2 + B 2 + C 2 + D 2$
Assertion 4sqlem15 $⊢ φ ∧ R = M → M 2 2 2 − E 2 = 0 ∧ M 2 2 2 − F 2 = 0 ∧ M 2 2 2 − G 2 = 0 ∧ M 2 2 2 − H 2 = 0$

### Proof

Step Hyp Ref Expression
1 4sq.1 $⊢ S = n | ∃ x ∈ ℤ ∃ y ∈ ℤ ∃ z ∈ ℤ ∃ w ∈ ℤ n = x 2 + y 2 + z 2 + w 2$
2 4sq.2 $⊢ φ → N ∈ ℕ$
3 4sq.3 $⊢ φ → P = 2 ⋅ N + 1$
4 4sq.4 $⊢ φ → P ∈ ℙ$
5 4sq.5 $⊢ φ → 0 … 2 ⋅ N ⊆ S$
6 4sq.6 $⊢ T = i ∈ ℕ | i ⁢ P ∈ S$
7 4sq.7 $⊢ M = sup T ℝ <$
8 4sq.m $⊢ φ → M ∈ ℤ ≥ 2$
9 4sq.a $⊢ φ → A ∈ ℤ$
10 4sq.b $⊢ φ → B ∈ ℤ$
11 4sq.c $⊢ φ → C ∈ ℤ$
12 4sq.d $⊢ φ → D ∈ ℤ$
13 4sq.e $⊢ E = A + M 2 mod M − M 2$
14 4sq.f $⊢ F = B + M 2 mod M − M 2$
15 4sq.g $⊢ G = C + M 2 mod M − M 2$
16 4sq.h $⊢ H = D + M 2 mod M − M 2$
17 4sq.r $⊢ R = E 2 + F 2 + G 2 + H 2 M$
18 4sq.p $⊢ φ → M ⁢ P = A 2 + B 2 + C 2 + D 2$
19 eluz2nn $⊢ M ∈ ℤ ≥ 2 → M ∈ ℕ$
20 8 19 syl $⊢ φ → M ∈ ℕ$
21 20 nnred $⊢ φ → M ∈ ℝ$
22 21 resqcld $⊢ φ → M 2 ∈ ℝ$
23 22 rehalfcld $⊢ φ → M 2 2 ∈ ℝ$
24 23 rehalfcld $⊢ φ → M 2 2 2 ∈ ℝ$
25 24 recnd $⊢ φ → M 2 2 2 ∈ ℂ$
26 9 20 13 4sqlem5 $⊢ φ → E ∈ ℤ ∧ A − E M ∈ ℤ$
27 26 simpld $⊢ φ → E ∈ ℤ$
28 zsqcl $⊢ E ∈ ℤ → E 2 ∈ ℤ$
29 27 28 syl $⊢ φ → E 2 ∈ ℤ$
30 29 zred $⊢ φ → E 2 ∈ ℝ$
31 30 recnd $⊢ φ → E 2 ∈ ℂ$
32 10 20 14 4sqlem5 $⊢ φ → F ∈ ℤ ∧ B − F M ∈ ℤ$
33 32 simpld $⊢ φ → F ∈ ℤ$
34 zsqcl $⊢ F ∈ ℤ → F 2 ∈ ℤ$
35 33 34 syl $⊢ φ → F 2 ∈ ℤ$
36 35 zred $⊢ φ → F 2 ∈ ℝ$
37 36 recnd $⊢ φ → F 2 ∈ ℂ$
38 25 25 31 37 addsub4d $⊢ φ → M 2 2 2 + M 2 2 2 - E 2 + F 2 = M 2 2 2 − E 2 + M 2 2 2 - F 2$
39 23 recnd $⊢ φ → M 2 2 ∈ ℂ$
40 39 2halvesd $⊢ φ → M 2 2 2 + M 2 2 2 = M 2 2$
41 40 oveq1d $⊢ φ → M 2 2 2 + M 2 2 2 - E 2 + F 2 = M 2 2 − E 2 + F 2$
42 38 41 eqtr3d $⊢ φ → M 2 2 2 − E 2 + M 2 2 2 - F 2 = M 2 2 − E 2 + F 2$
43 42 adantr $⊢ φ ∧ R = M → M 2 2 2 − E 2 + M 2 2 2 - F 2 = M 2 2 − E 2 + F 2$
44 22 recnd $⊢ φ → M 2 ∈ ℂ$
45 44 2halvesd $⊢ φ → M 2 2 + M 2 2 = M 2$
46 45 adantr $⊢ φ ∧ R = M → M 2 2 + M 2 2 = M 2$
47 21 recnd $⊢ φ → M ∈ ℂ$
48 47 sqvald $⊢ φ → M 2 = M ⋅ M$
49 48 adantr $⊢ φ ∧ R = M → M 2 = M ⋅ M$
50 simpr $⊢ φ ∧ R = M → R = M$
51 17 50 syl5eqr $⊢ φ ∧ R = M → E 2 + F 2 + G 2 + H 2 M = M$
52 51 oveq1d $⊢ φ ∧ R = M → E 2 + F 2 + G 2 + H 2 M ⋅ M = M ⋅ M$
53 30 36 readdcld $⊢ φ → E 2 + F 2 ∈ ℝ$
54 11 20 15 4sqlem5 $⊢ φ → G ∈ ℤ ∧ C − G M ∈ ℤ$
55 54 simpld $⊢ φ → G ∈ ℤ$
56 zsqcl $⊢ G ∈ ℤ → G 2 ∈ ℤ$
57 55 56 syl $⊢ φ → G 2 ∈ ℤ$
58 57 zred $⊢ φ → G 2 ∈ ℝ$
59 12 20 16 4sqlem5 $⊢ φ → H ∈ ℤ ∧ D − H M ∈ ℤ$
60 59 simpld $⊢ φ → H ∈ ℤ$
61 zsqcl $⊢ H ∈ ℤ → H 2 ∈ ℤ$
62 60 61 syl $⊢ φ → H 2 ∈ ℤ$
63 62 zred $⊢ φ → H 2 ∈ ℝ$
64 58 63 readdcld $⊢ φ → G 2 + H 2 ∈ ℝ$
65 53 64 readdcld $⊢ φ → E 2 + F 2 + G 2 + H 2 ∈ ℝ$
66 65 recnd $⊢ φ → E 2 + F 2 + G 2 + H 2 ∈ ℂ$
67 20 nnne0d $⊢ φ → M ≠ 0$
68 66 47 67 divcan1d $⊢ φ → E 2 + F 2 + G 2 + H 2 M ⋅ M = E 2 + F 2 + G 2 + H 2$
69 68 adantr $⊢ φ ∧ R = M → E 2 + F 2 + G 2 + H 2 M ⋅ M = E 2 + F 2 + G 2 + H 2$
70 49 52 69 3eqtr2rd $⊢ φ ∧ R = M → E 2 + F 2 + G 2 + H 2 = M 2$
71 46 70 oveq12d $⊢ φ ∧ R = M → M 2 2 + M 2 2 - E 2 + F 2 + G 2 + H 2 = M 2 − M 2$
72 53 recnd $⊢ φ → E 2 + F 2 ∈ ℂ$
73 64 recnd $⊢ φ → G 2 + H 2 ∈ ℂ$
74 39 39 72 73 addsub4d $⊢ φ → M 2 2 + M 2 2 - E 2 + F 2 + G 2 + H 2 = M 2 2 − E 2 + F 2 + M 2 2 - G 2 + H 2$
75 74 adantr $⊢ φ ∧ R = M → M 2 2 + M 2 2 - E 2 + F 2 + G 2 + H 2 = M 2 2 − E 2 + F 2 + M 2 2 - G 2 + H 2$
76 44 subidd $⊢ φ → M 2 − M 2 = 0$
77 76 adantr $⊢ φ ∧ R = M → M 2 − M 2 = 0$
78 71 75 77 3eqtr3d $⊢ φ ∧ R = M → M 2 2 − E 2 + F 2 + M 2 2 - G 2 + H 2 = 0$
79 23 53 resubcld $⊢ φ → M 2 2 − E 2 + F 2 ∈ ℝ$
80 9 20 13 4sqlem7 $⊢ φ → E 2 ≤ M 2 2 2$
81 10 20 14 4sqlem7 $⊢ φ → F 2 ≤ M 2 2 2$
82 30 36 24 24 80 81 le2addd $⊢ φ → E 2 + F 2 ≤ M 2 2 2 + M 2 2 2$
83 82 40 breqtrd $⊢ φ → E 2 + F 2 ≤ M 2 2$
84 23 53 subge0d $⊢ φ → 0 ≤ M 2 2 − E 2 + F 2 ↔ E 2 + F 2 ≤ M 2 2$
85 83 84 mpbird $⊢ φ → 0 ≤ M 2 2 − E 2 + F 2$
86 23 64 resubcld $⊢ φ → M 2 2 − G 2 + H 2 ∈ ℝ$
87 11 20 15 4sqlem7 $⊢ φ → G 2 ≤ M 2 2 2$
88 12 20 16 4sqlem7 $⊢ φ → H 2 ≤ M 2 2 2$
89 58 63 24 24 87 88 le2addd $⊢ φ → G 2 + H 2 ≤ M 2 2 2 + M 2 2 2$
90 89 40 breqtrd $⊢ φ → G 2 + H 2 ≤ M 2 2$
91 23 64 subge0d $⊢ φ → 0 ≤ M 2 2 − G 2 + H 2 ↔ G 2 + H 2 ≤ M 2 2$
92 90 91 mpbird $⊢ φ → 0 ≤ M 2 2 − G 2 + H 2$
93 add20 $⊢ M 2 2 − E 2 + F 2 ∈ ℝ ∧ 0 ≤ M 2 2 − E 2 + F 2 ∧ M 2 2 − G 2 + H 2 ∈ ℝ ∧ 0 ≤ M 2 2 − G 2 + H 2 → M 2 2 − E 2 + F 2 + M 2 2 - G 2 + H 2 = 0 ↔ M 2 2 − E 2 + F 2 = 0 ∧ M 2 2 − G 2 + H 2 = 0$
94 79 85 86 92 93 syl22anc $⊢ φ → M 2 2 − E 2 + F 2 + M 2 2 - G 2 + H 2 = 0 ↔ M 2 2 − E 2 + F 2 = 0 ∧ M 2 2 − G 2 + H 2 = 0$
95 94 biimpa $⊢ φ ∧ M 2 2 − E 2 + F 2 + M 2 2 - G 2 + H 2 = 0 → M 2 2 − E 2 + F 2 = 0 ∧ M 2 2 − G 2 + H 2 = 0$
96 78 95 syldan $⊢ φ ∧ R = M → M 2 2 − E 2 + F 2 = 0 ∧ M 2 2 − G 2 + H 2 = 0$
97 96 simpld $⊢ φ ∧ R = M → M 2 2 − E 2 + F 2 = 0$
98 43 97 eqtrd $⊢ φ ∧ R = M → M 2 2 2 − E 2 + M 2 2 2 - F 2 = 0$
99 24 30 resubcld $⊢ φ → M 2 2 2 − E 2 ∈ ℝ$
100 24 30 subge0d $⊢ φ → 0 ≤ M 2 2 2 − E 2 ↔ E 2 ≤ M 2 2 2$
101 80 100 mpbird $⊢ φ → 0 ≤ M 2 2 2 − E 2$
102 24 36 resubcld $⊢ φ → M 2 2 2 − F 2 ∈ ℝ$
103 24 36 subge0d $⊢ φ → 0 ≤ M 2 2 2 − F 2 ↔ F 2 ≤ M 2 2 2$
104 81 103 mpbird $⊢ φ → 0 ≤ M 2 2 2 − F 2$
105 add20 $⊢ M 2 2 2 − E 2 ∈ ℝ ∧ 0 ≤ M 2 2 2 − E 2 ∧ M 2 2 2 − F 2 ∈ ℝ ∧ 0 ≤ M 2 2 2 − F 2 → M 2 2 2 − E 2 + M 2 2 2 - F 2 = 0 ↔ M 2 2 2 − E 2 = 0 ∧ M 2 2 2 − F 2 = 0$
106 99 101 102 104 105 syl22anc $⊢ φ → M 2 2 2 − E 2 + M 2 2 2 - F 2 = 0 ↔ M 2 2 2 − E 2 = 0 ∧ M 2 2 2 − F 2 = 0$
107 106 biimpa $⊢ φ ∧ M 2 2 2 − E 2 + M 2 2 2 - F 2 = 0 → M 2 2 2 − E 2 = 0 ∧ M 2 2 2 − F 2 = 0$
108 98 107 syldan $⊢ φ ∧ R = M → M 2 2 2 − E 2 = 0 ∧ M 2 2 2 − F 2 = 0$
109 58 recnd $⊢ φ → G 2 ∈ ℂ$
110 63 recnd $⊢ φ → H 2 ∈ ℂ$
111 25 25 109 110 addsub4d $⊢ φ → M 2 2 2 + M 2 2 2 - G 2 + H 2 = M 2 2 2 − G 2 + M 2 2 2 - H 2$
112 40 oveq1d $⊢ φ → M 2 2 2 + M 2 2 2 - G 2 + H 2 = M 2 2 − G 2 + H 2$
113 111 112 eqtr3d $⊢ φ → M 2 2 2 − G 2 + M 2 2 2 - H 2 = M 2 2 − G 2 + H 2$
114 113 adantr $⊢ φ ∧ R = M → M 2 2 2 − G 2 + M 2 2 2 - H 2 = M 2 2 − G 2 + H 2$
115 96 simprd $⊢ φ ∧ R = M → M 2 2 − G 2 + H 2 = 0$
116 114 115 eqtrd $⊢ φ ∧ R = M → M 2 2 2 − G 2 + M 2 2 2 - H 2 = 0$
117 24 58 resubcld $⊢ φ → M 2 2 2 − G 2 ∈ ℝ$
118 24 58 subge0d $⊢ φ → 0 ≤ M 2 2 2 − G 2 ↔ G 2 ≤ M 2 2 2$
119 87 118 mpbird $⊢ φ → 0 ≤ M 2 2 2 − G 2$
120 24 63 resubcld $⊢ φ → M 2 2 2 − H 2 ∈ ℝ$
121 24 63 subge0d $⊢ φ → 0 ≤ M 2 2 2 − H 2 ↔ H 2 ≤ M 2 2 2$
122 88 121 mpbird $⊢ φ → 0 ≤ M 2 2 2 − H 2$
123 add20 $⊢ M 2 2 2 − G 2 ∈ ℝ ∧ 0 ≤ M 2 2 2 − G 2 ∧ M 2 2 2 − H 2 ∈ ℝ ∧ 0 ≤ M 2 2 2 − H 2 → M 2 2 2 − G 2 + M 2 2 2 - H 2 = 0 ↔ M 2 2 2 − G 2 = 0 ∧ M 2 2 2 − H 2 = 0$
124 117 119 120 122 123 syl22anc $⊢ φ → M 2 2 2 − G 2 + M 2 2 2 - H 2 = 0 ↔ M 2 2 2 − G 2 = 0 ∧ M 2 2 2 − H 2 = 0$
125 124 biimpa $⊢ φ ∧ M 2 2 2 − G 2 + M 2 2 2 - H 2 = 0 → M 2 2 2 − G 2 = 0 ∧ M 2 2 2 − H 2 = 0$
126 116 125 syldan $⊢ φ ∧ R = M → M 2 2 2 − G 2 = 0 ∧ M 2 2 2 − H 2 = 0$
127 108 126 jca $⊢ φ ∧ R = M → M 2 2 2 − E 2 = 0 ∧ M 2 2 2 − F 2 = 0 ∧ M 2 2 2 − G 2 = 0 ∧ M 2 2 2 − H 2 = 0$