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

Theorem 4sqlem17 12442
Description: Lemma for 4sq 12445. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
Hypotheses
Ref Expression
4sqlem11.1 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
4sq.2 (𝜑𝑁 ∈ ℕ)
4sq.3 (𝜑𝑃 = ((2 · 𝑁) + 1))
4sq.4 (𝜑𝑃 ∈ ℙ)
4sq.5 (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)
4sq.6 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}
4sq.7 𝑀 = inf(𝑇, ℝ, < )
4sq.m (𝜑𝑀 ∈ (ℤ‘2))
4sq.a (𝜑𝐴 ∈ ℤ)
4sq.b (𝜑𝐵 ∈ ℤ)
4sq.c (𝜑𝐶 ∈ ℤ)
4sq.d (𝜑𝐷 ∈ ℤ)
4sq.e 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
4sq.f 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
4sq.g 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
4sq.h 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
4sq.r 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)
4sq.p (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
Assertion
Ref Expression
4sqlem17 ¬ 𝜑
Distinct variable groups:   𝑛,𝑁   𝑃,𝑖,𝑛,𝑤,𝑥,𝑦,𝑧   𝑆,𝑖,𝑛   𝑇,𝑖   𝜑,𝑖,𝑛   𝑅,𝑖   𝐶,𝑛   𝐷,𝑛   𝐴,𝑛   𝐵,𝑛   𝑛,𝐸   𝑛,𝐹   𝑛,𝐺   𝑛,𝐻   𝑛,𝑀
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤)   𝐴(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐵(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐶(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑖)   𝑅(𝑥,𝑦,𝑧,𝑤,𝑛)   𝑆(𝑥,𝑦,𝑧,𝑤)   𝑇(𝑥,𝑦,𝑧,𝑤,𝑛)   𝐸(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐹(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐺(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐻(𝑥,𝑦,𝑧,𝑤,𝑖)   𝑀(𝑥,𝑦,𝑧,𝑤,𝑖)   𝑁(𝑥,𝑦,𝑧,𝑤,𝑖)

Proof of Theorem 4sqlem17
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 4sqlem11.1 . . . . . . 7 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
2 4sq.2 . . . . . . 7 (𝜑𝑁 ∈ ℕ)
3 4sq.3 . . . . . . 7 (𝜑𝑃 = ((2 · 𝑁) + 1))
4 4sq.4 . . . . . . 7 (𝜑𝑃 ∈ ℙ)
5 4sq.5 . . . . . . 7 (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)
6 4sq.6 . . . . . . 7 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}
7 4sq.7 . . . . . . 7 𝑀 = inf(𝑇, ℝ, < )
8 4sq.m . . . . . . 7 (𝜑𝑀 ∈ (ℤ‘2))
9 4sq.a . . . . . . 7 (𝜑𝐴 ∈ ℤ)
10 4sq.b . . . . . . 7 (𝜑𝐵 ∈ ℤ)
11 4sq.c . . . . . . 7 (𝜑𝐶 ∈ ℤ)
12 4sq.d . . . . . . 7 (𝜑𝐷 ∈ ℤ)
13 4sq.e . . . . . . 7 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
14 4sq.f . . . . . . 7 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
15 4sq.g . . . . . . 7 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
16 4sq.h . . . . . . 7 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
17 4sq.r . . . . . . 7 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)
18 4sq.p . . . . . . 7 (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
191, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 184sqlem16 12441 . . . . . 6 (𝜑 → (𝑅𝑀 ∧ ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃))))
2019simpld 112 . . . . 5 (𝜑𝑅𝑀)
211, 2, 3, 4, 5, 6, 74sqlem13m 12438 . . . . . . . 8 (𝜑 → (∃𝑗 𝑗𝑇𝑀 < 𝑃))
2221simpld 112 . . . . . . 7 (𝜑 → ∃𝑗 𝑗𝑇)
23 1zzd 9311 . . . . . . . 8 ((𝜑𝑗𝑇) → 1 ∈ ℤ)
24 nnuz 9595 . . . . . . . . . 10 ℕ = (ℤ‘1)
2524rabeqi 2745 . . . . . . . . 9 {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} = {𝑖 ∈ (ℤ‘1) ∣ (𝑖 · 𝑃) ∈ 𝑆}
266, 25eqtri 2210 . . . . . . . 8 𝑇 = {𝑖 ∈ (ℤ‘1) ∣ (𝑖 · 𝑃) ∈ 𝑆}
276ssrab3 3256 . . . . . . . . . . . . . . . 16 𝑇 ⊆ ℕ
28 simpr 110 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑇) → 𝑗𝑇)
29 elfznn 10086 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (1...𝑗) → 𝑖 ∈ ℕ)
3029adantl 277 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑇) ∧ 𝑖 ∈ (1...𝑗)) → 𝑖 ∈ ℕ)
31 prmnn 12145 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
324, 31syl 14 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑃 ∈ ℕ)
3332ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑇) ∧ 𝑖 ∈ (1...𝑗)) → 𝑃 ∈ ℕ)
3430, 33nnmulcld 8999 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗𝑇) ∧ 𝑖 ∈ (1...𝑗)) → (𝑖 · 𝑃) ∈ ℕ)
3534nnnn0d 9260 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑇) ∧ 𝑖 ∈ (1...𝑗)) → (𝑖 · 𝑃) ∈ ℕ0)
3614sqlemsdc 12435 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 · 𝑃) ∈ ℕ0DECID (𝑖 · 𝑃) ∈ 𝑆)
3735, 36syl 14 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗𝑇) ∧ 𝑖 ∈ (1...𝑗)) → DECID (𝑖 · 𝑃) ∈ 𝑆)
3823, 26, 28, 37infssuzcldc 11987 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑇) → inf(𝑇, ℝ, < ) ∈ 𝑇)
3922, 38exlimddv 1910 . . . . . . . . . . . . . . . . 17 (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇)
407, 39eqeltrid 2276 . . . . . . . . . . . . . . . 16 (𝜑𝑀𝑇)
4127, 40sselid 3168 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℕ)
4241nnred 8963 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℝ)
4321simprd 114 . . . . . . . . . . . . . 14 (𝜑𝑀 < 𝑃)
4442, 43ltned 8102 . . . . . . . . . . . . 13 (𝜑𝑀𝑃)
4541nncnd 8964 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℂ)
4645sqvald 10685 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
4746breq1d 4028 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ (𝑀 · 𝑀) ∥ (𝑀 · 𝑃)))
4841nnzd 9405 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
49 prmz 12146 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
504, 49syl 14 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ ℤ)
5141nnne0d 8995 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ≠ 0)
52 dvdscmulr 11862 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀𝑃))
5348, 50, 48, 51, 52syl112anc 1253 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀𝑃))
54 dvdsprm 12172 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (𝑀𝑃𝑀 = 𝑃))
558, 4, 54syl2anc 411 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀𝑃𝑀 = 𝑃))
5647, 53, 553bitrd 214 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 = 𝑃))
5756necon3bbid 2400 . . . . . . . . . . . . 13 (𝜑 → (¬ (𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀𝑃))
5844, 57mpbird 167 . . . . . . . . . . . 12 (𝜑 → ¬ (𝑀↑2) ∥ (𝑀 · 𝑃))
59 orc 713 . . . . . . . . . . . . 13 (𝑅 = 0 → (𝑅 = 0 ∨ 𝑅 = 𝑀))
6019simprd 114 . . . . . . . . . . . . 13 (𝜑 → ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃)))
6159, 60syl5 32 . . . . . . . . . . . 12 (𝜑 → (𝑅 = 0 → (𝑀↑2) ∥ (𝑀 · 𝑃)))
6258, 61mtod 664 . . . . . . . . . . 11 (𝜑 → ¬ 𝑅 = 0)
631, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 184sqlem14 12439 . . . . . . . . . . . 12 (𝜑𝑅 ∈ ℕ0)
64 elnn0 9209 . . . . . . . . . . . 12 (𝑅 ∈ ℕ0 ↔ (𝑅 ∈ ℕ ∨ 𝑅 = 0))
6563, 64sylib 122 . . . . . . . . . . 11 (𝜑 → (𝑅 ∈ ℕ ∨ 𝑅 = 0))
6662, 65ecased 1360 . . . . . . . . . 10 (𝜑𝑅 ∈ ℕ)
67 gzreim 12414 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
689, 10, 67syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
69 gzcn 12407 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 + (i · 𝐵)) ∈ ℤ[i] → (𝐴 + (i · 𝐵)) ∈ ℂ)
7068, 69syl 14 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℂ)
7170absvalsq2d 11227 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)))
729zred 9406 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 ∈ ℝ)
7310zred 9406 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ ℝ)
7472, 73crred 11020 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
7574oveq1d 5912 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵)))↑2) = (𝐴↑2))
7672, 73crimd 11021 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
7776oveq1d 5912 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵)))↑2) = (𝐵↑2))
7875, 77oveq12d 5915 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)) = ((𝐴↑2) + (𝐵↑2)))
7971, 78eqtrd 2222 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2)))
80 gzreim 12414 . . . . . . . . . . . . . . . . . . . . 21 ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
8111, 12, 80syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
82 gzcn 12407 . . . . . . . . . . . . . . . . . . . 20 ((𝐶 + (i · 𝐷)) ∈ ℤ[i] → (𝐶 + (i · 𝐷)) ∈ ℂ)
8381, 82syl 14 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℂ)
8483absvalsq2d 11227 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)))
8511zred 9406 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐶 ∈ ℝ)
8612zred 9406 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐷 ∈ ℝ)
8785, 86crred 11020 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶)
8887oveq1d 5912 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((ℜ‘(𝐶 + (i · 𝐷)))↑2) = (𝐶↑2))
8985, 86crimd 11021 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷)
9089oveq1d 5912 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((ℑ‘(𝐶 + (i · 𝐷)))↑2) = (𝐷↑2))
9188, 90oveq12d 5915 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)) = ((𝐶↑2) + (𝐷↑2)))
9284, 91eqtrd 2222 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = ((𝐶↑2) + (𝐷↑2)))
9379, 92oveq12d 5915 . . . . . . . . . . . . . . . 16 (𝜑 → (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
9418, 93eqtr4d 2225 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 · 𝑃) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)))
9594oveq1d 5912 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀 · 𝑃) / 𝑀) = ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀))
9632nncnd 8964 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ ℂ)
9741nnap0d 8996 . . . . . . . . . . . . . . 15 (𝜑𝑀 # 0)
9896, 45, 97divcanap3d 8783 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀 · 𝑃) / 𝑀) = 𝑃)
9995, 98eqtr3d 2224 . . . . . . . . . . . . 13 (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) = 𝑃)
1009, 41, 134sqlem5 12417 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴𝐸) / 𝑀) ∈ ℤ))
101100simpld 112 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐸 ∈ ℤ)
10210, 41, 144sqlem5 12417 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵𝐹) / 𝑀) ∈ ℤ))
103102simpld 112 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹 ∈ ℤ)
104 gzreim 12414 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
105101, 103, 104syl2anc 411 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
106 gzcn 12407 . . . . . . . . . . . . . . . . . . 19 ((𝐸 + (i · 𝐹)) ∈ ℤ[i] → (𝐸 + (i · 𝐹)) ∈ ℂ)
107105, 106syl 14 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℂ)
108107absvalsq2d 11227 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)))
109101zred 9406 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐸 ∈ ℝ)
110103zred 9406 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹 ∈ ℝ)
111109, 110crred 11020 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℜ‘(𝐸 + (i · 𝐹))) = 𝐸)
112111oveq1d 5912 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((ℜ‘(𝐸 + (i · 𝐹)))↑2) = (𝐸↑2))
113109, 110crimd 11021 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℑ‘(𝐸 + (i · 𝐹))) = 𝐹)
114113oveq1d 5912 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((ℑ‘(𝐸 + (i · 𝐹)))↑2) = (𝐹↑2))
115112, 114oveq12d 5915 . . . . . . . . . . . . . . . . 17 (𝜑 → (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)) = ((𝐸↑2) + (𝐹↑2)))
116108, 115eqtrd 2222 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = ((𝐸↑2) + (𝐹↑2)))
11711, 41, 154sqlem5 12417 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶𝐺) / 𝑀) ∈ ℤ))
118117simpld 112 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺 ∈ ℤ)
11912, 41, 164sqlem5 12417 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷𝐻) / 𝑀) ∈ ℤ))
120119simpld 112 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐻 ∈ ℤ)
121 gzreim 12414 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ ℤ ∧ 𝐻 ∈ ℤ) → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
122118, 120, 121syl2anc 411 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
123 gzcn 12407 . . . . . . . . . . . . . . . . . . 19 ((𝐺 + (i · 𝐻)) ∈ ℤ[i] → (𝐺 + (i · 𝐻)) ∈ ℂ)
124122, 123syl 14 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℂ)
125124absvalsq2d 11227 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)))
126118zred 9406 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺 ∈ ℝ)
127120zred 9406 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐻 ∈ ℝ)
128126, 127crred 11020 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℜ‘(𝐺 + (i · 𝐻))) = 𝐺)
129128oveq1d 5912 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((ℜ‘(𝐺 + (i · 𝐻)))↑2) = (𝐺↑2))
130126, 127crimd 11021 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℑ‘(𝐺 + (i · 𝐻))) = 𝐻)
131130oveq1d 5912 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((ℑ‘(𝐺 + (i · 𝐻)))↑2) = (𝐻↑2))
132129, 131oveq12d 5915 . . . . . . . . . . . . . . . . 17 (𝜑 → (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)) = ((𝐺↑2) + (𝐻↑2)))
133125, 132eqtrd 2222 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = ((𝐺↑2) + (𝐻↑2)))
134116, 133oveq12d 5915 . . . . . . . . . . . . . . 15 (𝜑 → (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
135134oveq1d 5912 . . . . . . . . . . . . . 14 (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
136135, 17eqtr4di 2240 . . . . . . . . . . . . 13 (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = 𝑅)
13799, 136oveq12d 5915 . . . . . . . . . . . 12 (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑃 · 𝑅))
13866nncnd 8964 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ ℂ)
13996, 138mulcomd 8010 . . . . . . . . . . . 12 (𝜑 → (𝑃 · 𝑅) = (𝑅 · 𝑃))
140137, 139eqtrd 2222 . . . . . . . . . . 11 (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑅 · 𝑃))
141 eqid 2189 . . . . . . . . . . . 12 (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2))
142 eqid 2189 . . . . . . . . . . . 12 (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2))
1439zcnd 9407 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℂ)
144 ax-icn 7937 . . . . . . . . . . . . . . . . . 18 i ∈ ℂ
14510zcnd 9407 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ ℂ)
146 mulcl 7969 . . . . . . . . . . . . . . . . . 18 ((i ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i · 𝐵) ∈ ℂ)
147144, 145, 146sylancr 414 . . . . . . . . . . . . . . . . 17 (𝜑 → (i · 𝐵) ∈ ℂ)
148101zcnd 9407 . . . . . . . . . . . . . . . . 17 (𝜑𝐸 ∈ ℂ)
149103zcnd 9407 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 ∈ ℂ)
150 mulcl 7969 . . . . . . . . . . . . . . . . . 18 ((i ∈ ℂ ∧ 𝐹 ∈ ℂ) → (i · 𝐹) ∈ ℂ)
151144, 149, 150sylancr 414 . . . . . . . . . . . . . . . . 17 (𝜑 → (i · 𝐹) ∈ ℂ)
152143, 147, 148, 151addsub4d 8346 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴𝐸) + ((i · 𝐵) − (i · 𝐹))))
153144a1i 9 . . . . . . . . . . . . . . . . . 18 (𝜑 → i ∈ ℂ)
154153, 145, 149subdid 8402 . . . . . . . . . . . . . . . . 17 (𝜑 → (i · (𝐵𝐹)) = ((i · 𝐵) − (i · 𝐹)))
155154oveq2d 5913 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴𝐸) + (i · (𝐵𝐹))) = ((𝐴𝐸) + ((i · 𝐵) − (i · 𝐹))))
156152, 155eqtr4d 2225 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴𝐸) + (i · (𝐵𝐹))))
157156oveq1d 5912 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴𝐸) + (i · (𝐵𝐹))) / 𝑀))
158143, 148subcld 8299 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐸) ∈ ℂ)
159145, 149subcld 8299 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝐹) ∈ ℂ)
160 mulcl 7969 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ (𝐵𝐹) ∈ ℂ) → (i · (𝐵𝐹)) ∈ ℂ)
161144, 159, 160sylancr 414 . . . . . . . . . . . . . . 15 (𝜑 → (i · (𝐵𝐹)) ∈ ℂ)
162158, 161, 45, 97divdirapd 8817 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴𝐸) + (i · (𝐵𝐹))) / 𝑀) = (((𝐴𝐸) / 𝑀) + ((i · (𝐵𝐹)) / 𝑀)))
163153, 159, 45, 97divassapd 8814 . . . . . . . . . . . . . . 15 (𝜑 → ((i · (𝐵𝐹)) / 𝑀) = (i · ((𝐵𝐹) / 𝑀)))
164163oveq2d 5913 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴𝐸) / 𝑀) + ((i · (𝐵𝐹)) / 𝑀)) = (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))))
165157, 162, 1643eqtrd 2226 . . . . . . . . . . . . 13 (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))))
166100simprd 114 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝐸) / 𝑀) ∈ ℤ)
167102simprd 114 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐹) / 𝑀) ∈ ℤ)
168 gzreim 12414 . . . . . . . . . . . . . 14 ((((𝐴𝐸) / 𝑀) ∈ ℤ ∧ ((𝐵𝐹) / 𝑀) ∈ ℤ) → (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))) ∈ ℤ[i])
169166, 167, 168syl2anc 411 . . . . . . . . . . . . 13 (𝜑 → (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))) ∈ ℤ[i])
170165, 169eqeltrd 2266 . . . . . . . . . . . 12 (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) ∈ ℤ[i])
17111zcnd 9407 . . . . . . . . . . . . . . . . 17 (𝜑𝐶 ∈ ℂ)
17212zcnd 9407 . . . . . . . . . . . . . . . . . 18 (𝜑𝐷 ∈ ℂ)
173 mulcl 7969 . . . . . . . . . . . . . . . . . 18 ((i ∈ ℂ ∧ 𝐷 ∈ ℂ) → (i · 𝐷) ∈ ℂ)
174144, 172, 173sylancr 414 . . . . . . . . . . . . . . . . 17 (𝜑 → (i · 𝐷) ∈ ℂ)
175118zcnd 9407 . . . . . . . . . . . . . . . . 17 (𝜑𝐺 ∈ ℂ)
176120zcnd 9407 . . . . . . . . . . . . . . . . . 18 (𝜑𝐻 ∈ ℂ)
177 mulcl 7969 . . . . . . . . . . . . . . . . . 18 ((i ∈ ℂ ∧ 𝐻 ∈ ℂ) → (i · 𝐻) ∈ ℂ)
178144, 176, 177sylancr 414 . . . . . . . . . . . . . . . . 17 (𝜑 → (i · 𝐻) ∈ ℂ)
179171, 174, 175, 178addsub4d 8346 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶𝐺) + ((i · 𝐷) − (i · 𝐻))))
180153, 172, 176subdid 8402 . . . . . . . . . . . . . . . . 17 (𝜑 → (i · (𝐷𝐻)) = ((i · 𝐷) − (i · 𝐻)))
181180oveq2d 5913 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶𝐺) + (i · (𝐷𝐻))) = ((𝐶𝐺) + ((i · 𝐷) − (i · 𝐻))))
182179, 181eqtr4d 2225 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶𝐺) + (i · (𝐷𝐻))))
183182oveq1d 5912 . . . . . . . . . . . . . 14 (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶𝐺) + (i · (𝐷𝐻))) / 𝑀))
184171, 175subcld 8299 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶𝐺) ∈ ℂ)
185172, 176subcld 8299 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷𝐻) ∈ ℂ)
186 mulcl 7969 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ (𝐷𝐻) ∈ ℂ) → (i · (𝐷𝐻)) ∈ ℂ)
187144, 185, 186sylancr 414 . . . . . . . . . . . . . . 15 (𝜑 → (i · (𝐷𝐻)) ∈ ℂ)
188184, 187, 45, 97divdirapd 8817 . . . . . . . . . . . . . 14 (𝜑 → (((𝐶𝐺) + (i · (𝐷𝐻))) / 𝑀) = (((𝐶𝐺) / 𝑀) + ((i · (𝐷𝐻)) / 𝑀)))
189153, 185, 45, 97divassapd 8814 . . . . . . . . . . . . . . 15 (𝜑 → ((i · (𝐷𝐻)) / 𝑀) = (i · ((𝐷𝐻) / 𝑀)))
190189oveq2d 5913 . . . . . . . . . . . . . 14 (𝜑 → (((𝐶𝐺) / 𝑀) + ((i · (𝐷𝐻)) / 𝑀)) = (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))))
191183, 188, 1903eqtrd 2226 . . . . . . . . . . . . 13 (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))))
192117simprd 114 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶𝐺) / 𝑀) ∈ ℤ)
193119simprd 114 . . . . . . . . . . . . . 14 (𝜑 → ((𝐷𝐻) / 𝑀) ∈ ℤ)
194 gzreim 12414 . . . . . . . . . . . . . 14 ((((𝐶𝐺) / 𝑀) ∈ ℤ ∧ ((𝐷𝐻) / 𝑀) ∈ ℤ) → (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))) ∈ ℤ[i])
195192, 193, 194syl2anc 411 . . . . . . . . . . . . 13 (𝜑 → (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))) ∈ ℤ[i])
196191, 195eqeltrd 2266 . . . . . . . . . . . 12 (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) ∈ ℤ[i])
19732nnnn0d 9260 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℕ0)
19899, 197eqeltrd 2266 . . . . . . . . . . . 12 (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) ∈ ℕ0)
1991, 68, 81, 105, 122, 141, 142, 41, 170, 196, 198mul4sqlem 12428 . . . . . . . . . . 11 (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) ∈ 𝑆)
200140, 199eqeltrrd 2267 . . . . . . . . . 10 (𝜑 → (𝑅 · 𝑃) ∈ 𝑆)
201 oveq1 5904 . . . . . . . . . . . 12 (𝑖 = 𝑅 → (𝑖 · 𝑃) = (𝑅 · 𝑃))
202201eleq1d 2258 . . . . . . . . . . 11 (𝑖 = 𝑅 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑅 · 𝑃) ∈ 𝑆))
203202, 6elrab2 2911 . . . . . . . . . 10 (𝑅𝑇 ↔ (𝑅 ∈ ℕ ∧ (𝑅 · 𝑃) ∈ 𝑆))
20466, 200, 203sylanbrc 417 . . . . . . . . 9 (𝜑𝑅𝑇)
205204adantr 276 . . . . . . . 8 ((𝜑𝑗𝑇) → 𝑅𝑇)
206 elfznn 10086 . . . . . . . . . . . 12 (𝑖 ∈ (1...𝑅) → 𝑖 ∈ ℕ)
207206adantl 277 . . . . . . . . . . 11 (((𝜑𝑗𝑇) ∧ 𝑖 ∈ (1...𝑅)) → 𝑖 ∈ ℕ)
20832ad2antrr 488 . . . . . . . . . . 11 (((𝜑𝑗𝑇) ∧ 𝑖 ∈ (1...𝑅)) → 𝑃 ∈ ℕ)
209207, 208nnmulcld 8999 . . . . . . . . . 10 (((𝜑𝑗𝑇) ∧ 𝑖 ∈ (1...𝑅)) → (𝑖 · 𝑃) ∈ ℕ)
210209nnnn0d 9260 . . . . . . . . 9 (((𝜑𝑗𝑇) ∧ 𝑖 ∈ (1...𝑅)) → (𝑖 · 𝑃) ∈ ℕ0)
211210, 36syl 14 . . . . . . . 8 (((𝜑𝑗𝑇) ∧ 𝑖 ∈ (1...𝑅)) → DECID (𝑖 · 𝑃) ∈ 𝑆)
21223, 26, 205, 211infssuzledc 11986 . . . . . . 7 ((𝜑𝑗𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑅)
21322, 212exlimddv 1910 . . . . . 6 (𝜑 → inf(𝑇, ℝ, < ) ≤ 𝑅)
2147, 213eqbrtrid 4053 . . . . 5 (𝜑𝑀𝑅)
21566nnred 8963 . . . . . 6 (𝜑𝑅 ∈ ℝ)
216215, 42letri3d 8104 . . . . 5 (𝜑 → (𝑅 = 𝑀 ↔ (𝑅𝑀𝑀𝑅)))
21720, 214, 216mpbir2and 946 . . . 4 (𝜑𝑅 = 𝑀)
218217olcd 735 . . 3 (𝜑 → (𝑅 = 0 ∨ 𝑅 = 𝑀))
219218, 60mpd 13 . 2 (𝜑 → (𝑀↑2) ∥ (𝑀 · 𝑃))
220219, 58pm2.65i 640 1 ¬ 𝜑
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 709  DECID wdc 835   = wceq 1364  wex 1503  wcel 2160  {cab 2175  wne 2360  wrex 2469  {crab 2472  wss 3144   class class class wbr 4018  cfv 5235  (class class class)co 5897  infcinf 7013  cc 7840  cr 7841  0cc0 7842  1c1 7843  ici 7844   + caddc 7845   · cmul 7847   < clt 8023  cle 8024  cmin 8159   / cdiv 8660  cn 8950  2c2 9001  0cn0 9207  cz 9284  cuz 9559  ...cfz 10040   mod cmo 10355  cexp 10553  cre 10884  cim 10885  abscabs 11041  cdvds 11829  cprime 12142  ℤ[i]cgz 12404
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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-setind 4554  ax-iinf 4605  ax-cnex 7933  ax-resscn 7934  ax-1cn 7935  ax-1re 7936  ax-icn 7937  ax-addcl 7938  ax-addrcl 7939  ax-mulcl 7940  ax-mulrcl 7941  ax-addcom 7942  ax-mulcom 7943  ax-addass 7944  ax-mulass 7945  ax-distr 7946  ax-i2m1 7947  ax-0lt1 7948  ax-1rid 7949  ax-0id 7950  ax-rnegex 7951  ax-precex 7952  ax-cnre 7953  ax-pre-ltirr 7954  ax-pre-ltwlin 7955  ax-pre-lttrn 7956  ax-pre-apti 7957  ax-pre-ltadd 7958  ax-pre-mulgt0 7959  ax-pre-mulext 7960  ax-arch 7961  ax-caucvg 7962
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 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-if 3550  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4311  df-po 4314  df-iso 4315  df-iord 4384  df-on 4386  df-ilim 4387  df-suc 4389  df-iom 4608  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-f1 5240  df-fo 5241  df-f1o 5242  df-fv 5243  df-isom 5244  df-riota 5852  df-ov 5900  df-oprab 5901  df-mpo 5902  df-1st 6166  df-2nd 6167  df-recs 6331  df-irdg 6396  df-frec 6417  df-1o 6442  df-2o 6443  df-oadd 6446  df-er 6560  df-en 6768  df-dom 6769  df-fin 6770  df-sup 7014  df-inf 7015  df-pnf 8025  df-mnf 8026  df-xr 8027  df-ltxr 8028  df-le 8029  df-sub 8161  df-neg 8162  df-reap 8563  df-ap 8570  df-div 8661  df-inn 8951  df-2 9009  df-3 9010  df-4 9011  df-n0 9208  df-z 9285  df-uz 9560  df-q 9652  df-rp 9686  df-fz 10041  df-fzo 10175  df-fl 10303  df-mod 10356  df-seqfrec 10479  df-exp 10554  df-ihash 10791  df-cj 10886  df-re 10887  df-im 10888  df-rsqrt 11042  df-abs 11043  df-dvds 11830  df-gcd 11979  df-prm 12143  df-gz 12405
This theorem is referenced by:  4sqlem18  12443
  Copyright terms: Public domain W3C validator