Theorem 4sqlemsdc 12991

Description: Lemma for 4sq 13001. The property of being the sum of four squares is decidable.

The proof involves showing that (for a particular 𝐴) there are only a finite number of possible ways that it could be the sum of four squares, so checking each of those possibilities in turn decides whether the number is the sum of four squares. If this proof is hard to follow, especially because of its length, the simplified versions at 4sqexercise1 12989 and 4sqexercise2 12990 may help clarify, as they are using very much the same techniques on simplified versions of this lemma. (Contributed by Jim Kingdon, 25-May-2025.)

Hypothesis

Ref	Expression
4sqlem11.1	⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}

Assertion

Ref	Expression
4sqlemsdc	⊢ (𝐴 ∈ ℕ0 → DECID 𝐴 ∈ 𝑆)

Distinct variable group:   𝐴,𝑛,𝑤,𝑥,𝑦,𝑧

Allowed substitution hints:   𝑆(𝑥,𝑦,𝑧,𝑤,𝑛)

Proof of Theorem 4sqlemsdc

Step	Hyp	Ref	Expression
1		nn0negz 9513	. . . 4 ⊢ (𝐴 ∈ ℕ0 → -𝐴 ∈ ℤ)
2		nn0z 9499	. . . 4 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ)
3	1	adantr 276	. . . . . 6 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) → -𝐴 ∈ ℤ)
4	2	adantr 276	. . . . . 6 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) → 𝐴 ∈ ℤ)
5	3	adantr 276	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) → -𝐴 ∈ ℤ)
6	4	adantr 276	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) → 𝐴 ∈ ℤ)
7	5	adantr 276	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) → -𝐴 ∈ ℤ)
8	6	adantr 276	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) → 𝐴 ∈ ℤ)
9	8	adantr 276	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ (-𝐴...𝐴)) → 𝐴 ∈ ℤ)
10		elfzelz 10260	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (-𝐴...𝐴) → 𝑥 ∈ ℤ)
11	10	ad4antlr 495	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ (-𝐴...𝐴)) → 𝑥 ∈ ℤ)
12		zsqcl2 10880	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℤ → (𝑥↑2) ∈ ℕ0)
13	11, 12	syl 14	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ (-𝐴...𝐴)) → (𝑥↑2) ∈ ℕ0)
14		elfzelz 10260	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (-𝐴...𝐴) → 𝑦 ∈ ℤ)
15	14	ad3antlr 493	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ (-𝐴...𝐴)) → 𝑦 ∈ ℤ)
16		zsqcl2 10880	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℤ → (𝑦↑2) ∈ ℕ0)
17	15, 16	syl 14	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ (-𝐴...𝐴)) → (𝑦↑2) ∈ ℕ0)
18	13, 17	nn0addcld 9459	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ (-𝐴...𝐴)) → ((𝑥↑2) + (𝑦↑2)) ∈ ℕ0)
19		elfzelz 10260	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (-𝐴...𝐴) → 𝑧 ∈ ℤ)
20	19	ad2antlr 489	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ (-𝐴...𝐴)) → 𝑧 ∈ ℤ)
21		zsqcl2 10880	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈ ℕ0)
22	20, 21	syl 14	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ (-𝐴...𝐴)) → (𝑧↑2) ∈ ℕ0)
23		elfzelz 10260	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (-𝐴...𝐴) → 𝑤 ∈ ℤ)
24	23	adantl 277	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ (-𝐴...𝐴)) → 𝑤 ∈ ℤ)
25		zsqcl2 10880	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ ℤ → (𝑤↑2) ∈ ℕ0)
26	24, 25	syl 14	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ (-𝐴...𝐴)) → (𝑤↑2) ∈ ℕ0)
27	22, 26	nn0addcld 9459	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ (-𝐴...𝐴)) → ((𝑧↑2) + (𝑤↑2)) ∈ ℕ0)
28	18, 27	nn0addcld 9459	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ (-𝐴...𝐴)) → (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ∈ ℕ0)
29	28	nn0zd 9600	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ (-𝐴...𝐴)) → (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ∈ ℤ)
30		zdceq 9555	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ∈ ℤ) → DECID 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
31	9, 29, 30	syl2anc 411	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ (-𝐴...𝐴)) → DECID 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
32	7, 8, 31	exfzdc 10487	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) → DECID ∃𝑤 ∈ (-𝐴...𝐴)𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
33	1	ad5antr 496	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → -𝐴 ∈ ℤ)
34	2	ad5antr 496	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → 𝐴 ∈ ℤ)
35		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → 𝑤 ∈ ℤ)
36	35	zred 9602	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → 𝑤 ∈ ℝ)
37	34	zred 9602	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → 𝐴 ∈ ℝ)
38	36	renegcld 8559	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → -𝑤 ∈ ℝ)
39	36	resqcld 10962	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → (𝑤↑2) ∈ ℝ)
40	35	znegcld 9604	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → -𝑤 ∈ ℤ)
41		zzlesq 10971	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-𝑤 ∈ ℤ → -𝑤 ≤ (-𝑤↑2))
42	40, 41	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → -𝑤 ≤ (-𝑤↑2))
43	35	zcnd 9603	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → 𝑤 ∈ ℂ)
44		sqneg 10861	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℂ → (-𝑤↑2) = (𝑤↑2))
45	43, 44	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → (-𝑤↑2) = (𝑤↑2))
46	42, 45	breqtrd 4114	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → -𝑤 ≤ (𝑤↑2))
47	19	ad3antlr 493	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → 𝑧 ∈ ℤ)
48	47, 21	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → (𝑧↑2) ∈ ℕ0)
49	25	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → (𝑤↑2) ∈ ℕ0)
50	48, 49	nn0addcld 9459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → ((𝑧↑2) + (𝑤↑2)) ∈ ℕ0)
51	50	nn0red 9456	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → ((𝑧↑2) + (𝑤↑2)) ∈ ℝ)
52	10	ad5antlr 497	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → 𝑥 ∈ ℤ)
53	52, 12	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → (𝑥↑2) ∈ ℕ0)
54	14	ad4antlr 495	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → 𝑦 ∈ ℤ)
55	54, 16	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → (𝑦↑2) ∈ ℕ0)
56	53, 55	nn0addcld 9459	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → ((𝑥↑2) + (𝑦↑2)) ∈ ℕ0)
57	56, 50	nn0addcld 9459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ∈ ℕ0)
58	57	nn0red 9456	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ∈ ℝ)
59		nn0addge2 9449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑤↑2) ∈ ℝ ∧ (𝑧↑2) ∈ ℕ0) → (𝑤↑2) ≤ ((𝑧↑2) + (𝑤↑2)))
60	39, 48, 59	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → (𝑤↑2) ≤ ((𝑧↑2) + (𝑤↑2)))
61		nn0addge2 9449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑧↑2) + (𝑤↑2)) ∈ ℝ ∧ ((𝑥↑2) + (𝑦↑2)) ∈ ℕ0) → ((𝑧↑2) + (𝑤↑2)) ≤ (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
62	51, 56, 61	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → ((𝑧↑2) + (𝑤↑2)) ≤ (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
63	39, 51, 58, 60, 62	letrd 8303	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → (𝑤↑2) ≤ (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
64		simplr 529	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
65	63, 64	breqtrrd 4116	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → (𝑤↑2) ≤ 𝐴)
66	38, 39, 37, 46, 65	letrd 8303	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → -𝑤 ≤ 𝐴)
67	36, 37, 66	lenegcon1d 8707	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → -𝐴 ≤ 𝑤)
68		zzlesq 10971	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℤ → 𝑤 ≤ (𝑤↑2))
69	68	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → 𝑤 ≤ (𝑤↑2))
70	36, 39, 37, 69, 65	letrd 8303	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → 𝑤 ≤ 𝐴)
71	33, 34, 35, 67, 70	elfzd 10251	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑤 ∈ ℤ) → 𝑤 ∈ (-𝐴...𝐴))
72	71	ex 115	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) → (𝑤 ∈ ℤ → 𝑤 ∈ (-𝐴...𝐴)))
73	72, 23	impbid1 142	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) → (𝑤 ∈ ℤ ↔ 𝑤 ∈ (-𝐴...𝐴)))
74	73	ex 115	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) → (𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) → (𝑤 ∈ ℤ ↔ 𝑤 ∈ (-𝐴...𝐴))))
75	74	pm5.32rd 451	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) → ((𝑤 ∈ ℤ ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ↔ (𝑤 ∈ (-𝐴...𝐴) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))))
76	75	rexbidv2 2535	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) → (∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ↔ ∃𝑤 ∈ (-𝐴...𝐴)𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))))
77	76	dcbid 845	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) → (DECID ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ↔ DECID ∃𝑤 ∈ (-𝐴...𝐴)𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))))
78	32, 77	mpbird 167	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ (-𝐴...𝐴)) → DECID ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
79	5, 6, 78	exfzdc 10487	. . . . . . 7 ⊢ (((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) → DECID ∃𝑧 ∈ (-𝐴...𝐴)∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
80	1	ad5antr 496	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → -𝐴 ∈ ℤ)
81	2	ad5antr 496	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → 𝐴 ∈ ℤ)
82		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℤ)
83	82	zred 9602	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℝ)
84	81	zred 9602	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → 𝐴 ∈ ℝ)
85	83	renegcld 8559	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → -𝑧 ∈ ℝ)
86	83	resqcld 10962	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → (𝑧↑2) ∈ ℝ)
87	82	znegcld 9604	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → -𝑧 ∈ ℤ)
88		zzlesq 10971	. . . . . . . . . . . . . . . . . 18 ⊢ (-𝑧 ∈ ℤ → -𝑧 ≤ (-𝑧↑2))
89	87, 88	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → -𝑧 ≤ (-𝑧↑2))
90	82	zcnd 9603	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℂ)
91		sqneg 10861	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℂ → (-𝑧↑2) = (𝑧↑2))
92	90, 91	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → (-𝑧↑2) = (𝑧↑2))
93	89, 92	breqtrd 4114	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → -𝑧 ≤ (𝑧↑2))
94	21	adantl 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → (𝑧↑2) ∈ ℕ0)
95	25	ad3antlr 493	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → (𝑤↑2) ∈ ℕ0)
96	94, 95	nn0addcld 9459	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → ((𝑧↑2) + (𝑤↑2)) ∈ ℕ0)
97	96	nn0red 9456	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → ((𝑧↑2) + (𝑤↑2)) ∈ ℝ)
98	10	ad5antlr 497	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → 𝑥 ∈ ℤ)
99	98, 12	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → (𝑥↑2) ∈ ℕ0)
100	14	ad4antlr 495	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → 𝑦 ∈ ℤ)
101	100, 16	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → (𝑦↑2) ∈ ℕ0)
102	99, 101	nn0addcld 9459	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → ((𝑥↑2) + (𝑦↑2)) ∈ ℕ0)
103	102, 96	nn0addcld 9459	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ∈ ℕ0)
104	103	nn0red 9456	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ∈ ℝ)
105		nn0addge1 9448	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧↑2) ∈ ℝ ∧ (𝑤↑2) ∈ ℕ0) → (𝑧↑2) ≤ ((𝑧↑2) + (𝑤↑2)))
106	86, 95, 105	syl2anc 411	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → (𝑧↑2) ≤ ((𝑧↑2) + (𝑤↑2)))
107	97, 102, 61	syl2anc 411	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → ((𝑧↑2) + (𝑤↑2)) ≤ (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
108	86, 97, 104, 106, 107	letrd 8303	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → (𝑧↑2) ≤ (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
109		simplr 529	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
110	108, 109	breqtrrd 4116	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → (𝑧↑2) ≤ 𝐴)
111	85, 86, 84, 93, 110	letrd 8303	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → -𝑧 ≤ 𝐴)
112	83, 84, 111	lenegcon1d 8707	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → -𝐴 ≤ 𝑧)
113		zzlesq 10971	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℤ → 𝑧 ≤ (𝑧↑2))
114	113	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → 𝑧 ≤ (𝑧↑2))
115	83, 86, 84, 114, 110	letrd 8303	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → 𝑧 ≤ 𝐴)
116	80, 81, 82, 112, 115	elfzd 10251	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ (-𝐴...𝐴))
117	116	ex 115	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) → (𝑧 ∈ ℤ → 𝑧 ∈ (-𝐴...𝐴)))
118	117, 19	impbid1 142	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) → (𝑧 ∈ ℤ ↔ 𝑧 ∈ (-𝐴...𝐴)))
119	118	rexlimdva2 2653	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) → (∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) → (𝑧 ∈ ℤ ↔ 𝑧 ∈ (-𝐴...𝐴))))
120	119	pm5.32rd 451	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) → ((𝑧 ∈ ℤ ∧ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ↔ (𝑧 ∈ (-𝐴...𝐴) ∧ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))))
121	120	rexbidv2 2535	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) → (∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ↔ ∃𝑧 ∈ (-𝐴...𝐴)∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))))
122	121	dcbid 845	. . . . . . 7 ⊢ (((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) → (DECID ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ↔ DECID ∃𝑧 ∈ (-𝐴...𝐴)∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))))
123	79, 122	mpbird 167	. . . . . 6 ⊢ (((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑦 ∈ (-𝐴...𝐴)) → DECID ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
124	3, 4, 123	exfzdc 10487	. . . . 5 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) → DECID ∃𝑦 ∈ (-𝐴...𝐴)∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
125	1	ad5antr 496	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → -𝐴 ∈ ℤ)
126	2	ad5antr 496	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → 𝐴 ∈ ℤ)
127		simpr 110	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ ℤ)
128	127	zred 9602	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ ℝ)
129	126	zred 9602	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → 𝐴 ∈ ℝ)
130	128	renegcld 8559	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → -𝑦 ∈ ℝ)
131	128	resqcld 10962	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → (𝑦↑2) ∈ ℝ)
132	127	znegcld 9604	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → -𝑦 ∈ ℤ)
133		zzlesq 10971	. . . . . . . . . . . . . . . . 17 ⊢ (-𝑦 ∈ ℤ → -𝑦 ≤ (-𝑦↑2))
134	132, 133	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → -𝑦 ≤ (-𝑦↑2))
135	127	zcnd 9603	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ ℂ)
136		sqneg 10861	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℂ → (-𝑦↑2) = (𝑦↑2))
137	135, 136	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → (-𝑦↑2) = (𝑦↑2))
138	134, 137	breqtrd 4114	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → -𝑦 ≤ (𝑦↑2))
139	10	ad5antlr 497	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → 𝑥 ∈ ℤ)
140	139, 12	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → (𝑥↑2) ∈ ℕ0)
141	16	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → (𝑦↑2) ∈ ℕ0)
142	140, 141	nn0addcld 9459	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → ((𝑥↑2) + (𝑦↑2)) ∈ ℕ0)
143	142	nn0red 9456	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → ((𝑥↑2) + (𝑦↑2)) ∈ ℝ)
144	21	ad4antlr 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → (𝑧↑2) ∈ ℕ0)
145	25	ad3antlr 493	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → (𝑤↑2) ∈ ℕ0)
146	144, 145	nn0addcld 9459	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → ((𝑧↑2) + (𝑤↑2)) ∈ ℕ0)
147	142, 146	nn0addcld 9459	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ∈ ℕ0)
148	147	nn0red 9456	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ∈ ℝ)
149		nn0addge2 9449	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦↑2) ∈ ℝ ∧ (𝑥↑2) ∈ ℕ0) → (𝑦↑2) ≤ ((𝑥↑2) + (𝑦↑2)))
150	131, 140, 149	syl2anc 411	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → (𝑦↑2) ≤ ((𝑥↑2) + (𝑦↑2)))
151		nn0addge1 9448	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥↑2) + (𝑦↑2)) ∈ ℝ ∧ ((𝑧↑2) + (𝑤↑2)) ∈ ℕ0) → ((𝑥↑2) + (𝑦↑2)) ≤ (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
152	143, 146, 151	syl2anc 411	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → ((𝑥↑2) + (𝑦↑2)) ≤ (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
153	131, 143, 148, 150, 152	letrd 8303	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → (𝑦↑2) ≤ (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
154		simplr 529	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
155	153, 154	breqtrrd 4116	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → (𝑦↑2) ≤ 𝐴)
156	130, 131, 129, 138, 155	letrd 8303	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → -𝑦 ≤ 𝐴)
157	128, 129, 156	lenegcon1d 8707	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → -𝐴 ≤ 𝑦)
158		zzlesq 10971	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℤ → 𝑦 ≤ (𝑦↑2))
159	158	adantl 277	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → 𝑦 ≤ (𝑦↑2))
160	128, 131, 129, 159, 155	letrd 8303	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → 𝑦 ≤ 𝐴)
161	125, 126, 127, 157, 160	elfzd 10251	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ (-𝐴...𝐴))
162	161	ex 115	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) → (𝑦 ∈ ℤ → 𝑦 ∈ (-𝐴...𝐴)))
163	162, 14	impbid1 142	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) → (𝑦 ∈ ℤ ↔ 𝑦 ∈ (-𝐴...𝐴)))
164	163	r19.29an 2675	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) ∧ 𝑧 ∈ ℤ) ∧ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) → (𝑦 ∈ ℤ ↔ 𝑦 ∈ (-𝐴...𝐴)))
165	164	rexlimdva2 2653	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) → (∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) → (𝑦 ∈ ℤ ↔ 𝑦 ∈ (-𝐴...𝐴))))
166	165	pm5.32rd 451	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) → ((𝑦 ∈ ℤ ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ↔ (𝑦 ∈ (-𝐴...𝐴) ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))))
167	166	rexbidv2 2535	. . . . . 6 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) → (∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ↔ ∃𝑦 ∈ (-𝐴...𝐴)∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))))
168	167	dcbid 845	. . . . 5 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) → (DECID ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ↔ DECID ∃𝑦 ∈ (-𝐴...𝐴)∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))))
169	124, 168	mpbird 167	. . . 4 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝑥 ∈ (-𝐴...𝐴)) → DECID ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
170	1, 2, 169	exfzdc 10487	. . 3 ⊢ (𝐴 ∈ ℕ0 → DECID ∃𝑥 ∈ (-𝐴...𝐴)∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
171	1	ad5antr 496	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → -𝐴 ∈ ℤ)
172	2	ad5antr 496	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → 𝐴 ∈ ℤ)
173		simpr 110	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℤ)
174	173	zred 9602	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℝ)
175	172	zred 9602	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → 𝐴 ∈ ℝ)
176	174	renegcld 8559	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → -𝑥 ∈ ℝ)
177	174	resqcld 10962	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → (𝑥↑2) ∈ ℝ)
178	173	znegcld 9604	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → -𝑥 ∈ ℤ)
179		zzlesq 10971	. . . . . . . . . . . . . . . 16 ⊢ (-𝑥 ∈ ℤ → -𝑥 ≤ (-𝑥↑2))
180	178, 179	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → -𝑥 ≤ (-𝑥↑2))
181	173	zcnd 9603	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℂ)
182		sqneg 10861	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → (-𝑥↑2) = (𝑥↑2))
183	181, 182	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → (-𝑥↑2) = (𝑥↑2))
184	180, 183	breqtrd 4114	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → -𝑥 ≤ (𝑥↑2))
185	12	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → (𝑥↑2) ∈ ℕ0)
186	16	ad5antlr 497	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → (𝑦↑2) ∈ ℕ0)
187	185, 186	nn0addcld 9459	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → ((𝑥↑2) + (𝑦↑2)) ∈ ℕ0)
188	187	nn0red 9456	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → ((𝑥↑2) + (𝑦↑2)) ∈ ℝ)
189	21	ad4antlr 495	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → (𝑧↑2) ∈ ℕ0)
190	25	ad3antlr 493	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → (𝑤↑2) ∈ ℕ0)
191	189, 190	nn0addcld 9459	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → ((𝑧↑2) + (𝑤↑2)) ∈ ℕ0)
192	187, 191	nn0addcld 9459	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ∈ ℕ0)
193	192	nn0red 9456	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ∈ ℝ)
194		nn0addge1 9448	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥↑2) ∈ ℝ ∧ (𝑦↑2) ∈ ℕ0) → (𝑥↑2) ≤ ((𝑥↑2) + (𝑦↑2)))
195	177, 186, 194	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → (𝑥↑2) ≤ ((𝑥↑2) + (𝑦↑2)))
196	188, 191, 151	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → ((𝑥↑2) + (𝑦↑2)) ≤ (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
197	177, 188, 193, 195, 196	letrd 8303	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → (𝑥↑2) ≤ (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
198		simplr 529	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
199	197, 198	breqtrrd 4116	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → (𝑥↑2) ≤ 𝐴)
200	176, 177, 175, 184, 199	letrd 8303	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → -𝑥 ≤ 𝐴)
201	174, 175, 200	lenegcon1d 8707	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → -𝐴 ≤ 𝑥)
202		zzlesq 10971	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℤ → 𝑥 ≤ (𝑥↑2))
203	202	adantl 277	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → 𝑥 ≤ (𝑥↑2))
204	174, 177, 175, 203, 199	letrd 8303	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → 𝑥 ≤ 𝐴)
205	171, 172, 173, 201, 204	elfzd 10251	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ (-𝐴...𝐴))
206	205	ex 115	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) → (𝑥 ∈ ℤ → 𝑥 ∈ (-𝐴...𝐴)))
207	206, 10	impbid1 142	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 ∈ ℤ) ∧ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) → (𝑥 ∈ ℤ ↔ 𝑥 ∈ (-𝐴...𝐴)))
208	207	r19.29an 2675	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) → (𝑥 ∈ ℤ ↔ 𝑥 ∈ (-𝐴...𝐴)))
209	208	r19.29an 2675	. . . . . . 7 ⊢ (((𝐴 ∈ ℕ0 ∧ 𝑦 ∈ ℤ) ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) → (𝑥 ∈ ℤ ↔ 𝑥 ∈ (-𝐴...𝐴)))
210	209	rexlimdva2 2653	. . . . . 6 ⊢ (𝐴 ∈ ℕ0 → (∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) → (𝑥 ∈ ℤ ↔ 𝑥 ∈ (-𝐴...𝐴))))
211	210	pm5.32rd 451	. . . . 5 ⊢ (𝐴 ∈ ℕ0 → ((𝑥 ∈ ℤ ∧ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))) ↔ (𝑥 ∈ (-𝐴...𝐴) ∧ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))))
212	211	rexbidv2 2535	. . . 4 ⊢ (𝐴 ∈ ℕ0 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ↔ ∃𝑥 ∈ (-𝐴...𝐴)∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))))
213	212	dcbid 845	. . 3 ⊢ (𝐴 ∈ ℕ0 → (DECID ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ↔ DECID ∃𝑥 ∈ (-𝐴...𝐴)∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))))
214	170, 213	mpbird 167	. 2 ⊢ (𝐴 ∈ ℕ0 → DECID ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))))
215		eqeq1 2238	. . . . . 6 ⊢ (𝑛 = 𝐴 → (𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ↔ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))))
216	215	2rexbidv 2557	. . . . 5 ⊢ (𝑛 = 𝐴 → (∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ↔ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))))
217	216	2rexbidv 2557	. . . 4 ⊢ (𝑛 = 𝐴 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))))
218		4sqlem11.1	. . . 4 ⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
219	217, 218	elab2g 2953	. . 3 ⊢ (𝐴 ∈ ℕ0 → (𝐴 ∈ 𝑆 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))))
220	219	dcbid 845	. 2 ⊢ (𝐴 ∈ ℕ0 → (DECID 𝐴 ∈ 𝑆 ↔ DECID ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝐴 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))))
221	214, 220	mpbird 167	1 ⊢ (𝐴 ∈ ℕ0 → DECID 𝐴 ∈ 𝑆)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  DECID wdc 841   = wceq 1397   ∈ wcel 2202  {cab 2217  ∃wrex 2511   class class class wbr 4088  (class class class)co 6018  ℂcc 8030  ℝcr 8031   + caddc 8035   ≤ cle 8215  -cneg 8351  2c2 9194  ℕ₀cn0 9402  ℤcz 9479  ...cfz 10243  ↑cexp 10801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-coll 4204  ax-sep 4207  ax-nul 4215  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-iinf 4686  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-mulrcl 8131  ax-addcom 8132  ax-mulcom 8133  ax-addass 8134  ax-mulass 8135  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-1rid 8139  ax-0id 8140  ax-rnegex 8141  ax-precex 8142  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-apti 8147  ax-pre-ltadd 8148  ax-pre-mulgt0 8149  ax-pre-mulext 8150

This theorem depends on definitions:  df-bi 117  df-dc 842  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rmo 2518  df-rab 2519  df-v 2804  df-sbc 3032  df-csb 3128  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-nul 3495  df-if 3606  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-iun 3972  df-br 4089  df-opab 4151  df-mpt 4152  df-tr 4188  df-id 4390  df-po 4393  df-iso 4394  df-iord 4463  df-on 4465  df-ilim 4466  df-suc 4468  df-iom 4689  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-f1 5331  df-fo 5332  df-f1o 5333  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-1st 6303  df-2nd 6304  df-recs 6471  df-frec 6557  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-reap 8755  df-ap 8762  df-div 8853  df-inn 9144  df-2 9202  df-n0 9403  df-z 9480  df-uz 9756  df-fz 10244  df-fzo 10378  df-seqfrec 10711  df-exp 10802

This theorem is referenced by:  4sqlem13m  12994  4sqlem14  12995  4sqlem17  12998  4sqlem18  12999