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 27344

Description: Lemma for 2sq 27348. (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 12888	. . . 4 ⊢ (𝑀 ∈ (ℤ_≥‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
4	2, 3	sylib 218	. . 3 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
5	4	simpld 494	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
6		2sqlem9.7	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∥ 𝑁)
7		eluzelz 12810	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘2) → 𝑀 ∈ ℤ)
8	2, 7	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
9		2sqlem8.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
10	9	nnzd 12563	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
11		2sqlem8.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℤ)
12		2sqlem8.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
13	11, 5, 12	4sqlem5 16920	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ∈ ℤ ∧ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
14	13	simpld 494	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℤ)
15		zsqcl 14101	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈ ℤ)
16	14, 15	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐶↑2) ∈ ℤ)
17		2sqlem8.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℤ)
18		2sqlem8.d	. . . . . . . . . . . 12 ⊢ 𝐷 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
19	17, 5, 18	4sqlem5 16920	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 ∈ ℤ ∧ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
20	19	simpld 494	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℤ)
21		zsqcl 14101	. . . . . . . . . 10 ⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
22	20, 21	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐷↑2) ∈ ℤ)
23	16, 22	zaddcld 12649	. . . . . . . 8 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ)
24		zsqcl 14101	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
25	11, 24	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑2) ∈ ℤ)
26	25, 16	zsubcld 12650	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴↑2) − (𝐶↑2)) ∈ ℤ)
27		zsqcl 14101	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
28	17, 27	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵↑2) ∈ ℤ)
29	28, 22	zsubcld 12650	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵↑2) − (𝐷↑2)) ∈ ℤ)
30	11, 5, 12	4sqlem8 16923	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐶↑2)))
31	17, 5, 18	4sqlem8 16923	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐷↑2)))
32	8, 26, 29, 30, 31	dvds2addd 16269	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
33		2sqlem8.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 = ((𝐴↑2) + (𝐵↑2)))
34	33	oveq1d 7405	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))))
35	25	zcnd 12646	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
36	28	zcnd 12646	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
37	16	zcnd 12646	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
38	22	zcnd 12646	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
39	35, 36, 37, 38	addsub4d 11587	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
40	34, 39	eqtrd 2765	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
41	32, 40	breqtrrd 5138	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2))))
42		dvdssub2 16278	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) ∧ 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2)))) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ((𝐶↑2) + (𝐷↑2))))
43	8, 10, 23, 41, 42	syl31anc 1375	. . . . . . 7 ⊢ (𝜑 → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ((𝐶↑2) + (𝐷↑2))))
44	6, 43	mpbid 232	. . . . . 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 27343	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ)
49	48	nnzd 12563	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℤ)
50		zsqcl2 14110	. . . . . . . . . 10 ⊢ ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℕ₀)
51	49, 50	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ₀)
52	51	nn0cnd 12512	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℂ)
53		2sqlem8.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐶 / (𝐶 gcd 𝐷))
54		gcddvds 16480	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
55	14, 20, 54	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
56	55	simpld 494	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐶)
57	48	nnne0d 12243	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 gcd 𝐷) ≠ 0)
58		dvdsval2 16232	. . . . . . . . . . . . 13 ⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐶 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
59	49, 57, 14, 58	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
60	56, 59	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ)
61	53, 60	eqeltrid 2833	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℤ)
62		zsqcl2 14110	. . . . . . . . . 10 ⊢ (𝐸 ∈ ℤ → (𝐸↑2) ∈ ℕ₀)
63	61, 62	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐸↑2) ∈ ℕ₀)
64	63	nn0cnd 12512	. . . . . . . 8 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
65		2sqlem8.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝐷 / (𝐶 gcd 𝐷))
66	55	simprd 495	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐷)
67		dvdsval2 16232	. . . . . . . . . . . . 13 ⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
68	49, 57, 20, 67	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
69	66, 68	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ)
70	65, 69	eqeltrid 2833	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ℤ)
71		zsqcl2 14110	. . . . . . . . . 10 ⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈ ℕ₀)
72	70, 71	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐹↑2) ∈ ℕ₀)
73	72	nn0cnd 12512	. . . . . . . 8 ⊢ (𝜑 → (𝐹↑2) ∈ ℂ)
74	52, 64, 73	adddid 11205	. . . . . . 7 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))))
75	49	zcnd 12646	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℂ)
76	61	zcnd 12646	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℂ)
77	75, 76	sqmuld 14130	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)))
78	53	oveq2i 7401	. . . . . . . . . . 11 ⊢ ((𝐶 gcd 𝐷) · 𝐸) = ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷)))
79	14	zcnd 12646	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℂ)
80	79, 75, 57	divcan2d 11967	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷))) = 𝐶)
81	78, 80	eqtrid 2777	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 𝐸) = 𝐶)
82	81	oveq1d 7405	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (𝐶↑2))
83	77, 82	eqtr3d 2767	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) = (𝐶↑2))
84	70	zcnd 12646	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ℂ)
85	75, 84	sqmuld 14130	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)))
86	65	oveq2i 7401	. . . . . . . . . . 11 ⊢ ((𝐶 gcd 𝐷) · 𝐹) = ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷)))
87	20	zcnd 12646	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 ∈ ℂ)
88	87, 75, 57	divcan2d 11967	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷))) = 𝐷)
89	86, 88	eqtrid 2777	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 𝐹) = 𝐷)
90	89	oveq1d 7405	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (𝐷↑2))
91	85, 90	eqtr3d 2767	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)) = (𝐷↑2))
92	83, 91	oveq12d 7408	. . . . . . 7 ⊢ (𝜑 → ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
93	74, 92	eqtrd 2765	. . . . . 6 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
94	44, 93	breqtrrd 5138	. . . . 5 ⊢ (𝜑 → 𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
95		zsqcl 14101	. . . . . . . 8 ⊢ ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
96	49, 95	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
97	8, 96	gcdcomd 16491	. . . . . 6 ⊢ (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = (((𝐶 gcd 𝐷)↑2) gcd 𝑀))
98	49, 8	gcdcld 16485	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ₀)
99	98	nn0zd 12562	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ)
100		gcddvds 16480	. . . . . . . . . . . . . 14 ⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀))
101	49, 8, 100	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀))
102	101	simpld 494	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷))
103	99, 49, 14, 102, 56	dvdstrd 16272	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶)
104	11, 14	zsubcld 12650	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℤ)
105	101	simprd 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀)
106	13	simprd 495	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ)
107	5	nnne0d 12243	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ≠ 0)
108		dvdsval2 16232	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐴 − 𝐶) ∈ ℤ) → (𝑀 ∥ (𝐴 − 𝐶) ↔ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
109	8, 107, 104, 108	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 ∥ (𝐴 − 𝐶) ↔ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
110	106, 109	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∥ (𝐴 − 𝐶))
111	99, 8, 104, 105, 110	dvdstrd 16272	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴 − 𝐶))
112		dvdssub2 16278	. . . . . . . . . . . 12 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴 − 𝐶)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
113	99, 11, 14, 111, 112	syl31anc 1375	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
114	103, 113	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴)
115	99, 49, 20, 102, 66	dvdstrd 16272	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷)
116	17, 20	zsubcld 12650	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐷) ∈ ℤ)
117	19	simprd 495	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ)
118		dvdsval2 16232	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐵 − 𝐷) ∈ ℤ) → (𝑀 ∥ (𝐵 − 𝐷) ↔ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
119	8, 107, 116, 118	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 ∥ (𝐵 − 𝐷) ↔ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
120	117, 119	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∥ (𝐵 − 𝐷))
121	99, 8, 116, 105, 120	dvdstrd 16272	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵 − 𝐷))
122		dvdssub2 16278	. . . . . . . . . . . 12 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵 − 𝐷)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
123	99, 17, 20, 121, 122	syl31anc 1375	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
124	115, 123	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵)
125		ax-1ne0 11144	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
126	125	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ≠ 0)
127	47, 126	eqnetrd 2993	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 gcd 𝐵) ≠ 0)
128	127	neneqd 2931	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ (𝐴 gcd 𝐵) = 0)
129		gcdeq0 16494	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
130	11, 17, 129	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
131	128, 130	mtbid 324	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
132		dvdslegcd 16481	. . . . . . . . . . 11 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
133	99, 11, 17, 131, 132	syl31anc 1375	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
134	114, 124, 133	mp2and 699	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵))
135	134, 47	breqtrd 5136	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1)
136		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
137	136	necon3ai 2951	. . . . . . . . . . 11 ⊢ (𝑀 ≠ 0 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
138	107, 137	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
139		gcdn0cl 16479	. . . . . . . . . 10 ⊢ ((((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0)) → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
140	49, 8, 138, 139	syl21anc 837	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
141		nnle1eq1 12223	. . . . . . . . 9 ⊢ (((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ → (((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) = 1))
142	140, 141	syl 17	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) = 1))
143	135, 142	mpbid 232	. . . . . . 7 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) = 1)
144		2nn 12266	. . . . . . . . 9 ⊢ 2 ∈ ℕ
145	144	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℕ)
146		rplpwr 16535	. . . . . . . 8 ⊢ (((𝐶 gcd 𝐷) ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 2 ∈ ℕ) → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
147	48, 5, 145, 146	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
148	143, 147	mpd 15	. . . . . 6 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1)
149	97, 148	eqtrd 2765	. . . . 5 ⊢ (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1)
150	63, 72	nn0addcld 12514	. . . . . . 7 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ₀)
151	150	nn0zd 12562	. . . . . 6 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
152		coprmdvds 16630	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ ((𝐶 gcd 𝐷)↑2) ∈ ℤ ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
153	8, 96, 151, 152	syl3anc 1373	. . . . 5 ⊢ (𝜑 → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
154	94, 149, 153	mp2and 699	. . . 4 ⊢ (𝜑 → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2)))
155		dvdsval2 16232	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
156	8, 107, 151, 155	syl3anc 1373	. . . 4 ⊢ (𝜑 → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
157	154, 156	mpbid 232	. . 3 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
158	63	nn0red 12511	. . . . 5 ⊢ (𝜑 → (𝐸↑2) ∈ ℝ)
159	72	nn0red 12511	. . . . 5 ⊢ (𝜑 → (𝐹↑2) ∈ ℝ)
160	158, 159	readdcld 11210	. . . 4 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℝ)
161	5	nnred 12208	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℝ)
162	1, 45	2sqlem7 27342	. . . . . . 7 ⊢ 𝑌 ⊆ (𝑆 ∩ ℕ)
163		inss2 4204	. . . . . . 7 ⊢ (𝑆 ∩ ℕ) ⊆ ℕ
164	162, 163	sstri 3959	. . . . . 6 ⊢ 𝑌 ⊆ ℕ
165	61, 70	gcdcld 16485	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 gcd 𝐹) ∈ ℕ₀)
166	165	nn0cnd 12512	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 gcd 𝐹) ∈ ℂ)
167		1cnd 11176	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
168	75	mulridd 11198	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 1) = (𝐶 gcd 𝐷))
169	81, 89	oveq12d 7408	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = (𝐶 gcd 𝐷))
170	14, 20	gcdcld 16485	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ₀)
171		mulgcd 16525	. . . . . . . . . . 11 ⊢ (((𝐶 gcd 𝐷) ∈ ℕ₀ ∧ 𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
172	170, 61, 70, 171	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
173	168, 169, 172	3eqtr2rd 2772	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)) = ((𝐶 gcd 𝐷) · 1))
174	166, 167, 75, 57, 173	mulcanad 11820	. . . . . . . 8 ⊢ (𝜑 → (𝐸 gcd 𝐹) = 1)
175		eqidd 2731	. . . . . . . 8 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))
176		oveq1 7397	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐸 → (𝑥 gcd 𝑦) = (𝐸 gcd 𝑦))
177	176	eqeq1d 2732	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → ((𝑥 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝑦) = 1))
178		oveq1 7397	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐸 → (𝑥↑2) = (𝐸↑2))
179	178	oveq1d 7405	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐸 → ((𝑥↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝑦↑2)))
180	179	eqeq2d 2741	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → (((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))))
181	177, 180	anbi12d 632	. . . . . . . . 9 ⊢ (𝑥 = 𝐸 → (((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)))))
182		oveq2 7398	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → (𝐸 gcd 𝑦) = (𝐸 gcd 𝐹))
183	182	eqeq1d 2732	. . . . . . . . . 10 ⊢ (𝑦 = 𝐹 → ((𝐸 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝐹) = 1))
184		oveq1 7397	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐹 → (𝑦↑2) = (𝐹↑2))
185	184	oveq2d 7406	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → ((𝐸↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝐹↑2)))
186	185	eqeq2d 2741	. . . . . . . . . 10 ⊢ (𝑦 = 𝐹 → (((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2))))
187	183, 186	anbi12d 632	. . . . . . . . 9 ⊢ (𝑦 = 𝐹 → (((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))))
188	181, 187	rspc2ev 3604	. . . . . . . 8 ⊢ ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ ∧ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
189	61, 70, 174, 175, 188	syl112anc 1376	. . . . . . 7 ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
190		ovex 7423	. . . . . . . 8 ⊢ ((𝐸↑2) + (𝐹↑2)) ∈ V
191		eqeq1 2734	. . . . . . . . . 10 ⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (𝑧 = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
192	191	anbi2d 630	. . . . . . . . 9 ⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
193	192	2rexbidv 3203	. . . . . . . 8 ⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
194	190, 193, 45	elab2 3652	. . . . . . 7 ⊢ (((𝐸↑2) + (𝐹↑2)) ∈ 𝑌 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
195	189, 194	sylibr 234	. . . . . 6 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌)
196	164, 195	sselid 3947	. . . . 5 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ)
197	196	nngt0d 12242	. . . 4 ⊢ (𝜑 → 0 < ((𝐸↑2) + (𝐹↑2)))
198	5	nngt0d 12242	. . . 4 ⊢ (𝜑 → 0 < 𝑀)
199	160, 161, 197, 198	divgt0d 12125	. . 3 ⊢ (𝜑 → 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀))
200		elnnz 12546	. . 3 ⊢ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ ↔ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
201	157, 199, 200	sylanbrc 583	. 2 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
202		prmnn 16651	. . . . . . . 8 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
203	202	ad2antrl 728	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℕ)
204	203	nnred 12208	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℝ)
205	157	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
206	205	zred 12645	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℝ)
207		peano2zm 12583	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
208	8, 207	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
209	208	zred 12645	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
210	209	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℝ)
211		simprr 772	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))
212		prmz 16652	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
213	212	ad2antrl 728	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℤ)
214	201	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
215		dvdsle 16287	. . . . . . . . . 10 ⊢ ((𝑝 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
216	213, 214, 215	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
217	211, 216	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀))
218		zsqcl 14101	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℤ → (𝑀↑2) ∈ ℤ)
219	8, 218	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑2) ∈ ℤ)
220	219	zred 12645	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀↑2) ∈ ℝ)
221	220	rehalfcld 12436	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑2) / 2) ∈ ℝ)
222	16	zred 12645	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶↑2) ∈ ℝ)
223	22	zred 12645	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷↑2) ∈ ℝ)
224	222, 223	readdcld 11210	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℝ)
225		1red 11182	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℝ)
226	48	nnsqcld 14216	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ)
227	226	nnred 12208	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℝ)
228	150	nn0ge0d 12513	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ ((𝐸↑2) + (𝐹↑2)))
229	226	nnge1d 12241	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ≤ ((𝐶 gcd 𝐷)↑2))
230	225, 227, 160, 228, 229	lemul1ad 12129	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) ≤ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
231	150	nn0cnd 12512	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ)
232	231	mullidd 11199	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) = ((𝐸↑2) + (𝐹↑2)))
233	230, 232, 93	3brtr3d 5141	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝐶↑2) + (𝐷↑2)))
234	221	rehalfcld 12436	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑀↑2) / 2) / 2) ∈ ℝ)
235	11, 5, 12	4sqlem7 16922	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶↑2) ≤ (((𝑀↑2) / 2) / 2))
236	17, 5, 18	4sqlem7 16922	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷↑2) ≤ (((𝑀↑2) / 2) / 2))
237	222, 223, 234, 234, 235, 236	le2addd 11804	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)))
238	221	recnd 11209	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀↑2) / 2) ∈ ℂ)
239	238	2halvesd 12435	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) = ((𝑀↑2) / 2))
240	237, 239	breqtrd 5136	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((𝑀↑2) / 2))
241	160, 224, 221, 233, 240	letrd 11338	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝑀↑2) / 2))
242	5	nnsqcld 14216	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑2) ∈ ℕ)
243	242	nnrpd 13000	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀↑2) ∈ ℝ⁺)
244		rphalflt 12989	. . . . . . . . . . . . . 14 ⊢ ((𝑀↑2) ∈ ℝ⁺ → ((𝑀↑2) / 2) < (𝑀↑2))
245	243, 244	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑2) / 2) < (𝑀↑2))
246	160, 221, 220, 241, 245	lelttrd 11339	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀↑2))
247	8	zcnd 12646	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℂ)
248	247	sqvald 14115	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
249	246, 248	breqtrd 5136	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀))
250		ltdivmul 12065	. . . . . . . . . . . 12 ⊢ ((((𝐸↑2) + (𝐹↑2)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
251	160, 161, 161, 198, 250	syl112anc 1376	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
252	249, 251	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀)
253		zltlem1 12593	. . . . . . . . . . 11 ⊢ (((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)))
254	157, 8, 253	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)))
255	252, 254	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))
256	255	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))
257	204, 206, 210, 217, 256	letrd 11338	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (𝑀 − 1))
258	208	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℤ)
259		fznn 13560	. . . . . . . 8 ⊢ ((𝑀 − 1) ∈ ℤ → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
260	258, 259	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
261	203, 257, 260	mpbir2and 713	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ (1...(𝑀 − 1)))
262	195	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌)
263	261, 262	jca 511	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌))
264	46	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))
265	151	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
266		dvdsmul2 16255	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
267	8, 157, 266	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
268	231, 247, 107	divcan2d 11967	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) = ((𝐸↑2) + (𝐹↑2)))
269	267, 268	breqtrd 5136	. . . . . . 7 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
270	269	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
271	213, 205, 265, 211, 270	dvdstrd 16272	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ ((𝐸↑2) + (𝐹↑2)))
272		breq1 5113	. . . . . . 7 ⊢ (𝑏 = 𝑝 → (𝑏 ∥ 𝑎 ↔ 𝑝 ∥ 𝑎))
273		eleq1w 2812	. . . . . . 7 ⊢ (𝑏 = 𝑝 → (𝑏 ∈ 𝑆 ↔ 𝑝 ∈ 𝑆))
274	272, 273	imbi12d 344	. . . . . 6 ⊢ (𝑏 = 𝑝 → ((𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ (𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆)))
275		breq2 5114	. . . . . . 7 ⊢ (𝑎 = ((𝐸↑2) + (𝐹↑2)) → (𝑝 ∥ 𝑎 ↔ 𝑝 ∥ ((𝐸↑2) + (𝐹↑2))))
276	275	imbi1d 341	. . . . . 6 ⊢ (𝑎 = ((𝐸↑2) + (𝐹↑2)) → ((𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝 ∈ 𝑆)))
277	274, 276	rspc2v 3602	. . . . 5 ⊢ ((𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌) → (∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) → (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝 ∈ 𝑆)))
278	263, 264, 271, 277	syl3c 66	. . . 4 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ 𝑆)
279	278	expr 456	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ∈ 𝑆))
280	279	ralrimiva 3126	. 2 ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ∈ 𝑆))
281		inss1 4203	. . . . 5 ⊢ (𝑆 ∩ ℕ) ⊆ 𝑆
282	162, 281	sstri 3959	. . . 4 ⊢ 𝑌 ⊆ 𝑆
283	282, 195	sselid 3947	. . 3 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑆)
284	268, 283	eqeltrd 2829	. 2 ⊢ (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) ∈ 𝑆)
285	1, 5, 201, 280, 284	2sqlem6 27341	1 ⊢ (𝜑 → 𝑀 ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 {cab 2708 ≠ wne 2926 ∀wral 3045 ∃wrex 3054 ∩ cin 3916 class class class wbr 5110 ↦ cmpt 5191 ran crn 5642 ‘cfv 6514 (class class class)co 7390 ℝcr 11074 0cc0 11075 1c1 11076 + caddc 11078 · cmul 11080 < clt 11215 ≤ cle 11216 − cmin 11412 / cdiv 11842 ℕcn 12193 2c2 12248 ℕ₀cn0 12449 ℤcz 12536 ℤ_≥cuz 12800 ℝ⁺crp 12958 ...cfz 13475 mod cmo 13838 ↑cexp 14033 abscabs 15207 ∥ cdvds 16229 gcd cgcd 16471 ℙcprime 16648 ℤ[i]cgz 16907

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7846 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-2o 8438 df-er 8674 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-sup 9400 df-inf 9401 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-n0 12450 df-z 12537 df-uz 12801 df-rp 12959 df-fz 13476 df-fl 13761 df-mod 13839 df-seq 13974 df-exp 14034 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-dvds 16230 df-gcd 16472 df-prm 16649 df-gz 16908

This theorem is referenced by: 2sqlem9 27345

W3C validator