4sqlem14 - Metamath Proof Explorer

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

Theorem 4sqlem14 17018

Description: Lemma for 4sq 17024. (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	⊢ (𝜑 → 𝑅 ∈ ℕ₀)

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 4042	. . . . . . . 8 ⊢ 𝑇 ⊆ ℕ
4		4sq.7	. . . . . . . . 9 ⊢ 𝑀 = inf(𝑇, ℝ, < )
5		nnuz 12901	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
6	3, 5	sseqtri 3991	. . . . . . . . . 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 17017	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃))
13	12	simpld 499	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ≠ ∅)
14		infssuzcl 12956	. . . . . . . . . 10 ⊢ ((𝑇 ⊆ (ℤ_≥‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇)
15	6, 13, 14	sylancr 598	. . . . . . . . 9 ⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇)
16	4, 15	eqeltrid 2873	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ 𝑇)
17	3, 16	sselid 3941	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ)
18	17	nnzd 12617	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
19		prmz 16733	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
20	10, 19	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℤ)
21	18, 20	zmulcld 12706	. . . . . 6 ⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℤ)
22		4sq.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℤ)
23		4sq.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
24	22, 17, 23	4sqlem5 17002	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ))
25	24	simpld 499	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℤ)
26		zsqcl2 14174	. . . . . . . . . . 11 ⊢ (𝐸 ∈ ℤ → (𝐸↑2) ∈ ℕ₀)
27	25, 26	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸↑2) ∈ ℕ₀)
28		4sq.b	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℤ)
29		4sq.f	. . . . . . . . . . . . 13 ⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
30	28, 17, 29	4sqlem5 17002	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ))
31	30	simpld 499	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ℤ)
32		zsqcl2 14174	. . . . . . . . . . 11 ⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈ ℕ₀)
33	31, 32	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹↑2) ∈ ℕ₀)
34	27, 33	nn0addcld 12569	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ₀)
35	34	nn0zd 12616	. . . . . . . 8 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
36		4sq.c	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ℤ)
37		4sq.g	. . . . . . . . . . . . 13 ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
38	36, 17, 37	4sqlem5 17002	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ))
39	38	simpld 499	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ ℤ)
40		zsqcl2 14174	. . . . . . . . . . 11 ⊢ (𝐺 ∈ ℤ → (𝐺↑2) ∈ ℕ₀)
41	39, 40	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺↑2) ∈ ℕ₀)
42		4sq.d	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ ℤ)
43		4sq.h	. . . . . . . . . . . . 13 ⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
44	42, 17, 43	4sqlem5 17002	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ))
45	44	simpld 499	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ ℤ)
46		zsqcl2 14174	. . . . . . . . . . 11 ⊢ (𝐻 ∈ ℤ → (𝐻↑2) ∈ ℕ₀)
47	45, 46	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻↑2) ∈ ℕ₀)
48	41, 47	nn0addcld 12569	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℕ₀)
49	48	nn0zd 12616	. . . . . . . 8 ⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℤ)
50	35, 49	zaddcld 12704	. . . . . . 7 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ)
51	21, 50	zsubcld 12705	. . . . . 6 ⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∈ ℤ)
52		dvdsmul1 16335	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑃))
53	18, 20, 52	syl2anc 595	. . . . . 6 ⊢ (𝜑 → 𝑀 ∥ (𝑀 · 𝑃))
54		zsqcl 14165	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
55	22, 54	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴↑2) ∈ ℤ)
56		zsqcl 14165	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
57	28, 56	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵↑2) ∈ ℤ)
58	55, 57	zaddcld 12704	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℤ)
59	58, 35	zsubcld 12705	. . . . . . . 8 ⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) ∈ ℤ)
60		zsqcl 14165	. . . . . . . . . . 11 ⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈ ℤ)
61	36, 60	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶↑2) ∈ ℤ)
62		zsqcl 14165	. . . . . . . . . . 11 ⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
63	42, 62	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷↑2) ∈ ℤ)
64	61, 63	zaddcld 12704	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ)
65	64, 49	zsubcld 12705	. . . . . . . 8 ⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) ∈ ℤ)
66	27	nn0zd 12616	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸↑2) ∈ ℤ)
67	55, 66	zsubcld 12705	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴↑2) − (𝐸↑2)) ∈ ℤ)
68	33	nn0zd 12616	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹↑2) ∈ ℤ)
69	57, 68	zsubcld 12705	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵↑2) − (𝐹↑2)) ∈ ℤ)
70	22, 17, 23	4sqlem8 17005	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐸↑2)))
71	28, 17, 29	4sqlem8 17005	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐹↑2)))
72	18, 67, 69, 70, 71	dvds2addd 16350	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2))))
73	22	zcnd 12701	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
74	73	sqcld 14180	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
75	28	zcnd 12701	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
76	75	sqcld 14180	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
77	25	zcnd 12701	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℂ)
78	77	sqcld 14180	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
79	31	zcnd 12701	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ℂ)
80	79	sqcld 14180	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹↑2) ∈ ℂ)
81	74, 76, 78, 80	addsub4d 11616	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) = (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2))))
82	72, 81	breqtrrd 5141	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))))
83	41	nn0zd 12616	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺↑2) ∈ ℤ)
84	61, 83	zsubcld 12705	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶↑2) − (𝐺↑2)) ∈ ℤ)
85	47	nn0zd 12616	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻↑2) ∈ ℤ)
86	63, 85	zsubcld 12705	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷↑2) − (𝐻↑2)) ∈ ℤ)
87	36, 17, 37	4sqlem8 17005	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐶↑2) − (𝐺↑2)))
88	42, 17, 43	4sqlem8 17005	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐷↑2) − (𝐻↑2)))
89	18, 84, 86, 87, 88	dvds2addd 16350	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2))))
90	36	zcnd 12701	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℂ)
91	90	sqcld 14180	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
92	42	zcnd 12701	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℂ)
93	92	sqcld 14180	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
94	39	zcnd 12701	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ ℂ)
95	94	sqcld 14180	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺↑2) ∈ ℂ)
96	45	zcnd 12701	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ ℂ)
97	96	sqcld 14180	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻↑2) ∈ ℂ)
98	91, 93, 95, 97	addsub4d 11616	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) = (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2))))
99	89, 98	breqtrrd 5141	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))
100	18, 59, 65, 82, 99	dvds2addd 16350	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∥ ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))
101		4sq.p	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
102	101	oveq1d 7426	. . . . . . . 8 ⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))))
103	74, 76	addcld 11228	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℂ)
104	91, 93	addcld 11228	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℂ)
105	78, 80	addcld 11228	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ)
106	95, 97	addcld 11228	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℂ)
107	103, 104, 105, 106	addsub4d 11616	. . . . . . . 8 ⊢ (𝜑 → ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))
108	102, 107	eqtrd 2804	. . . . . . 7 ⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))
109	100, 108	breqtrrd 5141	. . . . . 6 ⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))))
110	18, 21, 51, 53, 109	dvds2subd 16351	. . . . 5 ⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))))
111	17	nncnd 12249	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
112		prmnn 16732	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
113	10, 112	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℕ)
114	113	nncnd 12249	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℂ)
115	111, 114	mulcld 11229	. . . . . 6 ⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℂ)
116	105, 106	addcld 11228	. . . . . 6 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℂ)
117	115, 116	nncand 11574	. . . . 5 ⊢ (𝜑 → ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
118	110, 117	breqtrd 5139	. . . 4 ⊢ (𝜑 → 𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
119	17	nnne0d 12286	. . . . 5 ⊢ (𝜑 → 𝑀 ≠ 0)
120	34, 48	nn0addcld 12569	. . . . . 6 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℕ₀)
121	120	nn0zd 12616	. . . . 5 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ)
122		dvdsval2 16313	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ))
123	18, 119, 121, 122	syl3anc 1396	. . . 4 ⊢ (𝜑 → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ))
124	118, 123	mpbid 235	. . 3 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ)
125	120	nn0red 12566	. . . 4 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ)
126	120	nn0ge0d 12568	. . . 4 ⊢ (𝜑 → 0 ≤ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
127	17	nnred 12248	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℝ)
128	17	nngt0d 12285	. . . 4 ⊢ (𝜑 → 0 < 𝑀)
129		divge0 12084	. . . 4 ⊢ ((((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ ∧ 0 ≤ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
130	125, 126, 127, 128, 129	syl22anc 851	. . 3 ⊢ (𝜑 → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
131		elnn0z 12604	. . 3 ⊢ (((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℕ₀ ↔ (((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ ∧ 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)))
132	124, 130, 131	sylanbrc 594	. 2 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℕ₀)
133	1, 132	eqeltrid 2873	1 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 = wceq 1567 ∈ wcel 2149 {cab 2747 ≠ wne 2964 ∃wrex 3095 {crab 3422 ⊆ wss 3911 ∅c0 4292 class class class wbr 5111 ‘cfv 6537 (class class class)co 7411 infcinf 9401 ℝcr 11099 0cc0 11100 1c1 11101 + caddc 11103 · cmul 11105 < clt 11243 ≤ cle 11244 − cmin 11441 / cdiv 11871 ℕcn 12233 2c2 12295 ℕ₀cn0 12504 ℤcz 12591 ℤ_≥cuz 12862 ...cfz 13535 mod cmo 13902 ↑cexp 14097 ∥ cdvds 16310 ℙcprime 16729

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-pre-sup 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3375 df-reu 3376 df-rab 3423 df-v 3463 df-sbc 3752 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-2o 8454 df-oadd 8457 df-er 8694 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-sup 9402 df-inf 9403 df-dju 9887 df-card 9925 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-div 11872 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-n0 12505 df-xnn0 12578 df-z 12592 df-uz 12863 df-rp 13017 df-fz 13536 df-fl 13825 df-mod 13903 df-seq 14038 df-exp 14098 df-hash 14367 df-cj 15150 df-re 15151 df-im 15152 df-sqrt 15286 df-abs 15287 df-dvds 16311 df-gcd 16553 df-prm 16730 df-gz 16990

This theorem is referenced by: 4sqlem17 17021

W3C validator