4sqlem17 - Intuitionistic Logic Explorer

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

Theorem 4sqlem17 13043

Description: Lemma for 4sq 13046. (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 13042	. . . . . 6 ⊢ (𝜑 → (𝑅 ≤ 𝑀 ∧ ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃))))
20	19	simpld 112	. . . . 5 ⊢ (𝜑 → 𝑅 ≤ 𝑀)
21	1, 2, 3, 4, 5, 6, 7	4sqlem13m 13039	. . . . . . . 8 ⊢ (𝜑 → (∃𝑗 𝑗 ∈ 𝑇 ∧ 𝑀 < 𝑃))
22	21	simpld 112	. . . . . . 7 ⊢ (𝜑 → ∃𝑗 𝑗 ∈ 𝑇)
23		1zzd 9550	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 1 ∈ ℤ)
24		nnuz 9836	. . . . . . . . . 10 ⊢ ℕ = (ℤ_≥‘1)
25	24	rabeqi 2796	. . . . . . . . 9 ⊢ {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} = {𝑖 ∈ (ℤ_≥‘1) ∣ (𝑖 · 𝑃) ∈ 𝑆}
26	6, 25	eqtri 2252	. . . . . . . 8 ⊢ 𝑇 = {𝑖 ∈ (ℤ_≥‘1) ∣ (𝑖 · 𝑃) ∈ 𝑆}
27	6	ssrab3 3314	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 ⊆ ℕ
28		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 𝑗 ∈ 𝑇)
29		elfznn 10334	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ (1...𝑗) → 𝑖 ∈ ℕ)
30	29	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → 𝑖 ∈ ℕ)
31		prmnn 12745	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
32	4, 31	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑃 ∈ ℕ)
33	32	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → 𝑃 ∈ ℕ)
34	30, 33	nnmulcld 9234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → (𝑖 · 𝑃) ∈ ℕ)
35	34	nnnn0d 9499	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → (𝑖 · 𝑃) ∈ ℕ₀)
36	1	4sqlemsdc 13036	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 · 𝑃) ∈ ℕ₀ → DECID (𝑖 · 𝑃) ∈ 𝑆)
37	35, 36	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → DECID (𝑖 · 𝑃) ∈ 𝑆)
38	23, 26, 28, 37	infssuzcldc 10541	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → inf(𝑇, ℝ, < ) ∈ 𝑇)
39	22, 38	exlimddv 1947	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇)
40	7, 39	eqeltrid 2318	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ 𝑇)
41	27, 40	sselid 3226	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ)
42	41	nnred 9198	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℝ)
43	21	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < 𝑃)
44	42, 43	ltned 8335	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ≠ 𝑃)
45	41	nncnd 9199	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℂ)
46	45	sqvald 10978	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
47	46	breq1d 4103	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ (𝑀 · 𝑀) ∥ (𝑀 · 𝑃)))
48	41	nnzd 9645	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℤ)
49		prmz 12746	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
50	4, 49	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℤ)
51	41	nnne0d 9230	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≠ 0)
52		dvdscmulr 12444	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀 ∥ 𝑃))
53	48, 50, 48, 51, 52	syl112anc 1278	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀 ∥ 𝑃))
54		dvdsprm 12772	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ (ℤ_≥‘2) ∧ 𝑃 ∈ ℙ) → (𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃))
55	8, 4, 54	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃))
56	47, 53, 55	3bitrd 214	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 = 𝑃))
57	56	necon3bbid 2443	. . . . . . . . . . . . 13 ⊢ (𝜑 → (¬ (𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 ≠ 𝑃))
58	44, 57	mpbird 167	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ (𝑀↑2) ∥ (𝑀 · 𝑃))
59		orc 720	. . . . . . . . . . . . 13 ⊢ (𝑅 = 0 → (𝑅 = 0 ∨ 𝑅 = 𝑀))
60	19	simprd 114	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃)))
61	59, 60	syl5 32	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑅 = 0 → (𝑀↑2) ∥ (𝑀 · 𝑃)))
62	58, 61	mtod 669	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑅 = 0)
63	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18	4sqlem14 13040	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
64		elnn0 9446	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℕ₀ ↔ (𝑅 ∈ ℕ ∨ 𝑅 = 0))
65	63, 64	sylib 122	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑅 ∈ ℕ ∨ 𝑅 = 0))
66	62, 65	ecased 1386	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ ℕ)
67		gzreim 13015	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
68	9, 10, 67	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
69		gzcn 13008	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 + (i · 𝐵)) ∈ ℤ[i] → (𝐴 + (i · 𝐵)) ∈ ℂ)
70	68, 69	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℂ)
71	70	absvalsq2d 11806	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)))
72	9	zred 9646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ ℝ)
73	10	zred 9646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℝ)
74	72, 73	crred 11599	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
75	74	oveq1d 6043	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵)))↑2) = (𝐴↑2))
76	72, 73	crimd 11600	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
77	76	oveq1d 6043	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵)))↑2) = (𝐵↑2))
78	75, 77	oveq12d 6046	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)) = ((𝐴↑2) + (𝐵↑2)))
79	71, 78	eqtrd 2264	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2)))
80		gzreim 13015	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
81	11, 12, 80	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
82		gzcn 13008	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 + (i · 𝐷)) ∈ ℤ[i] → (𝐶 + (i · 𝐷)) ∈ ℂ)
83	81, 82	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℂ)
84	83	absvalsq2d 11806	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)))
85	11	zred 9646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
86	12	zred 9646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ∈ ℝ)
87	85, 86	crred 11599	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶)
88	87	oveq1d 6043	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℜ‘(𝐶 + (i · 𝐷)))↑2) = (𝐶↑2))
89	85, 86	crimd 11600	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷)
90	89	oveq1d 6043	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℑ‘(𝐶 + (i · 𝐷)))↑2) = (𝐷↑2))
91	88, 90	oveq12d 6046	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)) = ((𝐶↑2) + (𝐷↑2)))
92	84, 91	eqtrd 2264	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = ((𝐶↑2) + (𝐷↑2)))
93	79, 92	oveq12d 6046	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
94	18, 93	eqtr4d 2267	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 · 𝑃) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)))
95	94	oveq1d 6043	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 · 𝑃) / 𝑀) = ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀))
96	32	nncnd 9199	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ ℂ)
97	41	nnap0d 9231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 # 0)
98	96, 45, 97	divcanap3d 9017	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 · 𝑃) / 𝑀) = 𝑃)
99	95, 98	eqtr3d 2266	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) = 𝑃)
100	9, 41, 13	4sqlem5 13018	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ))
101	100	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐸 ∈ ℤ)
102	10, 41, 14	4sqlem5 13018	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ))
103	102	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 ∈ ℤ)
104		gzreim 13015	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
105	101, 103, 104	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
106		gzcn 13008	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 + (i · 𝐹)) ∈ ℤ[i] → (𝐸 + (i · 𝐹)) ∈ ℂ)
107	105, 106	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℂ)
108	107	absvalsq2d 11806	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)))
109	101	zred 9646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐸 ∈ ℝ)
110	103	zred 9646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 ∈ ℝ)
111	109, 110	crred 11599	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℜ‘(𝐸 + (i · 𝐹))) = 𝐸)
112	111	oveq1d 6043	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℜ‘(𝐸 + (i · 𝐹)))↑2) = (𝐸↑2))
113	109, 110	crimd 11600	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℑ‘(𝐸 + (i · 𝐹))) = 𝐹)
114	113	oveq1d 6043	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℑ‘(𝐸 + (i · 𝐹)))↑2) = (𝐹↑2))
115	112, 114	oveq12d 6046	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)) = ((𝐸↑2) + (𝐹↑2)))
116	108, 115	eqtrd 2264	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = ((𝐸↑2) + (𝐹↑2)))
117	11, 41, 15	4sqlem5 13018	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ))
118	117	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ ℤ)
119	12, 41, 16	4sqlem5 13018	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ))
120	119	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐻 ∈ ℤ)
121		gzreim 13015	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ ℤ ∧ 𝐻 ∈ ℤ) → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
122	118, 120, 121	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
123		gzcn 13008	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 + (i · 𝐻)) ∈ ℤ[i] → (𝐺 + (i · 𝐻)) ∈ ℂ)
124	122, 123	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℂ)
125	124	absvalsq2d 11806	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)))
126	118	zred 9646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ ℝ)
127	120	zred 9646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐻 ∈ ℝ)
128	126, 127	crred 11599	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℜ‘(𝐺 + (i · 𝐻))) = 𝐺)
129	128	oveq1d 6043	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℜ‘(𝐺 + (i · 𝐻)))↑2) = (𝐺↑2))
130	126, 127	crimd 11600	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℑ‘(𝐺 + (i · 𝐻))) = 𝐻)
131	130	oveq1d 6043	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℑ‘(𝐺 + (i · 𝐻)))↑2) = (𝐻↑2))
132	129, 131	oveq12d 6046	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)) = ((𝐺↑2) + (𝐻↑2)))
133	125, 132	eqtrd 2264	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = ((𝐺↑2) + (𝐻↑2)))
134	116, 133	oveq12d 6046	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
135	134	oveq1d 6043	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
136	135, 17	eqtr4di 2282	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = 𝑅)
137	99, 136	oveq12d 6046	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑃 · 𝑅))
138	66	nncnd 9199	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ ℂ)
139	96, 138	mulcomd 8243	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · 𝑅) = (𝑅 · 𝑃))
140	137, 139	eqtrd 2264	. . . . . . . . . . 11 ⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑅 · 𝑃))
141		eqid 2231	. . . . . . . . . . . 12 ⊢ (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2))
142		eqid 2231	. . . . . . . . . . . 12 ⊢ (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2))
143	9	zcnd 9647	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℂ)
144		ax-icn 8170	. . . . . . . . . . . . . . . . . 18 ⊢ i ∈ ℂ
145	10	zcnd 9647	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℂ)
146		mulcl 8202	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i · 𝐵) ∈ ℂ)
147	144, 145, 146	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐵) ∈ ℂ)
148	101	zcnd 9647	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸 ∈ ℂ)
149	103	zcnd 9647	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ ℂ)
150		mulcl 8202	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐹 ∈ ℂ) → (i · 𝐹) ∈ ℂ)
151	144, 149, 150	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐹) ∈ ℂ)
152	143, 147, 148, 151	addsub4d 8579	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴 − 𝐸) + ((i · 𝐵) − (i · 𝐹))))
153	144	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → i ∈ ℂ)
154	153, 145, 149	subdid 8635	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · (𝐵 − 𝐹)) = ((i · 𝐵) − (i · 𝐹)))
155	154	oveq2d 6044	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) = ((𝐴 − 𝐸) + ((i · 𝐵) − (i · 𝐹))))
156	152, 155	eqtr4d 2267	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))))
157	156	oveq1d 6043	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) / 𝑀))
158	143, 148	subcld 8532	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 − 𝐸) ∈ ℂ)
159	145, 149	subcld 8532	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝐹) ∈ ℂ)
160		mulcl 8202	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (𝐵 − 𝐹) ∈ ℂ) → (i · (𝐵 − 𝐹)) ∈ ℂ)
161	144, 159, 160	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (i · (𝐵 − 𝐹)) ∈ ℂ)
162	158, 161, 45, 97	divdirapd 9051	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) / 𝑀) = (((𝐴 − 𝐸) / 𝑀) + ((i · (𝐵 − 𝐹)) / 𝑀)))
163	153, 159, 45, 97	divassapd 9048	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((i · (𝐵 − 𝐹)) / 𝑀) = (i · ((𝐵 − 𝐹) / 𝑀)))
164	163	oveq2d 6044	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 − 𝐸) / 𝑀) + ((i · (𝐵 − 𝐹)) / 𝑀)) = (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))))
165	157, 162, 164	3eqtrd 2268	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))))
166	100	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 − 𝐸) / 𝑀) ∈ ℤ)
167	102	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 − 𝐹) / 𝑀) ∈ ℤ)
168		gzreim 13015	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 − 𝐸) / 𝑀) ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ) → (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))) ∈ ℤ[i])
169	166, 167, 168	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))) ∈ ℤ[i])
170	165, 169	eqeltrd 2308	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) ∈ ℤ[i])
171	11	zcnd 9647	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ℂ)
172	12	zcnd 9647	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ∈ ℂ)
173		mulcl 8202	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐷 ∈ ℂ) → (i · 𝐷) ∈ ℂ)
174	144, 172, 173	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐷) ∈ ℂ)
175	118	zcnd 9647	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 ∈ ℂ)
176	120	zcnd 9647	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ∈ ℂ)
177		mulcl 8202	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐻 ∈ ℂ) → (i · 𝐻) ∈ ℂ)
178	144, 176, 177	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐻) ∈ ℂ)
179	171, 174, 175, 178	addsub4d 8579	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶 − 𝐺) + ((i · 𝐷) − (i · 𝐻))))
180	153, 172, 176	subdid 8635	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · (𝐷 − 𝐻)) = ((i · 𝐷) − (i · 𝐻)))
181	180	oveq2d 6044	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) = ((𝐶 − 𝐺) + ((i · 𝐷) − (i · 𝐻))))
182	179, 181	eqtr4d 2267	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))))
183	182	oveq1d 6043	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) / 𝑀))
184	171, 175	subcld 8532	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶 − 𝐺) ∈ ℂ)
185	172, 176	subcld 8532	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 − 𝐻) ∈ ℂ)
186		mulcl 8202	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (𝐷 − 𝐻) ∈ ℂ) → (i · (𝐷 − 𝐻)) ∈ ℂ)
187	144, 185, 186	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (i · (𝐷 − 𝐻)) ∈ ℂ)
188	184, 187, 45, 97	divdirapd 9051	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) / 𝑀) = (((𝐶 − 𝐺) / 𝑀) + ((i · (𝐷 − 𝐻)) / 𝑀)))
189	153, 185, 45, 97	divassapd 9048	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((i · (𝐷 − 𝐻)) / 𝑀) = (i · ((𝐷 − 𝐻) / 𝑀)))
190	189	oveq2d 6044	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐶 − 𝐺) / 𝑀) + ((i · (𝐷 − 𝐻)) / 𝑀)) = (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))))
191	183, 188, 190	3eqtrd 2268	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))))
192	117	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶 − 𝐺) / 𝑀) ∈ ℤ)
193	119	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐷 − 𝐻) / 𝑀) ∈ ℤ)
194		gzreim 13015	. . . . . . . . . . . . . 14 ⊢ ((((𝐶 − 𝐺) / 𝑀) ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ) → (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))) ∈ ℤ[i])
195	192, 193, 194	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))) ∈ ℤ[i])
196	191, 195	eqeltrd 2308	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) ∈ ℤ[i])
197	32	nnnn0d 9499	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
198	99, 197	eqeltrd 2308	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) ∈ ℕ₀)
199	1, 68, 81, 105, 122, 141, 142, 41, 170, 196, 198	mul4sqlem 13029	. . . . . . . . . . 11 ⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) ∈ 𝑆)
200	140, 199	eqeltrrd 2309	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 · 𝑃) ∈ 𝑆)
201		oveq1 6035	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑅 → (𝑖 · 𝑃) = (𝑅 · 𝑃))
202	201	eleq1d 2300	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑅 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑅 · 𝑃) ∈ 𝑆))
203	202, 6	elrab2 2966	. . . . . . . . . 10 ⊢ (𝑅 ∈ 𝑇 ↔ (𝑅 ∈ ℕ ∧ (𝑅 · 𝑃) ∈ 𝑆))
204	66, 200, 203	sylanbrc 417	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ 𝑇)
205	204	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 𝑅 ∈ 𝑇)
206		elfznn 10334	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (1...𝑅) → 𝑖 ∈ ℕ)
207	206	adantl 277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → 𝑖 ∈ ℕ)
208	32	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → 𝑃 ∈ ℕ)
209	207, 208	nnmulcld 9234	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → (𝑖 · 𝑃) ∈ ℕ)
210	209	nnnn0d 9499	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → (𝑖 · 𝑃) ∈ ℕ₀)
211	210, 36	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → DECID (𝑖 · 𝑃) ∈ 𝑆)
212	23, 26, 205, 211	infssuzledc 10540	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑅)
213	22, 212	exlimddv 1947	. . . . . 6 ⊢ (𝜑 → inf(𝑇, ℝ, < ) ≤ 𝑅)
214	7, 213	eqbrtrid 4128	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑅)
215	66	nnred 9198	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ ℝ)
216	215, 42	letri3d 8337	. . . . 5 ⊢ (𝜑 → (𝑅 = 𝑀 ↔ (𝑅 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)))
217	20, 214, 216	mpbir2and 953	. . . 4 ⊢ (𝜑 → 𝑅 = 𝑀)
218	217	olcd 742	. . 3 ⊢ (𝜑 → (𝑅 = 0 ∨ 𝑅 = 𝑀))
219	218, 60	mpd 13	. 2 ⊢ (𝜑 → (𝑀↑2) ∥ (𝑀 · 𝑃))
220	219, 58	pm2.65i 644	1 ⊢ ¬ 𝜑

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 716 DECID wdc 842 = wceq 1398 ∃wex 1541 ∈ wcel 2202 {cab 2217 ≠ wne 2403 ∃wrex 2512 {crab 2515 ⊆ wss 3201 class class class wbr 4093 ‘cfv 5333 (class class class)co 6028 infcinf 7225 ℂcc 8073 ℝcr 8074 0cc0 8075 1c1 8076 ici 8077 + caddc 8078 · cmul 8080 < clt 8256 ≤ cle 8257 − cmin 8392 / cdiv 8894 ℕcn 9185 2c2 9236 ℕ₀cn0 9444 ℤcz 9523 ℤ_≥cuz 9799 ...cfz 10288 mod cmo 10630 ↑cexp 10846 ℜcre 11463 ℑcim 11464 abscabs 11620 ∥ cdvds 12411 ℙcprime 12742 ℤ[i]cgz 13005

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4209 ax-sep 4212 ax-nul 4220 ax-pow 4270 ax-pr 4305 ax-un 4536 ax-setind 4641 ax-iinf 4692 ax-cnex 8166 ax-resscn 8167 ax-1cn 8168 ax-1re 8169 ax-icn 8170 ax-addcl 8171 ax-addrcl 8172 ax-mulcl 8173 ax-mulrcl 8174 ax-addcom 8175 ax-mulcom 8176 ax-addass 8177 ax-mulass 8178 ax-distr 8179 ax-i2m1 8180 ax-0lt1 8181 ax-1rid 8182 ax-0id 8183 ax-rnegex 8184 ax-precex 8185 ax-cnre 8186 ax-pre-ltirr 8187 ax-pre-ltwlin 8188 ax-pre-lttrn 8189 ax-pre-apti 8190 ax-pre-ltadd 8191 ax-pre-mulgt0 8192 ax-pre-mulext 8193 ax-arch 8194 ax-caucvg 8195

This theorem depends on definitions: df-bi 117 df-stab 839 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ne 2404 df-nel 2499 df-ral 2516 df-rex 2517 df-reu 2518 df-rmo 2519 df-rab 2520 df-v 2805 df-sbc 3033 df-csb 3129 df-dif 3203 df-un 3205 df-in 3207 df-ss 3214 df-nul 3497 df-if 3608 df-pw 3658 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-int 3934 df-iun 3977 df-br 4094 df-opab 4156 df-mpt 4157 df-tr 4193 df-id 4396 df-po 4399 df-iso 4400 df-iord 4469 df-on 4471 df-ilim 4472 df-suc 4474 df-iom 4695 df-xp 4737 df-rel 4738 df-cnv 4739 df-co 4740 df-dm 4741 df-rn 4742 df-res 4743 df-ima 4744 df-iota 5293 df-fun 5335 df-fn 5336 df-f 5337 df-f1 5338 df-fo 5339 df-f1o 5340 df-fv 5341 df-isom 5342 df-riota 5981 df-ov 6031 df-oprab 6032 df-mpo 6033 df-1st 6312 df-2nd 6313 df-recs 6514 df-irdg 6579 df-frec 6600 df-1o 6625 df-2o 6626 df-oadd 6629 df-er 6745 df-en 6953 df-dom 6954 df-fin 6955 df-sup 7226 df-inf 7227 df-pnf 8258 df-mnf 8259 df-xr 8260 df-ltxr 8261 df-le 8262 df-sub 8394 df-neg 8395 df-reap 8797 df-ap 8804 df-div 8895 df-inn 9186 df-2 9244 df-3 9245 df-4 9246 df-n0 9445 df-z 9524 df-uz 9800 df-q 9898 df-rp 9933 df-fz 10289 df-fzo 10423 df-fl 10576 df-mod 10631 df-seqfrec 10756 df-exp 10847 df-ihash 11084 df-cj 11465 df-re 11466 df-im 11467 df-rsqrt 11621 df-abs 11622 df-dvds 12412 df-gcd 12588 df-prm 12743 df-gz 13006

This theorem is referenced by: 4sqlem18 13044

W3C validator