2sqlem8 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 2sqlem8		Structured version Visualization version GIF version

Theorem 2sqlem8 27660

Description: Lemma for 2sq 27664. (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 12974	. . . 4 ⊢ (𝑀 ∈ (ℤ_≥‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
4	2, 3	sylib 221	. . 3 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
5	4	simpld 500	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
6		2sqlem9.7	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∥ 𝑁)
7		eluzelz 12900	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘2) → 𝑀 ∈ ℤ)
8	2, 7	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
9		2sqlem8.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
10	9	nnzd 12644	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
11		2sqlem8.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℤ)
12		2sqlem8.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
13	11, 5, 12	4sqlem5 17038	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ∈ ℤ ∧ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
14	13	simpld 500	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℤ)
15		zsqcl 14195	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈ ℤ)
16	14, 15	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝐶↑2) ∈ ℤ)
17		2sqlem8.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℤ)
18		2sqlem8.d	. . . . . . . . . . . 12 ⊢ 𝐷 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
19	17, 5, 18	4sqlem5 17038	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 ∈ ℤ ∧ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
20	19	simpld 500	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℤ)
21		zsqcl 14195	. . . . . . . . . 10 ⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
22	20, 21	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝐷↑2) ∈ ℤ)
23	16, 22	zaddcld 12732	. . . . . . . 8 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ)
24		zsqcl 14195	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
25	11, 24	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑2) ∈ ℤ)
26	25, 16	zsubcld 12733	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴↑2) − (𝐶↑2)) ∈ ℤ)
27		zsqcl 14195	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
28	17, 27	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵↑2) ∈ ℤ)
29	28, 22	zsubcld 12733	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵↑2) − (𝐷↑2)) ∈ ℤ)
30	11, 5, 12	4sqlem8 17041	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐶↑2)))
31	17, 5, 18	4sqlem8 17041	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐷↑2)))
32	8, 26, 29, 30, 31	dvds2addd 16386	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
33		2sqlem8.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 = ((𝐴↑2) + (𝐵↑2)))
34	33	oveq1d 7431	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))))
35	25	zcnd 12729	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
36	28	zcnd 12729	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
37	16	zcnd 12729	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
38	22	zcnd 12729	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
39	35, 36, 37, 38	addsub4d 11643	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
40	34, 39	eqtrd 2797	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
41	32, 40	breqtrrd 5137	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2))))
42		dvdssub2 16395	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) ∧ 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2)))) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ((𝐶↑2) + (𝐷↑2))))
43	8, 10, 23, 41, 42	syl31anc 1400	. . . . . . 7 ⊢ (𝜑 → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ((𝐶↑2) + (𝐷↑2))))
44	6, 43	mpbid 235	. . . . . 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 27659	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ)
49	48	nnzd 12644	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℤ)
50		zsqcl2 14204	. . . . . . . . . 10 ⊢ ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℕ₀)
51	49, 50	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ₀)
52	51	nn0cnd 12594	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℂ)
53		2sqlem8.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐶 / (𝐶 gcd 𝐷))
54		gcddvds 16597	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
55	14, 20, 54	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
56	55	simpld 500	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐶)
57	48	nnne0d 12313	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 gcd 𝐷) ≠ 0)
58		dvdsval2 16349	. . . . . . . . . . . . 13 ⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐶 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
59	49, 57, 14, 58	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
60	56, 59	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ)
61	53, 60	eqeltrid 2866	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℤ)
62		zsqcl2 14204	. . . . . . . . . 10 ⊢ (𝐸 ∈ ℤ → (𝐸↑2) ∈ ℕ₀)
63	61, 62	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝐸↑2) ∈ ℕ₀)
64	63	nn0cnd 12594	. . . . . . . 8 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
65		2sqlem8.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝐷 / (𝐶 gcd 𝐷))
66	55	simprd 501	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐷)
67		dvdsval2 16349	. . . . . . . . . . . . 13 ⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
68	49, 57, 20, 67	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
69	66, 68	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ)
70	65, 69	eqeltrid 2866	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ℤ)
71		zsqcl2 14204	. . . . . . . . . 10 ⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈ ℕ₀)
72	70, 71	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝐹↑2) ∈ ℕ₀)
73	72	nn0cnd 12594	. . . . . . . 8 ⊢ (𝜑 → (𝐹↑2) ∈ ℂ)
74	52, 64, 73	adddid 11260	. . . . . . 7 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))))
75	49	zcnd 12729	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℂ)
76	61	zcnd 12729	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℂ)
77	75, 76	sqmuld 14224	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)))
78	53	oveq2i 7427	. . . . . . . . . . 11 ⊢ ((𝐶 gcd 𝐷) · 𝐸) = ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷)))
79	14	zcnd 12729	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℂ)
80	79, 75, 57	divcan2d 12020	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷))) = 𝐶)
81	78, 80	eqtrid 2809	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 𝐸) = 𝐶)
82	81	oveq1d 7431	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (𝐶↑2))
83	77, 82	eqtr3d 2799	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) = (𝐶↑2))
84	70	zcnd 12729	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ℂ)
85	75, 84	sqmuld 14224	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)))
86	65	oveq2i 7427	. . . . . . . . . . 11 ⊢ ((𝐶 gcd 𝐷) · 𝐹) = ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷)))
87	20	zcnd 12729	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 ∈ ℂ)
88	87, 75, 57	divcan2d 12020	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷))) = 𝐷)
89	86, 88	eqtrid 2809	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 𝐹) = 𝐷)
90	89	oveq1d 7431	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (𝐷↑2))
91	85, 90	eqtr3d 2799	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)) = (𝐷↑2))
92	83, 91	oveq12d 7434	. . . . . . 7 ⊢ (𝜑 → ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
93	74, 92	eqtrd 2797	. . . . . 6 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
94	44, 93	breqtrrd 5137	. . . . 5 ⊢ (𝜑 → 𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
95		zsqcl 14195	. . . . . . . 8 ⊢ ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
96	49, 95	syl 18	. . . . . . 7 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
97	8, 96	gcdcomd 16608	. . . . . 6 ⊢ (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = (((𝐶 gcd 𝐷)↑2) gcd 𝑀))
98	49, 8	gcdcld 16602	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ₀)
99	98	nn0zd 12643	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ)
100		gcddvds 16597	. . . . . . . . . . . . . 14 ⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀))
101	49, 8, 100	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀))
102	101	simpld 500	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷))
103	99, 49, 14, 102, 56	dvdstrd 16389	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶)
104	11, 14	zsubcld 12733	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℤ)
105	101	simprd 501	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀)
106	13	simprd 501	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ)
107	5	nnne0d 12313	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ≠ 0)
108		dvdsval2 16349	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐴 − 𝐶) ∈ ℤ) → (𝑀 ∥ (𝐴 − 𝐶) ↔ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
109	8, 107, 104, 108	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 ∥ (𝐴 − 𝐶) ↔ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
110	106, 109	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∥ (𝐴 − 𝐶))
111	99, 8, 104, 105, 110	dvdstrd 16389	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴 − 𝐶))
112		dvdssub2 16395	. . . . . . . . . . . 12 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴 − 𝐶)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
113	99, 11, 14, 111, 112	syl31anc 1400	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
114	103, 113	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴)
115	99, 49, 20, 102, 66	dvdstrd 16389	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷)
116	17, 20	zsubcld 12733	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐷) ∈ ℤ)
117	19	simprd 501	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ)
118		dvdsval2 16349	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐵 − 𝐷) ∈ ℤ) → (𝑀 ∥ (𝐵 − 𝐷) ↔ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
119	8, 107, 116, 118	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 ∥ (𝐵 − 𝐷) ↔ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
120	117, 119	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∥ (𝐵 − 𝐷))
121	99, 8, 116, 105, 120	dvdstrd 16389	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵 − 𝐷))
122		dvdssub2 16395	. . . . . . . . . . . 12 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵 − 𝐷)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
123	99, 17, 20, 121, 122	syl31anc 1400	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
124	115, 123	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵)
125		ax-1ne0 11196	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
126	125	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ≠ 0)
127	47, 126	eqnetrd 3024	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 gcd 𝐵) ≠ 0)
128	127	neneqd 2962	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ (𝐴 gcd 𝐵) = 0)
129		gcdeq0 16611	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
130	11, 17, 129	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
131	128, 130	mtbid 327	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
132		dvdslegcd 16598	. . . . . . . . . . 11 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
133	99, 11, 17, 131, 132	syl31anc 1400	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
134	114, 124, 133	mp2and 712	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵))
135	134, 47	breqtrd 5135	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1)
136		simpr 490	. . . . . . . . . . . 12 ⊢ (((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
137	136	necon3ai 2982	. . . . . . . . . . 11 ⊢ (𝑀 ≠ 0 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
138	107, 137	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
139		gcdn0cl 16596	. . . . . . . . . 10 ⊢ ((((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0)) → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
140	49, 8, 138, 139	syl21anc 851	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
141		nnle1eq1 12293	. . . . . . . . 9 ⊢ (((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ → (((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) = 1))
142	140, 141	syl 18	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) = 1))
143	135, 142	mpbid 235	. . . . . . 7 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) = 1)
144		2nn 12341	. . . . . . . . 9 ⊢ 2 ∈ ℕ
145	144	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℕ)
146		rplpwr 16652	. . . . . . . 8 ⊢ (((𝐶 gcd 𝐷) ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 2 ∈ ℕ) → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
147	48, 5, 145, 146	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
148	143, 147	mpd 16	. . . . . 6 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1)
149	97, 148	eqtrd 2797	. . . . 5 ⊢ (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1)
150	63, 72	nn0addcld 12596	. . . . . . 7 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ₀)
151	150	nn0zd 12643	. . . . . 6 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
152		coprmdvds 16747	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ ((𝐶 gcd 𝐷)↑2) ∈ ℤ ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
153	8, 96, 151, 152	syl3anc 1398	. . . . 5 ⊢ (𝜑 → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
154	94, 149, 153	mp2and 712	. . . 4 ⊢ (𝜑 → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2)))
155		dvdsval2 16349	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
156	8, 107, 151, 155	syl3anc 1398	. . . 4 ⊢ (𝜑 → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
157	154, 156	mpbid 235	. . 3 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
158	63	nn0red 12593	. . . . 5 ⊢ (𝜑 → (𝐸↑2) ∈ ℝ)
159	72	nn0red 12593	. . . . 5 ⊢ (𝜑 → (𝐹↑2) ∈ ℝ)
160	158, 159	readdcld 11265	. . . 4 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℝ)
161	5	nnred 12275	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℝ)
162	1, 45	2sqlem7 27658	. . . . . . 7 ⊢ 𝑌 ⊆ (𝑆 ∩ ℕ)
163		inss2 4186	. . . . . . 7 ⊢ (𝑆 ∩ ℕ) ⊆ ℕ
164	162, 163	sstri 3943	. . . . . 6 ⊢ 𝑌 ⊆ ℕ
165	61, 70	gcdcld 16602	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 gcd 𝐹) ∈ ℕ₀)
166	165	nn0cnd 12594	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 gcd 𝐹) ∈ ℂ)
167		1cnd 11229	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
168	75	mulridd 11253	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 1) = (𝐶 gcd 𝐷))
169	81, 89	oveq12d 7434	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = (𝐶 gcd 𝐷))
170	14, 20	gcdcld 16602	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ₀)
171		mulgcd 16642	. . . . . . . . . . 11 ⊢ (((𝐶 gcd 𝐷) ∈ ℕ₀ ∧ 𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
172	170, 61, 70, 171	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
173	168, 169, 172	3eqtr2rd 2804	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)) = ((𝐶 gcd 𝐷) · 1))
174	166, 167, 75, 57, 173	mulcanad 11876	. . . . . . . 8 ⊢ (𝜑 → (𝐸 gcd 𝐹) = 1)
175		eqidd 2763	. . . . . . . 8 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))
176		oveq1 7423	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐸 → (𝑥 gcd 𝑦) = (𝐸 gcd 𝑦))
177	176	eqeq1d 2764	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → ((𝑥 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝑦) = 1))
178		oveq1 7423	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐸 → (𝑥↑2) = (𝐸↑2))
179	178	oveq1d 7431	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐸 → ((𝑥↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝑦↑2)))
180	179	eqeq2d 2773	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → (((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))))
181	177, 180	anbi12d 644	. . . . . . . . 9 ⊢ (𝑥 = 𝐸 → (((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)))))
182		oveq2 7424	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → (𝐸 gcd 𝑦) = (𝐸 gcd 𝐹))
183	182	eqeq1d 2764	. . . . . . . . . 10 ⊢ (𝑦 = 𝐹 → ((𝐸 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝐹) = 1))
184		oveq1 7423	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐹 → (𝑦↑2) = (𝐹↑2))
185	184	oveq2d 7432	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → ((𝐸↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝐹↑2)))
186	185	eqeq2d 2773	. . . . . . . . . 10 ⊢ (𝑦 = 𝐹 → (((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2))))
187	183, 186	anbi12d 644	. . . . . . . . 9 ⊢ (𝑦 = 𝐹 → (((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))))
188	181, 187	rspc2ev 3592	. . . . . . . 8 ⊢ ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ ∧ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
189	61, 70, 174, 175, 188	syl112anc 1401	. . . . . . 7 ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
190		ovex 7449	. . . . . . . 8 ⊢ ((𝐸↑2) + (𝐹↑2)) ∈ V
191		eqeq1 2766	. . . . . . . . . 10 ⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (𝑧 = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
192	191	anbi2d 642	. . . . . . . . 9 ⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
193	192	2rexbidv 3229	. . . . . . . 8 ⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
194	190, 193, 45	elab2 3639	. . . . . . 7 ⊢ (((𝐸↑2) + (𝐹↑2)) ∈ 𝑌 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
195	189, 194	sylibr 237	. . . . . 6 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌)
196	164, 195	sselid 3932	. . . . 5 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ)
197	196	nngt0d 12312	. . . 4 ⊢ (𝜑 → 0 < ((𝐸↑2) + (𝐹↑2)))
198	5	nngt0d 12312	. . . 4 ⊢ (𝜑 → 0 < 𝑀)
199	160, 161, 197, 198	divgt0d 12177	. . 3 ⊢ (𝜑 → 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀))
200		elnnz 12628	. . 3 ⊢ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ ↔ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
201	157, 199, 200	sylanbrc 595	. 2 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
202		prmnn 16768	. . . . . . . 8 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
203	202	ad2antrl 741	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℕ)
204	203	nnred 12275	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℝ)
205	157	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
206	205	zred 12728	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℝ)
207		peano2zm 12664	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
208	8, 207	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
209	208	zred 12728	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
210	209	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℝ)
211		simprr 785	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))
212		prmz 16769	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
213	212	ad2antrl 741	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℤ)
214	201	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
215		dvdsle 16404	. . . . . . . . . 10 ⊢ ((𝑝 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
216	213, 214, 215	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
217	211, 216	mpd 16	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀))
218		zsqcl 14195	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℤ → (𝑀↑2) ∈ ℤ)
219	8, 218	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑2) ∈ ℤ)
220	219	zred 12728	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀↑2) ∈ ℝ)
221	220	rehalfcld 12518	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑2) / 2) ∈ ℝ)
222	16	zred 12728	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶↑2) ∈ ℝ)
223	22	zred 12728	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷↑2) ∈ ℝ)
224	222, 223	readdcld 11265	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℝ)
225		1red 11236	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℝ)
226	48	nnsqcld 14310	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ)
227	226	nnred 12275	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℝ)
228	150	nn0ge0d 12595	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ ((𝐸↑2) + (𝐹↑2)))
229	226	nnge1d 12311	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ≤ ((𝐶 gcd 𝐷)↑2))
230	225, 227, 160, 228, 229	lemul1ad 12181	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) ≤ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
231	150	nn0cnd 12594	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ)
232	231	mullidd 11254	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) = ((𝐸↑2) + (𝐹↑2)))
233	230, 232, 93	3brtr3d 5140	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝐶↑2) + (𝐷↑2)))
234	221	rehalfcld 12518	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑀↑2) / 2) / 2) ∈ ℝ)
235	11, 5, 12	4sqlem7 17040	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶↑2) ≤ (((𝑀↑2) / 2) / 2))
236	17, 5, 18	4sqlem7 17040	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷↑2) ≤ (((𝑀↑2) / 2) / 2))
237	222, 223, 234, 234, 235, 236	le2addd 11860	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)))
238	221	recnd 11264	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀↑2) / 2) ∈ ℂ)
239	238	2halvesd 12517	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) = ((𝑀↑2) / 2))
240	237, 239	breqtrd 5135	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((𝑀↑2) / 2))
241	160, 224, 221, 233, 240	letrd 11394	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝑀↑2) / 2))
242	5	nnsqcld 14310	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑2) ∈ ℕ)
243	242	nnrpd 13086	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀↑2) ∈ ℝ⁺)
244		rphalflt 13075	. . . . . . . . . . . . . 14 ⊢ ((𝑀↑2) ∈ ℝ⁺ → ((𝑀↑2) / 2) < (𝑀↑2))
245	243, 244	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑2) / 2) < (𝑀↑2))
246	160, 221, 220, 241, 245	lelttrd 11395	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀↑2))
247	8	zcnd 12729	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℂ)
248	247	sqvald 14209	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
249	246, 248	breqtrd 5135	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀))
250		ltdivmul 12117	. . . . . . . . . . . 12 ⊢ ((((𝐸↑2) + (𝐹↑2)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
251	160, 161, 161, 198, 250	syl112anc 1401	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
252	249, 251	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀)
253		zltlem1 12674	. . . . . . . . . . 11 ⊢ (((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)))
254	157, 8, 253	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)))
255	252, 254	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))
256	255	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))
257	204, 206, 210, 217, 256	letrd 11394	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (𝑀 − 1))
258	208	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℤ)
259		fznn 13649	. . . . . . . 8 ⊢ ((𝑀 − 1) ∈ ℤ → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
260	258, 259	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
261	203, 257, 260	mpbir2and 726	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ (1...(𝑀 − 1)))
262	195	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌)
263	261, 262	jca 521	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌))
264	46	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))
265	151	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
266		dvdsmul2 16372	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
267	8, 157, 266	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
268	231, 247, 107	divcan2d 12020	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) = ((𝐸↑2) + (𝐹↑2)))
269	267, 268	breqtrd 5135	. . . . . . 7 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
270	269	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
271	213, 205, 265, 211, 270	dvdstrd 16389	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ ((𝐸↑2) + (𝐹↑2)))
272		breq1 5110	. . . . . . 7 ⊢ (𝑏 = 𝑝 → (𝑏 ∥ 𝑎 ↔ 𝑝 ∥ 𝑎))
273		eleq1w 2845	. . . . . . 7 ⊢ (𝑏 = 𝑝 → (𝑏 ∈ 𝑆 ↔ 𝑝 ∈ 𝑆))
274	272, 273	imbi12d 347	. . . . . 6 ⊢ (𝑏 = 𝑝 → ((𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ (𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆)))
275		breq2 5111	. . . . . . 7 ⊢ (𝑎 = ((𝐸↑2) + (𝐹↑2)) → (𝑝 ∥ 𝑎 ↔ 𝑝 ∥ ((𝐸↑2) + (𝐹↑2))))
276	275	imbi1d 344	. . . . . 6 ⊢ (𝑎 = ((𝐸↑2) + (𝐹↑2)) → ((𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝 ∈ 𝑆)))
277	274, 276	rspc2v 3590	. . . . 5 ⊢ ((𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌) → (∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) → (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝 ∈ 𝑆)))
278	263, 264, 271, 277	syl3c 67	. . . 4 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ 𝑆)
279	278	expr 462	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ∈ 𝑆))
280	279	ralrimiva 3156	. 2 ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ∈ 𝑆))
281		inss1 4185	. . . . 5 ⊢ (𝑆 ∩ ℕ) ⊆ 𝑆
282	162, 281	sstri 3943	. . . 4 ⊢ 𝑌 ⊆ 𝑆
283	282, 195	sselid 3932	. . 3 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑆)
284	268, 283	eqeltrd 2862	. 2 ⊢ (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) ∈ 𝑆)
285	1, 5, 201, 280, 284	2sqlem6 27657	1 ⊢ (𝜑 → 𝑀 ∈ 𝑆)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 {cab 2740 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 ∩ cin 3901 class class class wbr 5107 ↦ cmpt 5190 ran crn 5660 ‘cfv 6537 (class class class)co 7416 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 < clt 11270 ≤ cle 11271 − cmin 11468 / cdiv 11898 ℕcn 12260 2c2 12322 ℕ₀cn0 12531 ℤcz 12618 ℤ_≥cuz 12890 ℝ⁺crp 13044 ...cfz 13563 mod cmo 13932 ↑cexp 14127 abscabs 15323 ∥ cdvds 16346 gcd cgcd 16588 ℙcprime 16765 ℤ[i]cgz 17025

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-2o 8459 df-er 8699 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-sup 9415 df-inf 9416 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-n0 12532 df-z 12619 df-uz 12891 df-rp 13045 df-fz 13564 df-fl 13855 df-mod 13933 df-seq 14068 df-exp 14128 df-cj 15188 df-re 15189 df-im 15190 df-sqrt 15324 df-abs 15325 df-dvds 16347 df-gcd 16589 df-prm 16766 df-gz 17026

This theorem is used by: 2sqlem9 27661

W3C validator