4sqlem10 - Intuitionistic Logic Explorer

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

Theorem 4sqlem10 13166

Description: Lemma for 4sq 13189. (Contributed by Mario Carneiro, 16-Jul-2014.)

**Hypotheses**
Ref	Expression
4sqlem5.2	⊢ (𝜑 → 𝐴 ∈ ℤ)
4sqlem5.3	⊢ (𝜑 → 𝑀 ∈ ℕ)
4sqlem5.4	⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
4sqlem10.5	⊢ ((𝜑 ∧ 𝜓) → ((((𝑀↑2) / 2) / 2) − (𝐵↑2)) = 0)

**Assertion**
Ref	Expression
4sqlem10	⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ ((𝐴↑2) − (((𝑀↑2) / 2) / 2)))

**Proof of Theorem 4sqlem10**
Step	Hyp	Ref	Expression
1		4sqlem5.3	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ)
2	1	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℕ)
3	2	nnzd 9767	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℤ)
4		zsqcl 11047	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑀↑2) ∈ ℤ)
5	3, 4	syl 14	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∈ ℤ)
6		4sqlem5.2	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℤ)
7	6	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ ℤ)
8	2	nnred 9317	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℝ)
9	8	rehalfcld 9552	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑀 / 2) ∈ ℝ)
10	9	recnd 8354	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝑀 / 2) ∈ ℂ)
11	10	negnegd 8628	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → --(𝑀 / 2) = (𝑀 / 2))
12		4sqlem5.4	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
13	6, 1, 12	4sqlem5 13161	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 ∈ ℤ ∧ ((𝐴 − 𝐵) / 𝑀) ∈ ℤ))
14	13	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝐵 ∈ ℤ ∧ ((𝐴 − 𝐵) / 𝑀) ∈ ℤ))
15	14	simpld 112	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ ℤ)
16	15	zred 9768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ ℝ)
17	6, 1, 12	4sqlem6 13162	. . . . . . . . . . . . 13 ⊢ (𝜑 → (-(𝑀 / 2) ≤ 𝐵 ∧ 𝐵 < (𝑀 / 2)))
18	17	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (-(𝑀 / 2) ≤ 𝐵 ∧ 𝐵 < (𝑀 / 2)))
19	18	simprd 114	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝐵 < (𝑀 / 2))
20	16, 19	ltned 8439	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝐵 ≠ (𝑀 / 2))
21	20	neneqd 2441	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝐵 = (𝑀 / 2))
22		2cnd 9377	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 2 ∈ ℂ)
23	22	sqvald 11108	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (2↑2) = (2 · 2))
24	23	oveq2d 6101	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ((𝑀↑2) / (2↑2)) = ((𝑀↑2) / (2 · 2)))
25	2	nncnd 9318	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℂ)
26		2ap0 9397	. . . . . . . . . . . . . . 15 ⊢ 2 # 0
27	26	a1i 9	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 2 # 0)
28	25, 22, 27	sqdivapd 11124	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ((𝑀 / 2)↑2) = ((𝑀↑2) / (2↑2)))
29	25	sqcld 11109	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∈ ℂ)
30	29, 22, 22, 27, 27	divdivap1d 9152	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (((𝑀↑2) / 2) / 2) = ((𝑀↑2) / (2 · 2)))
31	24, 28, 30	3eqtr4d 2281	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → ((𝑀 / 2)↑2) = (((𝑀↑2) / 2) / 2))
32	29	halfcld 9550	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → ((𝑀↑2) / 2) ∈ ℂ)
33	32	halfcld 9550	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (((𝑀↑2) / 2) / 2) ∈ ℂ)
34	15	zcnd 9769	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ ℂ)
35	34	sqcld 11109	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝐵↑2) ∈ ℂ)
36		4sqlem10.5	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ((((𝑀↑2) / 2) / 2) − (𝐵↑2)) = 0)
37	33, 35, 36	subeq0d 8645	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (((𝑀↑2) / 2) / 2) = (𝐵↑2))
38	31, 37	eqtr2d 2272	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝐵↑2) = ((𝑀 / 2)↑2))
39		zq 10026	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℚ)
40	15, 39	syl 14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ ℚ)
41		2nn 9466	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
42	41	a1i 9	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 2 ∈ ℕ)
43		znq 10024	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 2 ∈ ℕ) → (𝑀 / 2) ∈ ℚ)
44	3, 42, 43	syl2anc 415	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑀 / 2) ∈ ℚ)
45		qsqeqor 11087	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℚ ∧ (𝑀 / 2) ∈ ℚ) → ((𝐵↑2) = ((𝑀 / 2)↑2) ↔ (𝐵 = (𝑀 / 2) ∨ 𝐵 = -(𝑀 / 2))))
46	40, 44, 45	syl2anc 415	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ((𝐵↑2) = ((𝑀 / 2)↑2) ↔ (𝐵 = (𝑀 / 2) ∨ 𝐵 = -(𝑀 / 2))))
47	38, 46	mpbid 147	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝐵 = (𝑀 / 2) ∨ 𝐵 = -(𝑀 / 2)))
48	47	ord 736	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (¬ 𝐵 = (𝑀 / 2) → 𝐵 = -(𝑀 / 2)))
49	21, 48	mpd 13	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → 𝐵 = -(𝑀 / 2))
50	49, 15	eqeltrrd 2316	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → -(𝑀 / 2) ∈ ℤ)
51	50	znegcld 9770	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → --(𝑀 / 2) ∈ ℤ)
52	11, 51	eqeltrrd 2316	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (𝑀 / 2) ∈ ℤ)
53	7, 52	zaddcld 9772	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 + (𝑀 / 2)) ∈ ℤ)
54		zsqcl 11047	. . . 4 ⊢ ((𝐴 + (𝑀 / 2)) ∈ ℤ → ((𝐴 + (𝑀 / 2))↑2) ∈ ℤ)
55	53, 54	syl 14	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2))↑2) ∈ ℤ)
56	53, 3	zmulcld 9774	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) · 𝑀) ∈ ℤ)
57		zq 10026	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ)
58	7, 57	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ ℚ)
59		qaddcl 10035	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℚ ∧ (𝑀 / 2) ∈ ℚ) → (𝐴 + (𝑀 / 2)) ∈ ℚ)
60	58, 44, 59	syl2anc 415	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 + (𝑀 / 2)) ∈ ℚ)
61		nnq 10033	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
62	2, 61	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℚ)
63	2	nngt0d 9348	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → 0 < 𝑀)
64	60, 62, 63	modqcld 10765	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) mod 𝑀) ∈ ℚ)
65		qcn 10034	. . . . . . 7 ⊢ (((𝐴 + (𝑀 / 2)) mod 𝑀) ∈ ℚ → ((𝐴 + (𝑀 / 2)) mod 𝑀) ∈ ℂ)
66	64, 65	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) mod 𝑀) ∈ ℂ)
67		0cnd 8319	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 0 ∈ ℂ)
68		df-neg 8500	. . . . . . 7 ⊢ -(𝑀 / 2) = (0 − (𝑀 / 2))
69	49, 12, 68	3eqtr3g 2294	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (0 − (𝑀 / 2)))
70	66, 67, 10, 69	subcan2d 8679	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) mod 𝑀) = 0)
71		dvdsval3 12558	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ (𝐴 + (𝑀 / 2)) ∈ ℤ) → (𝑀 ∥ (𝐴 + (𝑀 / 2)) ↔ ((𝐴 + (𝑀 / 2)) mod 𝑀) = 0))
72	2, 53, 71	syl2anc 415	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (𝑀 ∥ (𝐴 + (𝑀 / 2)) ↔ ((𝐴 + (𝑀 / 2)) mod 𝑀) = 0))
73	70, 72	mpbird 167	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∥ (𝐴 + (𝑀 / 2)))
74		dvdssq 12808	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ (𝐴 + (𝑀 / 2)) ∈ ℤ) → (𝑀 ∥ (𝐴 + (𝑀 / 2)) ↔ (𝑀↑2) ∥ ((𝐴 + (𝑀 / 2))↑2)))
75	3, 53, 74	syl2anc 415	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝑀 ∥ (𝐴 + (𝑀 / 2)) ↔ (𝑀↑2) ∥ ((𝐴 + (𝑀 / 2))↑2)))
76	73, 75	mpbid 147	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ ((𝐴 + (𝑀 / 2))↑2))
77	25	sqvald 11108	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) = (𝑀 · 𝑀))
78	2	nnne0d 9349	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ≠ 0)
79		dvdsmulcr 12588	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ (𝐴 + (𝑀 / 2)) ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ((𝑀 · 𝑀) ∥ ((𝐴 + (𝑀 / 2)) · 𝑀) ↔ 𝑀 ∥ (𝐴 + (𝑀 / 2))))
80	3, 53, 3, 78, 79	syl112anc 1282	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ((𝑀 · 𝑀) ∥ ((𝐴 + (𝑀 / 2)) · 𝑀) ↔ 𝑀 ∥ (𝐴 + (𝑀 / 2))))
81	73, 80	mpbird 167	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝑀 · 𝑀) ∥ ((𝐴 + (𝑀 / 2)) · 𝑀))
82	77, 81	eqbrtrd 4152	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ ((𝐴 + (𝑀 / 2)) · 𝑀))
83	5, 55, 56, 76, 82	dvds2subd 12594	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ (((𝐴 + (𝑀 / 2))↑2) − ((𝐴 + (𝑀 / 2)) · 𝑀)))
84	53	zcnd 9769	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 + (𝑀 / 2)) ∈ ℂ)
85	84	sqvald 11108	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2))↑2) = ((𝐴 + (𝑀 / 2)) · (𝐴 + (𝑀 / 2))))
86	85	oveq1d 6100	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (((𝐴 + (𝑀 / 2))↑2) − ((𝐴 + (𝑀 / 2)) · 𝑀)) = (((𝐴 + (𝑀 / 2)) · (𝐴 + (𝑀 / 2))) − ((𝐴 + (𝑀 / 2)) · 𝑀)))
87	84, 84, 25	subdid 8741	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) · ((𝐴 + (𝑀 / 2)) − 𝑀)) = (((𝐴 + (𝑀 / 2)) · (𝐴 + (𝑀 / 2))) − ((𝐴 + (𝑀 / 2)) · 𝑀)))
88	25	2halvesd 9551	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ((𝑀 / 2) + (𝑀 / 2)) = 𝑀)
89	88	oveq2d 6101	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) − ((𝑀 / 2) + (𝑀 / 2))) = ((𝐴 + (𝑀 / 2)) − 𝑀))
90	7	zcnd 9769	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ ℂ)
91	90, 10, 10	pnpcan2d 8675	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) − ((𝑀 / 2) + (𝑀 / 2))) = (𝐴 − (𝑀 / 2)))
92	89, 91	eqtr3d 2273	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) − 𝑀) = (𝐴 − (𝑀 / 2)))
93	92	oveq2d 6101	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) · ((𝐴 + (𝑀 / 2)) − 𝑀)) = ((𝐴 + (𝑀 / 2)) · (𝐴 − (𝑀 / 2))))
94		subsq 11083	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (𝑀 / 2) ∈ ℂ) → ((𝐴↑2) − ((𝑀 / 2)↑2)) = ((𝐴 + (𝑀 / 2)) · (𝐴 − (𝑀 / 2))))
95	90, 10, 94	syl2anc 415	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴↑2) − ((𝑀 / 2)↑2)) = ((𝐴 + (𝑀 / 2)) · (𝐴 − (𝑀 / 2))))
96	31	oveq2d 6101	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴↑2) − ((𝑀 / 2)↑2)) = ((𝐴↑2) − (((𝑀↑2) / 2) / 2)))
97	93, 95, 96	3eqtr2d 2277	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) · ((𝐴 + (𝑀 / 2)) − 𝑀)) = ((𝐴↑2) − (((𝑀↑2) / 2) / 2)))
98	86, 87, 97	3eqtr2d 2277	. 2 ⊢ ((𝜑 ∧ 𝜓) → (((𝐴 + (𝑀 / 2))↑2) − ((𝐴 + (𝑀 / 2)) · 𝑀)) = ((𝐴↑2) − (((𝑀↑2) / 2) / 2)))
99	83, 98	breqtrd 4156	1 ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ ((𝐴↑2) − (((𝑀↑2) / 2) / 2)))

Colors of variables: wff set class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 = wceq 1402 ∈ wcel 2209 ≠ wne 2420 class class class wbr 4130 (class class class)co 6085 ℂcc 8177 0cc0 8179 + caddc 8182 · cmul 8184 < clt 8360 ≤ cle 8361 − cmin 8497 -cneg 8498 # cap 8909 / cdiv 9002 ℕcn 9304 2c2 9355 ℤcz 9644 ℚcq 10019 mod cmo 10759 ↑cexp 10975 ∥ cdvds 12554

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297 ax-arch 8298 ax-caucvg 8299

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-recs 6576 df-frec 6662 df-sup 7324 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-reap 8903 df-ap 8910 df-div 9003 df-inn 9305 df-2 9363 df-3 9364 df-4 9365 df-n0 9564 df-z 9645 df-uz 9922 df-q 10020 df-rp 10055 df-fz 10412 df-fzo 10550 df-fl 10705 df-mod 10760 df-seqfrec 10885 df-exp 10976 df-cj 11607 df-re 11608 df-im 11609 df-rsqrt 11764 df-abs 11765 df-dvds 12555 df-gcd 12731

This theorem is used by: 4sqlem16 13185

W3C validator