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 17005

Description: Lemma for 4sq 17011. (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 4105	. . . . . . . 8 ⊢ 𝑇 ⊆ ℕ
4		4sq.7	. . . . . . . . 9 ⊢ 𝑀 = inf(𝑇, ℝ, < )
5		nnuz 12946	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
6	3, 5	sseqtri 4045	. . . . . . . . . 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 17004	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃))
13	12	simpld 494	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ≠ ∅)
14		infssuzcl 12997	. . . . . . . . . 10 ⊢ ((𝑇 ⊆ (ℤ_≥‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇)
15	6, 13, 14	sylancr 586	. . . . . . . . 9 ⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇)
16	4, 15	eqeltrid 2848	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ 𝑇)
17	3, 16	sselid 4006	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ)
18	17	nnzd 12666	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
19		prmz 16722	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
20	10, 19	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℤ)
21	18, 20	zmulcld 12753	. . . . . 6 ⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℤ)
22		4sq.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℤ)
23		4sq.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
24	22, 17, 23	4sqlem5 16989	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ))
25	24	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℤ)
26		zsqcl2 14188	. . . . . . . . . . 11 ⊢ (𝐸 ∈ ℤ → (𝐸↑2) ∈ ℕ₀)
27	25, 26	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸↑2) ∈ ℕ₀)
28		4sq.b	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℤ)
29		4sq.f	. . . . . . . . . . . . 13 ⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
30	28, 17, 29	4sqlem5 16989	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ))
31	30	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ℤ)
32		zsqcl2 14188	. . . . . . . . . . 11 ⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈ ℕ₀)
33	31, 32	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹↑2) ∈ ℕ₀)
34	27, 33	nn0addcld 12617	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ₀)
35	34	nn0zd 12665	. . . . . . . 8 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
36		4sq.c	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ℤ)
37		4sq.g	. . . . . . . . . . . . 13 ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
38	36, 17, 37	4sqlem5 16989	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ))
39	38	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ ℤ)
40		zsqcl2 14188	. . . . . . . . . . 11 ⊢ (𝐺 ∈ ℤ → (𝐺↑2) ∈ ℕ₀)
41	39, 40	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺↑2) ∈ ℕ₀)
42		4sq.d	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ ℤ)
43		4sq.h	. . . . . . . . . . . . 13 ⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
44	42, 17, 43	4sqlem5 16989	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ))
45	44	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ ℤ)
46		zsqcl2 14188	. . . . . . . . . . 11 ⊢ (𝐻 ∈ ℤ → (𝐻↑2) ∈ ℕ₀)
47	45, 46	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻↑2) ∈ ℕ₀)
48	41, 47	nn0addcld 12617	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℕ₀)
49	48	nn0zd 12665	. . . . . . . 8 ⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℤ)
50	35, 49	zaddcld 12751	. . . . . . 7 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ)
51	21, 50	zsubcld 12752	. . . . . 6 ⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∈ ℤ)
52		dvdsmul1 16326	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑃))
53	18, 20, 52	syl2anc 583	. . . . . 6 ⊢ (𝜑 → 𝑀 ∥ (𝑀 · 𝑃))
54		zsqcl 14179	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
55	22, 54	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴↑2) ∈ ℤ)
56		zsqcl 14179	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
57	28, 56	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵↑2) ∈ ℤ)
58	55, 57	zaddcld 12751	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℤ)
59	58, 35	zsubcld 12752	. . . . . . . 8 ⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) ∈ ℤ)
60		zsqcl 14179	. . . . . . . . . . 11 ⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈ ℤ)
61	36, 60	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶↑2) ∈ ℤ)
62		zsqcl 14179	. . . . . . . . . . 11 ⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
63	42, 62	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷↑2) ∈ ℤ)
64	61, 63	zaddcld 12751	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ)
65	64, 49	zsubcld 12752	. . . . . . . 8 ⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) ∈ ℤ)
66	27	nn0zd 12665	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸↑2) ∈ ℤ)
67	55, 66	zsubcld 12752	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴↑2) − (𝐸↑2)) ∈ ℤ)
68	33	nn0zd 12665	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹↑2) ∈ ℤ)
69	57, 68	zsubcld 12752	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵↑2) − (𝐹↑2)) ∈ ℤ)
70	22, 17, 23	4sqlem8 16992	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐸↑2)))
71	28, 17, 29	4sqlem8 16992	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐹↑2)))
72	18, 67, 69, 70, 71	dvds2addd 16340	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2))))
73	22	zcnd 12748	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
74	73	sqcld 14194	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
75	28	zcnd 12748	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
76	75	sqcld 14194	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
77	25	zcnd 12748	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℂ)
78	77	sqcld 14194	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
79	31	zcnd 12748	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ℂ)
80	79	sqcld 14194	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹↑2) ∈ ℂ)
81	74, 76, 78, 80	addsub4d 11694	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) = (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2))))
82	72, 81	breqtrrd 5194	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))))
83	41	nn0zd 12665	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺↑2) ∈ ℤ)
84	61, 83	zsubcld 12752	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶↑2) − (𝐺↑2)) ∈ ℤ)
85	47	nn0zd 12665	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻↑2) ∈ ℤ)
86	63, 85	zsubcld 12752	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷↑2) − (𝐻↑2)) ∈ ℤ)
87	36, 17, 37	4sqlem8 16992	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐶↑2) − (𝐺↑2)))
88	42, 17, 43	4sqlem8 16992	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐷↑2) − (𝐻↑2)))
89	18, 84, 86, 87, 88	dvds2addd 16340	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2))))
90	36	zcnd 12748	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℂ)
91	90	sqcld 14194	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
92	42	zcnd 12748	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℂ)
93	92	sqcld 14194	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
94	39	zcnd 12748	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ ℂ)
95	94	sqcld 14194	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺↑2) ∈ ℂ)
96	45	zcnd 12748	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ ℂ)
97	96	sqcld 14194	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻↑2) ∈ ℂ)
98	91, 93, 95, 97	addsub4d 11694	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) = (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2))))
99	89, 98	breqtrrd 5194	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))
100	18, 59, 65, 82, 99	dvds2addd 16340	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∥ ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))
101		4sq.p	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
102	101	oveq1d 7463	. . . . . . . 8 ⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))))
103	74, 76	addcld 11309	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℂ)
104	91, 93	addcld 11309	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℂ)
105	78, 80	addcld 11309	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ)
106	95, 97	addcld 11309	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℂ)
107	103, 104, 105, 106	addsub4d 11694	. . . . . . . 8 ⊢ (𝜑 → ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))
108	102, 107	eqtrd 2780	. . . . . . 7 ⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))
109	100, 108	breqtrrd 5194	. . . . . 6 ⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))))
110	18, 21, 51, 53, 109	dvds2subd 16341	. . . . 5 ⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))))
111	17	nncnd 12309	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
112		prmnn 16721	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
113	10, 112	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℕ)
114	113	nncnd 12309	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℂ)
115	111, 114	mulcld 11310	. . . . . 6 ⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℂ)
116	105, 106	addcld 11309	. . . . . 6 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℂ)
117	115, 116	nncand 11652	. . . . 5 ⊢ (𝜑 → ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
118	110, 117	breqtrd 5192	. . . 4 ⊢ (𝜑 → 𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
119	17	nnne0d 12343	. . . . 5 ⊢ (𝜑 → 𝑀 ≠ 0)
120	34, 48	nn0addcld 12617	. . . . . 6 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℕ₀)
121	120	nn0zd 12665	. . . . 5 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ)
122		dvdsval2 16305	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ))
123	18, 119, 121, 122	syl3anc 1371	. . . 4 ⊢ (𝜑 → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ))
124	118, 123	mpbid 232	. . 3 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ)
125	120	nn0red 12614	. . . 4 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ)
126	120	nn0ge0d 12616	. . . 4 ⊢ (𝜑 → 0 ≤ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
127	17	nnred 12308	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℝ)
128	17	nngt0d 12342	. . . 4 ⊢ (𝜑 → 0 < 𝑀)
129		divge0 12164	. . . 4 ⊢ ((((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ ∧ 0 ≤ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
130	125, 126, 127, 128, 129	syl22anc 838	. . 3 ⊢ (𝜑 → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
131		elnn0z 12652	. . 3 ⊢ (((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℕ₀ ↔ (((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ ∧ 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)))
132	124, 130, 131	sylanbrc 582	. 2 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℕ₀)
133	1, 132	eqeltrid 2848	1 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 = wceq 1537 ∈ wcel 2108 {cab 2717 ≠ wne 2946 ∃wrex 3076 {crab 3443 ⊆ wss 3976 ∅c0 4352 class class class wbr 5166 ‘cfv 6573 (class class class)co 7448 infcinf 9510 ℝcr 11183 0cc0 11184 1c1 11185 + caddc 11187 · cmul 11189 < clt 11324 ≤ cle 11325 − cmin 11520 / cdiv 11947 ℕcn 12293 2c2 12348 ℕ₀cn0 12553 ℤcz 12639 ℤ_≥cuz 12903 ...cfz 13567 mod cmo 13920 ↑cexp 14112 ∥ cdvds 16302 ℙcprime 16718

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-om 7904 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-2o 8523 df-oadd 8526 df-er 8763 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-sup 9511 df-inf 9512 df-dju 9970 df-card 10008 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-4 12358 df-n0 12554 df-xnn0 12626 df-z 12640 df-uz 12904 df-rp 13058 df-fz 13568 df-fl 13843 df-mod 13921 df-seq 14053 df-exp 14113 df-hash 14380 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-dvds 16303 df-gcd 16541 df-prm 16719 df-gz 16977

This theorem is referenced by: 4sqlem17 17008

W3C validator