aks5lem8 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > aks5lem8		Structured version Visualization version GIF version

Theorem aks5lem8 43443

Description: Lemma for aks5. Clean up the conclusion. (Contributed by metakunt, 9-Aug-2025.)

**Hypotheses**
Ref	Expression
aks5lem7.1	⊢ (𝜑 → (♯‘(Base‘𝐾)) ∈ ℕ)
aks5lem7.2	⊢ 𝑃 = (chr‘𝐾)
aks5lem7.3	⊢ (𝜑 → 𝐾 ∈ Field)
aks5lem7.4	⊢ (𝜑 → 𝑃 ∈ ℙ)
aks5lem7.5	⊢ (𝜑 → 𝑅 ∈ ℕ)
aks5lem7.6	⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘3))
aks5lem7.7	⊢ (𝜑 → 𝑃 ∥ 𝑁)
aks5lem7.8	⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)
aks5lem7.9	⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 log_b 𝑁)))
aks5lem7.10	⊢ (𝜑 → ((2 log_b 𝑁)↑2) < ((od_ℤ‘𝑅)‘𝑁))
aks5lem7.11	⊢ (𝜑 → 𝑅 ∥ ((♯‘(Base‘𝐾)) − 1))
aks5lem7.12	⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(._g‘(mulGrp‘𝑆))(𝑋(+_g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~_QG 𝐿) = [((𝑁(._g‘(mulGrp‘𝑆))𝑋)(+_g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~_QG 𝐿))
aks5lem7.13	⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1)
aks5lem7.14	⊢ 𝑆 = (Poly₁‘(ℤ/nℤ‘𝑁))
aks5lem7.15	⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(._g‘(mulGrp‘𝑆))𝑋)(-_g‘𝑆)(1_r‘𝑆))})
aks5lem7.16	⊢ 𝑋 = (var₁‘(ℤ/nℤ‘𝑁))

**Assertion**
Ref	Expression
aks5lem8	⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑛 ∈ ℕ 𝑁 = (𝑝↑𝑛))

Distinct variable groups: 𝐴,𝑎 𝐴,𝑏 𝐾,𝑎 𝐾,𝑏 𝑁,𝑎 𝑁,𝑏 𝑃,𝑎 𝑃,𝑏 𝑅,𝑎 𝑅,𝑏 𝜑,𝑎 𝜑,𝑏 𝑛,𝑁,𝑝 𝑃,𝑛,𝑝 𝜑,𝑛,𝑝 Allowed substitution hints: 𝐴(𝑛, 𝑝) 𝑅(𝑛, 𝑝) 𝑆(𝑛, 𝑝, 𝑎, 𝑏) 𝐾(𝑛, 𝑝) 𝐿(𝑛, 𝑝, 𝑎, 𝑏) 𝑋(𝑛, 𝑝, 𝑎, 𝑏)

**Proof of Theorem aks5lem8**
Step	Hyp	Ref	Expression
1		aks5lem7.4	. 2 ⊢ (𝜑 → 𝑃 ∈ ℙ)
2		simpr 490	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃)
3	2	oveq1d 7458	. . . 4 ⊢ ((𝜑 ∧ 𝑝 = 𝑃) → (𝑝↑𝑛) = (𝑃↑𝑛))
4	3	eqeq2d 2774	. . 3 ⊢ ((𝜑 ∧ 𝑝 = 𝑃) → (𝑁 = (𝑝↑𝑛) ↔ 𝑁 = (𝑃↑𝑛)))
5	4	rexbidv 3190	. 2 ⊢ ((𝜑 ∧ 𝑝 = 𝑃) → (∃𝑛 ∈ ℕ 𝑁 = (𝑝↑𝑛) ↔ ∃𝑛 ∈ ℕ 𝑁 = (𝑃↑𝑛)))
6		aks5lem7.1	. . . . 5 ⊢ (𝜑 → (♯‘(Base‘𝐾)) ∈ ℕ)
7		aks5lem7.2	. . . . 5 ⊢ 𝑃 = (chr‘𝐾)
8		aks5lem7.3	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ Field)
9		aks5lem7.5	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ ℕ)
10		aks5lem7.6	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘3))
11		aks5lem7.7	. . . . 5 ⊢ (𝜑 → 𝑃 ∥ 𝑁)
12		aks5lem7.8	. . . . 5 ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)
13		aks5lem7.9	. . . . 5 ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 log_b 𝑁)))
14		aks5lem7.10	. . . . 5 ⊢ (𝜑 → ((2 log_b 𝑁)↑2) < ((od_ℤ‘𝑅)‘𝑁))
15		aks5lem7.11	. . . . 5 ⊢ (𝜑 → 𝑅 ∥ ((♯‘(Base‘𝐾)) − 1))
16		aks5lem7.12	. . . . 5 ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(._g‘(mulGrp‘𝑆))(𝑋(+_g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~_QG 𝐿) = [((𝑁(._g‘(mulGrp‘𝑆))𝑋)(+_g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~_QG 𝐿))
17		aks5lem7.13	. . . . 5 ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1)
18		aks5lem7.14	. . . . 5 ⊢ 𝑆 = (Poly₁‘(ℤ/nℤ‘𝑁))
19		aks5lem7.15	. . . . 5 ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(._g‘(mulGrp‘𝑆))𝑋)(-_g‘𝑆)(1_r‘𝑆))})
20		aks5lem7.16	. . . . 5 ⊢ 𝑋 = (var₁‘(ℤ/nℤ‘𝑁))
21	6, 7, 8, 1, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20	aks5lem7 43442	. . . 4 ⊢ (𝜑 → 𝑁 = (𝑃↑(𝑃 pCnt 𝑁)))
22		eluzelz 13002	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℤ)
23	10, 22	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℤ)
24		0red 11338	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℝ)
25		3re 12450	. . . . . . . . 9 ⊢ 3 ∈ ℝ
26	25	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 3 ∈ ℝ)
27	23	zred 12830	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℝ)
28		3pos 12478	. . . . . . . . 9 ⊢ 0 < 3
29	28	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 < 3)
30		eluzle 13005	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 3 ≤ 𝑁)
31	10, 30	syl 18	. . . . . . . 8 ⊢ (𝜑 → 3 ≤ 𝑁)
32	24, 26, 27, 29, 31	ltletrd 11497	. . . . . . 7 ⊢ (𝜑 → 0 < 𝑁)
33	23, 32	jca 521	. . . . . 6 ⊢ (𝜑 → (𝑁 ∈ ℤ ∧ 0 < 𝑁))
34		elnnz 12730	. . . . . 6 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
35	33, 34	sylibr 237	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ)
36		pcprmpw 17090	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (∃𝑛 ∈ ℕ₀ 𝑁 = (𝑃↑𝑛) ↔ 𝑁 = (𝑃↑(𝑃 pCnt 𝑁))))
37	1, 35, 36	syl2anc 596	. . . 4 ⊢ (𝜑 → (∃𝑛 ∈ ℕ₀ 𝑁 = (𝑃↑𝑛) ↔ 𝑁 = (𝑃↑(𝑃 pCnt 𝑁))))
38	21, 37	mpbird 260	. . 3 ⊢ (𝜑 → ∃𝑛 ∈ ℕ₀ 𝑁 = (𝑃↑𝑛))
39		simprl 783	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) → 𝑛 ∈ ℕ₀)
40	39	nn0zd 12745	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) → 𝑛 ∈ ℤ)
41		simpr 490	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 0 < 𝑛) → 0 < 𝑛)
42	39	nn0red 12695	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) → 𝑛 ∈ ℝ)
43		0red 11338	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) → 0 ∈ ℝ)
44	42, 43	lenltd 11483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) → (𝑛 ≤ 0 ↔ ¬ 0 < 𝑛))
45	44	bicomd 226	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) → (¬ 0 < 𝑛 ↔ 𝑛 ≤ 0))
46	45	biimpd 232	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) → (¬ 0 < 𝑛 → 𝑛 ≤ 0))
47	46	imp 412	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ ¬ 0 < 𝑛) → 𝑛 ≤ 0)
48		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 ≤ 0) → 𝑛 ≤ 0)
49	39	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 ≤ 0) → 𝑛 ∈ ℕ₀)
50		nn0le0eq0 12661	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 ≤ 0 ↔ 𝑛 = 0))
51	50	bicomd 226	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 = 0 ↔ 𝑛 ≤ 0))
52	49, 51	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 ≤ 0) → (𝑛 = 0 ↔ 𝑛 ≤ 0))
53	48, 52	mpbird 260	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 ≤ 0) → 𝑛 = 0)
54		simplrr 790	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → 𝑁 = (𝑃↑𝑛))
55		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → 𝑛 = 0)
56	55	oveq2d 7459	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → (𝑃↑𝑛) = (𝑃↑0))
57	1	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → 𝑃 ∈ ℙ)
58		prmnn 16878	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
59	57, 58	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → 𝑃 ∈ ℕ)
60	59	nncnd 12378	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → 𝑃 ∈ ℂ)
61	60	exp0d 14310	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → (𝑃↑0) = 1)
62	56, 61	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → (𝑃↑𝑛) = 1)
63	54, 62	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → 𝑁 = 1)
64		1red 11336	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → 1 ∈ ℝ)
65		1red 11336	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 1 ∈ ℝ)
66	35	nnred 12377	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℝ)
67		1lt3 12545	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 < 3
68	67	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 1 < 3)
69	65, 26, 66, 68, 31	ltletrd 11497	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 < 𝑁)
70	69	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) → 1 < 𝑁)
71	70	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → 1 < 𝑁)
72	64, 71	ltned 11473	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → 1 ≠ 𝑁)
73	72	necomd 3014	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → 𝑁 ≠ 1)
74	73	neneqd 2964	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → ¬ 𝑁 = 1)
75	63, 74	pm2.21dd 198	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 = 0) → 0 < 𝑛)
76	75	ex 418	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) → (𝑛 = 0 → 0 < 𝑛))
77	76	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 ≤ 0) → (𝑛 = 0 → 0 < 𝑛))
78	53, 77	mpd 16	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ 𝑛 ≤ 0) → 0 < 𝑛)
79	78	ex 418	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) → (𝑛 ≤ 0 → 0 < 𝑛))
80	79	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ ¬ 0 < 𝑛) → (𝑛 ≤ 0 → 0 < 𝑛))
81	47, 80	mpd 16	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) ∧ ¬ 0 < 𝑛) → 0 < 𝑛)
82	41, 81	pm2.61dan 825	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) → 0 < 𝑛)
83	40, 82	jca 521	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) → (𝑛 ∈ ℤ ∧ 0 < 𝑛))
84		elnnz 12730	. . . 4 ⊢ (𝑛 ∈ ℕ ↔ (𝑛 ∈ ℤ ∧ 0 < 𝑛))
85	83, 84	sylibr 237	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) → 𝑛 ∈ ℕ)
86		simprr 785	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ 𝑁 = (𝑃↑𝑛))) → 𝑁 = (𝑃↑𝑛))
87	38, 85, 86	reximssdv 3184	. 2 ⊢ (𝜑 → ∃𝑛 ∈ ℕ 𝑁 = (𝑃↑𝑛))
88	1, 5, 87	rspcedvd 3582	1 ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑛 ∈ ℕ 𝑁 = (𝑝↑𝑛))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ∀wral 3080 ∃wrex 3090 {csn 4588 class class class wbr 5106 ‘cfv 6558 (class class class)co 7443 [cec 8743 ℝcr 11226 0cc0 11227 1c1 11228 · cmul 11232 < clt 11370 ≤ cle 11371 − cmin 11568 ℕcn 12362 2c2 12424 3c3 12425 ℕ₀cn0 12633 ℤcz 12720 ℤ_≥cuz 12992 ...cfz 13666 ⌊cfl 13957 ↑cexp 14231 ♯chash 14501 √csqrt 15429 ∥ cdvds 16451 gcd cgcd 16693 ℙcprime 16875 od_ℤcodz 16969 ϕcphi 16970 pCnt cpc 17043 Basecbs 17416 +_gcplusg 17457 -_gcsg 19175 ._gcmg 19306 ~_QG cqg 19361 mulGrpcmgp 20390 1_rcur 20437 Fieldcfield 21011 RSpancrsp 21515 ℤRHomczrh 21835 chrcchr 21837 ℤ/nℤczn 21838 var₁cv1 22524 Poly₁cpl1 22525 log_b clogb 27122

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-inf2 9669 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304 ax-pre-sup 11305 ax-addf 11306 ax-mulf 11307

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-disj 5074 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-isom 6567 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-of 7717 df-ofr 7718 df-om 7902 df-1st 8025 df-2nd 8026 df-supp 8205 df-tpos 8271 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-2o 8505 df-oadd 8508 df-omul 8509 df-er 8745 df-ec 8747 df-qs 8751 df-map 8877 df-pm 8878 df-ixp 8954 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-fsupp 9382 df-fi 9430 df-sup 9461 df-inf 9462 df-oi 9531 df-dju 10009 df-card 10047 df-acn 10050 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-div 12001 df-nn 12363 df-2 12432 df-3 12433 df-4 12434 df-5 12435 df-6 12436 df-7 12437 df-8 12438 df-9 12439 df-n0 12634 df-xnn0 12707 df-z 12721 df-dec 12842 df-uz 12993 df-q 13103 df-rp 13148 df-xneg 13268 df-xadd 13269 df-xmul 13270 df-ioo 13507 df-ioc 13508 df-ico 13509 df-icc 13510 df-fz 13667 df-fzo 13816 df-fl 13959 df-mod 14037 df-seq 14172 df-exp 14232 df-fac 14445 df-bc 14474 df-hash 14502 df-shft 15249 df-cj 15295 df-re 15296 df-im 15297 df-sqrt 15431 df-abs 15432 df-limsup 15667 df-clim 15684 df-rlim 15685 df-sum 15883 df-prod 16102 df-fallfac 16203 df-ef 16262 df-sin 16264 df-cos 16265 df-pi 16267 df-dvds 16452 df-gcd 16694 df-prm 16876 df-odz 16971 df-phi 16972 df-pc 17044 df-struct 17354 df-sets 17371 df-slot 17389 df-ndx 17401 df-base 17417 df-ress 17438 df-plusg 17470 df-mulr 17471 df-starv 17472 df-sca 17473 df-vsca 17474 df-ip 17475 df-tset 17476 df-ple 17477 df-ds 17479 df-unif 17480 df-hom 17481 df-cco 17482 df-rest 17622 df-topn 17623 df-0g 17641 df-gsum 17642 df-topgen 17643 df-pt 17644 df-prds 17647 df-pws 17649 df-xrs 17703 df-qtop 17708 df-imas 17709 df-qus 17710 df-xps 17711 df-mre 17785 df-mrc 17786 df-acs 17788 df-mgm 18845 df-sgrp 18937 df-mnd 18953 df-mhm 19007 df-submnd 19008 df-grp 19176 df-minusg 19177 df-sbg 19178 df-mulg 19307 df-subg 19362 df-nsg 19363 df-eqg 19364 df-ghm 19457 df-gim 19502 df-cntz 19561 df-od 19772 df-cmn 20026 df-abl 20027 df-mgp 20391 df-rng 20405 df-ur 20438 df-srg 20443 df-ring 20491 df-cring 20492 df-oppr 20597 df-dvdsr 20617 df-unit 20618 df-invr 20648 df-dvr 20661 df-rhm 20732 df-rim 20733 df-nzr 20793 df-subrng 20828 df-subrg 20852 df-rlreg 20976 df-domn 20977 df-idom 20978 df-drng 21012 df-field 21013 df-lmod 21167 df-lss 21237 df-lsp 21277 df-sra 21478 df-rgmod 21479 df-lidl 21516 df-rsp 21517 df-2idl 21573 df-psmet 21700 df-xmet 21701 df-met 21702 df-bl 21703 df-mopn 21704 df-fbas 21705 df-fg 21706 df-cnfld 21709 df-zring 21783 df-zrh 21839 df-chr 21841 df-zn 21842 df-assa 22191 df-asp 22192 df-ascl 22193 df-psr 22247 df-mvr 22248 df-mpl 22249 df-opsr 22251 df-evls 22413 df-evl 22414 df-psr1 22528 df-vr1 22529 df-ply1 22530 df-coe1 22531 df-evls1 22663 df-evl1 22664 df-top 23242 df-topon 23259 df-topsp 23281 df-bases 23294 df-cld 23367 df-ntr 23368 df-cls 23369 df-nei 23446 df-lp 23484 df-perf 23485 df-cn 23575 df-cnp 23576 df-haus 23663 df-tx 23911 df-hmeo 24104 df-fil 24195 df-fm 24287 df-flim 24288 df-flf 24289 df-xms 24669 df-ms 24670 df-tms 24671 df-cncf 25229 df-limc 26216 df-dv 26217 df-mdeg 26403 df-deg1 26404 df-mon1 26479 df-uc1p 26480 df-q1p 26481 df-r1p 26482 df-log 26914 df-cxp 26915 df-logb 27123 df-primroots 43334

This theorem is used by: aks5 43446

W3C validator