4sqlem17 - Intuitionistic Logic Explorer

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

Theorem 4sqlem17 12576

Description: Lemma for 4sq 12579. (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 12575	. . . . . 6 ⊢ (𝜑 → (𝑅 ≤ 𝑀 ∧ ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃))))
20	19	simpld 112	. . . . 5 ⊢ (𝜑 → 𝑅 ≤ 𝑀)
21	1, 2, 3, 4, 5, 6, 7	4sqlem13m 12572	. . . . . . . 8 ⊢ (𝜑 → (∃𝑗 𝑗 ∈ 𝑇 ∧ 𝑀 < 𝑃))
22	21	simpld 112	. . . . . . 7 ⊢ (𝜑 → ∃𝑗 𝑗 ∈ 𝑇)
23		1zzd 9353	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 1 ∈ ℤ)
24		nnuz 9637	. . . . . . . . . 10 ⊢ ℕ = (ℤ_≥‘1)
25	24	rabeqi 2756	. . . . . . . . 9 ⊢ {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} = {𝑖 ∈ (ℤ_≥‘1) ∣ (𝑖 · 𝑃) ∈ 𝑆}
26	6, 25	eqtri 2217	. . . . . . . 8 ⊢ 𝑇 = {𝑖 ∈ (ℤ_≥‘1) ∣ (𝑖 · 𝑃) ∈ 𝑆}
27	6	ssrab3 3269	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 ⊆ ℕ
28		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 𝑗 ∈ 𝑇)
29		elfznn 10129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ (1...𝑗) → 𝑖 ∈ ℕ)
30	29	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → 𝑖 ∈ ℕ)
31		prmnn 12278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
32	4, 31	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑃 ∈ ℕ)
33	32	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → 𝑃 ∈ ℕ)
34	30, 33	nnmulcld 9039	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → (𝑖 · 𝑃) ∈ ℕ)
35	34	nnnn0d 9302	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → (𝑖 · 𝑃) ∈ ℕ₀)
36	1	4sqlemsdc 12569	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 · 𝑃) ∈ ℕ₀ → DECID (𝑖 · 𝑃) ∈ 𝑆)
37	35, 36	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → DECID (𝑖 · 𝑃) ∈ 𝑆)
38	23, 26, 28, 37	infssuzcldc 10325	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → inf(𝑇, ℝ, < ) ∈ 𝑇)
39	22, 38	exlimddv 1913	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇)
40	7, 39	eqeltrid 2283	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ 𝑇)
41	27, 40	sselid 3181	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ)
42	41	nnred 9003	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℝ)
43	21	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < 𝑃)
44	42, 43	ltned 8140	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ≠ 𝑃)
45	41	nncnd 9004	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℂ)
46	45	sqvald 10762	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
47	46	breq1d 4043	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ (𝑀 · 𝑀) ∥ (𝑀 · 𝑃)))
48	41	nnzd 9447	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℤ)
49		prmz 12279	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
50	4, 49	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℤ)
51	41	nnne0d 9035	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≠ 0)
52		dvdscmulr 11985	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀 ∥ 𝑃))
53	48, 50, 48, 51, 52	syl112anc 1253	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀 ∥ 𝑃))
54		dvdsprm 12305	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ (ℤ_≥‘2) ∧ 𝑃 ∈ ℙ) → (𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃))
55	8, 4, 54	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃))
56	47, 53, 55	3bitrd 214	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 = 𝑃))
57	56	necon3bbid 2407	. . . . . . . . . . . . 13 ⊢ (𝜑 → (¬ (𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 ≠ 𝑃))
58	44, 57	mpbird 167	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ (𝑀↑2) ∥ (𝑀 · 𝑃))
59		orc 713	. . . . . . . . . . . . 13 ⊢ (𝑅 = 0 → (𝑅 = 0 ∨ 𝑅 = 𝑀))
60	19	simprd 114	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃)))
61	59, 60	syl5 32	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑅 = 0 → (𝑀↑2) ∥ (𝑀 · 𝑃)))
62	58, 61	mtod 664	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑅 = 0)
63	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18	4sqlem14 12573	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
64		elnn0 9251	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℕ₀ ↔ (𝑅 ∈ ℕ ∨ 𝑅 = 0))
65	63, 64	sylib 122	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑅 ∈ ℕ ∨ 𝑅 = 0))
66	62, 65	ecased 1360	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ ℕ)
67		gzreim 12548	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
68	9, 10, 67	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
69		gzcn 12541	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 + (i · 𝐵)) ∈ ℤ[i] → (𝐴 + (i · 𝐵)) ∈ ℂ)
70	68, 69	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℂ)
71	70	absvalsq2d 11348	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)))
72	9	zred 9448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ ℝ)
73	10	zred 9448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℝ)
74	72, 73	crred 11141	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
75	74	oveq1d 5937	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵)))↑2) = (𝐴↑2))
76	72, 73	crimd 11142	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
77	76	oveq1d 5937	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵)))↑2) = (𝐵↑2))
78	75, 77	oveq12d 5940	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)) = ((𝐴↑2) + (𝐵↑2)))
79	71, 78	eqtrd 2229	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2)))
80		gzreim 12548	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
81	11, 12, 80	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
82		gzcn 12541	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 + (i · 𝐷)) ∈ ℤ[i] → (𝐶 + (i · 𝐷)) ∈ ℂ)
83	81, 82	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℂ)
84	83	absvalsq2d 11348	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)))
85	11	zred 9448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
86	12	zred 9448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ∈ ℝ)
87	85, 86	crred 11141	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶)
88	87	oveq1d 5937	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℜ‘(𝐶 + (i · 𝐷)))↑2) = (𝐶↑2))
89	85, 86	crimd 11142	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷)
90	89	oveq1d 5937	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℑ‘(𝐶 + (i · 𝐷)))↑2) = (𝐷↑2))
91	88, 90	oveq12d 5940	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)) = ((𝐶↑2) + (𝐷↑2)))
92	84, 91	eqtrd 2229	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = ((𝐶↑2) + (𝐷↑2)))
93	79, 92	oveq12d 5940	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
94	18, 93	eqtr4d 2232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 · 𝑃) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)))
95	94	oveq1d 5937	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 · 𝑃) / 𝑀) = ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀))
96	32	nncnd 9004	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ ℂ)
97	41	nnap0d 9036	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 # 0)
98	96, 45, 97	divcanap3d 8822	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 · 𝑃) / 𝑀) = 𝑃)
99	95, 98	eqtr3d 2231	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) = 𝑃)
100	9, 41, 13	4sqlem5 12551	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ))
101	100	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐸 ∈ ℤ)
102	10, 41, 14	4sqlem5 12551	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ))
103	102	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 ∈ ℤ)
104		gzreim 12548	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
105	101, 103, 104	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
106		gzcn 12541	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 + (i · 𝐹)) ∈ ℤ[i] → (𝐸 + (i · 𝐹)) ∈ ℂ)
107	105, 106	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℂ)
108	107	absvalsq2d 11348	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)))
109	101	zred 9448	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐸 ∈ ℝ)
110	103	zred 9448	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 ∈ ℝ)
111	109, 110	crred 11141	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℜ‘(𝐸 + (i · 𝐹))) = 𝐸)
112	111	oveq1d 5937	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℜ‘(𝐸 + (i · 𝐹)))↑2) = (𝐸↑2))
113	109, 110	crimd 11142	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℑ‘(𝐸 + (i · 𝐹))) = 𝐹)
114	113	oveq1d 5937	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℑ‘(𝐸 + (i · 𝐹)))↑2) = (𝐹↑2))
115	112, 114	oveq12d 5940	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)) = ((𝐸↑2) + (𝐹↑2)))
116	108, 115	eqtrd 2229	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = ((𝐸↑2) + (𝐹↑2)))
117	11, 41, 15	4sqlem5 12551	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ))
118	117	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ ℤ)
119	12, 41, 16	4sqlem5 12551	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ))
120	119	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐻 ∈ ℤ)
121		gzreim 12548	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ ℤ ∧ 𝐻 ∈ ℤ) → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
122	118, 120, 121	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
123		gzcn 12541	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 + (i · 𝐻)) ∈ ℤ[i] → (𝐺 + (i · 𝐻)) ∈ ℂ)
124	122, 123	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℂ)
125	124	absvalsq2d 11348	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)))
126	118	zred 9448	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ ℝ)
127	120	zred 9448	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐻 ∈ ℝ)
128	126, 127	crred 11141	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℜ‘(𝐺 + (i · 𝐻))) = 𝐺)
129	128	oveq1d 5937	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℜ‘(𝐺 + (i · 𝐻)))↑2) = (𝐺↑2))
130	126, 127	crimd 11142	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℑ‘(𝐺 + (i · 𝐻))) = 𝐻)
131	130	oveq1d 5937	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℑ‘(𝐺 + (i · 𝐻)))↑2) = (𝐻↑2))
132	129, 131	oveq12d 5940	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)) = ((𝐺↑2) + (𝐻↑2)))
133	125, 132	eqtrd 2229	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = ((𝐺↑2) + (𝐻↑2)))
134	116, 133	oveq12d 5940	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
135	134	oveq1d 5937	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
136	135, 17	eqtr4di 2247	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = 𝑅)
137	99, 136	oveq12d 5940	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑃 · 𝑅))
138	66	nncnd 9004	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ ℂ)
139	96, 138	mulcomd 8048	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · 𝑅) = (𝑅 · 𝑃))
140	137, 139	eqtrd 2229	. . . . . . . . . . 11 ⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑅 · 𝑃))
141		eqid 2196	. . . . . . . . . . . 12 ⊢ (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2))
142		eqid 2196	. . . . . . . . . . . 12 ⊢ (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2))
143	9	zcnd 9449	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℂ)
144		ax-icn 7974	. . . . . . . . . . . . . . . . . 18 ⊢ i ∈ ℂ
145	10	zcnd 9449	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℂ)
146		mulcl 8006	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i · 𝐵) ∈ ℂ)
147	144, 145, 146	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐵) ∈ ℂ)
148	101	zcnd 9449	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸 ∈ ℂ)
149	103	zcnd 9449	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ ℂ)
150		mulcl 8006	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐹 ∈ ℂ) → (i · 𝐹) ∈ ℂ)
151	144, 149, 150	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐹) ∈ ℂ)
152	143, 147, 148, 151	addsub4d 8384	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴 − 𝐸) + ((i · 𝐵) − (i · 𝐹))))
153	144	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → i ∈ ℂ)
154	153, 145, 149	subdid 8440	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · (𝐵 − 𝐹)) = ((i · 𝐵) − (i · 𝐹)))
155	154	oveq2d 5938	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) = ((𝐴 − 𝐸) + ((i · 𝐵) − (i · 𝐹))))
156	152, 155	eqtr4d 2232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))))
157	156	oveq1d 5937	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) / 𝑀))
158	143, 148	subcld 8337	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 − 𝐸) ∈ ℂ)
159	145, 149	subcld 8337	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝐹) ∈ ℂ)
160		mulcl 8006	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (𝐵 − 𝐹) ∈ ℂ) → (i · (𝐵 − 𝐹)) ∈ ℂ)
161	144, 159, 160	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (i · (𝐵 − 𝐹)) ∈ ℂ)
162	158, 161, 45, 97	divdirapd 8856	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) / 𝑀) = (((𝐴 − 𝐸) / 𝑀) + ((i · (𝐵 − 𝐹)) / 𝑀)))
163	153, 159, 45, 97	divassapd 8853	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((i · (𝐵 − 𝐹)) / 𝑀) = (i · ((𝐵 − 𝐹) / 𝑀)))
164	163	oveq2d 5938	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 − 𝐸) / 𝑀) + ((i · (𝐵 − 𝐹)) / 𝑀)) = (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))))
165	157, 162, 164	3eqtrd 2233	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))))
166	100	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 − 𝐸) / 𝑀) ∈ ℤ)
167	102	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 − 𝐹) / 𝑀) ∈ ℤ)
168		gzreim 12548	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 − 𝐸) / 𝑀) ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ) → (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))) ∈ ℤ[i])
169	166, 167, 168	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))) ∈ ℤ[i])
170	165, 169	eqeltrd 2273	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) ∈ ℤ[i])
171	11	zcnd 9449	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ℂ)
172	12	zcnd 9449	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ∈ ℂ)
173		mulcl 8006	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐷 ∈ ℂ) → (i · 𝐷) ∈ ℂ)
174	144, 172, 173	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐷) ∈ ℂ)
175	118	zcnd 9449	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 ∈ ℂ)
176	120	zcnd 9449	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ∈ ℂ)
177		mulcl 8006	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐻 ∈ ℂ) → (i · 𝐻) ∈ ℂ)
178	144, 176, 177	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐻) ∈ ℂ)
179	171, 174, 175, 178	addsub4d 8384	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶 − 𝐺) + ((i · 𝐷) − (i · 𝐻))))
180	153, 172, 176	subdid 8440	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · (𝐷 − 𝐻)) = ((i · 𝐷) − (i · 𝐻)))
181	180	oveq2d 5938	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) = ((𝐶 − 𝐺) + ((i · 𝐷) − (i · 𝐻))))
182	179, 181	eqtr4d 2232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))))
183	182	oveq1d 5937	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) / 𝑀))
184	171, 175	subcld 8337	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶 − 𝐺) ∈ ℂ)
185	172, 176	subcld 8337	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 − 𝐻) ∈ ℂ)
186		mulcl 8006	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (𝐷 − 𝐻) ∈ ℂ) → (i · (𝐷 − 𝐻)) ∈ ℂ)
187	144, 185, 186	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (i · (𝐷 − 𝐻)) ∈ ℂ)
188	184, 187, 45, 97	divdirapd 8856	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) / 𝑀) = (((𝐶 − 𝐺) / 𝑀) + ((i · (𝐷 − 𝐻)) / 𝑀)))
189	153, 185, 45, 97	divassapd 8853	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((i · (𝐷 − 𝐻)) / 𝑀) = (i · ((𝐷 − 𝐻) / 𝑀)))
190	189	oveq2d 5938	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐶 − 𝐺) / 𝑀) + ((i · (𝐷 − 𝐻)) / 𝑀)) = (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))))
191	183, 188, 190	3eqtrd 2233	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))))
192	117	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶 − 𝐺) / 𝑀) ∈ ℤ)
193	119	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐷 − 𝐻) / 𝑀) ∈ ℤ)
194		gzreim 12548	. . . . . . . . . . . . . 14 ⊢ ((((𝐶 − 𝐺) / 𝑀) ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ) → (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))) ∈ ℤ[i])
195	192, 193, 194	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))) ∈ ℤ[i])
196	191, 195	eqeltrd 2273	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) ∈ ℤ[i])
197	32	nnnn0d 9302	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
198	99, 197	eqeltrd 2273	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) ∈ ℕ₀)
199	1, 68, 81, 105, 122, 141, 142, 41, 170, 196, 198	mul4sqlem 12562	. . . . . . . . . . 11 ⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) ∈ 𝑆)
200	140, 199	eqeltrrd 2274	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 · 𝑃) ∈ 𝑆)
201		oveq1 5929	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑅 → (𝑖 · 𝑃) = (𝑅 · 𝑃))
202	201	eleq1d 2265	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑅 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑅 · 𝑃) ∈ 𝑆))
203	202, 6	elrab2 2923	. . . . . . . . . 10 ⊢ (𝑅 ∈ 𝑇 ↔ (𝑅 ∈ ℕ ∧ (𝑅 · 𝑃) ∈ 𝑆))
204	66, 200, 203	sylanbrc 417	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ 𝑇)
205	204	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 𝑅 ∈ 𝑇)
206		elfznn 10129	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (1...𝑅) → 𝑖 ∈ ℕ)
207	206	adantl 277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → 𝑖 ∈ ℕ)
208	32	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → 𝑃 ∈ ℕ)
209	207, 208	nnmulcld 9039	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → (𝑖 · 𝑃) ∈ ℕ)
210	209	nnnn0d 9302	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → (𝑖 · 𝑃) ∈ ℕ₀)
211	210, 36	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → DECID (𝑖 · 𝑃) ∈ 𝑆)
212	23, 26, 205, 211	infssuzledc 10324	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑅)
213	22, 212	exlimddv 1913	. . . . . 6 ⊢ (𝜑 → inf(𝑇, ℝ, < ) ≤ 𝑅)
214	7, 213	eqbrtrid 4068	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑅)
215	66	nnred 9003	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ ℝ)
216	215, 42	letri3d 8142	. . . . 5 ⊢ (𝜑 → (𝑅 = 𝑀 ↔ (𝑅 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)))
217	20, 214, 216	mpbir2and 946	. . . 4 ⊢ (𝜑 → 𝑅 = 𝑀)
218	217	olcd 735	. . 3 ⊢ (𝜑 → (𝑅 = 0 ∨ 𝑅 = 𝑀))
219	218, 60	mpd 13	. 2 ⊢ (𝜑 → (𝑀↑2) ∥ (𝑀 · 𝑃))
220	219, 58	pm2.65i 640	1 ⊢ ¬ 𝜑

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 DECID wdc 835 = wceq 1364 ∃wex 1506 ∈ wcel 2167 {cab 2182 ≠ wne 2367 ∃wrex 2476 {crab 2479 ⊆ wss 3157 class class class wbr 4033 ‘cfv 5258 (class class class)co 5922 infcinf 7049 ℂcc 7877 ℝcr 7878 0cc0 7879 1c1 7880 ici 7881 + caddc 7882 · cmul 7884 < clt 8061 ≤ cle 8062 − cmin 8197 / cdiv 8699 ℕcn 8990 2c2 9041 ℕ₀cn0 9249 ℤcz 9326 ℤ_≥cuz 9601 ...cfz 10083 mod cmo 10414 ↑cexp 10630 ℜcre 11005 ℑcim 11006 abscabs 11162 ∥ cdvds 11952 ℙcprime 12275 ℤ[i]cgz 12538

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 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-mulrcl 7978 ax-addcom 7979 ax-mulcom 7980 ax-addass 7981 ax-mulass 7982 ax-distr 7983 ax-i2m1 7984 ax-0lt1 7985 ax-1rid 7986 ax-0id 7987 ax-rnegex 7988 ax-precex 7989 ax-cnre 7990 ax-pre-ltirr 7991 ax-pre-ltwlin 7992 ax-pre-lttrn 7993 ax-pre-apti 7994 ax-pre-ltadd 7995 ax-pre-mulgt0 7996 ax-pre-mulext 7997 ax-arch 7998 ax-caucvg 7999

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-isom 5267 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-recs 6363 df-irdg 6428 df-frec 6449 df-1o 6474 df-2o 6475 df-oadd 6478 df-er 6592 df-en 6800 df-dom 6801 df-fin 6802 df-sup 7050 df-inf 7051 df-pnf 8063 df-mnf 8064 df-xr 8065 df-ltxr 8066 df-le 8067 df-sub 8199 df-neg 8200 df-reap 8602 df-ap 8609 df-div 8700 df-inn 8991 df-2 9049 df-3 9050 df-4 9051 df-n0 9250 df-z 9327 df-uz 9602 df-q 9694 df-rp 9729 df-fz 10084 df-fzo 10218 df-fl 10360 df-mod 10415 df-seqfrec 10540 df-exp 10631 df-ihash 10868 df-cj 11007 df-re 11008 df-im 11009 df-rsqrt 11163 df-abs 11164 df-dvds 11953 df-gcd 12121 df-prm 12276 df-gz 12539

This theorem is referenced by: 4sqlem18 12577

W3C validator