2sqlem8 - Intuitionistic Logic Explorer

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

Theorem 2sqlem8 15472

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 9697	. . . 4 ⊢ (𝑀 ∈ (ℤ_≥‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
4	2, 3	sylib 122	. . 3 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
5	4	simpld 112	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
6		2sqlem9.7	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∥ 𝑁)
7		eluzelz 9629	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘2) → 𝑀 ∈ ℤ)
8	2, 7	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
9		2sqlem8.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
10	9	nnzd 9466	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
11		2sqlem8.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℤ)
12		2sqlem8.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
13	11, 5, 12	4sqlem5 12578	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ∈ ℤ ∧ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
14	13	simpld 112	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℤ)
15		zsqcl 10721	. . . . . . . . . 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 12578	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 ∈ ℤ ∧ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
20	19	simpld 112	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℤ)
21		zsqcl 10721	. . . . . . . . . 10 ⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
22	20, 21	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐷↑2) ∈ ℤ)
23	16, 22	zaddcld 9471	. . . . . . . 8 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ)
24		zsqcl 10721	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
25	11, 24	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑2) ∈ ℤ)
26	25, 16	zsubcld 9472	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴↑2) − (𝐶↑2)) ∈ ℤ)
27		zsqcl 10721	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
28	17, 27	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵↑2) ∈ ℤ)
29	28, 22	zsubcld 9472	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵↑2) − (𝐷↑2)) ∈ ℤ)
30	11, 5, 12	4sqlem8 12581	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐶↑2)))
31	17, 5, 18	4sqlem8 12581	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐷↑2)))
32	8, 26, 29, 30, 31	dvds2addd 12013	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
33		2sqlem8.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 = ((𝐴↑2) + (𝐵↑2)))
34	33	oveq1d 5940	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))))
35	25	zcnd 9468	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
36	28	zcnd 9468	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
37	16	zcnd 9468	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
38	22	zcnd 9468	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
39	35, 36, 37, 38	addsub4d 8403	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
40	34, 39	eqtrd 2229	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
41	32, 40	breqtrrd 4062	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2))))
42		dvdssub2 12019	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) ∧ 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2)))) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ((𝐶↑2) + (𝐷↑2))))
43	8, 10, 23, 41, 42	syl31anc 1252	. . . . . . 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 15471	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ)
49	48	nnzd 9466	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℤ)
50		zsqcl2 10728	. . . . . . . . . 10 ⊢ ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℕ₀)
51	49, 50	syl 14	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ₀)
52	51	nn0cnd 9323	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℂ)
53		2sqlem8.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐶 / (𝐶 gcd 𝐷))
54		gcddvds 12157	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
55	14, 20, 54	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
56	55	simpld 112	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐶)
57	48	nnne0d 9054	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 gcd 𝐷) ≠ 0)
58		dvdsval2 11974	. . . . . . . . . . . . 13 ⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐶 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
59	49, 57, 14, 58	syl3anc 1249	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
60	56, 59	mpbid 147	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ)
61	53, 60	eqeltrid 2283	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℤ)
62		zsqcl2 10728	. . . . . . . . . 10 ⊢ (𝐸 ∈ ℤ → (𝐸↑2) ∈ ℕ₀)
63	61, 62	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐸↑2) ∈ ℕ₀)
64	63	nn0cnd 9323	. . . . . . . 8 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
65		2sqlem8.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝐷 / (𝐶 gcd 𝐷))
66	55	simprd 114	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐷)
67		dvdsval2 11974	. . . . . . . . . . . . 13 ⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
68	49, 57, 20, 67	syl3anc 1249	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
69	66, 68	mpbid 147	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ)
70	65, 69	eqeltrid 2283	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ℤ)
71		zsqcl2 10728	. . . . . . . . . 10 ⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈ ℕ₀)
72	70, 71	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐹↑2) ∈ ℕ₀)
73	72	nn0cnd 9323	. . . . . . . 8 ⊢ (𝜑 → (𝐹↑2) ∈ ℂ)
74	52, 64, 73	adddid 8070	. . . . . . 7 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))))
75	49	zcnd 9468	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℂ)
76	61	zcnd 9468	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℂ)
77	75, 76	sqmuld 10796	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)))
78	53	oveq2i 5936	. . . . . . . . . . 11 ⊢ ((𝐶 gcd 𝐷) · 𝐸) = ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷)))
79	14	zcnd 9468	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℂ)
80	48	nnap0d 9055	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 gcd 𝐷) # 0)
81	79, 75, 80	divcanap2d 8838	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷))) = 𝐶)
82	78, 81	eqtrid 2241	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 𝐸) = 𝐶)
83	82	oveq1d 5940	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (𝐶↑2))
84	77, 83	eqtr3d 2231	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) = (𝐶↑2))
85	70	zcnd 9468	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ℂ)
86	75, 85	sqmuld 10796	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)))
87	65	oveq2i 5936	. . . . . . . . . . 11 ⊢ ((𝐶 gcd 𝐷) · 𝐹) = ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷)))
88	20	zcnd 9468	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 ∈ ℂ)
89	88, 75, 80	divcanap2d 8838	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷))) = 𝐷)
90	87, 89	eqtrid 2241	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 𝐹) = 𝐷)
91	90	oveq1d 5940	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (𝐷↑2))
92	86, 91	eqtr3d 2231	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)) = (𝐷↑2))
93	84, 92	oveq12d 5943	. . . . . . 7 ⊢ (𝜑 → ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
94	74, 93	eqtrd 2229	. . . . . 6 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
95	44, 94	breqtrrd 4062	. . . . 5 ⊢ (𝜑 → 𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
96		zsqcl 10721	. . . . . . . 8 ⊢ ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
97	49, 96	syl 14	. . . . . . 7 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
98	8, 97	gcdcomd 12168	. . . . . 6 ⊢ (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = (((𝐶 gcd 𝐷)↑2) gcd 𝑀))
99	49, 8	gcdcld 12162	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ₀)
100	99	nn0zd 9465	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ)
101		gcddvds 12157	. . . . . . . . . . . . . 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 12014	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶)
105	11, 14	zsubcld 9472	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℤ)
106	102	simprd 114	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀)
107	13	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ)
108	5	nnne0d 9054	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ≠ 0)
109		dvdsval2 11974	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐴 − 𝐶) ∈ ℤ) → (𝑀 ∥ (𝐴 − 𝐶) ↔ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
110	8, 108, 105, 109	syl3anc 1249	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 ∥ (𝐴 − 𝐶) ↔ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
111	107, 110	mpbird 167	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∥ (𝐴 − 𝐶))
112	100, 8, 105, 106, 111	dvdstrd 12014	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴 − 𝐶))
113		dvdssub2 12019	. . . . . . . . . . . 12 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴 − 𝐶)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
114	100, 11, 14, 112, 113	syl31anc 1252	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
115	104, 114	mpbird 167	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴)
116	100, 49, 20, 103, 66	dvdstrd 12014	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷)
117	17, 20	zsubcld 9472	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐷) ∈ ℤ)
118	19	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ)
119		dvdsval2 11974	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐵 − 𝐷) ∈ ℤ) → (𝑀 ∥ (𝐵 − 𝐷) ↔ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
120	8, 108, 117, 119	syl3anc 1249	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 ∥ (𝐵 − 𝐷) ↔ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
121	118, 120	mpbird 167	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∥ (𝐵 − 𝐷))
122	100, 8, 117, 106, 121	dvdstrd 12014	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵 − 𝐷))
123		dvdssub2 12019	. . . . . . . . . . . 12 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵 − 𝐷)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
124	100, 17, 20, 122, 123	syl31anc 1252	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
125	116, 124	mpbird 167	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵)
126		1ne0 9077	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
127	126	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ≠ 0)
128	47, 127	eqnetrd 2391	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 gcd 𝐵) ≠ 0)
129	128	neneqd 2388	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ (𝐴 gcd 𝐵) = 0)
130		gcdeq0 12171	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
131	11, 17, 130	syl2anc 411	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
132	129, 131	mtbid 673	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
133		dvdslegcd 12158	. . . . . . . . . . 11 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
134	100, 11, 17, 132, 133	syl31anc 1252	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
135	115, 125, 134	mp2and 433	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵))
136	135, 47	breqtrd 4060	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1)
137		simpr 110	. . . . . . . . . . . 12 ⊢ (((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
138	137	necon3ai 2416	. . . . . . . . . . 11 ⊢ (𝑀 ≠ 0 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
139	108, 138	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
140		gcdn0cl 12156	. . . . . . . . . 10 ⊢ ((((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0)) → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
141	49, 8, 139, 140	syl21anc 1248	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
142		nnle1eq1 9033	. . . . . . . . 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 9171	. . . . . . . . 9 ⊢ 2 ∈ ℕ
146	145	a1i 9	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℕ)
147		rplpwr 12221	. . . . . . . 8 ⊢ (((𝐶 gcd 𝐷) ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 2 ∈ ℕ) → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
148	48, 5, 146, 147	syl3anc 1249	. . . . . . 7 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
149	144, 148	mpd 13	. . . . . 6 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1)
150	98, 149	eqtrd 2229	. . . . 5 ⊢ (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1)
151	63, 72	nn0addcld 9325	. . . . . . 7 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ₀)
152	151	nn0zd 9465	. . . . . 6 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
153		coprmdvds 12287	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ ((𝐶 gcd 𝐷)↑2) ∈ ℤ ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
154	8, 97, 152, 153	syl3anc 1249	. . . . 5 ⊢ (𝜑 → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
155	95, 150, 154	mp2and 433	. . . 4 ⊢ (𝜑 → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2)))
156		dvdsval2 11974	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
157	8, 108, 152, 156	syl3anc 1249	. . . 4 ⊢ (𝜑 → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
158	155, 157	mpbid 147	. . 3 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
159	63	nn0red 9322	. . . . 5 ⊢ (𝜑 → (𝐸↑2) ∈ ℝ)
160	72	nn0red 9322	. . . . 5 ⊢ (𝜑 → (𝐹↑2) ∈ ℝ)
161	159, 160	readdcld 8075	. . . 4 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℝ)
162	5	nnred 9022	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℝ)
163	1, 45	2sqlem7 15470	. . . . . . 7 ⊢ 𝑌 ⊆ (𝑆 ∩ ℕ)
164		inss2 3385	. . . . . . 7 ⊢ (𝑆 ∩ ℕ) ⊆ ℕ
165	163, 164	sstri 3193	. . . . . 6 ⊢ 𝑌 ⊆ ℕ
166	61, 70	gcdcld 12162	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 gcd 𝐹) ∈ ℕ₀)
167	166	nn0cnd 9323	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 gcd 𝐹) ∈ ℂ)
168		1cnd 8061	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
169	75	mulridd 8062	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 1) = (𝐶 gcd 𝐷))
170	82, 90	oveq12d 5943	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = (𝐶 gcd 𝐷))
171	14, 20	gcdcld 12162	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ₀)
172		mulgcd 12210	. . . . . . . . . . 11 ⊢ (((𝐶 gcd 𝐷) ∈ ℕ₀ ∧ 𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
173	171, 61, 70, 172	syl3anc 1249	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
174	169, 170, 173	3eqtr2rd 2236	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)) = ((𝐶 gcd 𝐷) · 1))
175	167, 168, 75, 80, 174	mulcanapad 8709	. . . . . . . 8 ⊢ (𝜑 → (𝐸 gcd 𝐹) = 1)
176		eqidd 2197	. . . . . . . 8 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))
177		oveq1 5932	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐸 → (𝑥 gcd 𝑦) = (𝐸 gcd 𝑦))
178	177	eqeq1d 2205	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → ((𝑥 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝑦) = 1))
179		oveq1 5932	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐸 → (𝑥↑2) = (𝐸↑2))
180	179	oveq1d 5940	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐸 → ((𝑥↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝑦↑2)))
181	180	eqeq2d 2208	. . . . . . . . . 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 5933	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → (𝐸 gcd 𝑦) = (𝐸 gcd 𝐹))
184	183	eqeq1d 2205	. . . . . . . . . 10 ⊢ (𝑦 = 𝐹 → ((𝐸 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝐹) = 1))
185		oveq1 5932	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐹 → (𝑦↑2) = (𝐹↑2))
186	185	oveq2d 5941	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → ((𝐸↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝐹↑2)))
187	186	eqeq2d 2208	. . . . . . . . . 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 2883	. . . . . . . 8 ⊢ ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ ∧ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
190	61, 70, 175, 176, 189	syl112anc 1253	. . . . . . 7 ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
191		eqeq1 2203	. . . . . . . . . . 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 2522	. . . . . . . . 9 ⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
194	193, 45	elab2g 2911	. . . . . . . 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 3182	. . . . 5 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ)
198	197	nngt0d 9053	. . . 4 ⊢ (𝜑 → 0 < ((𝐸↑2) + (𝐹↑2)))
199	5	nngt0d 9053	. . . 4 ⊢ (𝜑 → 0 < 𝑀)
200	161, 162, 198, 199	divgt0d 8981	. . 3 ⊢ (𝜑 → 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀))
201		elnnz 9355	. . 3 ⊢ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ ↔ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
202	158, 200, 201	sylanbrc 417	. 2 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
203		prmnn 12305	. . . . . . . 8 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
204	203	ad2antrl 490	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℕ)
205	204	nnred 9022	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℝ)
206	158	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
207	206	zred 9467	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℝ)
208		peano2zm 9383	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
209	8, 208	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
210	209	zred 9467	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
211	210	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℝ)
212		simprr 531	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))
213		prmz 12306	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
214	213	ad2antrl 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℤ)
215	202	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
216		dvdsle 12028	. . . . . . . . . 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 10721	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℤ → (𝑀↑2) ∈ ℤ)
220	8, 219	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑2) ∈ ℤ)
221	220	zred 9467	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀↑2) ∈ ℝ)
222	221	rehalfcld 9257	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑2) / 2) ∈ ℝ)
223	16	zred 9467	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶↑2) ∈ ℝ)
224	22	zred 9467	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷↑2) ∈ ℝ)
225	223, 224	readdcld 8075	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℝ)
226		1red 8060	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℝ)
227	48	nnsqcld 10805	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ)
228	227	nnred 9022	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℝ)
229	151	nn0ge0d 9324	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ ((𝐸↑2) + (𝐹↑2)))
230	227	nnge1d 9052	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ≤ ((𝐶 gcd 𝐷)↑2))
231	226, 228, 161, 229, 230	lemul1ad 8985	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) ≤ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
232	151	nn0cnd 9323	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ)
233	232	mulid2d 8064	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) = ((𝐸↑2) + (𝐹↑2)))
234	231, 233, 94	3brtr3d 4065	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝐶↑2) + (𝐷↑2)))
235	222	rehalfcld 9257	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑀↑2) / 2) / 2) ∈ ℝ)
236	11, 5, 12	4sqlem7 12580	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶↑2) ≤ (((𝑀↑2) / 2) / 2))
237	17, 5, 18	4sqlem7 12580	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷↑2) ≤ (((𝑀↑2) / 2) / 2))
238	223, 224, 235, 235, 236, 237	le2addd 8609	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)))
239	222	recnd 8074	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀↑2) / 2) ∈ ℂ)
240	239	2halvesd 9256	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) = ((𝑀↑2) / 2))
241	238, 240	breqtrd 4060	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((𝑀↑2) / 2))
242	161, 225, 222, 234, 241	letrd 8169	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝑀↑2) / 2))
243	5	nnsqcld 10805	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑2) ∈ ℕ)
244	243	nnrpd 9788	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀↑2) ∈ ℝ⁺)
245		rphalflt 9777	. . . . . . . . . . . . . 14 ⊢ ((𝑀↑2) ∈ ℝ⁺ → ((𝑀↑2) / 2) < (𝑀↑2))
246	244, 245	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑2) / 2) < (𝑀↑2))
247	161, 222, 221, 242, 246	lelttrd 8170	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀↑2))
248	8	zcnd 9468	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℂ)
249	248	sqvald 10781	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
250	247, 249	breqtrd 4060	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀))
251		ltdivmul 8922	. . . . . . . . . . . 12 ⊢ ((((𝐸↑2) + (𝐹↑2)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
252	161, 162, 162, 199, 251	syl112anc 1253	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
253	250, 252	mpbird 167	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀)
254		zltlem1 9402	. . . . . . . . . . 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 8169	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (𝑀 − 1))
259	209	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℤ)
260		fznn 10183	. . . . . . . 8 ⊢ ((𝑀 − 1) ∈ ℤ → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
261	259, 260	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
262	204, 258, 261	mpbir2and 946	. . . . . 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 11998	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
268	8, 158, 267	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
269	5	nnap0d 9055	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 # 0)
270	232, 248, 269	divcanap2d 8838	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) = ((𝐸↑2) + (𝐹↑2)))
271	268, 270	breqtrd 4060	. . . . . . 7 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
272	271	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
273	214, 206, 266, 212, 272	dvdstrd 12014	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ ((𝐸↑2) + (𝐹↑2)))
274		breq1 4037	. . . . . . 7 ⊢ (𝑏 = 𝑝 → (𝑏 ∥ 𝑎 ↔ 𝑝 ∥ 𝑎))
275		eleq1w 2257	. . . . . . 7 ⊢ (𝑏 = 𝑝 → (𝑏 ∈ 𝑆 ↔ 𝑝 ∈ 𝑆))
276	274, 275	imbi12d 234	. . . . . 6 ⊢ (𝑏 = 𝑝 → ((𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ (𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆)))
277		breq2 4038	. . . . . . 7 ⊢ (𝑎 = ((𝐸↑2) + (𝐹↑2)) → (𝑝 ∥ 𝑎 ↔ 𝑝 ∥ ((𝐸↑2) + (𝐹↑2))))
278	277	imbi1d 231	. . . . . 6 ⊢ (𝑎 = ((𝐸↑2) + (𝐹↑2)) → ((𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝 ∈ 𝑆)))
279	276, 278	rspc2v 2881	. . . . 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 2570	. 2 ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ∈ 𝑆))
283		inss1 3384	. . . . 5 ⊢ (𝑆 ∩ ℕ) ⊆ 𝑆
284	163, 283	sstri 3193	. . . 4 ⊢ 𝑌 ⊆ 𝑆
285	284, 196	sselid 3182	. . 3 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑆)
286	270, 285	eqeltrd 2273	. 2 ⊢ (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) ∈ 𝑆)
287	1, 5, 202, 282, 286	2sqlem6 15469	1 ⊢ (𝜑 → 𝑀 ∈ 𝑆)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1364 ∈ wcel 2167 {cab 2182 ≠ wne 2367 ∀wral 2475 ∃wrex 2476 ∩ cin 3156 class class class wbr 4034 ↦ cmpt 4095 ran crn 4665 ‘cfv 5259 (class class class)co 5925 ℝcr 7897 0cc0 7898 1c1 7899 + caddc 7901 · cmul 7903 < clt 8080 ≤ cle 8081 − cmin 8216 / cdiv 8718 ℕcn 9009 2c2 9060 ℕ₀cn0 9268 ℤcz 9345 ℤ_≥cuz 9620 ℝ⁺crp 9747 ...cfz 10102 mod cmo 10433 ↑cexp 10649 abscabs 11181 ∥ cdvds 11971 gcd cgcd 12147 ℙcprime 12302 ℤ[i]cgz 12565

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7989 ax-resscn 7990 ax-1cn 7991 ax-1re 7992 ax-icn 7993 ax-addcl 7994 ax-addrcl 7995 ax-mulcl 7996 ax-mulrcl 7997 ax-addcom 7998 ax-mulcom 7999 ax-addass 8000 ax-mulass 8001 ax-distr 8002 ax-i2m1 8003 ax-0lt1 8004 ax-1rid 8005 ax-0id 8006 ax-rnegex 8007 ax-precex 8008 ax-cnre 8009 ax-pre-ltirr 8010 ax-pre-ltwlin 8011 ax-pre-lttrn 8012 ax-pre-apti 8013 ax-pre-ltadd 8014 ax-pre-mulgt0 8015 ax-pre-mulext 8016 ax-arch 8017 ax-caucvg 8018

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-po 4332 df-iso 4333 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-riota 5880 df-ov 5928 df-oprab 5929 df-mpo 5930 df-1st 6207 df-2nd 6208 df-recs 6372 df-frec 6458 df-1o 6483 df-2o 6484 df-er 6601 df-en 6809 df-sup 7059 df-pnf 8082 df-mnf 8083 df-xr 8084 df-ltxr 8085 df-le 8086 df-sub 8218 df-neg 8219 df-reap 8621 df-ap 8628 df-div 8719 df-inn 9010 df-2 9068 df-3 9069 df-4 9070 df-n0 9269 df-z 9346 df-uz 9621 df-q 9713 df-rp 9748 df-fz 10103 df-fzo 10237 df-fl 10379 df-mod 10434 df-seqfrec 10559 df-exp 10650 df-cj 11026 df-re 11027 df-im 11028 df-rsqrt 11182 df-abs 11183 df-dvds 11972 df-gcd 12148 df-prm 12303 df-gz 12566

This theorem is referenced by: 2sqlem9 15473

W3C validator