Theorem 4sqlem17

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	4sqlem17	⊢ ¬ 𝜑

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	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	4sqlem16	⊢ ( 𝜑 → ( 𝑅 ≤ 𝑀 ∧ ( ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ) ) )
20	19	simpld	⊢ ( 𝜑 → 𝑅 ≤ 𝑀 )
21	6	ssrab3	⊢ 𝑇 ⊆ ℕ
22		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
23	21 22	sseqtri	⊢ 𝑇 ⊆ ( ℤ≥ ‘ 1 )
24	1 2 3 4 5 6 7	4sqlem13	⊢ ( 𝜑 → ( 𝑇 ≠ ∅ ∧ 𝑀 < 𝑃 ) )
25	24	simpld	⊢ ( 𝜑 → 𝑇 ≠ ∅ )
26		infssuzcl	⊢ ( ( 𝑇 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 )
27	23 25 26	sylancr	⊢ ( 𝜑 → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 )
28	7 27	eqeltrid	⊢ ( 𝜑 → 𝑀 ∈ 𝑇 )
29	21 28	sselid	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
30	29	nnred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
31	24	simprd	⊢ ( 𝜑 → 𝑀 < 𝑃 )
32	30 31	ltned	⊢ ( 𝜑 → 𝑀 ≠ 𝑃 )
33	29	nncnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
34	33	sqvald	⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) = ( 𝑀 · 𝑀 ) )
35	34	breq1d	⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ↔ ( 𝑀 · 𝑀 ) ∥ ( 𝑀 · 𝑃 ) ) )
36	29	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
37		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
38	4 37	syl	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
39	29	nnne0d	⊢ ( 𝜑 → 𝑀 ≠ 0 )
40		dvdscmulr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → ( ( 𝑀 · 𝑀 ) ∥ ( 𝑀 · 𝑃 ) ↔ 𝑀 ∥ 𝑃 ) )
41	36 38 36 39 40	syl112anc	⊢ ( 𝜑 → ( ( 𝑀 · 𝑀 ) ∥ ( 𝑀 · 𝑃 ) ↔ 𝑀 ∥ 𝑃 ) )
42		dvdsprm	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃 ) )
43	8 4 42	syl2anc	⊢ ( 𝜑 → ( 𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃 ) )
44	35 41 43	3bitrd	⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ↔ 𝑀 = 𝑃 ) )
45	44	necon3bbid	⊢ ( 𝜑 → ( ¬ ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ↔ 𝑀 ≠ 𝑃 ) )
46	32 45	mpbird	⊢ ( 𝜑 → ¬ ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) )
47	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	4sqlem14	⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
48		elnn0	⊢ ( 𝑅 ∈ ℕ0 ↔ ( 𝑅 ∈ ℕ ∨ 𝑅 = 0 ) )
49	47 48	sylib	⊢ ( 𝜑 → ( 𝑅 ∈ ℕ ∨ 𝑅 = 0 ) )
50	49	ord	⊢ ( 𝜑 → ( ¬ 𝑅 ∈ ℕ → 𝑅 = 0 ) )
51		orc	⊢ ( 𝑅 = 0 → ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) )
52	19	simprd	⊢ ( 𝜑 → ( ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ) )
53	51 52	syl5	⊢ ( 𝜑 → ( 𝑅 = 0 → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ) )
54	50 53	syld	⊢ ( 𝜑 → ( ¬ 𝑅 ∈ ℕ → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ) )
55	46 54	mt3d	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
56		gzreim	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℤ[i] )
57	9 10 56	syl2anc	⊢ ( 𝜑 → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℤ[i] )
58		gzcn	⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℤ[i] → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
59	57 58	syl	⊢ ( 𝜑 → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
60	59	absvalsq2d	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) )
61	9	zred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
62	10	zred	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
63	61 62	crred	⊢ ( 𝜑 → ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐴 )
64	63	oveq1d	⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( 𝐴 ↑ 2 ) )
65	61 62	crimd	⊢ ( 𝜑 → ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐵 )
66	65	oveq1d	⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( 𝐵 ↑ 2 ) )
67	64 66	oveq12d	⊢ ( 𝜑 → ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
68	60 67	eqtrd	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
69		gzreim	⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( 𝐶 + ( i · 𝐷 ) ) ∈ ℤ[i] )
70	11 12 69	syl2anc	⊢ ( 𝜑 → ( 𝐶 + ( i · 𝐷 ) ) ∈ ℤ[i] )
71		gzcn	⊢ ( ( 𝐶 + ( i · 𝐷 ) ) ∈ ℤ[i] → ( 𝐶 + ( i · 𝐷 ) ) ∈ ℂ )
72	70 71	syl	⊢ ( 𝜑 → ( 𝐶 + ( i · 𝐷 ) ) ∈ ℂ )
73	72	absvalsq2d	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) )
74	11	zred	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
75	12	zred	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
76	74 75	crred	⊢ ( 𝜑 → ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) = 𝐶 )
77	76	oveq1d	⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) = ( 𝐶 ↑ 2 ) )
78	74 75	crimd	⊢ ( 𝜑 → ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) = 𝐷 )
79	78	oveq1d	⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) = ( 𝐷 ↑ 2 ) )
80	77 79	oveq12d	⊢ ( 𝜑 → ( ( ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
81	73 80	eqtrd	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
82	68 81	oveq12d	⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
83	18 82	eqtr4d	⊢ ( 𝜑 → ( 𝑀 · 𝑃 ) = ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) )
84	83	oveq1d	⊢ ( 𝜑 → ( ( 𝑀 · 𝑃 ) / 𝑀 ) = ( ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) / 𝑀 ) )
85		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
86	4 85	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
87	86	nncnd	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
88	87 33 39	divcan3d	⊢ ( 𝜑 → ( ( 𝑀 · 𝑃 ) / 𝑀 ) = 𝑃 )
89	84 88	eqtr3d	⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) / 𝑀 ) = 𝑃 )
90	9 29 13	4sqlem5	⊢ ( 𝜑 → ( 𝐸 ∈ ℤ ∧ ( ( 𝐴 − 𝐸 ) / 𝑀 ) ∈ ℤ ) )
91	90	simpld	⊢ ( 𝜑 → 𝐸 ∈ ℤ )
92	10 29 14	4sqlem5	⊢ ( 𝜑 → ( 𝐹 ∈ ℤ ∧ ( ( 𝐵 − 𝐹 ) / 𝑀 ) ∈ ℤ ) )
93	92	simpld	⊢ ( 𝜑 → 𝐹 ∈ ℤ )
94		gzreim	⊢ ( ( 𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ ) → ( 𝐸 + ( i · 𝐹 ) ) ∈ ℤ[i] )
95	91 93 94	syl2anc	⊢ ( 𝜑 → ( 𝐸 + ( i · 𝐹 ) ) ∈ ℤ[i] )
96		gzcn	⊢ ( ( 𝐸 + ( i · 𝐹 ) ) ∈ ℤ[i] → ( 𝐸 + ( i · 𝐹 ) ) ∈ ℂ )
97	95 96	syl	⊢ ( 𝜑 → ( 𝐸 + ( i · 𝐹 ) ) ∈ ℂ )
98	97	absvalsq2d	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) ) )
99	91	zred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
100	93	zred	⊢ ( 𝜑 → 𝐹 ∈ ℝ )
101	99 100	crred	⊢ ( 𝜑 → ( ℜ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) = 𝐸 )
102	101	oveq1d	⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) = ( 𝐸 ↑ 2 ) )
103	99 100	crimd	⊢ ( 𝜑 → ( ℑ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) = 𝐹 )
104	103	oveq1d	⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) = ( 𝐹 ↑ 2 ) )
105	102 104	oveq12d	⊢ ( 𝜑 → ( ( ( ℜ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
106	98 105	eqtrd	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
107	11 29 15	4sqlem5	⊢ ( 𝜑 → ( 𝐺 ∈ ℤ ∧ ( ( 𝐶 − 𝐺 ) / 𝑀 ) ∈ ℤ ) )
108	107	simpld	⊢ ( 𝜑 → 𝐺 ∈ ℤ )
109	12 29 16	4sqlem5	⊢ ( 𝜑 → ( 𝐻 ∈ ℤ ∧ ( ( 𝐷 − 𝐻 ) / 𝑀 ) ∈ ℤ ) )
110	109	simpld	⊢ ( 𝜑 → 𝐻 ∈ ℤ )
111		gzreim	⊢ ( ( 𝐺 ∈ ℤ ∧ 𝐻 ∈ ℤ ) → ( 𝐺 + ( i · 𝐻 ) ) ∈ ℤ[i] )
112	108 110 111	syl2anc	⊢ ( 𝜑 → ( 𝐺 + ( i · 𝐻 ) ) ∈ ℤ[i] )
113		gzcn	⊢ ( ( 𝐺 + ( i · 𝐻 ) ) ∈ ℤ[i] → ( 𝐺 + ( i · 𝐻 ) ) ∈ ℂ )
114	112 113	syl	⊢ ( 𝜑 → ( 𝐺 + ( i · 𝐻 ) ) ∈ ℂ )
115	114	absvalsq2d	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) )
116	108	zred	⊢ ( 𝜑 → 𝐺 ∈ ℝ )
117	110	zred	⊢ ( 𝜑 → 𝐻 ∈ ℝ )
118	116 117	crred	⊢ ( 𝜑 → ( ℜ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) = 𝐺 )
119	118	oveq1d	⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) = ( 𝐺 ↑ 2 ) )
120	116 117	crimd	⊢ ( 𝜑 → ( ℑ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) = 𝐻 )
121	120	oveq1d	⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) = ( 𝐻 ↑ 2 ) )
122	119 121	oveq12d	⊢ ( 𝜑 → ( ( ( ℜ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) = ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) )
123	115 122	eqtrd	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) = ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) )
124	106 123	oveq12d	⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) = ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) )
125	124	oveq1d	⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) / 𝑀 ) = ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) )
126	125 17	eqtr4di	⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) / 𝑀 ) = 𝑅 )
127	89 126	oveq12d	⊢ ( 𝜑 → ( ( ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) / 𝑀 ) · ( ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) / 𝑀 ) ) = ( 𝑃 · 𝑅 ) )
128	55	nncnd	⊢ ( 𝜑 → 𝑅 ∈ ℂ )
129	87 128	mulcomd	⊢ ( 𝜑 → ( 𝑃 · 𝑅 ) = ( 𝑅 · 𝑃 ) )
130	127 129	eqtrd	⊢ ( 𝜑 → ( ( ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) / 𝑀 ) · ( ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) / 𝑀 ) ) = ( 𝑅 · 𝑃 ) )
131		eqid	⊢ ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) )
132		eqid	⊢ ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) )
133	9	zcnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
134		ax-icn	⊢ i ∈ ℂ
135	10	zcnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
136		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐵 ) ∈ ℂ )
137	134 135 136	sylancr	⊢ ( 𝜑 → ( i · 𝐵 ) ∈ ℂ )
138	91	zcnd	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
139	93	zcnd	⊢ ( 𝜑 → 𝐹 ∈ ℂ )
140		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐹 ∈ ℂ ) → ( i · 𝐹 ) ∈ ℂ )
141	134 139 140	sylancr	⊢ ( 𝜑 → ( i · 𝐹 ) ∈ ℂ )
142	133 137 138 141	addsub4d	⊢ ( 𝜑 → ( ( 𝐴 + ( i · 𝐵 ) ) − ( 𝐸 + ( i · 𝐹 ) ) ) = ( ( 𝐴 − 𝐸 ) + ( ( i · 𝐵 ) − ( i · 𝐹 ) ) ) )
143	134	a1i	⊢ ( 𝜑 → i ∈ ℂ )
144	143 135 139	subdid	⊢ ( 𝜑 → ( i · ( 𝐵 − 𝐹 ) ) = ( ( i · 𝐵 ) − ( i · 𝐹 ) ) )
145	144	oveq2d	⊢ ( 𝜑 → ( ( 𝐴 − 𝐸 ) + ( i · ( 𝐵 − 𝐹 ) ) ) = ( ( 𝐴 − 𝐸 ) + ( ( i · 𝐵 ) − ( i · 𝐹 ) ) ) )
146	142 145	eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 + ( i · 𝐵 ) ) − ( 𝐸 + ( i · 𝐹 ) ) ) = ( ( 𝐴 − 𝐸 ) + ( i · ( 𝐵 − 𝐹 ) ) ) )
147	146	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( 𝐸 + ( i · 𝐹 ) ) ) / 𝑀 ) = ( ( ( 𝐴 − 𝐸 ) + ( i · ( 𝐵 − 𝐹 ) ) ) / 𝑀 ) )
148	133 138	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐸 ) ∈ ℂ )
149	135 139	subcld	⊢ ( 𝜑 → ( 𝐵 − 𝐹 ) ∈ ℂ )
150		mulcl	⊢ ( ( i ∈ ℂ ∧ ( 𝐵 − 𝐹 ) ∈ ℂ ) → ( i · ( 𝐵 − 𝐹 ) ) ∈ ℂ )
151	134 149 150	sylancr	⊢ ( 𝜑 → ( i · ( 𝐵 − 𝐹 ) ) ∈ ℂ )
152	148 151 33 39	divdird	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐸 ) + ( i · ( 𝐵 − 𝐹 ) ) ) / 𝑀 ) = ( ( ( 𝐴 − 𝐸 ) / 𝑀 ) + ( ( i · ( 𝐵 − 𝐹 ) ) / 𝑀 ) ) )
153	143 149 33 39	divassd	⊢ ( 𝜑 → ( ( i · ( 𝐵 − 𝐹 ) ) / 𝑀 ) = ( i · ( ( 𝐵 − 𝐹 ) / 𝑀 ) ) )
154	153	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐸 ) / 𝑀 ) + ( ( i · ( 𝐵 − 𝐹 ) ) / 𝑀 ) ) = ( ( ( 𝐴 − 𝐸 ) / 𝑀 ) + ( i · ( ( 𝐵 − 𝐹 ) / 𝑀 ) ) ) )
155	147 152 154	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( 𝐸 + ( i · 𝐹 ) ) ) / 𝑀 ) = ( ( ( 𝐴 − 𝐸 ) / 𝑀 ) + ( i · ( ( 𝐵 − 𝐹 ) / 𝑀 ) ) ) )
156	90	simprd	⊢ ( 𝜑 → ( ( 𝐴 − 𝐸 ) / 𝑀 ) ∈ ℤ )
157	92	simprd	⊢ ( 𝜑 → ( ( 𝐵 − 𝐹 ) / 𝑀 ) ∈ ℤ )
158		gzreim	⊢ ( ( ( ( 𝐴 − 𝐸 ) / 𝑀 ) ∈ ℤ ∧ ( ( 𝐵 − 𝐹 ) / 𝑀 ) ∈ ℤ ) → ( ( ( 𝐴 − 𝐸 ) / 𝑀 ) + ( i · ( ( 𝐵 − 𝐹 ) / 𝑀 ) ) ) ∈ ℤ[i] )
159	156 157 158	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐸 ) / 𝑀 ) + ( i · ( ( 𝐵 − 𝐹 ) / 𝑀 ) ) ) ∈ ℤ[i] )
160	155 159	eqeltrd	⊢ ( 𝜑 → ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( 𝐸 + ( i · 𝐹 ) ) ) / 𝑀 ) ∈ ℤ[i] )
161	11	zcnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
162	12	zcnd	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
163		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( i · 𝐷 ) ∈ ℂ )
164	134 162 163	sylancr	⊢ ( 𝜑 → ( i · 𝐷 ) ∈ ℂ )
165	108	zcnd	⊢ ( 𝜑 → 𝐺 ∈ ℂ )
166	110	zcnd	⊢ ( 𝜑 → 𝐻 ∈ ℂ )
167		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐻 ∈ ℂ ) → ( i · 𝐻 ) ∈ ℂ )
168	134 166 167	sylancr	⊢ ( 𝜑 → ( i · 𝐻 ) ∈ ℂ )
169	161 164 165 168	addsub4d	⊢ ( 𝜑 → ( ( 𝐶 + ( i · 𝐷 ) ) − ( 𝐺 + ( i · 𝐻 ) ) ) = ( ( 𝐶 − 𝐺 ) + ( ( i · 𝐷 ) − ( i · 𝐻 ) ) ) )
170	143 162 166	subdid	⊢ ( 𝜑 → ( i · ( 𝐷 − 𝐻 ) ) = ( ( i · 𝐷 ) − ( i · 𝐻 ) ) )
171	170	oveq2d	⊢ ( 𝜑 → ( ( 𝐶 − 𝐺 ) + ( i · ( 𝐷 − 𝐻 ) ) ) = ( ( 𝐶 − 𝐺 ) + ( ( i · 𝐷 ) − ( i · 𝐻 ) ) ) )
172	169 171	eqtr4d	⊢ ( 𝜑 → ( ( 𝐶 + ( i · 𝐷 ) ) − ( 𝐺 + ( i · 𝐻 ) ) ) = ( ( 𝐶 − 𝐺 ) + ( i · ( 𝐷 − 𝐻 ) ) ) )
173	172	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐶 + ( i · 𝐷 ) ) − ( 𝐺 + ( i · 𝐻 ) ) ) / 𝑀 ) = ( ( ( 𝐶 − 𝐺 ) + ( i · ( 𝐷 − 𝐻 ) ) ) / 𝑀 ) )
174	161 165	subcld	⊢ ( 𝜑 → ( 𝐶 − 𝐺 ) ∈ ℂ )
175	162 166	subcld	⊢ ( 𝜑 → ( 𝐷 − 𝐻 ) ∈ ℂ )
176		mulcl	⊢ ( ( i ∈ ℂ ∧ ( 𝐷 − 𝐻 ) ∈ ℂ ) → ( i · ( 𝐷 − 𝐻 ) ) ∈ ℂ )
177	134 175 176	sylancr	⊢ ( 𝜑 → ( i · ( 𝐷 − 𝐻 ) ) ∈ ℂ )
178	174 177 33 39	divdird	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐺 ) + ( i · ( 𝐷 − 𝐻 ) ) ) / 𝑀 ) = ( ( ( 𝐶 − 𝐺 ) / 𝑀 ) + ( ( i · ( 𝐷 − 𝐻 ) ) / 𝑀 ) ) )
179	143 175 33 39	divassd	⊢ ( 𝜑 → ( ( i · ( 𝐷 − 𝐻 ) ) / 𝑀 ) = ( i · ( ( 𝐷 − 𝐻 ) / 𝑀 ) ) )
180	179	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐺 ) / 𝑀 ) + ( ( i · ( 𝐷 − 𝐻 ) ) / 𝑀 ) ) = ( ( ( 𝐶 − 𝐺 ) / 𝑀 ) + ( i · ( ( 𝐷 − 𝐻 ) / 𝑀 ) ) ) )
181	173 178 180	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝐶 + ( i · 𝐷 ) ) − ( 𝐺 + ( i · 𝐻 ) ) ) / 𝑀 ) = ( ( ( 𝐶 − 𝐺 ) / 𝑀 ) + ( i · ( ( 𝐷 − 𝐻 ) / 𝑀 ) ) ) )
182	107	simprd	⊢ ( 𝜑 → ( ( 𝐶 − 𝐺 ) / 𝑀 ) ∈ ℤ )
183	109	simprd	⊢ ( 𝜑 → ( ( 𝐷 − 𝐻 ) / 𝑀 ) ∈ ℤ )
184		gzreim	⊢ ( ( ( ( 𝐶 − 𝐺 ) / 𝑀 ) ∈ ℤ ∧ ( ( 𝐷 − 𝐻 ) / 𝑀 ) ∈ ℤ ) → ( ( ( 𝐶 − 𝐺 ) / 𝑀 ) + ( i · ( ( 𝐷 − 𝐻 ) / 𝑀 ) ) ) ∈ ℤ[i] )
185	182 183 184	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐺 ) / 𝑀 ) + ( i · ( ( 𝐷 − 𝐻 ) / 𝑀 ) ) ) ∈ ℤ[i] )
186	181 185	eqeltrd	⊢ ( 𝜑 → ( ( ( 𝐶 + ( i · 𝐷 ) ) − ( 𝐺 + ( i · 𝐻 ) ) ) / 𝑀 ) ∈ ℤ[i] )
187	86	nnnn0d	⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
188	89 187	eqeltrd	⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) / 𝑀 ) ∈ ℕ0 )
189	1 57 70 95 112 131 132 29 160 186 188	mul4sqlem	⊢ ( 𝜑 → ( ( ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) / 𝑀 ) · ( ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) / 𝑀 ) ) ∈ 𝑆 )
190	130 189	eqeltrrd	⊢ ( 𝜑 → ( 𝑅 · 𝑃 ) ∈ 𝑆 )
191		oveq1	⊢ ( 𝑖 = 𝑅 → ( 𝑖 · 𝑃 ) = ( 𝑅 · 𝑃 ) )
192	191	eleq1d	⊢ ( 𝑖 = 𝑅 → ( ( 𝑖 · 𝑃 ) ∈ 𝑆 ↔ ( 𝑅 · 𝑃 ) ∈ 𝑆 ) )
193	192 6	elrab2	⊢ ( 𝑅 ∈ 𝑇 ↔ ( 𝑅 ∈ ℕ ∧ ( 𝑅 · 𝑃 ) ∈ 𝑆 ) )
194	55 190 193	sylanbrc	⊢ ( 𝜑 → 𝑅 ∈ 𝑇 )
195		infssuzle	⊢ ( ( 𝑇 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑅 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ≤ 𝑅 )
196	23 194 195	sylancr	⊢ ( 𝜑 → inf ( 𝑇 , ℝ , < ) ≤ 𝑅 )
197	7 196	eqbrtrid	⊢ ( 𝜑 → 𝑀 ≤ 𝑅 )
198	55	nnred	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
199	198 30	letri3d	⊢ ( 𝜑 → ( 𝑅 = 𝑀 ↔ ( 𝑅 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅 ) ) )
200	20 197 199	mpbir2and	⊢ ( 𝜑 → 𝑅 = 𝑀 )
201	200	olcd	⊢ ( 𝜑 → ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) )
202	201 52	mpd	⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) )
203	202 46	pm2.65i	⊢ ¬ 𝜑