4sqlem17 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > 4sqlem17		GIF version

Theorem 4sqlem17 13186

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

**Hypotheses**
Ref	Expression
4sqlem11.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
4sqlem17	⊢ ¬ 𝜑

Distinct variable groups: 𝑛,𝑁 𝑃,𝑖,𝑛,𝑤,𝑥,𝑦,𝑧 𝑆,𝑖,𝑛 𝑇,𝑖 𝜑,𝑖,𝑛 𝑅,𝑖 𝐶,𝑛 𝐷,𝑛 𝐴,𝑛 𝐵,𝑛 𝑛,𝐸 𝑛,𝐹 𝑛,𝐺 𝑛,𝐻 𝑛,𝑀 Allowed substitution hints: 𝜑(𝑥, 𝑦, 𝑧, 𝑤) 𝐴(𝑥, 𝑦, 𝑧, 𝑤, 𝑖) 𝐵(𝑥, 𝑦, 𝑧, 𝑤, 𝑖) 𝐶(𝑥, 𝑦, 𝑧, 𝑤, 𝑖) 𝐷(𝑥, 𝑦, 𝑧, 𝑤, 𝑖) 𝑅(𝑥, 𝑦, 𝑧, 𝑤, 𝑛) 𝑆(𝑥, 𝑦, 𝑧, 𝑤) 𝑇(𝑥, 𝑦, 𝑧, 𝑤, 𝑛) 𝐸(𝑥, 𝑦, 𝑧, 𝑤, 𝑖) 𝐹(𝑥, 𝑦, 𝑧, 𝑤, 𝑖) 𝐺(𝑥, 𝑦, 𝑧, 𝑤, 𝑖) 𝐻(𝑥, 𝑦, 𝑧, 𝑤, 𝑖) 𝑀(𝑥, 𝑦, 𝑧, 𝑤, 𝑖) 𝑁(𝑥, 𝑦, 𝑧, 𝑤, 𝑖)

Proof of Theorem 4sqlem17 Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		4sqlem11.1	. . . . . . 7 ⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
2		4sq.2	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3		4sq.3	. . . . . . 7 ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))
4		4sq.4	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℙ)
5		4sq.5	. . . . . . 7 ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)
6		4sq.6	. . . . . . 7 ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}
7		4sq.7	. . . . . . 7 ⊢ 𝑀 = inf(𝑇, ℝ, < )
8		4sq.m	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘2))
9		4sq.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℤ)
10		4sq.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℤ)
11		4sq.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℤ)
12		4sq.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℤ)
13		4sq.e	. . . . . . 7 ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
14		4sq.f	. . . . . . 7 ⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
15		4sq.g	. . . . . . 7 ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
16		4sq.h	. . . . . . 7 ⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
17		4sq.r	. . . . . . 7 ⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)
18		4sq.p	. . . . . . 7 ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
19	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18	4sqlem16 13185	. . . . . 6 ⊢ (𝜑 → (𝑅 ≤ 𝑀 ∧ ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃))))
20	19	simpld 112	. . . . 5 ⊢ (𝜑 → 𝑅 ≤ 𝑀)
21	1, 2, 3, 4, 5, 6, 7	4sqlem13m 13182	. . . . . . . 8 ⊢ (𝜑 → (∃𝑗 𝑗 ∈ 𝑇 ∧ 𝑀 < 𝑃))
22	21	simpld 112	. . . . . . 7 ⊢ (𝜑 → ∃𝑗 𝑗 ∈ 𝑇)
23		1zzd 9671	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 1 ∈ ℤ)
24		nnuz 9958	. . . . . . . . . 10 ⊢ ℕ = (ℤ_≥‘1)
25	24	rabeqi 2814	. . . . . . . . 9 ⊢ {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} = {𝑖 ∈ (ℤ_≥‘1) ∣ (𝑖 · 𝑃) ∈ 𝑆}
26	6, 25	eqtri 2259	. . . . . . . 8 ⊢ 𝑇 = {𝑖 ∈ (ℤ_≥‘1) ∣ (𝑖 · 𝑃) ∈ 𝑆}
27	6	ssrab3 3334	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 ⊆ ℕ
28		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 𝑗 ∈ 𝑇)
29		elfznn 10460	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ (1...𝑗) → 𝑖 ∈ ℕ)
30	29	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → 𝑖 ∈ ℕ)
31		prmnn 12888	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
32	4, 31	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑃 ∈ ℕ)
33	32	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → 𝑃 ∈ ℕ)
34	30, 33	nnmulcld 9353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → (𝑖 · 𝑃) ∈ ℕ)
35	34	nnnn0d 9620	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → (𝑖 · 𝑃) ∈ ℕ₀)
36	1	4sqlemsdc 13179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 · 𝑃) ∈ ℕ₀ → DECID (𝑖 · 𝑃) ∈ 𝑆)
37	35, 36	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → DECID (𝑖 · 𝑃) ∈ 𝑆)
38	23, 26, 28, 37	infssuzcldc 10668	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → inf(𝑇, ℝ, < ) ∈ 𝑇)
39	22, 38	exlimddv 1954	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇)
40	7, 39	eqeltrid 2325	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ 𝑇)
41	27, 40	sselid 3246	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ)
42	41	nnred 9317	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℝ)
43	21	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < 𝑃)
44	42, 43	ltned 8439	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ≠ 𝑃)
45	41	nncnd 9318	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℂ)
46	45	sqvald 11108	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
47	46	breq1d 4140	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ (𝑀 · 𝑀) ∥ (𝑀 · 𝑃)))
48	41	nnzd 9767	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℤ)
49		prmz 12889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
50	4, 49	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℤ)
51	41	nnne0d 9349	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≠ 0)
52		dvdscmulr 12587	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀 ∥ 𝑃))
53	48, 50, 48, 51, 52	syl112anc 1282	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀 ∥ 𝑃))
54		dvdsprm 12915	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ (ℤ_≥‘2) ∧ 𝑃 ∈ ℙ) → (𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃))
55	8, 4, 54	syl2anc 415	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃))
56	47, 53, 55	3bitrd 214	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 = 𝑃))
57	56	necon3bbid 2460	. . . . . . . . . . . . 13 ⊢ (𝜑 → (¬ (𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 ≠ 𝑃))
58	44, 57	mpbird 167	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ (𝑀↑2) ∥ (𝑀 · 𝑃))
59		orc 724	. . . . . . . . . . . . 13 ⊢ (𝑅 = 0 → (𝑅 = 0 ∨ 𝑅 = 𝑀))
60	19	simprd 114	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃)))
61	59, 60	syl5 32	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑅 = 0 → (𝑀↑2) ∥ (𝑀 · 𝑃)))
62	58, 61	mtod 673	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑅 = 0)
63	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18	4sqlem14 13183	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
64		elnn0 9565	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℕ₀ ↔ (𝑅 ∈ ℕ ∨ 𝑅 = 0))
65	63, 64	sylib 122	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑅 ∈ ℕ ∨ 𝑅 = 0))
66	62, 65	ecased 1390	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ ℕ)
67		gzreim 13158	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
68	9, 10, 67	syl2anc 415	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
69		gzcn 13151	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 + (i · 𝐵)) ∈ ℤ[i] → (𝐴 + (i · 𝐵)) ∈ ℂ)
70	68, 69	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℂ)
71	70	absvalsq2d 11949	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)))
72	9	zred 9768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ ℝ)
73	10	zred 9768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℝ)
74	72, 73	crred 11742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
75	74	oveq1d 6100	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵)))↑2) = (𝐴↑2))
76	72, 73	crimd 11743	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
77	76	oveq1d 6100	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵)))↑2) = (𝐵↑2))
78	75, 77	oveq12d 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)) = ((𝐴↑2) + (𝐵↑2)))
79	71, 78	eqtrd 2271	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2)))
80		gzreim 13158	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
81	11, 12, 80	syl2anc 415	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
82		gzcn 13151	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 + (i · 𝐷)) ∈ ℤ[i] → (𝐶 + (i · 𝐷)) ∈ ℂ)
83	81, 82	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℂ)
84	83	absvalsq2d 11949	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)))
85	11	zred 9768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
86	12	zred 9768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ∈ ℝ)
87	85, 86	crred 11742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶)
88	87	oveq1d 6100	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℜ‘(𝐶 + (i · 𝐷)))↑2) = (𝐶↑2))
89	85, 86	crimd 11743	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷)
90	89	oveq1d 6100	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℑ‘(𝐶 + (i · 𝐷)))↑2) = (𝐷↑2))
91	88, 90	oveq12d 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)) = ((𝐶↑2) + (𝐷↑2)))
92	84, 91	eqtrd 2271	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = ((𝐶↑2) + (𝐷↑2)))
93	79, 92	oveq12d 6103	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
94	18, 93	eqtr4d 2274	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 · 𝑃) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)))
95	94	oveq1d 6100	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 · 𝑃) / 𝑀) = ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀))
96	32	nncnd 9318	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ ℂ)
97	41	nnap0d 9350	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 # 0)
98	96, 45, 97	divcanap3d 9125	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 · 𝑃) / 𝑀) = 𝑃)
99	95, 98	eqtr3d 2273	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) = 𝑃)
100	9, 41, 13	4sqlem5 13161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ))
101	100	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐸 ∈ ℤ)
102	10, 41, 14	4sqlem5 13161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ))
103	102	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 ∈ ℤ)
104		gzreim 13158	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
105	101, 103, 104	syl2anc 415	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
106		gzcn 13151	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 + (i · 𝐹)) ∈ ℤ[i] → (𝐸 + (i · 𝐹)) ∈ ℂ)
107	105, 106	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℂ)
108	107	absvalsq2d 11949	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)))
109	101	zred 9768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐸 ∈ ℝ)
110	103	zred 9768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 ∈ ℝ)
111	109, 110	crred 11742	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℜ‘(𝐸 + (i · 𝐹))) = 𝐸)
112	111	oveq1d 6100	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℜ‘(𝐸 + (i · 𝐹)))↑2) = (𝐸↑2))
113	109, 110	crimd 11743	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℑ‘(𝐸 + (i · 𝐹))) = 𝐹)
114	113	oveq1d 6100	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℑ‘(𝐸 + (i · 𝐹)))↑2) = (𝐹↑2))
115	112, 114	oveq12d 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)) = ((𝐸↑2) + (𝐹↑2)))
116	108, 115	eqtrd 2271	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = ((𝐸↑2) + (𝐹↑2)))
117	11, 41, 15	4sqlem5 13161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ))
118	117	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ ℤ)
119	12, 41, 16	4sqlem5 13161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ))
120	119	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐻 ∈ ℤ)
121		gzreim 13158	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ ℤ ∧ 𝐻 ∈ ℤ) → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
122	118, 120, 121	syl2anc 415	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
123		gzcn 13151	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 + (i · 𝐻)) ∈ ℤ[i] → (𝐺 + (i · 𝐻)) ∈ ℂ)
124	122, 123	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℂ)
125	124	absvalsq2d 11949	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)))
126	118	zred 9768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ ℝ)
127	120	zred 9768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐻 ∈ ℝ)
128	126, 127	crred 11742	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℜ‘(𝐺 + (i · 𝐻))) = 𝐺)
129	128	oveq1d 6100	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℜ‘(𝐺 + (i · 𝐻)))↑2) = (𝐺↑2))
130	126, 127	crimd 11743	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℑ‘(𝐺 + (i · 𝐻))) = 𝐻)
131	130	oveq1d 6100	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℑ‘(𝐺 + (i · 𝐻)))↑2) = (𝐻↑2))
132	129, 131	oveq12d 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)) = ((𝐺↑2) + (𝐻↑2)))
133	125, 132	eqtrd 2271	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = ((𝐺↑2) + (𝐻↑2)))
134	116, 133	oveq12d 6103	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
135	134	oveq1d 6100	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
136	135, 17	eqtr4di 2289	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = 𝑅)
137	99, 136	oveq12d 6103	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑃 · 𝑅))
138	66	nncnd 9318	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ ℂ)
139	96, 138	mulcomd 8347	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · 𝑅) = (𝑅 · 𝑃))
140	137, 139	eqtrd 2271	. . . . . . . . . . 11 ⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑅 · 𝑃))
141		eqid 2238	. . . . . . . . . . . 12 ⊢ (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2))
142		eqid 2238	. . . . . . . . . . . 12 ⊢ (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2))
143	9	zcnd 9769	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℂ)
144		ax-icn 8274	. . . . . . . . . . . . . . . . . 18 ⊢ i ∈ ℂ
145	10	zcnd 9769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℂ)
146		mulcl 8306	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i · 𝐵) ∈ ℂ)
147	144, 145, 146	sylancr 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐵) ∈ ℂ)
148	101	zcnd 9769	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸 ∈ ℂ)
149	103	zcnd 9769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ ℂ)
150		mulcl 8306	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐹 ∈ ℂ) → (i · 𝐹) ∈ ℂ)
151	144, 149, 150	sylancr 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐹) ∈ ℂ)
152	143, 147, 148, 151	addsub4d 8684	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴 − 𝐸) + ((i · 𝐵) − (i · 𝐹))))
153	144	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → i ∈ ℂ)
154	153, 145, 149	subdid 8741	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · (𝐵 − 𝐹)) = ((i · 𝐵) − (i · 𝐹)))
155	154	oveq2d 6101	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) = ((𝐴 − 𝐸) + ((i · 𝐵) − (i · 𝐹))))
156	152, 155	eqtr4d 2274	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))))
157	156	oveq1d 6100	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) / 𝑀))
158	143, 148	subcld 8637	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 − 𝐸) ∈ ℂ)
159	145, 149	subcld 8637	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝐹) ∈ ℂ)
160		mulcl 8306	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (𝐵 − 𝐹) ∈ ℂ) → (i · (𝐵 − 𝐹)) ∈ ℂ)
161	144, 159, 160	sylancr 418	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (i · (𝐵 − 𝐹)) ∈ ℂ)
162	158, 161, 45, 97	divdirapd 9159	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) / 𝑀) = (((𝐴 − 𝐸) / 𝑀) + ((i · (𝐵 − 𝐹)) / 𝑀)))
163	153, 159, 45, 97	divassapd 9156	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((i · (𝐵 − 𝐹)) / 𝑀) = (i · ((𝐵 − 𝐹) / 𝑀)))
164	163	oveq2d 6101	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 − 𝐸) / 𝑀) + ((i · (𝐵 − 𝐹)) / 𝑀)) = (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))))
165	157, 162, 164	3eqtrd 2275	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))))
166	100	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 − 𝐸) / 𝑀) ∈ ℤ)
167	102	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 − 𝐹) / 𝑀) ∈ ℤ)
168		gzreim 13158	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 − 𝐸) / 𝑀) ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ) → (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))) ∈ ℤ[i])
169	166, 167, 168	syl2anc 415	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))) ∈ ℤ[i])
170	165, 169	eqeltrd 2315	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) ∈ ℤ[i])
171	11	zcnd 9769	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ℂ)
172	12	zcnd 9769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ∈ ℂ)
173		mulcl 8306	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐷 ∈ ℂ) → (i · 𝐷) ∈ ℂ)
174	144, 172, 173	sylancr 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐷) ∈ ℂ)
175	118	zcnd 9769	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 ∈ ℂ)
176	120	zcnd 9769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ∈ ℂ)
177		mulcl 8306	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐻 ∈ ℂ) → (i · 𝐻) ∈ ℂ)
178	144, 176, 177	sylancr 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐻) ∈ ℂ)
179	171, 174, 175, 178	addsub4d 8684	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶 − 𝐺) + ((i · 𝐷) − (i · 𝐻))))
180	153, 172, 176	subdid 8741	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · (𝐷 − 𝐻)) = ((i · 𝐷) − (i · 𝐻)))
181	180	oveq2d 6101	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) = ((𝐶 − 𝐺) + ((i · 𝐷) − (i · 𝐻))))
182	179, 181	eqtr4d 2274	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))))
183	182	oveq1d 6100	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) / 𝑀))
184	171, 175	subcld 8637	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶 − 𝐺) ∈ ℂ)
185	172, 176	subcld 8637	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 − 𝐻) ∈ ℂ)
186		mulcl 8306	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (𝐷 − 𝐻) ∈ ℂ) → (i · (𝐷 − 𝐻)) ∈ ℂ)
187	144, 185, 186	sylancr 418	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (i · (𝐷 − 𝐻)) ∈ ℂ)
188	184, 187, 45, 97	divdirapd 9159	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) / 𝑀) = (((𝐶 − 𝐺) / 𝑀) + ((i · (𝐷 − 𝐻)) / 𝑀)))
189	153, 185, 45, 97	divassapd 9156	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((i · (𝐷 − 𝐻)) / 𝑀) = (i · ((𝐷 − 𝐻) / 𝑀)))
190	189	oveq2d 6101	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐶 − 𝐺) / 𝑀) + ((i · (𝐷 − 𝐻)) / 𝑀)) = (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))))
191	183, 188, 190	3eqtrd 2275	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))))
192	117	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶 − 𝐺) / 𝑀) ∈ ℤ)
193	119	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐷 − 𝐻) / 𝑀) ∈ ℤ)
194		gzreim 13158	. . . . . . . . . . . . . 14 ⊢ ((((𝐶 − 𝐺) / 𝑀) ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ) → (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))) ∈ ℤ[i])
195	192, 193, 194	syl2anc 415	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))) ∈ ℤ[i])
196	191, 195	eqeltrd 2315	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) ∈ ℤ[i])
197	32	nnnn0d 9620	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
198	99, 197	eqeltrd 2315	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) ∈ ℕ₀)
199	1, 68, 81, 105, 122, 141, 142, 41, 170, 196, 198	mul4sqlem 13172	. . . . . . . . . . 11 ⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) ∈ 𝑆)
200	140, 199	eqeltrrd 2316	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 · 𝑃) ∈ 𝑆)
201		oveq1 6092	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑅 → (𝑖 · 𝑃) = (𝑅 · 𝑃))
202	201	eleq1d 2307	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑅 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑅 · 𝑃) ∈ 𝑆))
203	202, 6	elrab2 2985	. . . . . . . . . 10 ⊢ (𝑅 ∈ 𝑇 ↔ (𝑅 ∈ ℕ ∧ (𝑅 · 𝑃) ∈ 𝑆))
204	66, 200, 203	sylanbrc 421	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ 𝑇)
205	204	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 𝑅 ∈ 𝑇)
206		elfznn 10460	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (1...𝑅) → 𝑖 ∈ ℕ)
207	206	adantl 277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → 𝑖 ∈ ℕ)
208	32	ad2antrr 492	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → 𝑃 ∈ ℕ)
209	207, 208	nnmulcld 9353	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → (𝑖 · 𝑃) ∈ ℕ)
210	209	nnnn0d 9620	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → (𝑖 · 𝑃) ∈ ℕ₀)
211	210, 36	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → DECID (𝑖 · 𝑃) ∈ 𝑆)
212	23, 26, 205, 211	infssuzledc 10667	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑅)
213	22, 212	exlimddv 1954	. . . . . 6 ⊢ (𝜑 → inf(𝑇, ℝ, < ) ≤ 𝑅)
214	7, 213	eqbrtrid 4165	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑅)
215	66	nnred 9317	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ ℝ)
216	215, 42	letri3d 8441	. . . . 5 ⊢ (𝜑 → (𝑅 = 𝑀 ↔ (𝑅 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)))
217	20, 214, 216	mpbir2and 957	. . . 4 ⊢ (𝜑 → 𝑅 = 𝑀)
218	217	olcd 746	. . 3 ⊢ (𝜑 → (𝑅 = 0 ∨ 𝑅 = 𝑀))
219	218, 60	mpd 13	. 2 ⊢ (𝜑 → (𝑀↑2) ∥ (𝑀 · 𝑃))
220	219, 58	pm2.65i 648	1 ⊢ ¬ 𝜑

Colors of variables: wff set class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 DECID wdc 846 = wceq 1402 ∃wex 1545 ∈ wcel 2209 {cab 2224 ≠ wne 2420 ∃wrex 2529 {crab 2532 ⊆ wss 3220 class class class wbr 4130 ‘cfv 5377 (class class class)co 6085 infcinf 7323 ℂcc 8177 ℝcr 8178 0cc0 8179 1c1 8180 ici 8181 + caddc 8182 · cmul 8184 < clt 8360 ≤ cle 8361 − cmin 8497 / cdiv 9002 ℕcn 9304 2c2 9355 ℕ₀cn0 9563 ℤcz 9644 ℤ_≥cuz 9921 ...cfz 10411 mod cmo 10759 ↑cexp 10975 ℜcre 11605 ℑcim 11606 abscabs 11763 ∥ cdvds 12554 ℙcprime 12885 ℤ[i]cgz 13148

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297 ax-arch 8298 ax-caucvg 8299

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-isom 5386 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-recs 6576 df-irdg 6641 df-frec 6662 df-1o 6687 df-2o 6688 df-oadd 6691 df-er 6807 df-en 7023 df-dom 7024 df-fin 7025 df-sup 7324 df-inf 7325 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-reap 8903 df-ap 8910 df-div 9003 df-inn 9305 df-2 9363 df-3 9364 df-4 9365 df-n0 9564 df-z 9645 df-uz 9922 df-q 10020 df-rp 10055 df-fz 10412 df-fzo 10550 df-fl 10705 df-mod 10760 df-seqfrec 10885 df-exp 10976 df-ihash 11215 df-cj 11607 df-re 11608 df-im 11609 df-rsqrt 11764 df-abs 11765 df-dvds 12555 df-gcd 12731 df-prm 12886 df-gz 13149

This theorem is used by: 4sqlem18 13187

W3C validator