2sqlem8 - Intuitionistic Logic Explorer

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

Theorem 2sqlem8 15996

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 9936	. . . 4 ⊢ (𝑀 ∈ (ℤ_≥‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
4	2, 3	sylib 122	. . 3 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
5	4	simpld 112	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
6		2sqlem9.7	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∥ 𝑁)
7		eluzelz 9863	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘2) → 𝑀 ∈ ℤ)
8	2, 7	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
9		2sqlem8.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
10	9	nnzd 9699	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
11		2sqlem8.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℤ)
12		2sqlem8.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
13	11, 5, 12	4sqlem5 13080	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ∈ ℤ ∧ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
14	13	simpld 112	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℤ)
15		zsqcl 10972	. . . . . . . . . 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 13080	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 ∈ ℤ ∧ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
20	19	simpld 112	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℤ)
21		zsqcl 10972	. . . . . . . . . 10 ⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
22	20, 21	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐷↑2) ∈ ℤ)
23	16, 22	zaddcld 9704	. . . . . . . 8 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ)
24		zsqcl 10972	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
25	11, 24	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑2) ∈ ℤ)
26	25, 16	zsubcld 9705	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴↑2) − (𝐶↑2)) ∈ ℤ)
27		zsqcl 10972	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
28	17, 27	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵↑2) ∈ ℤ)
29	28, 22	zsubcld 9705	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵↑2) − (𝐷↑2)) ∈ ℤ)
30	11, 5, 12	4sqlem8 13083	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐶↑2)))
31	17, 5, 18	4sqlem8 13083	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐷↑2)))
32	8, 26, 29, 30, 31	dvds2addd 12515	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
33		2sqlem8.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 = ((𝐴↑2) + (𝐵↑2)))
34	33	oveq1d 6065	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))))
35	25	zcnd 9701	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
36	28	zcnd 9701	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
37	16	zcnd 9701	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
38	22	zcnd 9701	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
39	35, 36, 37, 38	addsub4d 8631	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
40	34, 39	eqtrd 2265	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
41	32, 40	breqtrrd 4137	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2))))
42		dvdssub2 12521	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) ∧ 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2)))) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ((𝐶↑2) + (𝐷↑2))))
43	8, 10, 23, 41, 42	syl31anc 1277	. . . . . . 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 15995	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ)
49	48	nnzd 9699	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℤ)
50		zsqcl2 10979	. . . . . . . . . 10 ⊢ ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℕ₀)
51	49, 50	syl 14	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ₀)
52	51	nn0cnd 9555	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℂ)
53		2sqlem8.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐶 / (𝐶 gcd 𝐷))
54		gcddvds 12659	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
55	14, 20, 54	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
56	55	simpld 112	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐶)
57	48	nnne0d 9282	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 gcd 𝐷) ≠ 0)
58		dvdsval2 12476	. . . . . . . . . . . . 13 ⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐶 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
59	49, 57, 14, 58	syl3anc 1274	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
60	56, 59	mpbid 147	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ)
61	53, 60	eqeltrid 2319	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℤ)
62		zsqcl2 10979	. . . . . . . . . 10 ⊢ (𝐸 ∈ ℤ → (𝐸↑2) ∈ ℕ₀)
63	61, 62	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐸↑2) ∈ ℕ₀)
64	63	nn0cnd 9555	. . . . . . . 8 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
65		2sqlem8.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝐷 / (𝐶 gcd 𝐷))
66	55	simprd 114	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐷)
67		dvdsval2 12476	. . . . . . . . . . . . 13 ⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
68	49, 57, 20, 67	syl3anc 1274	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
69	66, 68	mpbid 147	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ)
70	65, 69	eqeltrid 2319	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ℤ)
71		zsqcl2 10979	. . . . . . . . . 10 ⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈ ℕ₀)
72	70, 71	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐹↑2) ∈ ℕ₀)
73	72	nn0cnd 9555	. . . . . . . 8 ⊢ (𝜑 → (𝐹↑2) ∈ ℂ)
74	52, 64, 73	adddid 8298	. . . . . . 7 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))))
75	49	zcnd 9701	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℂ)
76	61	zcnd 9701	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℂ)
77	75, 76	sqmuld 11047	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)))
78	53	oveq2i 6061	. . . . . . . . . . 11 ⊢ ((𝐶 gcd 𝐷) · 𝐸) = ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷)))
79	14	zcnd 9701	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℂ)
80	48	nnap0d 9283	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 gcd 𝐷) # 0)
81	79, 75, 80	divcanap2d 9066	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷))) = 𝐶)
82	78, 81	eqtrid 2277	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 𝐸) = 𝐶)
83	82	oveq1d 6065	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (𝐶↑2))
84	77, 83	eqtr3d 2267	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) = (𝐶↑2))
85	70	zcnd 9701	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ℂ)
86	75, 85	sqmuld 11047	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)))
87	65	oveq2i 6061	. . . . . . . . . . 11 ⊢ ((𝐶 gcd 𝐷) · 𝐹) = ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷)))
88	20	zcnd 9701	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 ∈ ℂ)
89	88, 75, 80	divcanap2d 9066	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷))) = 𝐷)
90	87, 89	eqtrid 2277	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 𝐹) = 𝐷)
91	90	oveq1d 6065	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (𝐷↑2))
92	86, 91	eqtr3d 2267	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)) = (𝐷↑2))
93	84, 92	oveq12d 6068	. . . . . . 7 ⊢ (𝜑 → ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
94	74, 93	eqtrd 2265	. . . . . 6 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
95	44, 94	breqtrrd 4137	. . . . 5 ⊢ (𝜑 → 𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
96		zsqcl 10972	. . . . . . . 8 ⊢ ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
97	49, 96	syl 14	. . . . . . 7 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
98	8, 97	gcdcomd 12670	. . . . . 6 ⊢ (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = (((𝐶 gcd 𝐷)↑2) gcd 𝑀))
99	49, 8	gcdcld 12664	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ₀)
100	99	nn0zd 9698	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ)
101		gcddvds 12659	. . . . . . . . . . . . . 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 12516	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶)
105	11, 14	zsubcld 9705	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℤ)
106	102	simprd 114	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀)
107	13	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ)
108	5	nnne0d 9282	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ≠ 0)
109		dvdsval2 12476	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐴 − 𝐶) ∈ ℤ) → (𝑀 ∥ (𝐴 − 𝐶) ↔ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
110	8, 108, 105, 109	syl3anc 1274	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 ∥ (𝐴 − 𝐶) ↔ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ))
111	107, 110	mpbird 167	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∥ (𝐴 − 𝐶))
112	100, 8, 105, 106, 111	dvdstrd 12516	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴 − 𝐶))
113		dvdssub2 12521	. . . . . . . . . . . 12 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴 − 𝐶)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
114	100, 11, 14, 112, 113	syl31anc 1277	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
115	104, 114	mpbird 167	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴)
116	100, 49, 20, 103, 66	dvdstrd 12516	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷)
117	17, 20	zsubcld 9705	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐷) ∈ ℤ)
118	19	simprd 114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ)
119		dvdsval2 12476	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐵 − 𝐷) ∈ ℤ) → (𝑀 ∥ (𝐵 − 𝐷) ↔ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
120	8, 108, 117, 119	syl3anc 1274	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 ∥ (𝐵 − 𝐷) ↔ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ))
121	118, 120	mpbird 167	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∥ (𝐵 − 𝐷))
122	100, 8, 117, 106, 121	dvdstrd 12516	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵 − 𝐷))
123		dvdssub2 12521	. . . . . . . . . . . 12 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵 − 𝐷)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
124	100, 17, 20, 122, 123	syl31anc 1277	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
125	116, 124	mpbird 167	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵)
126		1ne0 9305	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
127	126	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ≠ 0)
128	47, 127	eqnetrd 2436	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 gcd 𝐵) ≠ 0)
129	128	neneqd 2433	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ (𝐴 gcd 𝐵) = 0)
130		gcdeq0 12673	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
131	11, 17, 130	syl2anc 411	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
132	129, 131	mtbid 679	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
133		dvdslegcd 12660	. . . . . . . . . . 11 ⊢ (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
134	100, 11, 17, 132, 133	syl31anc 1277	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
135	115, 125, 134	mp2and 433	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵))
136	135, 47	breqtrd 4135	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1)
137		simpr 110	. . . . . . . . . . . 12 ⊢ (((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
138	137	necon3ai 2461	. . . . . . . . . . 11 ⊢ (𝑀 ≠ 0 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
139	108, 138	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
140		gcdn0cl 12658	. . . . . . . . . 10 ⊢ ((((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0)) → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
141	49, 8, 139, 140	syl21anc 1273	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
142		nnle1eq1 9261	. . . . . . . . 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 9399	. . . . . . . . 9 ⊢ 2 ∈ ℕ
146	145	a1i 9	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℕ)
147		rplpwr 12723	. . . . . . . 8 ⊢ (((𝐶 gcd 𝐷) ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 2 ∈ ℕ) → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
148	48, 5, 146, 147	syl3anc 1274	. . . . . . 7 ⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
149	144, 148	mpd 13	. . . . . 6 ⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1)
150	98, 149	eqtrd 2265	. . . . 5 ⊢ (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1)
151	63, 72	nn0addcld 9557	. . . . . . 7 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ₀)
152	151	nn0zd 9698	. . . . . 6 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
153		coprmdvds 12789	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ ((𝐶 gcd 𝐷)↑2) ∈ ℤ ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
154	8, 97, 152, 153	syl3anc 1274	. . . . 5 ⊢ (𝜑 → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
155	95, 150, 154	mp2and 433	. . . 4 ⊢ (𝜑 → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2)))
156		dvdsval2 12476	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
157	8, 108, 152, 156	syl3anc 1274	. . . 4 ⊢ (𝜑 → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
158	155, 157	mpbid 147	. . 3 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
159	63	nn0red 9554	. . . . 5 ⊢ (𝜑 → (𝐸↑2) ∈ ℝ)
160	72	nn0red 9554	. . . . 5 ⊢ (𝜑 → (𝐹↑2) ∈ ℝ)
161	159, 160	readdcld 8303	. . . 4 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℝ)
162	5	nnred 9250	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℝ)
163	1, 45	2sqlem7 15994	. . . . . . 7 ⊢ 𝑌 ⊆ (𝑆 ∩ ℕ)
164		inss2 3442	. . . . . . 7 ⊢ (𝑆 ∩ ℕ) ⊆ ℕ
165	163, 164	sstri 3247	. . . . . 6 ⊢ 𝑌 ⊆ ℕ
166	61, 70	gcdcld 12664	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 gcd 𝐹) ∈ ℕ₀)
167	166	nn0cnd 9555	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 gcd 𝐹) ∈ ℂ)
168		1cnd 8290	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
169	75	mulridd 8291	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · 1) = (𝐶 gcd 𝐷))
170	82, 90	oveq12d 6068	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = (𝐶 gcd 𝐷))
171	14, 20	gcdcld 12664	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ₀)
172		mulgcd 12712	. . . . . . . . . . 11 ⊢ (((𝐶 gcd 𝐷) ∈ ℕ₀ ∧ 𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
173	171, 61, 70, 172	syl3anc 1274	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
174	169, 170, 173	3eqtr2rd 2272	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)) = ((𝐶 gcd 𝐷) · 1))
175	167, 168, 75, 80, 174	mulcanapad 8937	. . . . . . . 8 ⊢ (𝜑 → (𝐸 gcd 𝐹) = 1)
176		eqidd 2233	. . . . . . . 8 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))
177		oveq1 6057	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐸 → (𝑥 gcd 𝑦) = (𝐸 gcd 𝑦))
178	177	eqeq1d 2241	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → ((𝑥 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝑦) = 1))
179		oveq1 6057	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐸 → (𝑥↑2) = (𝐸↑2))
180	179	oveq1d 6065	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐸 → ((𝑥↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝑦↑2)))
181	180	eqeq2d 2244	. . . . . . . . . 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 6058	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → (𝐸 gcd 𝑦) = (𝐸 gcd 𝐹))
184	183	eqeq1d 2241	. . . . . . . . . 10 ⊢ (𝑦 = 𝐹 → ((𝐸 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝐹) = 1))
185		oveq1 6057	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐹 → (𝑦↑2) = (𝐹↑2))
186	185	oveq2d 6066	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → ((𝐸↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝐹↑2)))
187	186	eqeq2d 2244	. . . . . . . . . 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 2936	. . . . . . . 8 ⊢ ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ ∧ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
190	61, 70, 175, 176, 189	syl112anc 1278	. . . . . . 7 ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
191		eqeq1 2239	. . . . . . . . . . 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 2567	. . . . . . . . 9 ⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
194	193, 45	elab2g 2964	. . . . . . . 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 3236	. . . . 5 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ)
198	197	nngt0d 9281	. . . 4 ⊢ (𝜑 → 0 < ((𝐸↑2) + (𝐹↑2)))
199	5	nngt0d 9281	. . . 4 ⊢ (𝜑 → 0 < 𝑀)
200	161, 162, 198, 199	divgt0d 9209	. . 3 ⊢ (𝜑 → 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀))
201		elnnz 9587	. . 3 ⊢ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ ↔ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
202	158, 200, 201	sylanbrc 417	. 2 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
203		prmnn 12807	. . . . . . . 8 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
204	203	ad2antrl 490	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℕ)
205	204	nnred 9250	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℝ)
206	158	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
207	206	zred 9700	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℝ)
208		peano2zm 9615	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
209	8, 208	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
210	209	zred 9700	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
211	210	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℝ)
212		simprr 533	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))
213		prmz 12808	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
214	213	ad2antrl 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℤ)
215	202	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
216		dvdsle 12530	. . . . . . . . . 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 10972	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℤ → (𝑀↑2) ∈ ℤ)
220	8, 219	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑2) ∈ ℤ)
221	220	zred 9700	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀↑2) ∈ ℝ)
222	221	rehalfcld 9485	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑2) / 2) ∈ ℝ)
223	16	zred 9700	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶↑2) ∈ ℝ)
224	22	zred 9700	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷↑2) ∈ ℝ)
225	223, 224	readdcld 8303	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℝ)
226		1red 8289	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℝ)
227	48	nnsqcld 11056	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ)
228	227	nnred 9250	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℝ)
229	151	nn0ge0d 9556	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ ((𝐸↑2) + (𝐹↑2)))
230	227	nnge1d 9280	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ≤ ((𝐶 gcd 𝐷)↑2))
231	226, 228, 161, 229, 230	lemul1ad 9213	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) ≤ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
232	151	nn0cnd 9555	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ)
233	232	mullidd 8292	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) = ((𝐸↑2) + (𝐹↑2)))
234	231, 233, 94	3brtr3d 4140	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝐶↑2) + (𝐷↑2)))
235	222	rehalfcld 9485	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑀↑2) / 2) / 2) ∈ ℝ)
236	11, 5, 12	4sqlem7 13082	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶↑2) ≤ (((𝑀↑2) / 2) / 2))
237	17, 5, 18	4sqlem7 13082	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷↑2) ≤ (((𝑀↑2) / 2) / 2))
238	223, 224, 235, 235, 236, 237	le2addd 8837	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)))
239	222	recnd 8302	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀↑2) / 2) ∈ ℂ)
240	239	2halvesd 9484	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) = ((𝑀↑2) / 2))
241	238, 240	breqtrd 4135	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((𝑀↑2) / 2))
242	161, 225, 222, 234, 241	letrd 8397	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝑀↑2) / 2))
243	5	nnsqcld 11056	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑2) ∈ ℕ)
244	243	nnrpd 10027	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀↑2) ∈ ℝ⁺)
245		rphalflt 10016	. . . . . . . . . . . . . 14 ⊢ ((𝑀↑2) ∈ ℝ⁺ → ((𝑀↑2) / 2) < (𝑀↑2))
246	244, 245	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑2) / 2) < (𝑀↑2))
247	161, 222, 221, 242, 246	lelttrd 8398	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀↑2))
248	8	zcnd 9701	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℂ)
249	248	sqvald 11032	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
250	247, 249	breqtrd 4135	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀))
251		ltdivmul 9150	. . . . . . . . . . . 12 ⊢ ((((𝐸↑2) + (𝐹↑2)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
252	161, 162, 162, 199, 251	syl112anc 1278	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
253	250, 252	mpbird 167	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀)
254		zltlem1 9635	. . . . . . . . . . 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 8397	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (𝑀 − 1))
259	209	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℤ)
260		fznn 10423	. . . . . . . 8 ⊢ ((𝑀 − 1) ∈ ℤ → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
261	259, 260	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
262	204, 258, 261	mpbir2and 953	. . . . . 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 12500	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
268	8, 158, 267	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
269	5	nnap0d 9283	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 # 0)
270	232, 248, 269	divcanap2d 9066	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) = ((𝐸↑2) + (𝐹↑2)))
271	268, 270	breqtrd 4135	. . . . . . 7 ⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
272	271	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
273	214, 206, 266, 212, 272	dvdstrd 12516	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ ((𝐸↑2) + (𝐹↑2)))
274		breq1 4112	. . . . . . 7 ⊢ (𝑏 = 𝑝 → (𝑏 ∥ 𝑎 ↔ 𝑝 ∥ 𝑎))
275		eleq1w 2293	. . . . . . 7 ⊢ (𝑏 = 𝑝 → (𝑏 ∈ 𝑆 ↔ 𝑝 ∈ 𝑆))
276	274, 275	imbi12d 234	. . . . . 6 ⊢ (𝑏 = 𝑝 → ((𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ (𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆)))
277		breq2 4113	. . . . . . 7 ⊢ (𝑎 = ((𝐸↑2) + (𝐹↑2)) → (𝑝 ∥ 𝑎 ↔ 𝑝 ∥ ((𝐸↑2) + (𝐹↑2))))
278	277	imbi1d 231	. . . . . 6 ⊢ (𝑎 = ((𝐸↑2) + (𝐹↑2)) → ((𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝 ∈ 𝑆)))
279	276, 278	rspc2v 2934	. . . . 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 2615	. 2 ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ∈ 𝑆))
283		inss1 3441	. . . . 5 ⊢ (𝑆 ∩ ℕ) ⊆ 𝑆
284	163, 283	sstri 3247	. . . 4 ⊢ 𝑌 ⊆ 𝑆
285	284, 196	sselid 3236	. . 3 ⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑆)
286	270, 285	eqeltrd 2309	. 2 ⊢ (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) ∈ 𝑆)
287	1, 5, 202, 282, 286	2sqlem6 15993	1 ⊢ (𝜑 → 𝑀 ∈ 𝑆)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1398 ∈ wcel 2203 {cab 2218 ≠ wne 2412 ∀wral 2520 ∃wrex 2521 ∩ cin 3210 class class class wbr 4109 ↦ cmpt 4171 ran crn 4750 ‘cfv 5352 (class class class)co 6050 ℝcr 8126 0cc0 8127 1c1 8128 + caddc 8130 · cmul 8132 < clt 8308 ≤ cle 8309 − cmin 8444 / cdiv 8946 ℕcn 9237 2c2 9288 ℕ₀cn0 9496 ℤcz 9577 ℤ_≥cuz 9853 ℝ⁺crp 9986 ...cfz 10342 mod cmo 10684 ↑cexp 10900 abscabs 11682 ∥ cdvds 12473 gcd cgcd 12649 ℙcprime 12804 ℤ[i]cgz 13067

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 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2205 ax-14 2206 ax-ext 2214 ax-coll 4225 ax-sep 4228 ax-nul 4236 ax-pow 4287 ax-pr 4322 ax-un 4554 ax-setind 4659 ax-iinf 4710 ax-cnex 8218 ax-resscn 8219 ax-1cn 8220 ax-1re 8221 ax-icn 8222 ax-addcl 8223 ax-addrcl 8224 ax-mulcl 8225 ax-mulrcl 8226 ax-addcom 8227 ax-mulcom 8228 ax-addass 8229 ax-mulass 8230 ax-distr 8231 ax-i2m1 8232 ax-0lt1 8233 ax-1rid 8234 ax-0id 8235 ax-rnegex 8236 ax-precex 8237 ax-cnre 8238 ax-pre-ltirr 8239 ax-pre-ltwlin 8240 ax-pre-lttrn 8241 ax-pre-apti 8242 ax-pre-ltadd 8243 ax-pre-mulgt0 8244 ax-pre-mulext 8245 ax-arch 8246 ax-caucvg 8247

This theorem depends on definitions: df-bi 117 df-stab 839 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2083 df-mo 2084 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ne 2413 df-nel 2508 df-ral 2525 df-rex 2526 df-reu 2527 df-rmo 2528 df-rab 2529 df-v 2815 df-sbc 3043 df-csb 3139 df-dif 3213 df-un 3215 df-in 3217 df-ss 3224 df-nul 3509 df-if 3621 df-pw 3671 df-sn 3695 df-pr 3696 df-op 3698 df-uni 3915 df-int 3950 df-iun 3993 df-br 4110 df-opab 4172 df-mpt 4173 df-tr 4209 df-id 4414 df-po 4417 df-iso 4418 df-iord 4487 df-on 4489 df-ilim 4490 df-suc 4492 df-iom 4713 df-xp 4755 df-rel 4756 df-cnv 4757 df-co 4758 df-dm 4759 df-rn 4760 df-res 4761 df-ima 4762 df-iota 5312 df-fun 5354 df-fn 5355 df-f 5356 df-f1 5357 df-fo 5358 df-f1o 5359 df-fv 5360 df-riota 6003 df-ov 6053 df-oprab 6054 df-mpo 6055 df-1st 6334 df-2nd 6335 df-recs 6536 df-frec 6622 df-1o 6647 df-2o 6648 df-er 6767 df-en 6976 df-sup 7275 df-pnf 8310 df-mnf 8311 df-xr 8312 df-ltxr 8313 df-le 8314 df-sub 8446 df-neg 8447 df-reap 8849 df-ap 8856 df-div 8947 df-inn 9238 df-2 9296 df-3 9297 df-4 9298 df-n0 9497 df-z 9578 df-uz 9854 df-q 9952 df-rp 9987 df-fz 10343 df-fzo 10477 df-fl 10630 df-mod 10685 df-seqfrec 10810 df-exp 10901 df-cj 11527 df-re 11528 df-im 11529 df-rsqrt 11683 df-abs 11684 df-dvds 12474 df-gcd 12650 df-prm 12805 df-gz 13068

This theorem is referenced by: 2sqlem9 15997

W3C validator