Theorem 4sqlem14

Description: Lemma for 4sq . (Contributed by Mario Carneiro, 16-Jul-2014) (Revised by AV, 14-Sep-2020)

	Ref	Expression
Hypotheses	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	4sqlem14	⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )

Proof

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