Theorem 4sqlem16

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	4sqlem16	⊢ ( 𝜑 → ( 𝑅 ≤ 𝑀 ∧ ( ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ) ) )

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		eluz2nn	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℕ )
20	8 19	syl	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
21	9 20 13	4sqlem5	⊢ ( 𝜑 → ( 𝐸 ∈ ℤ ∧ ( ( 𝐴 − 𝐸 ) / 𝑀 ) ∈ ℤ ) )
22	21	simpld	⊢ ( 𝜑 → 𝐸 ∈ ℤ )
23		zsqcl	⊢ ( 𝐸 ∈ ℤ → ( 𝐸 ↑ 2 ) ∈ ℤ )
24	22 23	syl	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℤ )
25	24	zred	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℝ )
26	10 20 14	4sqlem5	⊢ ( 𝜑 → ( 𝐹 ∈ ℤ ∧ ( ( 𝐵 − 𝐹 ) / 𝑀 ) ∈ ℤ ) )
27	26	simpld	⊢ ( 𝜑 → 𝐹 ∈ ℤ )
28		zsqcl	⊢ ( 𝐹 ∈ ℤ → ( 𝐹 ↑ 2 ) ∈ ℤ )
29	27 28	syl	⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℤ )
30	29	zred	⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℝ )
31	25 30	readdcld	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℝ )
32	11 20 15	4sqlem5	⊢ ( 𝜑 → ( 𝐺 ∈ ℤ ∧ ( ( 𝐶 − 𝐺 ) / 𝑀 ) ∈ ℤ ) )
33	32	simpld	⊢ ( 𝜑 → 𝐺 ∈ ℤ )
34		zsqcl	⊢ ( 𝐺 ∈ ℤ → ( 𝐺 ↑ 2 ) ∈ ℤ )
35	33 34	syl	⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) ∈ ℤ )
36	35	zred	⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) ∈ ℝ )
37	12 20 16	4sqlem5	⊢ ( 𝜑 → ( 𝐻 ∈ ℤ ∧ ( ( 𝐷 − 𝐻 ) / 𝑀 ) ∈ ℤ ) )
38	37	simpld	⊢ ( 𝜑 → 𝐻 ∈ ℤ )
39		zsqcl	⊢ ( 𝐻 ∈ ℤ → ( 𝐻 ↑ 2 ) ∈ ℤ )
40	38 39	syl	⊢ ( 𝜑 → ( 𝐻 ↑ 2 ) ∈ ℤ )
41	40	zred	⊢ ( 𝜑 → ( 𝐻 ↑ 2 ) ∈ ℝ )
42	36 41	readdcld	⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ∈ ℝ )
43	20	nnred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
44	43	resqcld	⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℝ )
45	44	rehalfcld	⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) / 2 ) ∈ ℝ )
46	45	rehalfcld	⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ∈ ℝ )
47	9 20 13	4sqlem7	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
48	10 20 14	4sqlem7	⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
49	25 30 46 46 47 48	le2addd	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
50	45	recnd	⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) / 2 ) ∈ ℂ )
51	50	2halvesd	⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) = ( ( 𝑀 ↑ 2 ) / 2 ) )
52	49 51	breqtrd	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ≤ ( ( 𝑀 ↑ 2 ) / 2 ) )
53	11 20 15	4sqlem7	⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
54	12 20 16	4sqlem7	⊢ ( 𝜑 → ( 𝐻 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
55	36 41 46 46 53 54	le2addd	⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
56	55 51	breqtrd	⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ≤ ( ( 𝑀 ↑ 2 ) / 2 ) )
57	31 42 45 45 52 56	le2addd	⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) + ( ( 𝑀 ↑ 2 ) / 2 ) ) )
58	44	recnd	⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℂ )
59	58	2halvesd	⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) / 2 ) + ( ( 𝑀 ↑ 2 ) / 2 ) ) = ( 𝑀 ↑ 2 ) )
60	57 59	breqtrd	⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ≤ ( 𝑀 ↑ 2 ) )
61	43	recnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
62	61	sqvald	⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) = ( 𝑀 · 𝑀 ) )
63	60 62	breqtrd	⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ≤ ( 𝑀 · 𝑀 ) )
64	31 42	readdcld	⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℝ )
65	20	nngt0d	⊢ ( 𝜑 → 0 < 𝑀 )
66		ledivmul	⊢ ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ) → ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) ≤ 𝑀 ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ≤ ( 𝑀 · 𝑀 ) ) )
67	64 43 43 65 66	syl112anc	⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) ≤ 𝑀 ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ≤ ( 𝑀 · 𝑀 ) ) )
68	63 67	mpbird	⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) ≤ 𝑀 )
69	17 68	eqbrtrid	⊢ ( 𝜑 → 𝑅 ≤ 𝑀 )
70		simpr	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → 𝑅 = 0 )
71	17 70	eqtr3id	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) = 0 )
72	64	recnd	⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℂ )
73	20	nnne0d	⊢ ( 𝜑 → 𝑀 ≠ 0 )
74	72 61 73	diveq0ad	⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) = 0 ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = 0 ) )
75		zsqcl2	⊢ ( 𝐸 ∈ ℤ → ( 𝐸 ↑ 2 ) ∈ ℕ0 )
76	22 75	syl	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℕ0 )
77		zsqcl2	⊢ ( 𝐹 ∈ ℤ → ( 𝐹 ↑ 2 ) ∈ ℕ0 )
78	27 77	syl	⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℕ0 )
79	76 78	nn0addcld	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℕ0 )
80	79	nn0ge0d	⊢ ( 𝜑 → 0 ≤ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
81		zsqcl2	⊢ ( 𝐺 ∈ ℤ → ( 𝐺 ↑ 2 ) ∈ ℕ0 )
82	33 81	syl	⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) ∈ ℕ0 )
83		zsqcl2	⊢ ( 𝐻 ∈ ℤ → ( 𝐻 ↑ 2 ) ∈ ℕ0 )
84	38 83	syl	⊢ ( 𝜑 → ( 𝐻 ↑ 2 ) ∈ ℕ0 )
85	82 84	nn0addcld	⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ∈ ℕ0 )
86	85	nn0ge0d	⊢ ( 𝜑 → 0 ≤ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) )
87		add20	⊢ ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) ∧ ( ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = 0 ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ∧ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ) ) )
88	31 80 42 86 87	syl22anc	⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = 0 ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ∧ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ) ) )
89	74 88	bitrd	⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) = 0 ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ∧ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ) ) )
90	89	biimpa	⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) = 0 ) → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ∧ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ) )
91	71 90	syldan	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ∧ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ) )
92	91	simpld	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 )
93	76	nn0ge0d	⊢ ( 𝜑 → 0 ≤ ( 𝐸 ↑ 2 ) )
94	78	nn0ge0d	⊢ ( 𝜑 → 0 ≤ ( 𝐹 ↑ 2 ) )
95		add20	⊢ ( ( ( ( 𝐸 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐸 ↑ 2 ) ) ∧ ( ( 𝐹 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ↑ 2 ) ) ) → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ↔ ( ( 𝐸 ↑ 2 ) = 0 ∧ ( 𝐹 ↑ 2 ) = 0 ) ) )
96	25 93 30 94 95	syl22anc	⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ↔ ( ( 𝐸 ↑ 2 ) = 0 ∧ ( 𝐹 ↑ 2 ) = 0 ) ) )
97	96	biimpa	⊢ ( ( 𝜑 ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ) → ( ( 𝐸 ↑ 2 ) = 0 ∧ ( 𝐹 ↑ 2 ) = 0 ) )
98	92 97	syldan	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( 𝐸 ↑ 2 ) = 0 ∧ ( 𝐹 ↑ 2 ) = 0 ) )
99	98	simpld	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝐸 ↑ 2 ) = 0 )
100	9 20 13 99	4sqlem9	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) )
101	98	simprd	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝐹 ↑ 2 ) = 0 )
102	10 20 14 101	4sqlem9	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) )
103	20	nnsqcld	⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℕ )
104	103	nnzd	⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℤ )
105		zsqcl	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
106	9 105	syl	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℤ )
107		zsqcl	⊢ ( 𝐵 ∈ ℤ → ( 𝐵 ↑ 2 ) ∈ ℤ )
108	10 107	syl	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℤ )
109		dvds2add	⊢ ( ( ( 𝑀 ↑ 2 ) ∈ ℤ ∧ ( 𝐴 ↑ 2 ) ∈ ℤ ∧ ( 𝐵 ↑ 2 ) ∈ ℤ ) → ( ( ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ∧ ( 𝑀 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
110	104 106 108 109	syl3anc	⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ∧ ( 𝑀 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
111	110	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ∧ ( 𝑀 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
112	100 102 111	mp2and	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
113	91	simprd	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 )
114	82	nn0ge0d	⊢ ( 𝜑 → 0 ≤ ( 𝐺 ↑ 2 ) )
115	84	nn0ge0d	⊢ ( 𝜑 → 0 ≤ ( 𝐻 ↑ 2 ) )
116		add20	⊢ ( ( ( ( 𝐺 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐺 ↑ 2 ) ) ∧ ( ( 𝐻 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐻 ↑ 2 ) ) ) → ( ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ↔ ( ( 𝐺 ↑ 2 ) = 0 ∧ ( 𝐻 ↑ 2 ) = 0 ) ) )
117	36 114 41 115 116	syl22anc	⊢ ( 𝜑 → ( ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ↔ ( ( 𝐺 ↑ 2 ) = 0 ∧ ( 𝐻 ↑ 2 ) = 0 ) ) )
118	117	biimpa	⊢ ( ( 𝜑 ∧ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ) → ( ( 𝐺 ↑ 2 ) = 0 ∧ ( 𝐻 ↑ 2 ) = 0 ) )
119	113 118	syldan	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( 𝐺 ↑ 2 ) = 0 ∧ ( 𝐻 ↑ 2 ) = 0 ) )
120	119	simpld	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝐺 ↑ 2 ) = 0 )
121	11 20 15 120	4sqlem9	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) )
122	119	simprd	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝐻 ↑ 2 ) = 0 )
123	12 20 16 122	4sqlem9	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝐷 ↑ 2 ) )
124		zsqcl	⊢ ( 𝐶 ∈ ℤ → ( 𝐶 ↑ 2 ) ∈ ℤ )
125	11 124	syl	⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℤ )
126		zsqcl	⊢ ( 𝐷 ∈ ℤ → ( 𝐷 ↑ 2 ) ∈ ℤ )
127	12 126	syl	⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℤ )
128		dvds2add	⊢ ( ( ( 𝑀 ↑ 2 ) ∈ ℤ ∧ ( 𝐶 ↑ 2 ) ∈ ℤ ∧ ( 𝐷 ↑ 2 ) ∈ ℤ ) → ( ( ( 𝑀 ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) ∧ ( 𝑀 ↑ 2 ) ∥ ( 𝐷 ↑ 2 ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
129	104 125 127 128	syl3anc	⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) ∧ ( 𝑀 ↑ 2 ) ∥ ( 𝐷 ↑ 2 ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
130	129	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( ( 𝑀 ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) ∧ ( 𝑀 ↑ 2 ) ∥ ( 𝐷 ↑ 2 ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
131	121 123 130	mp2and	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
132	106 108	zaddcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℤ )
133	125 127	zaddcld	⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℤ )
134		dvds2add	⊢ ( ( ( 𝑀 ↑ 2 ) ∈ ℤ ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℤ ∧ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℤ ) → ( ( ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∧ ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ) )
135	104 132 133 134	syl3anc	⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∧ ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ) )
136	135	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∧ ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ) )
137	112 131 136	mp2and	⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
138	104	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∈ ℤ )
139	132	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℤ )
140	51	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) = ( ( 𝑀 ↑ 2 ) / 2 ) )
141	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	4sqlem15	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) = 0 ) ∧ ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) = 0 ) ) )
142	141	simpld	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) = 0 ) )
143	142	simpld	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 )
144	46	recnd	⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ∈ ℂ )
145	24	zcnd	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
146	144 145	subeq0ad	⊢ ( 𝜑 → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 ↔ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) = ( 𝐸 ↑ 2 ) ) )
147	146	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 ↔ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) = ( 𝐸 ↑ 2 ) ) )
148	143 147	mpbid	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) = ( 𝐸 ↑ 2 ) )
149	24	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝐸 ↑ 2 ) ∈ ℤ )
150	148 149	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ∈ ℤ )
151	150 150	zaddcld	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ∈ ℤ )
152	140 151	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝑀 ↑ 2 ) / 2 ) ∈ ℤ )
153	139 152	zsubcld	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) ∈ ℤ )
154	133	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℤ )
155	154 152	zsubcld	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) ∈ ℤ )
156	106	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝐴 ↑ 2 ) ∈ ℤ )
157	156 150	zsubcld	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ∈ ℤ )
158	108	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝐵 ↑ 2 ) ∈ ℤ )
159	158 150	zsubcld	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝐵 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ∈ ℤ )
160	9 20 13 143	4sqlem10	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
161	142	simprd	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) = 0 )
162	10 20 14 161	4sqlem10	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐵 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
163	138 157 159 160 162	dvds2addd	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐵 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) )
164	106	zcnd	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
165	108	zcnd	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
166	164 165 144 144	addsub4d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐵 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) )
167	51	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
168	166 167	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐵 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
169	168	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐵 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
170	163 169	breqtrd	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
171	125	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝐶 ↑ 2 ) ∈ ℤ )
172	171 150	zsubcld	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝐶 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ∈ ℤ )
173	127	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝐷 ↑ 2 ) ∈ ℤ )
174	173 150	zsubcld	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝐷 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ∈ ℤ )
175	141	simprd	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) = 0 ) )
176	175	simpld	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) = 0 )
177	11 20 15 176	4sqlem10	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
178	175	simprd	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) = 0 )
179	12 20 16 178	4sqlem10	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐷 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
180	138 172 174 177 179	dvds2addd	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐶 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐷 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) )
181	125	zcnd	⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℂ )
182	127	zcnd	⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℂ )
183	181 182 144 144	addsub4d	⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐶 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐷 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) )
184	51	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
185	183 184	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐷 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
186	185	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝐶 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐷 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
187	180 186	breqtrd	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
188	138 153 155 170 187	dvds2addd	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) + ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) ) )
189	132	zcnd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℂ )
190	133	zcnd	⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℂ )
191	189 190 50 50	addsub4d	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) + ( ( 𝑀 ↑ 2 ) / 2 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) + ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) ) )
192	59	oveq2d	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) + ( ( 𝑀 ↑ 2 ) / 2 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝑀 ↑ 2 ) ) )
193	191 192	eqtr3d	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) + ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝑀 ↑ 2 ) ) )
194	193	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) + ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝑀 ↑ 2 ) ) )
195	188 194	breqtrd	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝑀 ↑ 2 ) ) )
196	132 133	zaddcld	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ∈ ℤ )
197	196	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ∈ ℤ )
198		dvdssubr	⊢ ( ( ( 𝑀 ↑ 2 ) ∈ ℤ ∧ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ∈ ℤ ) → ( ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ↔ ( 𝑀 ↑ 2 ) ∥ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝑀 ↑ 2 ) ) ) )
199	138 197 198	syl2anc	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ↔ ( 𝑀 ↑ 2 ) ∥ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝑀 ↑ 2 ) ) ) )
200	195 199	mpbird	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
201	137 200	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
202	18	adantr	⊢ ( ( 𝜑 ∧ ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) ) → ( 𝑀 · 𝑃 ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
203	201 202	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) ) → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) )
204	203	ex	⊢ ( 𝜑 → ( ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ) )
205	69 204	jca	⊢ ( 𝜑 → ( 𝑅 ≤ 𝑀 ∧ ( ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ) ) )