Theorem 4sqlem14 16900

Description: Lemma for 4sq 16906. (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(𝑇, ℝ, < )
4sq.m	⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))
4sq.a	⊢ (𝜑 → 𝐴 ∈ ℤ)
4sq.b	⊢ (𝜑 → 𝐵 ∈ ℤ)
4sq.c	⊢ (𝜑 → 𝐶 ∈ ℤ)
4sq.d	⊢ (𝜑 → 𝐷 ∈ ℤ)
4sq.e	⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
4sq.f	⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
4sq.g	⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
4sq.h	⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
4sq.r	⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)
4sq.p	⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))

Assertion

Ref	Expression
4sqlem14	⊢ (𝜑 → 𝑅 ∈ ℕ0)

Distinct variable groups:   𝑤,𝑛,𝑥,𝑦,𝑧   𝐵,𝑛   𝑛,𝐸   𝑛,𝐺   𝑛,𝐻   𝐴,𝑛   𝐶,𝑛   𝐷,𝑛   𝑛,𝐹   𝑖,𝑛,𝑀   𝑛,𝑁   𝑃,𝑖,𝑛   𝜑,𝑛   𝑆,𝑖,𝑛   𝑅,𝑖

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐴(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐵(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐶(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑖)   𝑃(𝑥,𝑦,𝑧,𝑤)   𝑅(𝑥,𝑦,𝑧,𝑤,𝑛)   𝑆(𝑥,𝑦,𝑧,𝑤)   𝑇(𝑥,𝑦,𝑧,𝑤,𝑖,𝑛)   𝐸(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐹(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐺(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐻(𝑥,𝑦,𝑧,𝑤,𝑖)   𝑀(𝑥,𝑦,𝑧,𝑤)   𝑁(𝑥,𝑦,𝑧,𝑤,𝑖)

Proof of Theorem 4sqlem14

Step	Hyp	Ref	Expression
1		4sq.r	. 2 ⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)
2		4sq.6	. . . . . . . . 9 ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}
3	2	ssrab3 4036	. . . . . . . 8 ⊢ 𝑇 ⊆ ℕ
4		4sq.7	. . . . . . . . 9 ⊢ 𝑀 = inf(𝑇, ℝ, < )
5		nnuz 12804	. . . . . . . . . . 11 ⊢ ℕ = (ℤ≥‘1)
6	3, 5	sseqtri 3984	. . . . . . . . . 10 ⊢ 𝑇 ⊆ (ℤ≥‘1)
7		4sq.1	. . . . . . . . . . . 12 ⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
8		4sq.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ)
9		4sq.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))
10		4sq.4	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℙ)
11		4sq.5	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)
12	7, 8, 9, 10, 11, 2, 4	4sqlem13 16899	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃))
13	12	simpld 494	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ≠ ∅)
14		infssuzcl 12859	. . . . . . . . . 10 ⊢ ((𝑇 ⊆ (ℤ≥‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇)
15	6, 13, 14	sylancr 588	. . . . . . . . 9 ⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇)
16	4, 15	eqeltrid 2841	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ 𝑇)
17	3, 16	sselid 3933	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ)
18	17	nnzd 12528	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
19		prmz 16616	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
20	10, 19	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℤ)
21	18, 20	zmulcld 12616	. . . . . 6 ⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℤ)
22		4sq.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℤ)
23		4sq.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
24	22, 17, 23	4sqlem5 16884	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ))
25	24	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℤ)
26		zsqcl2 14075	. . . . . . . . . . 11 ⊢ (𝐸 ∈ ℤ → (𝐸↑2) ∈ ℕ0)
27	25, 26	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸↑2) ∈ ℕ0)
28		4sq.b	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℤ)
29		4sq.f	. . . . . . . . . . . . 13 ⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
30	28, 17, 29	4sqlem5 16884	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ))
31	30	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ℤ)
32		zsqcl2 14075	. . . . . . . . . . 11 ⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈ ℕ0)
33	31, 32	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹↑2) ∈ ℕ0)
34	27, 33	nn0addcld 12480	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ0)
35	34	nn0zd 12527	. . . . . . . 8 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
36		4sq.c	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ℤ)
37		4sq.g	. . . . . . . . . . . . 13 ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
38	36, 17, 37	4sqlem5 16884	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ))
39	38	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ ℤ)
40		zsqcl2 14075	. . . . . . . . . . 11 ⊢ (𝐺 ∈ ℤ → (𝐺↑2) ∈ ℕ0)
41	39, 40	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺↑2) ∈ ℕ0)
42		4sq.d	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ ℤ)
43		4sq.h	. . . . . . . . . . . . 13 ⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
44	42, 17, 43	4sqlem5 16884	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ))
45	44	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ ℤ)
46		zsqcl2 14075	. . . . . . . . . . 11 ⊢ (𝐻 ∈ ℤ → (𝐻↑2) ∈ ℕ0)
47	45, 46	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻↑2) ∈ ℕ0)
48	41, 47	nn0addcld 12480	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℕ0)
49	48	nn0zd 12527	. . . . . . . 8 ⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℤ)
50	35, 49	zaddcld 12614	. . . . . . 7 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ)
51	21, 50	zsubcld 12615	. . . . . 6 ⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∈ ℤ)
52		dvdsmul1 16218	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑃))
53	18, 20, 52	syl2anc 585	. . . . . 6 ⊢ (𝜑 → 𝑀 ∥ (𝑀 · 𝑃))
54		zsqcl 14066	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
55	22, 54	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴↑2) ∈ ℤ)
56		zsqcl 14066	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
57	28, 56	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵↑2) ∈ ℤ)
58	55, 57	zaddcld 12614	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℤ)
59	58, 35	zsubcld 12615	. . . . . . . 8 ⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) ∈ ℤ)
60		zsqcl 14066	. . . . . . . . . . 11 ⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈ ℤ)
61	36, 60	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶↑2) ∈ ℤ)
62		zsqcl 14066	. . . . . . . . . . 11 ⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
63	42, 62	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷↑2) ∈ ℤ)
64	61, 63	zaddcld 12614	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ)
65	64, 49	zsubcld 12615	. . . . . . . 8 ⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) ∈ ℤ)
66	27	nn0zd 12527	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸↑2) ∈ ℤ)
67	55, 66	zsubcld 12615	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴↑2) − (𝐸↑2)) ∈ ℤ)
68	33	nn0zd 12527	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹↑2) ∈ ℤ)
69	57, 68	zsubcld 12615	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵↑2) − (𝐹↑2)) ∈ ℤ)
70	22, 17, 23	4sqlem8 16887	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐸↑2)))
71	28, 17, 29	4sqlem8 16887	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐹↑2)))
72	18, 67, 69, 70, 71	dvds2addd 16233	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2))))
73	22	zcnd 12611	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
74	73	sqcld 14081	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
75	28	zcnd 12611	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
76	75	sqcld 14081	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
77	25	zcnd 12611	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℂ)
78	77	sqcld 14081	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
79	31	zcnd 12611	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ℂ)
80	79	sqcld 14081	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹↑2) ∈ ℂ)
81	74, 76, 78, 80	addsub4d 11553	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) = (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2))))
82	72, 81	breqtrrd 5128	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))))
83	41	nn0zd 12527	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺↑2) ∈ ℤ)
84	61, 83	zsubcld 12615	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶↑2) − (𝐺↑2)) ∈ ℤ)
85	47	nn0zd 12527	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻↑2) ∈ ℤ)
86	63, 85	zsubcld 12615	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷↑2) − (𝐻↑2)) ∈ ℤ)
87	36, 17, 37	4sqlem8 16887	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐶↑2) − (𝐺↑2)))
88	42, 17, 43	4sqlem8 16887	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐷↑2) − (𝐻↑2)))
89	18, 84, 86, 87, 88	dvds2addd 16233	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2))))
90	36	zcnd 12611	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℂ)
91	90	sqcld 14081	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
92	42	zcnd 12611	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℂ)
93	92	sqcld 14081	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
94	39	zcnd 12611	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ ℂ)
95	94	sqcld 14081	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺↑2) ∈ ℂ)
96	45	zcnd 12611	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ ℂ)
97	96	sqcld 14081	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻↑2) ∈ ℂ)
98	91, 93, 95, 97	addsub4d 11553	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) = (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2))))
99	89, 98	breqtrrd 5128	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))
100	18, 59, 65, 82, 99	dvds2addd 16233	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∥ ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))
101		4sq.p	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
102	101	oveq1d 7385	. . . . . . . 8 ⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))))
103	74, 76	addcld 11165	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℂ)
104	91, 93	addcld 11165	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℂ)
105	78, 80	addcld 11165	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ)
106	95, 97	addcld 11165	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℂ)
107	103, 104, 105, 106	addsub4d 11553	. . . . . . . 8 ⊢ (𝜑 → ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))
108	102, 107	eqtrd 2772	. . . . . . 7 ⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))
109	100, 108	breqtrrd 5128	. . . . . 6 ⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))))
110	18, 21, 51, 53, 109	dvds2subd 16234	. . . . 5 ⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))))
111	17	nncnd 12175	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
112		prmnn 16615	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
113	10, 112	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℕ)
114	113	nncnd 12175	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℂ)
115	111, 114	mulcld 11166	. . . . . 6 ⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℂ)
116	105, 106	addcld 11165	. . . . . 6 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℂ)
117	115, 116	nncand 11511	. . . . 5 ⊢ (𝜑 → ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
118	110, 117	breqtrd 5126	. . . 4 ⊢ (𝜑 → 𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
119	17	nnne0d 12209	. . . . 5 ⊢ (𝜑 → 𝑀 ≠ 0)
120	34, 48	nn0addcld 12480	. . . . . 6 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℕ0)
121	120	nn0zd 12527	. . . . 5 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ)
122		dvdsval2 16196	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ))
123	18, 119, 121, 122	syl3anc 1374	. . . 4 ⊢ (𝜑 → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ))
124	118, 123	mpbid 232	. . 3 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ)
125	120	nn0red 12477	. . . 4 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ)
126	120	nn0ge0d 12479	. . . 4 ⊢ (𝜑 → 0 ≤ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
127	17	nnred 12174	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℝ)
128	17	nngt0d 12208	. . . 4 ⊢ (𝜑 → 0 < 𝑀)
129		divge0 12025	. . . 4 ⊢ ((((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ ∧ 0 ≤ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
130	125, 126, 127, 128, 129	syl22anc 839	. . 3 ⊢ (𝜑 → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
131		elnn0z 12515	. . 3 ⊢ (((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℕ0 ↔ (((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ ∧ 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)))
132	124, 130, 131	sylanbrc 584	. 2 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℕ0)
133	1, 132	eqeltrid 2841	1 ⊢ (𝜑 → 𝑅 ∈ ℕ0)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715   ≠ wne 2933  ∃wrex 3062  {crab 3401   ⊆ wss 3903  ∅c0 4287   class class class wbr 5100  ‘cfv 6502  (class class class)co 7370  infcinf 9358  ℝcr 11039  0cc0 11040  1c1 11041   + caddc 11043   · cmul 11045   < clt 11180   ≤ cle 11181   − cmin 11378   / cdiv 11808  ℕcn 12159  2c2 12214  ℕ₀cn0 12415  ℤcz 12502  ℤ_≥cuz 12765  ...cfz 13437   mod cmo 13803  ↑cexp 13998   ∥ cdvds 16193  ℙcprime 16612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-cnex 11096  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116  ax-pre-mulgt0 11117  ax-pre-sup 11118

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6269  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-om 7821  df-1st 7945  df-2nd 7946  df-frecs 8235  df-wrecs 8266  df-recs 8315  df-rdg 8353  df-1o 8409  df-2o 8410  df-oadd 8413  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-fin 8901  df-sup 9359  df-inf 9360  df-dju 9827  df-card 9865  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-sub 11380  df-neg 11381  df-div 11809  df-nn 12160  df-2 12222  df-3 12223  df-4 12224  df-n0 12416  df-xnn0 12489  df-z 12503  df-uz 12766  df-rp 12920  df-fz 13438  df-fl 13726  df-mod 13804  df-seq 13939  df-exp 13999  df-hash 14268  df-cj 15036  df-re 15037  df-im 15038  df-sqrt 15172  df-abs 15173  df-dvds 16194  df-gcd 16436  df-prm 16613  df-gz 16872

This theorem is referenced by:  4sqlem17  16903