2sqlem8 - Intuitionistic Logic Explorer

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

Theorem 2sqlem8 15851

Description: Lemma for 2sq . (Contributed by Mario Carneiro, 20-Jun-2015.)

**Hypotheses**
Ref	Expression
2sq.1	⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))
2sqlem7.2	⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}
2sqlem9.5	⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))
2sqlem9.7	⊢ (𝜑 → 𝑀 ∥ 𝑁)
2sqlem8.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
2sqlem8.m	⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘2))
2sqlem8.1	⊢ (𝜑 → 𝐴 ∈ ℤ)
2sqlem8.2	⊢ (𝜑 → 𝐵 ∈ ℤ)
2sqlem8.3	⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)
2sqlem8.4	⊢ (𝜑 → 𝑁 = ((𝐴↑2) + (𝐵↑2)))
2sqlem8.c	⊢ 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
2sqlem8.d	⊢ 𝐷 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
2sqlem8.e	⊢ 𝐸 = (𝐶 / (𝐶 gcd 𝐷))
2sqlem8.f	⊢ 𝐹 = (𝐷 / (𝐶 gcd 𝐷))

**Assertion**
Ref	Expression
2sqlem8	⊢ (𝜑 → 𝑀 ∈ 𝑆)

Distinct variable groups: 𝑎,𝑏,𝑤,𝑥,𝑦,𝑧 𝐴,𝑎,𝑥,𝑦,𝑧 𝑥,𝐶 𝜑,𝑥,𝑦 𝐵,𝑎,𝑏,𝑥,𝑦 𝑀,𝑎,𝑏,𝑥,𝑦,𝑧 𝑆,𝑎,𝑏,𝑥,𝑦,𝑧 𝑥,𝐷 𝐸,𝑎,𝑥,𝑦,𝑧 𝑥,𝑁,𝑦,𝑧 𝑌,𝑎,𝑏,𝑥,𝑦 𝐹,𝑎,𝑥,𝑦,𝑧 Allowed substitution hints: 𝜑(𝑧,𝑤,𝑎,𝑏) 𝐴(𝑤,𝑏) 𝐵(𝑧,𝑤) 𝐶(𝑦,𝑧,𝑤,𝑎,𝑏) 𝐷(𝑦,𝑧,𝑤,𝑎,𝑏) 𝑆(𝑤) 𝐸(𝑤,𝑏) 𝐹(𝑤,𝑏) 𝑀(𝑤) 𝑁(𝑤,𝑎,𝑏) 𝑌(𝑧,𝑤)

Proof of Theorem 2sqlem8 Dummy variable 𝑝 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2sq.1	. 2 ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))
2		2sqlem8.m	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘2))
3		eluz2b3 9837	. . . 4 ⊢ (𝑀 ∈ (ℤ_≥‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
4	2, 3	sylib 122	. . 3 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
5	4	simpld 112	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
6		2sqlem9.7	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∥ 𝑁)
7		eluzelz 9764	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘2) → 𝑀 ∈ ℤ)
8	2, 7	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
9		2sqlem8.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
10	9	nnzd 9600	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
11		2sqlem8.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℤ)
12		2sqlem8.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
13	11, 5, 12	4sqlem5 12954	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ∈ ℤ ∧ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
14	13	simpld 112	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℤ)
15		zsqcl 10871	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈ ℤ)
16	14, 15	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐶↑2) ∈ ℤ)
17		2sqlem8.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℤ)
18		2sqlem8.d	. . . . . . . . . . . 12 ⊢ 𝐷 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
19	17, 5, 18	4sqlem5 12954	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 ∈ ℤ ∧ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
20	19	simpld 112	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℤ)
21		zsqcl 10871	. . . . . . . . . 10 ⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
22	20, 21	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐷↑2) ∈ ℤ)
23	16, 22	zaddcld 9605	. . . . . . . 8 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ)
24		zsqcl 10871	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
25	11, 24	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑2) ∈ ℤ)
26	25, 16	zsubcld 9606	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴↑2) − (𝐶↑2)) ∈ ℤ)
27		zsqcl 10871	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
28	17, 27	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵↑2) ∈ ℤ)
29	28, 22	zsubcld 9606	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵↑2) − (𝐷↑2)) ∈ ℤ)
30	11, 5, 12	4sqlem8 12957	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐶↑2)))
31	17, 5, 18	4sqlem8 12957	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐷↑2)))
32	8, 26, 29, 30, 31	dvds2addd 12389	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
33		2sqlem8.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 = ((𝐴↑2) + (𝐵↑2)))
34	33	oveq1d 6032	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))))
35	25	zcnd 9602	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
36	28	zcnd 9602	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
37	16	zcnd 9602	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
38	22	zcnd 9602	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
39	35, 36, 37, 38	addsub4d 8536	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
40	34, 39	eqtrd 2264	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
41	32, 40	breqtrrd 4116	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2))))
42		dvdssub2 12395	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) ∧ 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2)))) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ((𝐶↑2) + (𝐷↑2))))
43	8, 10, 23, 41, 42	syl31anc 1276	. . . . . . 7 ⊢ (𝜑 → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ((𝐶↑2) + (𝐷↑2))))
44	6, 43	mpbid 147	. . . . . 6 ⊢ (𝜑 → 𝑀 ∥ ((𝐶↑2) + (𝐷↑2)))
45		2sqlem7.2	. . . . . . . . . . . 12 ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}
46		2sqlem9.5	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))
47		2sqlem8.3	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)
48	1, 45, 46, 6, 9, 2, 11, 17, 47, 33, 12, 18	2sqlem8a 15850	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ)
49	48	nnzd 9600	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℤ)
50		zsqcl2 10878	. . . . . . . . . 10 ⊢ ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℕ₀)
51	49, 50	syl 14	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ₀)
52	51	nn0cnd 9456	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℂ)
53		2sqlem8.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐶 / (𝐶 gcd 𝐷))
54		gcddvds 12533	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
55	14, 20, 54	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
56	55	simpld 112	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐶)
57	48	nnne0d 9187	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 gcd 𝐷) ≠ 0)
58		dvdsval2 12350	. . . . . . . . . . . . 13 ⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐶 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
59	49, 57, 14, 58	syl3anc 1273	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
60	56, 59	mpbid 147	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ)
61	53, 60	eqeltrid 2318	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℤ)
62		zsqcl2 10878	. . . . . . . . . 10 ⊢ (𝐸 ∈ ℤ → (𝐸↑2) ∈ ℕ₀)
63	61, 62	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐸↑2) ∈ ℕ₀)
64	63	nn0cnd 9456	. . . . . . . 8 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
65		2sqlem8.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝐷 / (𝐶 gcd 𝐷))
66	55	simprd 114	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐷)
67		dvdsval2 12350	. . . . . . . . . . . . 13 ⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
68	49, 57, 20, 67	syl3anc 1273	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
69	66, 68	mpbid 147	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ)
70	65, 69	eqeltrid 2318	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ℤ)
71		zsqcl2 10878	. . . . . . . . . 10 ⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈ ℕ₀)
72	70, 71	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐹↑2) ∈ ℕ₀)
73	72	nn0cnd 9456	. . . . . . . 8 ⊢ (𝜑 → (𝐹↑2) ∈ ℂ)
74	52, 64, 73	adddid 8203	. . . . . . 7 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))))
75	49	zcnd 9602	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℂ)
76	61	zcnd 9602	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℂ)
77	75, 76	sqmuld 10946	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)))
78	53	oveq2i 6028	. . . . . . . . . . 11 ⊢ ((𝐶 gcd 𝐷) · 𝐸) = ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷)))
79	14	zcnd 9602	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℂ)
80	48	nnap0d 9188	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 gcd 𝐷) # 0)
81	79, 75, 80	divcanap2d 8971	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷))) = 𝐶)
82	78, 81	eqtrid 2276	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 𝐸) = 𝐶)
83	82	oveq1d 6032	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (𝐶↑2))
84	77, 83	eqtr3d 2266	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) = (𝐶↑2))
85	70	zcnd 9602	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ℂ)
86	75, 85	sqmuld 10946	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)))
87	65	oveq2i 6028	. . . . . . . . . . 11 ⊢ ((𝐶 gcd 𝐷) · 𝐹) = ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷)))
88	20	zcnd 9602	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 ∈ ℂ)
89	88, 75, 80	divcanap2d 8971	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷))) = 𝐷)
90	87, 89	eqtrid 2276	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 𝐹) = 𝐷)
91	90	oveq1d 6032	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (𝐷↑2))
92	86, 91	eqtr3d 2266	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)) = (𝐷↑2))
93	84, 92	oveq12d 6035	. . . . . . 7 ⊢ (𝜑 → ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
94	74, 93	eqtrd 2264	. . . . . 6 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
95	44, 94	breqtrrd 4116	. . . . 5 ⊢ (𝜑 → 𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
96		zsqcl 10871	. . . . . . . 8 ⊢ ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
97	49, 96	syl 14	. . . . . . 7 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
98	8, 97	gcdcomd 12544	. . . . . 6 ⊢ (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = (((𝐶 gcd 𝐷)↑2) gcd 𝑀))
99	49, 8	gcdcld 12538	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ₀)
100	99	nn0zd 9599	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ)
101		gcddvds 12533	. . . . . . . . . . . . . 14 ⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀))
102	49, 8, 101	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀))
103	102	simpld 112	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷))
104	100, 49, 14, 103, 56	dvdstrd 12390	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶)
105	11, 14	zsubcld 9606	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℤ)
106	102	simprd 114	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀)
107	13	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ)
108	5	nnne0d 9187	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ≠ 0)
109		dvdsval2 12350	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐴 − 𝐶) ∈ ℤ) → (𝑀 ∥ (𝐴 − 𝐶) ↔ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
110	8, 108, 105, 109	syl3anc 1273	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 ∥ (𝐴 − 𝐶) ↔ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
111	107, 110	mpbird 167	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∥ (𝐴 − 𝐶))
112	100, 8, 105, 106, 111	dvdstrd 12390	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴 − 𝐶))
113		dvdssub2 12395	. . . . . . . . . . . 12 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴 − 𝐶)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
114	100, 11, 14, 112, 113	syl31anc 1276	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
115	104, 114	mpbird 167	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴)
116	100, 49, 20, 103, 66	dvdstrd 12390	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷)
117	17, 20	zsubcld 9606	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐷) ∈ ℤ)
118	19	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ)
119		dvdsval2 12350	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐵 − 𝐷) ∈ ℤ) → (𝑀 ∥ (𝐵 − 𝐷) ↔ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
120	8, 108, 117, 119	syl3anc 1273	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 ∥ (𝐵 − 𝐷) ↔ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
121	118, 120	mpbird 167	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∥ (𝐵 − 𝐷))
122	100, 8, 117, 106, 121	dvdstrd 12390	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵 − 𝐷))
123		dvdssub2 12395	. . . . . . . . . . . 12 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵 − 𝐷)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
124	100, 17, 20, 122, 123	syl31anc 1276	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
125	116, 124	mpbird 167	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵)
126		1ne0 9210	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
127	126	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ≠ 0)
128	47, 127	eqnetrd 2426	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 gcd 𝐵) ≠ 0)
129	128	neneqd 2423	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ (𝐴 gcd 𝐵) = 0)
130		gcdeq0 12547	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
131	11, 17, 130	syl2anc 411	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
132	129, 131	mtbid 678	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
133		dvdslegcd 12534	. . . . . . . . . . 11 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
134	100, 11, 17, 132, 133	syl31anc 1276	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
135	115, 125, 134	mp2and 433	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵))
136	135, 47	breqtrd 4114	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1)
137		simpr 110	. . . . . . . . . . . 12 ⊢ (((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
138	137	necon3ai 2451	. . . . . . . . . . 11 ⊢ (𝑀 ≠ 0 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
139	108, 138	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
140		gcdn0cl 12532	. . . . . . . . . 10 ⊢ ((((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0)) → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
141	49, 8, 139, 140	syl21anc 1272	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
142		nnle1eq1 9166	. . . . . . . . 9 ⊢ (((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ → (((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) = 1))
143	141, 142	syl 14	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) = 1))
144	136, 143	mpbid 147	. . . . . . 7 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) = 1)
145		2nn 9304	. . . . . . . . 9 ⊢ 2 ∈ ℕ
146	145	a1i 9	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℕ)
147		rplpwr 12597	. . . . . . . 8 ⊢ (((𝐶 gcd 𝐷) ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 2 ∈ ℕ) → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
148	48, 5, 146, 147	syl3anc 1273	. . . . . . 7 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
149	144, 148	mpd 13	. . . . . 6 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1)
150	98, 149	eqtrd 2264	. . . . 5 ⊢ (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1)
151	63, 72	nn0addcld 9458	. . . . . . 7 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ₀)
152	151	nn0zd 9599	. . . . . 6 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
153		coprmdvds 12663	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ ((𝐶 gcd 𝐷)↑2) ∈ ℤ ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
154	8, 97, 152, 153	syl3anc 1273	. . . . 5 ⊢ (𝜑 → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
155	95, 150, 154	mp2and 433	. . . 4 ⊢ (𝜑 → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2)))
156		dvdsval2 12350	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
157	8, 108, 152, 156	syl3anc 1273	. . . 4 ⊢ (𝜑 → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
158	155, 157	mpbid 147	. . 3 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
159	63	nn0red 9455	. . . . 5 ⊢ (𝜑 → (𝐸↑2) ∈ ℝ)
160	72	nn0red 9455	. . . . 5 ⊢ (𝜑 → (𝐹↑2) ∈ ℝ)
161	159, 160	readdcld 8208	. . . 4 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℝ)
162	5	nnred 9155	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℝ)
163	1, 45	2sqlem7 15849	. . . . . . 7 ⊢ 𝑌 ⊆ (𝑆 ∩ ℕ)
164		inss2 3428	. . . . . . 7 ⊢ (𝑆 ∩ ℕ) ⊆ ℕ
165	163, 164	sstri 3236	. . . . . 6 ⊢ 𝑌 ⊆ ℕ
166	61, 70	gcdcld 12538	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 gcd 𝐹) ∈ ℕ₀)
167	166	nn0cnd 9456	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 gcd 𝐹) ∈ ℂ)
168		1cnd 8194	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
169	75	mulridd 8195	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 1) = (𝐶 gcd 𝐷))
170	82, 90	oveq12d 6035	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = (𝐶 gcd 𝐷))
171	14, 20	gcdcld 12538	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ₀)
172		mulgcd 12586	. . . . . . . . . . 11 ⊢ (((𝐶 gcd 𝐷) ∈ ℕ₀ ∧ 𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
173	171, 61, 70, 172	syl3anc 1273	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
174	169, 170, 173	3eqtr2rd 2271	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)) = ((𝐶 gcd 𝐷) · 1))
175	167, 168, 75, 80, 174	mulcanapad 8842	. . . . . . . 8 ⊢ (𝜑 → (𝐸 gcd 𝐹) = 1)
176		eqidd 2232	. . . . . . . 8 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))
177		oveq1 6024	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐸 → (𝑥 gcd 𝑦) = (𝐸 gcd 𝑦))
178	177	eqeq1d 2240	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → ((𝑥 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝑦) = 1))
179		oveq1 6024	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐸 → (𝑥↑2) = (𝐸↑2))
180	179	oveq1d 6032	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐸 → ((𝑥↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝑦↑2)))
181	180	eqeq2d 2243	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → (((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))))
182	178, 181	anbi12d 473	. . . . . . . . 9 ⊢ (𝑥 = 𝐸 → (((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)))))
183		oveq2 6025	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → (𝐸 gcd 𝑦) = (𝐸 gcd 𝐹))
184	183	eqeq1d 2240	. . . . . . . . . 10 ⊢ (𝑦 = 𝐹 → ((𝐸 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝐹) = 1))
185		oveq1 6024	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐹 → (𝑦↑2) = (𝐹↑2))
186	185	oveq2d 6033	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → ((𝐸↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝐹↑2)))
187	186	eqeq2d 2243	. . . . . . . . . 10 ⊢ (𝑦 = 𝐹 → (((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2))))
188	184, 187	anbi12d 473	. . . . . . . . 9 ⊢ (𝑦 = 𝐹 → (((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))))
189	182, 188	rspc2ev 2925	. . . . . . . 8 ⊢ ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ ∧ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
190	61, 70, 175, 176, 189	syl112anc 1277	. . . . . . 7 ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
191		eqeq1 2238	. . . . . . . . . . 11 ⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (𝑧 = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
192	191	anbi2d 464	. . . . . . . . . 10 ⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
193	192	2rexbidv 2557	. . . . . . . . 9 ⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
194	193, 45	elab2g 2953	. . . . . . . 8 ⊢ (((𝐸↑2) + (𝐹↑2)) ∈ ℕ₀ → (((𝐸↑2) + (𝐹↑2)) ∈ 𝑌 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
195	151, 194	syl 14	. . . . . . 7 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) ∈ 𝑌 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
196	190, 195	mpbird 167	. . . . . 6 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌)
197	165, 196	sselid 3225	. . . . 5 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ)
198	197	nngt0d 9186	. . . 4 ⊢ (𝜑 → 0 < ((𝐸↑2) + (𝐹↑2)))
199	5	nngt0d 9186	. . . 4 ⊢ (𝜑 → 0 < 𝑀)
200	161, 162, 198, 199	divgt0d 9114	. . 3 ⊢ (𝜑 → 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀))
201		elnnz 9488	. . 3 ⊢ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ ↔ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
202	158, 200, 201	sylanbrc 417	. 2 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
203		prmnn 12681	. . . . . . . 8 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
204	203	ad2antrl 490	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℕ)
205	204	nnred 9155	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℝ)
206	158	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
207	206	zred 9601	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℝ)
208		peano2zm 9516	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
209	8, 208	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
210	209	zred 9601	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
211	210	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℝ)
212		simprr 533	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))
213		prmz 12682	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
214	213	ad2antrl 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℤ)
215	202	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
216		dvdsle 12404	. . . . . . . . . 10 ⊢ ((𝑝 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
217	214, 215, 216	syl2anc 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
218	212, 217	mpd 13	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀))
219		zsqcl 10871	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℤ → (𝑀↑2) ∈ ℤ)
220	8, 219	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑2) ∈ ℤ)
221	220	zred 9601	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀↑2) ∈ ℝ)
222	221	rehalfcld 9390	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑2) / 2) ∈ ℝ)
223	16	zred 9601	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶↑2) ∈ ℝ)
224	22	zred 9601	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷↑2) ∈ ℝ)
225	223, 224	readdcld 8208	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℝ)
226		1red 8193	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℝ)
227	48	nnsqcld 10955	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ)
228	227	nnred 9155	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℝ)
229	151	nn0ge0d 9457	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ ((𝐸↑2) + (𝐹↑2)))
230	227	nnge1d 9185	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ≤ ((𝐶 gcd 𝐷)↑2))
231	226, 228, 161, 229, 230	lemul1ad 9118	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) ≤ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
232	151	nn0cnd 9456	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ)
233	232	mulid2d 8197	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) = ((𝐸↑2) + (𝐹↑2)))
234	231, 233, 94	3brtr3d 4119	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝐶↑2) + (𝐷↑2)))
235	222	rehalfcld 9390	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑀↑2) / 2) / 2) ∈ ℝ)
236	11, 5, 12	4sqlem7 12956	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶↑2) ≤ (((𝑀↑2) / 2) / 2))
237	17, 5, 18	4sqlem7 12956	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷↑2) ≤ (((𝑀↑2) / 2) / 2))
238	223, 224, 235, 235, 236, 237	le2addd 8742	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)))
239	222	recnd 8207	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀↑2) / 2) ∈ ℂ)
240	239	2halvesd 9389	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) = ((𝑀↑2) / 2))
241	238, 240	breqtrd 4114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((𝑀↑2) / 2))
242	161, 225, 222, 234, 241	letrd 8302	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝑀↑2) / 2))
243	5	nnsqcld 10955	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑2) ∈ ℕ)
244	243	nnrpd 9928	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀↑2) ∈ ℝ⁺)
245		rphalflt 9917	. . . . . . . . . . . . . 14 ⊢ ((𝑀↑2) ∈ ℝ⁺ → ((𝑀↑2) / 2) < (𝑀↑2))
246	244, 245	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑2) / 2) < (𝑀↑2))
247	161, 222, 221, 242, 246	lelttrd 8303	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀↑2))
248	8	zcnd 9602	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℂ)
249	248	sqvald 10931	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
250	247, 249	breqtrd 4114	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀))
251		ltdivmul 9055	. . . . . . . . . . . 12 ⊢ ((((𝐸↑2) + (𝐹↑2)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
252	161, 162, 162, 199, 251	syl112anc 1277	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
253	250, 252	mpbird 167	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀)
254		zltlem1 9536	. . . . . . . . . . 11 ⊢ (((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)))
255	158, 8, 254	syl2anc 411	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)))
256	253, 255	mpbid 147	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))
257	256	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))
258	205, 207, 211, 218, 257	letrd 8302	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (𝑀 − 1))
259	209	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℤ)
260		fznn 10323	. . . . . . . 8 ⊢ ((𝑀 − 1) ∈ ℤ → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
261	259, 260	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
262	204, 258, 261	mpbir2and 952	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ (1...(𝑀 − 1)))
263	196	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌)
264	262, 263	jca 306	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌))
265	46	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))
266	152	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
267		dvdsmul2 12374	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
268	8, 158, 267	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
269	5	nnap0d 9188	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 # 0)
270	232, 248, 269	divcanap2d 8971	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) = ((𝐸↑2) + (𝐹↑2)))
271	268, 270	breqtrd 4114	. . . . . . 7 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
272	271	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
273	214, 206, 266, 212, 272	dvdstrd 12390	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ ((𝐸↑2) + (𝐹↑2)))
274		breq1 4091	. . . . . . 7 ⊢ (𝑏 = 𝑝 → (𝑏 ∥ 𝑎 ↔ 𝑝 ∥ 𝑎))
275		eleq1w 2292	. . . . . . 7 ⊢ (𝑏 = 𝑝 → (𝑏 ∈ 𝑆 ↔ 𝑝 ∈ 𝑆))
276	274, 275	imbi12d 234	. . . . . 6 ⊢ (𝑏 = 𝑝 → ((𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ (𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆)))
277		breq2 4092	. . . . . . 7 ⊢ (𝑎 = ((𝐸↑2) + (𝐹↑2)) → (𝑝 ∥ 𝑎 ↔ 𝑝 ∥ ((𝐸↑2) + (𝐹↑2))))
278	277	imbi1d 231	. . . . . 6 ⊢ (𝑎 = ((𝐸↑2) + (𝐹↑2)) → ((𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝 ∈ 𝑆)))
279	276, 278	rspc2v 2923	. . . . 5 ⊢ ((𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌) → (∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) → (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝 ∈ 𝑆)))
280	264, 265, 273, 279	syl3c 63	. . . 4 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ 𝑆)
281	280	expr 375	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ∈ 𝑆))
282	281	ralrimiva 2605	. 2 ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ∈ 𝑆))
283		inss1 3427	. . . . 5 ⊢ (𝑆 ∩ ℕ) ⊆ 𝑆
284	163, 283	sstri 3236	. . . 4 ⊢ 𝑌 ⊆ 𝑆
285	284, 196	sselid 3225	. . 3 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑆)
286	270, 285	eqeltrd 2308	. 2 ⊢ (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) ∈ 𝑆)
287	1, 5, 202, 282, 286	2sqlem6 15848	1 ⊢ (𝜑 → 𝑀 ∈ 𝑆)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1397 ∈ wcel 2202 {cab 2217 ≠ wne 2402 ∀wral 2510 ∃wrex 2511 ∩ cin 3199 class class class wbr 4088 ↦ cmpt 4150 ran crn 4726 ‘cfv 5326 (class class class)co 6017 ℝcr 8030 0cc0 8031 1c1 8032 + caddc 8034 · cmul 8036 < clt 8213 ≤ cle 8214 − cmin 8349 / cdiv 8851 ℕcn 9142 2c2 9193 ℕ₀cn0 9401 ℤcz 9478 ℤ_≥cuz 9754 ℝ⁺crp 9887 ...cfz 10242 mod cmo 10583 ↑cexp 10799 abscabs 11557 ∥ cdvds 12347 gcd cgcd 12523 ℙcprime 12678 ℤ[i]cgz 12941

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 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 ax-cnex 8122 ax-resscn 8123 ax-1cn 8124 ax-1re 8125 ax-icn 8126 ax-addcl 8127 ax-addrcl 8128 ax-mulcl 8129 ax-mulrcl 8130 ax-addcom 8131 ax-mulcom 8132 ax-addass 8133 ax-mulass 8134 ax-distr 8135 ax-i2m1 8136 ax-0lt1 8137 ax-1rid 8138 ax-0id 8139 ax-rnegex 8140 ax-precex 8141 ax-cnre 8142 ax-pre-ltirr 8143 ax-pre-ltwlin 8144 ax-pre-lttrn 8145 ax-pre-apti 8146 ax-pre-ltadd 8147 ax-pre-mulgt0 8148 ax-pre-mulext 8149 ax-arch 8150 ax-caucvg 8151

This theorem depends on definitions: df-bi 117 df-stab 838 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rmo 2518 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-po 4393 df-iso 4394 df-iord 4463 df-on 4465 df-ilim 4466 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-riota 5970 df-ov 6020 df-oprab 6021 df-mpo 6022 df-1st 6302 df-2nd 6303 df-recs 6470 df-frec 6556 df-1o 6581 df-2o 6582 df-er 6701 df-en 6909 df-sup 7182 df-pnf 8215 df-mnf 8216 df-xr 8217 df-ltxr 8218 df-le 8219 df-sub 8351 df-neg 8352 df-reap 8754 df-ap 8761 df-div 8852 df-inn 9143 df-2 9201 df-3 9202 df-4 9203 df-n0 9402 df-z 9479 df-uz 9755 df-q 9853 df-rp 9888 df-fz 10243 df-fzo 10377 df-fl 10529 df-mod 10584 df-seqfrec 10709 df-exp 10800 df-cj 11402 df-re 11403 df-im 11404 df-rsqrt 11558 df-abs 11559 df-dvds 12348 df-gcd 12524 df-prm 12679 df-gz 12942

This theorem is referenced by: 2sqlem9 15852

W3C validator