4sqlem17 - Intuitionistic Logic Explorer

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

Theorem 4sqlem17 12925

Description: Lemma for 4sq 12928. (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 12924	. . . . . 6 ⊢ (𝜑 → (𝑅 ≤ 𝑀 ∧ ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃))))
20	19	simpld 112	. . . . 5 ⊢ (𝜑 → 𝑅 ≤ 𝑀)
21	1, 2, 3, 4, 5, 6, 7	4sqlem13m 12921	. . . . . . . 8 ⊢ (𝜑 → (∃𝑗 𝑗 ∈ 𝑇 ∧ 𝑀 < 𝑃))
22	21	simpld 112	. . . . . . 7 ⊢ (𝜑 → ∃𝑗 𝑗 ∈ 𝑇)
23		1zzd 9469	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 1 ∈ ℤ)
24		nnuz 9754	. . . . . . . . . 10 ⊢ ℕ = (ℤ_≥‘1)
25	24	rabeqi 2792	. . . . . . . . 9 ⊢ {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} = {𝑖 ∈ (ℤ_≥‘1) ∣ (𝑖 · 𝑃) ∈ 𝑆}
26	6, 25	eqtri 2250	. . . . . . . 8 ⊢ 𝑇 = {𝑖 ∈ (ℤ_≥‘1) ∣ (𝑖 · 𝑃) ∈ 𝑆}
27	6	ssrab3 3310	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 ⊆ ℕ
28		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 𝑗 ∈ 𝑇)
29		elfznn 10246	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ (1...𝑗) → 𝑖 ∈ ℕ)
30	29	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → 𝑖 ∈ ℕ)
31		prmnn 12627	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
32	4, 31	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑃 ∈ ℕ)
33	32	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → 𝑃 ∈ ℕ)
34	30, 33	nnmulcld 9155	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → (𝑖 · 𝑃) ∈ ℕ)
35	34	nnnn0d 9418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → (𝑖 · 𝑃) ∈ ℕ₀)
36	1	4sqlemsdc 12918	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 · 𝑃) ∈ ℕ₀ → DECID (𝑖 · 𝑃) ∈ 𝑆)
37	35, 36	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → DECID (𝑖 · 𝑃) ∈ 𝑆)
38	23, 26, 28, 37	infssuzcldc 10450	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → inf(𝑇, ℝ, < ) ∈ 𝑇)
39	22, 38	exlimddv 1945	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇)
40	7, 39	eqeltrid 2316	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ 𝑇)
41	27, 40	sselid 3222	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ)
42	41	nnred 9119	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℝ)
43	21	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < 𝑃)
44	42, 43	ltned 8256	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ≠ 𝑃)
45	41	nncnd 9120	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℂ)
46	45	sqvald 10887	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
47	46	breq1d 4092	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ (𝑀 · 𝑀) ∥ (𝑀 · 𝑃)))
48	41	nnzd 9564	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℤ)
49		prmz 12628	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
50	4, 49	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℤ)
51	41	nnne0d 9151	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≠ 0)
52		dvdscmulr 12326	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀 ∥ 𝑃))
53	48, 50, 48, 51, 52	syl112anc 1275	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀 ∥ 𝑃))
54		dvdsprm 12654	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ (ℤ_≥‘2) ∧ 𝑃 ∈ ℙ) → (𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃))
55	8, 4, 54	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃))
56	47, 53, 55	3bitrd 214	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 = 𝑃))
57	56	necon3bbid 2440	. . . . . . . . . . . . 13 ⊢ (𝜑 → (¬ (𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 ≠ 𝑃))
58	44, 57	mpbird 167	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ (𝑀↑2) ∥ (𝑀 · 𝑃))
59		orc 717	. . . . . . . . . . . . 13 ⊢ (𝑅 = 0 → (𝑅 = 0 ∨ 𝑅 = 𝑀))
60	19	simprd 114	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃)))
61	59, 60	syl5 32	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑅 = 0 → (𝑀↑2) ∥ (𝑀 · 𝑃)))
62	58, 61	mtod 667	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑅 = 0)
63	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18	4sqlem14 12922	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
64		elnn0 9367	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℕ₀ ↔ (𝑅 ∈ ℕ ∨ 𝑅 = 0))
65	63, 64	sylib 122	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑅 ∈ ℕ ∨ 𝑅 = 0))
66	62, 65	ecased 1383	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ ℕ)
67		gzreim 12897	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
68	9, 10, 67	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
69		gzcn 12890	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 + (i · 𝐵)) ∈ ℤ[i] → (𝐴 + (i · 𝐵)) ∈ ℂ)
70	68, 69	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℂ)
71	70	absvalsq2d 11689	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)))
72	9	zred 9565	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ ℝ)
73	10	zred 9565	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℝ)
74	72, 73	crred 11482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
75	74	oveq1d 6015	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵)))↑2) = (𝐴↑2))
76	72, 73	crimd 11483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
77	76	oveq1d 6015	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵)))↑2) = (𝐵↑2))
78	75, 77	oveq12d 6018	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)) = ((𝐴↑2) + (𝐵↑2)))
79	71, 78	eqtrd 2262	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2)))
80		gzreim 12897	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
81	11, 12, 80	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
82		gzcn 12890	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 + (i · 𝐷)) ∈ ℤ[i] → (𝐶 + (i · 𝐷)) ∈ ℂ)
83	81, 82	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℂ)
84	83	absvalsq2d 11689	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)))
85	11	zred 9565	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
86	12	zred 9565	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ∈ ℝ)
87	85, 86	crred 11482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶)
88	87	oveq1d 6015	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℜ‘(𝐶 + (i · 𝐷)))↑2) = (𝐶↑2))
89	85, 86	crimd 11483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷)
90	89	oveq1d 6015	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℑ‘(𝐶 + (i · 𝐷)))↑2) = (𝐷↑2))
91	88, 90	oveq12d 6018	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)) = ((𝐶↑2) + (𝐷↑2)))
92	84, 91	eqtrd 2262	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = ((𝐶↑2) + (𝐷↑2)))
93	79, 92	oveq12d 6018	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
94	18, 93	eqtr4d 2265	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 · 𝑃) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)))
95	94	oveq1d 6015	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 · 𝑃) / 𝑀) = ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀))
96	32	nncnd 9120	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ ℂ)
97	41	nnap0d 9152	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 # 0)
98	96, 45, 97	divcanap3d 8938	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 · 𝑃) / 𝑀) = 𝑃)
99	95, 98	eqtr3d 2264	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) = 𝑃)
100	9, 41, 13	4sqlem5 12900	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ))
101	100	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐸 ∈ ℤ)
102	10, 41, 14	4sqlem5 12900	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ))
103	102	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 ∈ ℤ)
104		gzreim 12897	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
105	101, 103, 104	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
106		gzcn 12890	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 + (i · 𝐹)) ∈ ℤ[i] → (𝐸 + (i · 𝐹)) ∈ ℂ)
107	105, 106	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℂ)
108	107	absvalsq2d 11689	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)))
109	101	zred 9565	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐸 ∈ ℝ)
110	103	zred 9565	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 ∈ ℝ)
111	109, 110	crred 11482	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℜ‘(𝐸 + (i · 𝐹))) = 𝐸)
112	111	oveq1d 6015	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℜ‘(𝐸 + (i · 𝐹)))↑2) = (𝐸↑2))
113	109, 110	crimd 11483	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℑ‘(𝐸 + (i · 𝐹))) = 𝐹)
114	113	oveq1d 6015	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℑ‘(𝐸 + (i · 𝐹)))↑2) = (𝐹↑2))
115	112, 114	oveq12d 6018	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)) = ((𝐸↑2) + (𝐹↑2)))
116	108, 115	eqtrd 2262	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = ((𝐸↑2) + (𝐹↑2)))
117	11, 41, 15	4sqlem5 12900	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ))
118	117	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ ℤ)
119	12, 41, 16	4sqlem5 12900	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ))
120	119	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐻 ∈ ℤ)
121		gzreim 12897	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ ℤ ∧ 𝐻 ∈ ℤ) → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
122	118, 120, 121	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
123		gzcn 12890	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 + (i · 𝐻)) ∈ ℤ[i] → (𝐺 + (i · 𝐻)) ∈ ℂ)
124	122, 123	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℂ)
125	124	absvalsq2d 11689	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)))
126	118	zred 9565	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ ℝ)
127	120	zred 9565	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐻 ∈ ℝ)
128	126, 127	crred 11482	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℜ‘(𝐺 + (i · 𝐻))) = 𝐺)
129	128	oveq1d 6015	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℜ‘(𝐺 + (i · 𝐻)))↑2) = (𝐺↑2))
130	126, 127	crimd 11483	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℑ‘(𝐺 + (i · 𝐻))) = 𝐻)
131	130	oveq1d 6015	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℑ‘(𝐺 + (i · 𝐻)))↑2) = (𝐻↑2))
132	129, 131	oveq12d 6018	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)) = ((𝐺↑2) + (𝐻↑2)))
133	125, 132	eqtrd 2262	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = ((𝐺↑2) + (𝐻↑2)))
134	116, 133	oveq12d 6018	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
135	134	oveq1d 6015	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
136	135, 17	eqtr4di 2280	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = 𝑅)
137	99, 136	oveq12d 6018	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑃 · 𝑅))
138	66	nncnd 9120	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ ℂ)
139	96, 138	mulcomd 8164	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · 𝑅) = (𝑅 · 𝑃))
140	137, 139	eqtrd 2262	. . . . . . . . . . 11 ⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑅 · 𝑃))
141		eqid 2229	. . . . . . . . . . . 12 ⊢ (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2))
142		eqid 2229	. . . . . . . . . . . 12 ⊢ (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2))
143	9	zcnd 9566	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℂ)
144		ax-icn 8090	. . . . . . . . . . . . . . . . . 18 ⊢ i ∈ ℂ
145	10	zcnd 9566	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℂ)
146		mulcl 8122	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i · 𝐵) ∈ ℂ)
147	144, 145, 146	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐵) ∈ ℂ)
148	101	zcnd 9566	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸 ∈ ℂ)
149	103	zcnd 9566	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ ℂ)
150		mulcl 8122	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐹 ∈ ℂ) → (i · 𝐹) ∈ ℂ)
151	144, 149, 150	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐹) ∈ ℂ)
152	143, 147, 148, 151	addsub4d 8500	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴 − 𝐸) + ((i · 𝐵) − (i · 𝐹))))
153	144	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → i ∈ ℂ)
154	153, 145, 149	subdid 8556	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · (𝐵 − 𝐹)) = ((i · 𝐵) − (i · 𝐹)))
155	154	oveq2d 6016	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) = ((𝐴 − 𝐸) + ((i · 𝐵) − (i · 𝐹))))
156	152, 155	eqtr4d 2265	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))))
157	156	oveq1d 6015	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) / 𝑀))
158	143, 148	subcld 8453	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 − 𝐸) ∈ ℂ)
159	145, 149	subcld 8453	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝐹) ∈ ℂ)
160		mulcl 8122	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (𝐵 − 𝐹) ∈ ℂ) → (i · (𝐵 − 𝐹)) ∈ ℂ)
161	144, 159, 160	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (i · (𝐵 − 𝐹)) ∈ ℂ)
162	158, 161, 45, 97	divdirapd 8972	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) / 𝑀) = (((𝐴 − 𝐸) / 𝑀) + ((i · (𝐵 − 𝐹)) / 𝑀)))
163	153, 159, 45, 97	divassapd 8969	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((i · (𝐵 − 𝐹)) / 𝑀) = (i · ((𝐵 − 𝐹) / 𝑀)))
164	163	oveq2d 6016	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 − 𝐸) / 𝑀) + ((i · (𝐵 − 𝐹)) / 𝑀)) = (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))))
165	157, 162, 164	3eqtrd 2266	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))))
166	100	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 − 𝐸) / 𝑀) ∈ ℤ)
167	102	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 − 𝐹) / 𝑀) ∈ ℤ)
168		gzreim 12897	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 − 𝐸) / 𝑀) ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ) → (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))) ∈ ℤ[i])
169	166, 167, 168	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))) ∈ ℤ[i])
170	165, 169	eqeltrd 2306	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) ∈ ℤ[i])
171	11	zcnd 9566	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ℂ)
172	12	zcnd 9566	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ∈ ℂ)
173		mulcl 8122	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐷 ∈ ℂ) → (i · 𝐷) ∈ ℂ)
174	144, 172, 173	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐷) ∈ ℂ)
175	118	zcnd 9566	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 ∈ ℂ)
176	120	zcnd 9566	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ∈ ℂ)
177		mulcl 8122	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐻 ∈ ℂ) → (i · 𝐻) ∈ ℂ)
178	144, 176, 177	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐻) ∈ ℂ)
179	171, 174, 175, 178	addsub4d 8500	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶 − 𝐺) + ((i · 𝐷) − (i · 𝐻))))
180	153, 172, 176	subdid 8556	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · (𝐷 − 𝐻)) = ((i · 𝐷) − (i · 𝐻)))
181	180	oveq2d 6016	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) = ((𝐶 − 𝐺) + ((i · 𝐷) − (i · 𝐻))))
182	179, 181	eqtr4d 2265	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))))
183	182	oveq1d 6015	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) / 𝑀))
184	171, 175	subcld 8453	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶 − 𝐺) ∈ ℂ)
185	172, 176	subcld 8453	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 − 𝐻) ∈ ℂ)
186		mulcl 8122	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (𝐷 − 𝐻) ∈ ℂ) → (i · (𝐷 − 𝐻)) ∈ ℂ)
187	144, 185, 186	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (i · (𝐷 − 𝐻)) ∈ ℂ)
188	184, 187, 45, 97	divdirapd 8972	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) / 𝑀) = (((𝐶 − 𝐺) / 𝑀) + ((i · (𝐷 − 𝐻)) / 𝑀)))
189	153, 185, 45, 97	divassapd 8969	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((i · (𝐷 − 𝐻)) / 𝑀) = (i · ((𝐷 − 𝐻) / 𝑀)))
190	189	oveq2d 6016	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐶 − 𝐺) / 𝑀) + ((i · (𝐷 − 𝐻)) / 𝑀)) = (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))))
191	183, 188, 190	3eqtrd 2266	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))))
192	117	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶 − 𝐺) / 𝑀) ∈ ℤ)
193	119	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐷 − 𝐻) / 𝑀) ∈ ℤ)
194		gzreim 12897	. . . . . . . . . . . . . 14 ⊢ ((((𝐶 − 𝐺) / 𝑀) ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ) → (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))) ∈ ℤ[i])
195	192, 193, 194	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))) ∈ ℤ[i])
196	191, 195	eqeltrd 2306	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) ∈ ℤ[i])
197	32	nnnn0d 9418	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
198	99, 197	eqeltrd 2306	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) ∈ ℕ₀)
199	1, 68, 81, 105, 122, 141, 142, 41, 170, 196, 198	mul4sqlem 12911	. . . . . . . . . . 11 ⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) ∈ 𝑆)
200	140, 199	eqeltrrd 2307	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 · 𝑃) ∈ 𝑆)
201		oveq1 6007	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑅 → (𝑖 · 𝑃) = (𝑅 · 𝑃))
202	201	eleq1d 2298	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑅 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑅 · 𝑃) ∈ 𝑆))
203	202, 6	elrab2 2962	. . . . . . . . . 10 ⊢ (𝑅 ∈ 𝑇 ↔ (𝑅 ∈ ℕ ∧ (𝑅 · 𝑃) ∈ 𝑆))
204	66, 200, 203	sylanbrc 417	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ 𝑇)
205	204	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 𝑅 ∈ 𝑇)
206		elfznn 10246	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (1...𝑅) → 𝑖 ∈ ℕ)
207	206	adantl 277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → 𝑖 ∈ ℕ)
208	32	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → 𝑃 ∈ ℕ)
209	207, 208	nnmulcld 9155	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → (𝑖 · 𝑃) ∈ ℕ)
210	209	nnnn0d 9418	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → (𝑖 · 𝑃) ∈ ℕ₀)
211	210, 36	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → DECID (𝑖 · 𝑃) ∈ 𝑆)
212	23, 26, 205, 211	infssuzledc 10449	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑅)
213	22, 212	exlimddv 1945	. . . . . 6 ⊢ (𝜑 → inf(𝑇, ℝ, < ) ≤ 𝑅)
214	7, 213	eqbrtrid 4117	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑅)
215	66	nnred 9119	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ ℝ)
216	215, 42	letri3d 8258	. . . . 5 ⊢ (𝜑 → (𝑅 = 𝑀 ↔ (𝑅 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)))
217	20, 214, 216	mpbir2and 950	. . . 4 ⊢ (𝜑 → 𝑅 = 𝑀)
218	217	olcd 739	. . 3 ⊢ (𝜑 → (𝑅 = 0 ∨ 𝑅 = 𝑀))
219	218, 60	mpd 13	. 2 ⊢ (𝜑 → (𝑀↑2) ∥ (𝑀 · 𝑃))
220	219, 58	pm2.65i 642	1 ⊢ ¬ 𝜑

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 713 DECID wdc 839 = wceq 1395 ∃wex 1538 ∈ wcel 2200 {cab 2215 ≠ wne 2400 ∃wrex 2509 {crab 2512 ⊆ wss 3197 class class class wbr 4082 ‘cfv 5317 (class class class)co 6000 infcinf 7146 ℂcc 7993 ℝcr 7994 0cc0 7995 1c1 7996 ici 7997 + caddc 7998 · cmul 8000 < clt 8177 ≤ cle 8178 − cmin 8313 / cdiv 8815 ℕcn 9106 2c2 9157 ℕ₀cn0 9365 ℤcz 9442 ℤ_≥cuz 9718 ...cfz 10200 mod cmo 10539 ↑cexp 10755 ℜcre 11346 ℑcim 11347 abscabs 11503 ∥ cdvds 12293 ℙcprime 12624 ℤ[i]cgz 12887

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4198 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4523 ax-setind 4628 ax-iinf 4679 ax-cnex 8086 ax-resscn 8087 ax-1cn 8088 ax-1re 8089 ax-icn 8090 ax-addcl 8091 ax-addrcl 8092 ax-mulcl 8093 ax-mulrcl 8094 ax-addcom 8095 ax-mulcom 8096 ax-addass 8097 ax-mulass 8098 ax-distr 8099 ax-i2m1 8100 ax-0lt1 8101 ax-1rid 8102 ax-0id 8103 ax-rnegex 8104 ax-precex 8105 ax-cnre 8106 ax-pre-ltirr 8107 ax-pre-ltwlin 8108 ax-pre-lttrn 8109 ax-pre-apti 8110 ax-pre-ltadd 8111 ax-pre-mulgt0 8112 ax-pre-mulext 8113 ax-arch 8114 ax-caucvg 8115

This theorem depends on definitions: df-bi 117 df-stab 836 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-int 3923 df-iun 3966 df-br 4083 df-opab 4145 df-mpt 4146 df-tr 4182 df-id 4383 df-po 4386 df-iso 4387 df-iord 4456 df-on 4458 df-ilim 4459 df-suc 4461 df-iom 4682 df-xp 4724 df-rel 4725 df-cnv 4726 df-co 4727 df-dm 4728 df-rn 4729 df-res 4730 df-ima 4731 df-iota 5277 df-fun 5319 df-fn 5320 df-f 5321 df-f1 5322 df-fo 5323 df-f1o 5324 df-fv 5325 df-isom 5326 df-riota 5953 df-ov 6003 df-oprab 6004 df-mpo 6005 df-1st 6284 df-2nd 6285 df-recs 6449 df-irdg 6514 df-frec 6535 df-1o 6560 df-2o 6561 df-oadd 6564 df-er 6678 df-en 6886 df-dom 6887 df-fin 6888 df-sup 7147 df-inf 7148 df-pnf 8179 df-mnf 8180 df-xr 8181 df-ltxr 8182 df-le 8183 df-sub 8315 df-neg 8316 df-reap 8718 df-ap 8725 df-div 8816 df-inn 9107 df-2 9165 df-3 9166 df-4 9167 df-n0 9366 df-z 9443 df-uz 9719 df-q 9811 df-rp 9846 df-fz 10201 df-fzo 10335 df-fl 10485 df-mod 10540 df-seqfrec 10665 df-exp 10756 df-ihash 10993 df-cj 11348 df-re 11349 df-im 11350 df-rsqrt 11504 df-abs 11505 df-dvds 12294 df-gcd 12470 df-prm 12625 df-gz 12888

This theorem is referenced by: 4sqlem18 12926

W3C validator