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 17054

Description: Lemma for 4sq 17060. (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 4033	. . . . . . . 8 ⊢ 𝑇 ⊆ ℕ
4		4sq.7	. . . . . . . . 9 ⊢ 𝑀 = inf(𝑇, ℝ, < )
5		nnuz 12929	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
6	3, 5	sseqtri 3982	. . . . . . . . . 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 17053	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃))
13	12	simpld 500	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ≠ ∅)
14		infssuzcl 12984	. . . . . . . . . 10 ⊢ ((𝑇 ⊆ (ℤ_≥‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇)
15	6, 13, 14	sylancr 599	. . . . . . . . 9 ⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇)
16	4, 15	eqeltrid 2866	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ 𝑇)
17	3, 16	sselid 3932	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ)
18	17	nnzd 12644	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
19		prmz 16769	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
20	10, 19	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℤ)
21	18, 20	zmulcld 12734	. . . . . 6 ⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℤ)
22		4sq.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℤ)
23		4sq.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
24	22, 17, 23	4sqlem5 17038	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ))
25	24	simpld 500	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℤ)
26		zsqcl2 14204	. . . . . . . . . . 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 17038	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ))
31	30	simpld 500	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ℤ)
32		zsqcl2 14204	. . . . . . . . . . 11 ⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈ ℕ₀)
33	31, 32	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹↑2) ∈ ℕ₀)
34	27, 33	nn0addcld 12596	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ₀)
35	34	nn0zd 12643	. . . . . . . 8 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
36		4sq.c	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ℤ)
37		4sq.g	. . . . . . . . . . . . 13 ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
38	36, 17, 37	4sqlem5 17038	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ))
39	38	simpld 500	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ ℤ)
40		zsqcl2 14204	. . . . . . . . . . 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 17038	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ))
45	44	simpld 500	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ ℤ)
46		zsqcl2 14204	. . . . . . . . . . 11 ⊢ (𝐻 ∈ ℤ → (𝐻↑2) ∈ ℕ₀)
47	45, 46	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻↑2) ∈ ℕ₀)
48	41, 47	nn0addcld 12596	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℕ₀)
49	48	nn0zd 12643	. . . . . . . 8 ⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℤ)
50	35, 49	zaddcld 12732	. . . . . . 7 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ)
51	21, 50	zsubcld 12733	. . . . . 6 ⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∈ ℤ)
52		dvdsmul1 16371	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑃))
53	18, 20, 52	syl2anc 596	. . . . . 6 ⊢ (𝜑 → 𝑀 ∥ (𝑀 · 𝑃))
54		zsqcl 14195	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
55	22, 54	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴↑2) ∈ ℤ)
56		zsqcl 14195	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
57	28, 56	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵↑2) ∈ ℤ)
58	55, 57	zaddcld 12732	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℤ)
59	58, 35	zsubcld 12733	. . . . . . . 8 ⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) ∈ ℤ)
60		zsqcl 14195	. . . . . . . . . . 11 ⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈ ℤ)
61	36, 60	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶↑2) ∈ ℤ)
62		zsqcl 14195	. . . . . . . . . . 11 ⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
63	42, 62	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷↑2) ∈ ℤ)
64	61, 63	zaddcld 12732	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ)
65	64, 49	zsubcld 12733	. . . . . . . 8 ⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) ∈ ℤ)
66	27	nn0zd 12643	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸↑2) ∈ ℤ)
67	55, 66	zsubcld 12733	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴↑2) − (𝐸↑2)) ∈ ℤ)
68	33	nn0zd 12643	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹↑2) ∈ ℤ)
69	57, 68	zsubcld 12733	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵↑2) − (𝐹↑2)) ∈ ℤ)
70	22, 17, 23	4sqlem8 17041	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐸↑2)))
71	28, 17, 29	4sqlem8 17041	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐹↑2)))
72	18, 67, 69, 70, 71	dvds2addd 16386	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2))))
73	22	zcnd 12729	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
74	73	sqcld 14210	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
75	28	zcnd 12729	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
76	75	sqcld 14210	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
77	25	zcnd 12729	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℂ)
78	77	sqcld 14210	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
79	31	zcnd 12729	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ℂ)
80	79	sqcld 14210	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹↑2) ∈ ℂ)
81	74, 76, 78, 80	addsub4d 11643	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) = (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2))))
82	72, 81	breqtrrd 5137	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))))
83	41	nn0zd 12643	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺↑2) ∈ ℤ)
84	61, 83	zsubcld 12733	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶↑2) − (𝐺↑2)) ∈ ℤ)
85	47	nn0zd 12643	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻↑2) ∈ ℤ)
86	63, 85	zsubcld 12733	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷↑2) − (𝐻↑2)) ∈ ℤ)
87	36, 17, 37	4sqlem8 17041	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐶↑2) − (𝐺↑2)))
88	42, 17, 43	4sqlem8 17041	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐷↑2) − (𝐻↑2)))
89	18, 84, 86, 87, 88	dvds2addd 16386	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2))))
90	36	zcnd 12729	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℂ)
91	90	sqcld 14210	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
92	42	zcnd 12729	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℂ)
93	92	sqcld 14210	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
94	39	zcnd 12729	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ ℂ)
95	94	sqcld 14210	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺↑2) ∈ ℂ)
96	45	zcnd 12729	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ ℂ)
97	96	sqcld 14210	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻↑2) ∈ ℂ)
98	91, 93, 95, 97	addsub4d 11643	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) = (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2))))
99	89, 98	breqtrrd 5137	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))
100	18, 59, 65, 82, 99	dvds2addd 16386	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∥ ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))
101		4sq.p	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
102	101	oveq1d 7431	. . . . . . . 8 ⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))))
103	74, 76	addcld 11255	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℂ)
104	91, 93	addcld 11255	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℂ)
105	78, 80	addcld 11255	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ)
106	95, 97	addcld 11255	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℂ)
107	103, 104, 105, 106	addsub4d 11643	. . . . . . . 8 ⊢ (𝜑 → ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))
108	102, 107	eqtrd 2797	. . . . . . 7 ⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))
109	100, 108	breqtrrd 5137	. . . . . 6 ⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))))
110	18, 21, 51, 53, 109	dvds2subd 16387	. . . . 5 ⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))))
111	17	nncnd 12276	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
112		prmnn 16768	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
113	10, 112	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℕ)
114	113	nncnd 12276	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℂ)
115	111, 114	mulcld 11256	. . . . . 6 ⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℂ)
116	105, 106	addcld 11255	. . . . . 6 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℂ)
117	115, 116	nncand 11601	. . . . 5 ⊢ (𝜑 → ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
118	110, 117	breqtrd 5135	. . . 4 ⊢ (𝜑 → 𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
119	17	nnne0d 12313	. . . . 5 ⊢ (𝜑 → 𝑀 ≠ 0)
120	34, 48	nn0addcld 12596	. . . . . 6 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℕ₀)
121	120	nn0zd 12643	. . . . 5 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ)
122		dvdsval2 16349	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ))
123	18, 119, 121, 122	syl3anc 1398	. . . 4 ⊢ (𝜑 → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ))
124	118, 123	mpbid 235	. . 3 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ)
125	120	nn0red 12593	. . . 4 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ)
126	120	nn0ge0d 12595	. . . 4 ⊢ (𝜑 → 0 ≤ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
127	17	nnred 12275	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℝ)
128	17	nngt0d 12312	. . . 4 ⊢ (𝜑 → 0 < 𝑀)
129		divge0 12111	. . . 4 ⊢ ((((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ ∧ 0 ≤ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
130	125, 126, 127, 128, 129	syl22anc 852	. . 3 ⊢ (𝜑 → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
131		elnn0z 12631	. . 3 ⊢ (((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℕ₀ ↔ (((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ ∧ 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)))
132	124, 130, 131	sylanbrc 595	. 2 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℕ₀)
133	1, 132	eqeltrid 2866	1 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 = wceq 1570 ∈ wcel 2145 {cab 2740 ≠ wne 2957 ∃wrex 3088 {crab 3414 ⊆ wss 3902 ∅c0 4282 class class class wbr 5107 ‘cfv 6537 (class class class)co 7416 infcinf 9414 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 < clt 11270 ≤ cle 11271 − cmin 11468 / cdiv 11898 ℕcn 12260 2c2 12322 ℕ₀cn0 12531 ℤcz 12618 ℤ_≥cuz 12890 ...cfz 13563 mod cmo 13932 ↑cexp 14127 ∥ cdvds 16346 ℙcprime 16765

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 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 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-2o 8459 df-oadd 8462 df-er 8699 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-sup 9415 df-inf 9416 df-dju 9909 df-card 9947 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-n0 12532 df-xnn0 12605 df-z 12619 df-uz 12891 df-rp 13045 df-fz 13564 df-fl 13855 df-mod 13933 df-seq 14068 df-exp 14128 df-hash 14397 df-cj 15188 df-re 15189 df-im 15190 df-sqrt 15324 df-abs 15325 df-dvds 16347 df-gcd 16589 df-prm 16766 df-gz 17026

This theorem is used by: 4sqlem17 17057

W3C validator