4sqlem17 - Intuitionistic Logic Explorer

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

Theorem 4sqlem17 12970

Description: Lemma for 4sq 12973. (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 12969	. . . . . 6 ⊢ (𝜑 → (𝑅 ≤ 𝑀 ∧ ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃))))
20	19	simpld 112	. . . . 5 ⊢ (𝜑 → 𝑅 ≤ 𝑀)
21	1, 2, 3, 4, 5, 6, 7	4sqlem13m 12966	. . . . . . . 8 ⊢ (𝜑 → (∃𝑗 𝑗 ∈ 𝑇 ∧ 𝑀 < 𝑃))
22	21	simpld 112	. . . . . . 7 ⊢ (𝜑 → ∃𝑗 𝑗 ∈ 𝑇)
23		1zzd 9496	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 1 ∈ ℤ)
24		nnuz 9782	. . . . . . . . . 10 ⊢ ℕ = (ℤ_≥‘1)
25	24	rabeqi 2793	. . . . . . . . 9 ⊢ {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} = {𝑖 ∈ (ℤ_≥‘1) ∣ (𝑖 · 𝑃) ∈ 𝑆}
26	6, 25	eqtri 2250	. . . . . . . 8 ⊢ 𝑇 = {𝑖 ∈ (ℤ_≥‘1) ∣ (𝑖 · 𝑃) ∈ 𝑆}
27	6	ssrab3 3311	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 ⊆ ℕ
28		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 𝑗 ∈ 𝑇)
29		elfznn 10279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ (1...𝑗) → 𝑖 ∈ ℕ)
30	29	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → 𝑖 ∈ ℕ)
31		prmnn 12672	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
32	4, 31	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑃 ∈ ℕ)
33	32	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → 𝑃 ∈ ℕ)
34	30, 33	nnmulcld 9182	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → (𝑖 · 𝑃) ∈ ℕ)
35	34	nnnn0d 9445	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → (𝑖 · 𝑃) ∈ ℕ₀)
36	1	4sqlemsdc 12963	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 · 𝑃) ∈ ℕ₀ → DECID (𝑖 · 𝑃) ∈ 𝑆)
37	35, 36	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → DECID (𝑖 · 𝑃) ∈ 𝑆)
38	23, 26, 28, 37	infssuzcldc 10485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → inf(𝑇, ℝ, < ) ∈ 𝑇)
39	22, 38	exlimddv 1945	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇)
40	7, 39	eqeltrid 2316	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ 𝑇)
41	27, 40	sselid 3223	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ)
42	41	nnred 9146	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℝ)
43	21	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < 𝑃)
44	42, 43	ltned 8283	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ≠ 𝑃)
45	41	nncnd 9147	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℂ)
46	45	sqvald 10922	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
47	46	breq1d 4096	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ (𝑀 · 𝑀) ∥ (𝑀 · 𝑃)))
48	41	nnzd 9591	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℤ)
49		prmz 12673	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
50	4, 49	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℤ)
51	41	nnne0d 9178	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≠ 0)
52		dvdscmulr 12371	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀 ∥ 𝑃))
53	48, 50, 48, 51, 52	syl112anc 1275	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀 ∥ 𝑃))
54		dvdsprm 12699	. . . . . . . . . . . . . . . 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 12967	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
64		elnn0 9394	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℕ₀ ↔ (𝑅 ∈ ℕ ∨ 𝑅 = 0))
65	63, 64	sylib 122	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑅 ∈ ℕ ∨ 𝑅 = 0))
66	62, 65	ecased 1383	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ ℕ)
67		gzreim 12942	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
68	9, 10, 67	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
69		gzcn 12935	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 + (i · 𝐵)) ∈ ℤ[i] → (𝐴 + (i · 𝐵)) ∈ ℂ)
70	68, 69	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℂ)
71	70	absvalsq2d 11734	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)))
72	9	zred 9592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ ℝ)
73	10	zred 9592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℝ)
74	72, 73	crred 11527	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
75	74	oveq1d 6028	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵)))↑2) = (𝐴↑2))
76	72, 73	crimd 11528	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
77	76	oveq1d 6028	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵)))↑2) = (𝐵↑2))
78	75, 77	oveq12d 6031	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)) = ((𝐴↑2) + (𝐵↑2)))
79	71, 78	eqtrd 2262	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2)))
80		gzreim 12942	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
81	11, 12, 80	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
82		gzcn 12935	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 + (i · 𝐷)) ∈ ℤ[i] → (𝐶 + (i · 𝐷)) ∈ ℂ)
83	81, 82	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℂ)
84	83	absvalsq2d 11734	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)))
85	11	zred 9592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
86	12	zred 9592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ∈ ℝ)
87	85, 86	crred 11527	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶)
88	87	oveq1d 6028	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℜ‘(𝐶 + (i · 𝐷)))↑2) = (𝐶↑2))
89	85, 86	crimd 11528	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷)
90	89	oveq1d 6028	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((ℑ‘(𝐶 + (i · 𝐷)))↑2) = (𝐷↑2))
91	88, 90	oveq12d 6031	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)) = ((𝐶↑2) + (𝐷↑2)))
92	84, 91	eqtrd 2262	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = ((𝐶↑2) + (𝐷↑2)))
93	79, 92	oveq12d 6031	. . . . . . . . . . . . . . . 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 6028	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 · 𝑃) / 𝑀) = ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀))
96	32	nncnd 9147	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ ℂ)
97	41	nnap0d 9179	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 # 0)
98	96, 45, 97	divcanap3d 8965	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 · 𝑃) / 𝑀) = 𝑃)
99	95, 98	eqtr3d 2264	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) = 𝑃)
100	9, 41, 13	4sqlem5 12945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ))
101	100	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐸 ∈ ℤ)
102	10, 41, 14	4sqlem5 12945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ))
103	102	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 ∈ ℤ)
104		gzreim 12942	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
105	101, 103, 104	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
106		gzcn 12935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 + (i · 𝐹)) ∈ ℤ[i] → (𝐸 + (i · 𝐹)) ∈ ℂ)
107	105, 106	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℂ)
108	107	absvalsq2d 11734	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)))
109	101	zred 9592	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐸 ∈ ℝ)
110	103	zred 9592	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 ∈ ℝ)
111	109, 110	crred 11527	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℜ‘(𝐸 + (i · 𝐹))) = 𝐸)
112	111	oveq1d 6028	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℜ‘(𝐸 + (i · 𝐹)))↑2) = (𝐸↑2))
113	109, 110	crimd 11528	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℑ‘(𝐸 + (i · 𝐹))) = 𝐹)
114	113	oveq1d 6028	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℑ‘(𝐸 + (i · 𝐹)))↑2) = (𝐹↑2))
115	112, 114	oveq12d 6031	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)) = ((𝐸↑2) + (𝐹↑2)))
116	108, 115	eqtrd 2262	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = ((𝐸↑2) + (𝐹↑2)))
117	11, 41, 15	4sqlem5 12945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ))
118	117	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ ℤ)
119	12, 41, 16	4sqlem5 12945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ))
120	119	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐻 ∈ ℤ)
121		gzreim 12942	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ ℤ ∧ 𝐻 ∈ ℤ) → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
122	118, 120, 121	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
123		gzcn 12935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 + (i · 𝐻)) ∈ ℤ[i] → (𝐺 + (i · 𝐻)) ∈ ℂ)
124	122, 123	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℂ)
125	124	absvalsq2d 11734	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)))
126	118	zred 9592	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ ℝ)
127	120	zred 9592	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐻 ∈ ℝ)
128	126, 127	crred 11527	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℜ‘(𝐺 + (i · 𝐻))) = 𝐺)
129	128	oveq1d 6028	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℜ‘(𝐺 + (i · 𝐻)))↑2) = (𝐺↑2))
130	126, 127	crimd 11528	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℑ‘(𝐺 + (i · 𝐻))) = 𝐻)
131	130	oveq1d 6028	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((ℑ‘(𝐺 + (i · 𝐻)))↑2) = (𝐻↑2))
132	129, 131	oveq12d 6031	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)) = ((𝐺↑2) + (𝐻↑2)))
133	125, 132	eqtrd 2262	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = ((𝐺↑2) + (𝐻↑2)))
134	116, 133	oveq12d 6031	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
135	134	oveq1d 6028	. . . . . . . . . . . . . 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 6031	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑃 · 𝑅))
138	66	nncnd 9147	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ ℂ)
139	96, 138	mulcomd 8191	. . . . . . . . . . . 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 9593	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℂ)
144		ax-icn 8117	. . . . . . . . . . . . . . . . . 18 ⊢ i ∈ ℂ
145	10	zcnd 9593	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℂ)
146		mulcl 8149	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i · 𝐵) ∈ ℂ)
147	144, 145, 146	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐵) ∈ ℂ)
148	101	zcnd 9593	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸 ∈ ℂ)
149	103	zcnd 9593	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ ℂ)
150		mulcl 8149	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐹 ∈ ℂ) → (i · 𝐹) ∈ ℂ)
151	144, 149, 150	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐹) ∈ ℂ)
152	143, 147, 148, 151	addsub4d 8527	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴 − 𝐸) + ((i · 𝐵) − (i · 𝐹))))
153	144	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → i ∈ ℂ)
154	153, 145, 149	subdid 8583	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · (𝐵 − 𝐹)) = ((i · 𝐵) − (i · 𝐹)))
155	154	oveq2d 6029	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) = ((𝐴 − 𝐸) + ((i · 𝐵) − (i · 𝐹))))
156	152, 155	eqtr4d 2265	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))))
157	156	oveq1d 6028	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) / 𝑀))
158	143, 148	subcld 8480	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 − 𝐸) ∈ ℂ)
159	145, 149	subcld 8480	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝐹) ∈ ℂ)
160		mulcl 8149	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (𝐵 − 𝐹) ∈ ℂ) → (i · (𝐵 − 𝐹)) ∈ ℂ)
161	144, 159, 160	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (i · (𝐵 − 𝐹)) ∈ ℂ)
162	158, 161, 45, 97	divdirapd 8999	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) / 𝑀) = (((𝐴 − 𝐸) / 𝑀) + ((i · (𝐵 − 𝐹)) / 𝑀)))
163	153, 159, 45, 97	divassapd 8996	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((i · (𝐵 − 𝐹)) / 𝑀) = (i · ((𝐵 − 𝐹) / 𝑀)))
164	163	oveq2d 6029	. . . . . . . . . . . . . 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 12942	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 − 𝐸) / 𝑀) ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ) → (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))) ∈ ℤ[i])
169	166, 167, 168	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))) ∈ ℤ[i])
170	165, 169	eqeltrd 2306	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) ∈ ℤ[i])
171	11	zcnd 9593	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ℂ)
172	12	zcnd 9593	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ∈ ℂ)
173		mulcl 8149	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐷 ∈ ℂ) → (i · 𝐷) ∈ ℂ)
174	144, 172, 173	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐷) ∈ ℂ)
175	118	zcnd 9593	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 ∈ ℂ)
176	120	zcnd 9593	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ∈ ℂ)
177		mulcl 8149	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ 𝐻 ∈ ℂ) → (i · 𝐻) ∈ ℂ)
178	144, 176, 177	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · 𝐻) ∈ ℂ)
179	171, 174, 175, 178	addsub4d 8527	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶 − 𝐺) + ((i · 𝐷) − (i · 𝐻))))
180	153, 172, 176	subdid 8583	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (i · (𝐷 − 𝐻)) = ((i · 𝐷) − (i · 𝐻)))
181	180	oveq2d 6029	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) = ((𝐶 − 𝐺) + ((i · 𝐷) − (i · 𝐻))))
182	179, 181	eqtr4d 2265	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))))
183	182	oveq1d 6028	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) / 𝑀))
184	171, 175	subcld 8480	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶 − 𝐺) ∈ ℂ)
185	172, 176	subcld 8480	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 − 𝐻) ∈ ℂ)
186		mulcl 8149	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (𝐷 − 𝐻) ∈ ℂ) → (i · (𝐷 − 𝐻)) ∈ ℂ)
187	144, 185, 186	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (i · (𝐷 − 𝐻)) ∈ ℂ)
188	184, 187, 45, 97	divdirapd 8999	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) / 𝑀) = (((𝐶 − 𝐺) / 𝑀) + ((i · (𝐷 − 𝐻)) / 𝑀)))
189	153, 185, 45, 97	divassapd 8996	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((i · (𝐷 − 𝐻)) / 𝑀) = (i · ((𝐷 − 𝐻) / 𝑀)))
190	189	oveq2d 6029	. . . . . . . . . . . . . 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 12942	. . . . . . . . . . . . . 14 ⊢ ((((𝐶 − 𝐺) / 𝑀) ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ) → (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))) ∈ ℤ[i])
195	192, 193, 194	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))) ∈ ℤ[i])
196	191, 195	eqeltrd 2306	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) ∈ ℤ[i])
197	32	nnnn0d 9445	. . . . . . . . . . . . 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 12956	. . . . . . . . . . 11 ⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) ∈ 𝑆)
200	140, 199	eqeltrrd 2307	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 · 𝑃) ∈ 𝑆)
201		oveq1 6020	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑅 → (𝑖 · 𝑃) = (𝑅 · 𝑃))
202	201	eleq1d 2298	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑅 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑅 · 𝑃) ∈ 𝑆))
203	202, 6	elrab2 2963	. . . . . . . . . 10 ⊢ (𝑅 ∈ 𝑇 ↔ (𝑅 ∈ ℕ ∧ (𝑅 · 𝑃) ∈ 𝑆))
204	66, 200, 203	sylanbrc 417	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ 𝑇)
205	204	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 𝑅 ∈ 𝑇)
206		elfznn 10279	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (1...𝑅) → 𝑖 ∈ ℕ)
207	206	adantl 277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → 𝑖 ∈ ℕ)
208	32	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → 𝑃 ∈ ℕ)
209	207, 208	nnmulcld 9182	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → (𝑖 · 𝑃) ∈ ℕ)
210	209	nnnn0d 9445	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → (𝑖 · 𝑃) ∈ ℕ₀)
211	210, 36	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → DECID (𝑖 · 𝑃) ∈ 𝑆)
212	23, 26, 205, 211	infssuzledc 10484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑅)
213	22, 212	exlimddv 1945	. . . . . 6 ⊢ (𝜑 → inf(𝑇, ℝ, < ) ≤ 𝑅)
214	7, 213	eqbrtrid 4121	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑅)
215	66	nnred 9146	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ ℝ)
216	215, 42	letri3d 8285	. . . . 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 3198 class class class wbr 4086 ‘cfv 5324 (class class class)co 6013 infcinf 7173 ℂcc 8020 ℝcr 8021 0cc0 8022 1c1 8023 ici 8024 + caddc 8025 · cmul 8027 < clt 8204 ≤ cle 8205 − cmin 8340 / cdiv 8842 ℕcn 9133 2c2 9184 ℕ₀cn0 9392 ℤcz 9469 ℤ_≥cuz 9745 ...cfz 10233 mod cmo 10574 ↑cexp 10790 ℜcre 11391 ℑcim 11392 abscabs 11548 ∥ cdvds 12338 ℙcprime 12669 ℤ[i]cgz 12932

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 4202 ax-sep 4205 ax-nul 4213 ax-pow 4262 ax-pr 4297 ax-un 4528 ax-setind 4633 ax-iinf 4684 ax-cnex 8113 ax-resscn 8114 ax-1cn 8115 ax-1re 8116 ax-icn 8117 ax-addcl 8118 ax-addrcl 8119 ax-mulcl 8120 ax-mulrcl 8121 ax-addcom 8122 ax-mulcom 8123 ax-addass 8124 ax-mulass 8125 ax-distr 8126 ax-i2m1 8127 ax-0lt1 8128 ax-1rid 8129 ax-0id 8130 ax-rnegex 8131 ax-precex 8132 ax-cnre 8133 ax-pre-ltirr 8134 ax-pre-ltwlin 8135 ax-pre-lttrn 8136 ax-pre-apti 8137 ax-pre-ltadd 8138 ax-pre-mulgt0 8139 ax-pre-mulext 8140 ax-arch 8141 ax-caucvg 8142

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 2802 df-sbc 3030 df-csb 3126 df-dif 3200 df-un 3202 df-in 3204 df-ss 3211 df-nul 3493 df-if 3604 df-pw 3652 df-sn 3673 df-pr 3674 df-op 3676 df-uni 3892 df-int 3927 df-iun 3970 df-br 4087 df-opab 4149 df-mpt 4150 df-tr 4186 df-id 4388 df-po 4391 df-iso 4392 df-iord 4461 df-on 4463 df-ilim 4464 df-suc 4466 df-iom 4687 df-xp 4729 df-rel 4730 df-cnv 4731 df-co 4732 df-dm 4733 df-rn 4734 df-res 4735 df-ima 4736 df-iota 5284 df-fun 5326 df-fn 5327 df-f 5328 df-f1 5329 df-fo 5330 df-f1o 5331 df-fv 5332 df-isom 5333 df-riota 5966 df-ov 6016 df-oprab 6017 df-mpo 6018 df-1st 6298 df-2nd 6299 df-recs 6466 df-irdg 6531 df-frec 6552 df-1o 6577 df-2o 6578 df-oadd 6581 df-er 6697 df-en 6905 df-dom 6906 df-fin 6907 df-sup 7174 df-inf 7175 df-pnf 8206 df-mnf 8207 df-xr 8208 df-ltxr 8209 df-le 8210 df-sub 8342 df-neg 8343 df-reap 8745 df-ap 8752 df-div 8843 df-inn 9134 df-2 9192 df-3 9193 df-4 9194 df-n0 9393 df-z 9470 df-uz 9746 df-q 9844 df-rp 9879 df-fz 10234 df-fzo 10368 df-fl 10520 df-mod 10575 df-seqfrec 10700 df-exp 10791 df-ihash 11028 df-cj 11393 df-re 11394 df-im 11395 df-rsqrt 11549 df-abs 11550 df-dvds 12339 df-gcd 12515 df-prm 12670 df-gz 12933

This theorem is referenced by: 4sqlem18 12971

W3C validator