Theorem proot1ex 42398

Description: The complex field has primitive 𝑁-th roots of unity for all 𝑁. (Contributed by Stefan O'Rear, 12-Sep-2015.)

Hypotheses

Ref	Expression
proot1ex.g	⊢ 𝐺 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
proot1ex.o	⊢ 𝑂 = (od‘𝐺)

Assertion

Ref	Expression
proot1ex	⊢ (𝑁 ∈ ℕ → (-1↑𝑐(2 / 𝑁)) ∈ (◡𝑂 “ {𝑁}))

Proof of Theorem proot1ex

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		neg1cn 12322	. . . 4 ⊢ -1 ∈ ℂ
2		2rp 12975	. . . . . 6 ⊢ 2 ∈ ℝ+
3		nnrp 12981	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ+)
4		rpdivcl 12995	. . . . . 6 ⊢ ((2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+) → (2 / 𝑁) ∈ ℝ+)
5	2, 3, 4	sylancr 586	. . . . 5 ⊢ (𝑁 ∈ ℕ → (2 / 𝑁) ∈ ℝ+)
6	5	rpcnd 13014	. . . 4 ⊢ (𝑁 ∈ ℕ → (2 / 𝑁) ∈ ℂ)
7		cxpcl 26512	. . . 4 ⊢ ((-1 ∈ ℂ ∧ (2 / 𝑁) ∈ ℂ) → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
8	1, 6, 7	sylancr 586	. . 3 ⊢ (𝑁 ∈ ℕ → (-1↑𝑐(2 / 𝑁)) ∈ ℂ)
9	1	a1i 11	. . . 4 ⊢ (𝑁 ∈ ℕ → -1 ∈ ℂ)
10		neg1ne0 12324	. . . . 5 ⊢ -1 ≠ 0
11	10	a1i 11	. . . 4 ⊢ (𝑁 ∈ ℕ → -1 ≠ 0)
12	9, 11, 6	cxpne0d 26551	. . 3 ⊢ (𝑁 ∈ ℕ → (-1↑𝑐(2 / 𝑁)) ≠ 0)
13		eldifsn 4782	. . 3 ⊢ ((-1↑𝑐(2 / 𝑁)) ∈ (ℂ ∖ {0}) ↔ ((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ (-1↑𝑐(2 / 𝑁)) ≠ 0))
14	8, 12, 13	sylanbrc 582	. 2 ⊢ (𝑁 ∈ ℕ → (-1↑𝑐(2 / 𝑁)) ∈ (ℂ ∖ {0}))
15	1	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → -1 ∈ ℂ)
16	10	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → -1 ≠ 0)
17		nn0cn 12478	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℕ0 → 𝑥 ∈ ℂ)
18		mulcl 11189	. . . . . . . . . 10 ⊢ (((2 / 𝑁) ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((2 / 𝑁) · 𝑥) ∈ ℂ)
19	6, 17, 18	syl2an 595	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → ((2 / 𝑁) · 𝑥) ∈ ℂ)
20	15, 16, 19	cxpefd 26550	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (-1↑𝑐((2 / 𝑁) · 𝑥)) = (exp‘(((2 / 𝑁) · 𝑥) · (log‘-1))))
21	20	eqeq1d 2726	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → ((-1↑𝑐((2 / 𝑁) · 𝑥)) = 1 ↔ (exp‘(((2 / 𝑁) · 𝑥) · (log‘-1))) = 1))
22		logcl 26407	. . . . . . . . . 10 ⊢ ((-1 ∈ ℂ ∧ -1 ≠ 0) → (log‘-1) ∈ ℂ)
23	1, 10, 22	mp2an 689	. . . . . . . . 9 ⊢ (log‘-1) ∈ ℂ
24		mulcl 11189	. . . . . . . . 9 ⊢ ((((2 / 𝑁) · 𝑥) ∈ ℂ ∧ (log‘-1) ∈ ℂ) → (((2 / 𝑁) · 𝑥) · (log‘-1)) ∈ ℂ)
25	19, 23, 24	sylancl 585	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (((2 / 𝑁) · 𝑥) · (log‘-1)) ∈ ℂ)
26		efeq1 26367	. . . . . . . 8 ⊢ ((((2 / 𝑁) · 𝑥) · (log‘-1)) ∈ ℂ → ((exp‘(((2 / 𝑁) · 𝑥) · (log‘-1))) = 1 ↔ ((((2 / 𝑁) · 𝑥) · (log‘-1)) / (i · (2 · π))) ∈ ℤ))
27	25, 26	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → ((exp‘(((2 / 𝑁) · 𝑥) · (log‘-1))) = 1 ↔ ((((2 / 𝑁) · 𝑥) · (log‘-1)) / (i · (2 · π))) ∈ ℤ))
28		2cn 12283	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
29	28	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → 2 ∈ ℂ)
30		nncn 12216	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
31	30	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → 𝑁 ∈ ℂ)
32	17	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈ ℂ)
33		nnne0 12242	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
34	33	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → 𝑁 ≠ 0)
35	29, 31, 32, 34	div13d 12010	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → ((2 / 𝑁) · 𝑥) = ((𝑥 / 𝑁) · 2))
36		logm1 26427	. . . . . . . . . . . . 13 ⊢ (log‘-1) = (i · π)
37	36	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (log‘-1) = (i · π))
38	35, 37	oveq12d 7419	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (((2 / 𝑁) · 𝑥) · (log‘-1)) = (((𝑥 / 𝑁) · 2) · (i · π)))
39	32, 31, 34	divcld 11986	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (𝑥 / 𝑁) ∈ ℂ)
40		ax-icn 11164	. . . . . . . . . . . . . 14 ⊢ i ∈ ℂ
41		picn 26299	. . . . . . . . . . . . . 14 ⊢ π ∈ ℂ
42	40, 41	mulcli 11217	. . . . . . . . . . . . 13 ⊢ (i · π) ∈ ℂ
43	42	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (i · π) ∈ ℂ)
44	39, 29, 43	mulassd 11233	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (((𝑥 / 𝑁) · 2) · (i · π)) = ((𝑥 / 𝑁) · (2 · (i · π))))
45	40	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → i ∈ ℂ)
46	41	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → π ∈ ℂ)
47	29, 45, 46	mul12d 11419	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (2 · (i · π)) = (i · (2 · π)))
48	47	oveq2d 7417	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → ((𝑥 / 𝑁) · (2 · (i · π))) = ((𝑥 / 𝑁) · (i · (2 · π))))
49	38, 44, 48	3eqtrd 2768	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (((2 / 𝑁) · 𝑥) · (log‘-1)) = ((𝑥 / 𝑁) · (i · (2 · π))))
50	49	oveq1d 7416	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → ((((2 / 𝑁) · 𝑥) · (log‘-1)) / (i · (2 · π))) = (((𝑥 / 𝑁) · (i · (2 · π))) / (i · (2 · π))))
51	28, 41	mulcli 11217	. . . . . . . . . . . 12 ⊢ (2 · π) ∈ ℂ
52	40, 51	mulcli 11217	. . . . . . . . . . 11 ⊢ (i · (2 · π)) ∈ ℂ
53	52	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (i · (2 · π)) ∈ ℂ)
54		ine0 11645	. . . . . . . . . . . 12 ⊢ i ≠ 0
55		2ne0 12312	. . . . . . . . . . . . 13 ⊢ 2 ≠ 0
56		pire 26298	. . . . . . . . . . . . . 14 ⊢ π ∈ ℝ
57		pipos 26300	. . . . . . . . . . . . . 14 ⊢ 0 < π
58	56, 57	gt0ne0ii 11746	. . . . . . . . . . . . 13 ⊢ π ≠ 0
59	28, 41, 55, 58	mulne0i 11853	. . . . . . . . . . . 12 ⊢ (2 · π) ≠ 0
60	40, 51, 54, 59	mulne0i 11853	. . . . . . . . . . 11 ⊢ (i · (2 · π)) ≠ 0
61	60	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (i · (2 · π)) ≠ 0)
62	39, 53, 61	divcan4d 11992	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (((𝑥 / 𝑁) · (i · (2 · π))) / (i · (2 · π))) = (𝑥 / 𝑁))
63	50, 62	eqtrd 2764	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → ((((2 / 𝑁) · 𝑥) · (log‘-1)) / (i · (2 · π))) = (𝑥 / 𝑁))
64	63	eleq1d 2810	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (((((2 / 𝑁) · 𝑥) · (log‘-1)) / (i · (2 · π))) ∈ ℤ ↔ (𝑥 / 𝑁) ∈ ℤ))
65	21, 27, 64	3bitrd 305	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → ((-1↑𝑐((2 / 𝑁) · 𝑥)) = 1 ↔ (𝑥 / 𝑁) ∈ ℤ))
66	6	adantr 480	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (2 / 𝑁) ∈ ℂ)
67		simpr 484	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈ ℕ0)
68	15, 66, 67	cxpmul2d 26547	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (-1↑𝑐((2 / 𝑁) · 𝑥)) = ((-1↑𝑐(2 / 𝑁))↑𝑥))
69		cnfldexp 21257	. . . . . . . . 9 ⊢ (((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ 𝑥 ∈ ℕ0) → (𝑥(.g‘(mulGrp‘ℂfld))(-1↑𝑐(2 / 𝑁))) = ((-1↑𝑐(2 / 𝑁))↑𝑥))
70	8, 69	sylan 579	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (𝑥(.g‘(mulGrp‘ℂfld))(-1↑𝑐(2 / 𝑁))) = ((-1↑𝑐(2 / 𝑁))↑𝑥))
71		cnring 21246	. . . . . . . . . 10 ⊢ ℂfld ∈ Ring
72		cnfldbas 21227	. . . . . . . . . . . 12 ⊢ ℂ = (Base‘ℂfld)
73		cnfld0 21248	. . . . . . . . . . . 12 ⊢ 0 = (0g‘ℂfld)
74		cndrng 21253	. . . . . . . . . . . 12 ⊢ ℂfld ∈ DivRing
75	72, 73, 74	drngui 20578	. . . . . . . . . . 11 ⊢ (ℂ ∖ {0}) = (Unit‘ℂfld)
76		eqid 2724	. . . . . . . . . . 11 ⊢ (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
77	75, 76	unitsubm 20273	. . . . . . . . . 10 ⊢ (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂfld)))
78	71, 77	mp1i 13	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂfld)))
79	14	adantr 480	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (-1↑𝑐(2 / 𝑁)) ∈ (ℂ ∖ {0}))
80		eqid 2724	. . . . . . . . . 10 ⊢ (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
81		proot1ex.g	. . . . . . . . . 10 ⊢ 𝐺 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
82		eqid 2724	. . . . . . . . . 10 ⊢ (.g‘𝐺) = (.g‘𝐺)
83	80, 81, 82	submmulg 19030	. . . . . . . . 9 ⊢ (((ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂfld)) ∧ 𝑥 ∈ ℕ0 ∧ (-1↑𝑐(2 / 𝑁)) ∈ (ℂ ∖ {0})) → (𝑥(.g‘(mulGrp‘ℂfld))(-1↑𝑐(2 / 𝑁))) = (𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁))))
84	78, 67, 79, 83	syl3anc 1368	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (𝑥(.g‘(mulGrp‘ℂfld))(-1↑𝑐(2 / 𝑁))) = (𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁))))
85	68, 70, 84	3eqtr2rd 2771	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁))) = (-1↑𝑐((2 / 𝑁) · 𝑥)))
86	85	eqeq1d 2726	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → ((𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁))) = 1 ↔ (-1↑𝑐((2 / 𝑁) · 𝑥)) = 1))
87		nnz 12575	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
88	87	adantr 480	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → 𝑁 ∈ ℤ)
89		nn0z 12579	. . . . . . . 8 ⊢ (𝑥 ∈ ℕ0 → 𝑥 ∈ ℤ)
90	89	adantl 481	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈ ℤ)
91		dvdsval2 16196	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ 𝑥 ∈ ℤ) → (𝑁 ∥ 𝑥 ↔ (𝑥 / 𝑁) ∈ ℤ))
92	88, 34, 90, 91	syl3anc 1368	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (𝑁 ∥ 𝑥 ↔ (𝑥 / 𝑁) ∈ ℤ))
93	65, 86, 92	3bitr4rd 312	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0) → (𝑁 ∥ 𝑥 ↔ (𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁))) = 1))
94	93	ralrimiva 3138	. . . 4 ⊢ (𝑁 ∈ ℕ → ∀𝑥 ∈ ℕ0 (𝑁 ∥ 𝑥 ↔ (𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁))) = 1))
95	75, 81	unitgrp 20270	. . . . . 6 ⊢ (ℂfld ∈ Ring → 𝐺 ∈ Grp)
96	71, 95	mp1i 13	. . . . 5 ⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Grp)
97		nnnn0 12475	. . . . 5 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
98	75, 81	unitgrpbas 20269	. . . . . 6 ⊢ (ℂ ∖ {0}) = (Base‘𝐺)
99		proot1ex.o	. . . . . 6 ⊢ 𝑂 = (od‘𝐺)
100		cnfld1 21249	. . . . . . . 8 ⊢ 1 = (1r‘ℂfld)
101	75, 81, 100	unitgrpid 20272	. . . . . . 7 ⊢ (ℂfld ∈ Ring → 1 = (0g‘𝐺))
102	71, 101	ax-mp 5	. . . . . 6 ⊢ 1 = (0g‘𝐺)
103	98, 99, 82, 102	odeq 19455	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (-1↑𝑐(2 / 𝑁)) ∈ (ℂ ∖ {0}) ∧ 𝑁 ∈ ℕ0) → (𝑁 = (𝑂‘(-1↑𝑐(2 / 𝑁))) ↔ ∀𝑥 ∈ ℕ0 (𝑁 ∥ 𝑥 ↔ (𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁))) = 1)))
104	96, 14, 97, 103	syl3anc 1368	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 = (𝑂‘(-1↑𝑐(2 / 𝑁))) ↔ ∀𝑥 ∈ ℕ0 (𝑁 ∥ 𝑥 ↔ (𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁))) = 1)))
105	94, 104	mpbird 257	. . 3 ⊢ (𝑁 ∈ ℕ → 𝑁 = (𝑂‘(-1↑𝑐(2 / 𝑁))))
106	105	eqcomd 2730	. 2 ⊢ (𝑁 ∈ ℕ → (𝑂‘(-1↑𝑐(2 / 𝑁))) = 𝑁)
107	98, 99	odf 19442	. . . 4 ⊢ 𝑂:(ℂ ∖ {0})⟶ℕ0
108		ffn 6707	. . . 4 ⊢ (𝑂:(ℂ ∖ {0})⟶ℕ0 → 𝑂 Fn (ℂ ∖ {0}))
109	107, 108	ax-mp 5	. . 3 ⊢ 𝑂 Fn (ℂ ∖ {0})
110		fniniseg 7051	. . 3 ⊢ (𝑂 Fn (ℂ ∖ {0}) → ((-1↑𝑐(2 / 𝑁)) ∈ (◡𝑂 “ {𝑁}) ↔ ((-1↑𝑐(2 / 𝑁)) ∈ (ℂ ∖ {0}) ∧ (𝑂‘(-1↑𝑐(2 / 𝑁))) = 𝑁)))
111	109, 110	mp1i 13	. 2 ⊢ (𝑁 ∈ ℕ → ((-1↑𝑐(2 / 𝑁)) ∈ (◡𝑂 “ {𝑁}) ↔ ((-1↑𝑐(2 / 𝑁)) ∈ (ℂ ∖ {0}) ∧ (𝑂‘(-1↑𝑐(2 / 𝑁))) = 𝑁)))
112	14, 106, 111	mpbir2and 710	1 ⊢ (𝑁 ∈ ℕ → (-1↑𝑐(2 / 𝑁)) ∈ (◡𝑂 “ {𝑁}))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098   ≠ wne 2932  ∀wral 3053   ∖ cdif 3937  {csn 4620   class class class wbr 5138  ^◡ccnv 5665   “ cima 5669   Fn wfn 6528  ⟶wf 6529  ‘cfv 6533  (class class class)co 7401  ℂcc 11103  0cc0 11105  1c1 11106  ici 11107   · cmul 11110  -cneg 11441   / cdiv 11867  ℕcn 12208  2c2 12263  ℕ₀cn0 12468  ℤcz 12554  ℝ⁺crp 12970  ↑cexp 14023  expce 16001  πcpi 16006   ∥ cdvds 16193   ↾_s cress 17169  0_gc0g 17381  SubMndcsubmnd 18699  Grpcgrp 18850  ._gcmg 18982  odcod 19429  mulGrpcmgp 20024  Ringcrg 20123  ℂ_fldccnfld 21223  logclog 26393  ↑_𝑐ccxp 26394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9631  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182  ax-pre-sup 11183  ax-addf 11184  ax-mulf 11185

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-tpos 8206  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8698  df-map 8817  df-pm 8818  df-ixp 8887  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-fsupp 9357  df-fi 9401  df-sup 9432  df-inf 9433  df-oi 9500  df-card 9929  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ioc 13325  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-fac 14230  df-bc 14259  df-hash 14287  df-shft 15010  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-limsup 15411  df-clim 15428  df-rlim 15429  df-sum 15629  df-ef 16007  df-sin 16009  df-cos 16010  df-pi 16012  df-dvds 16194  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-rest 17364  df-topn 17365  df-0g 17383  df-gsum 17384  df-topgen 17385  df-pt 17386  df-prds 17389  df-xrs 17444  df-qtop 17449  df-imas 17450  df-xps 17452  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18560  df-sgrp 18639  df-mnd 18655  df-submnd 18701  df-grp 18853  df-minusg 18854  df-sbg 18855  df-mulg 18983  df-cntz 19218  df-od 19433  df-cmn 19687  df-abl 19688  df-mgp 20025  df-rng 20043  df-ur 20072  df-ring 20125  df-cring 20126  df-oppr 20221  df-dvdsr 20244  df-unit 20245  df-invr 20275  df-dvr 20288  df-drng 20574  df-psmet 21215  df-xmet 21216  df-met 21217  df-bl 21218  df-mopn 21219  df-fbas 21220  df-fg 21221  df-cnfld 21224  df-top 22706  df-topon 22723  df-topsp 22745  df-bases 22759  df-cld 22833  df-ntr 22834  df-cls 22835  df-nei 22912  df-lp 22950  df-perf 22951  df-cn 23041  df-cnp 23042  df-haus 23129  df-tx 23376  df-hmeo 23569  df-fil 23660  df-fm 23752  df-flim 23753  df-flf 23754  df-xms 24136  df-ms 24137  df-tms 24138  df-cncf 24708  df-limc 25705  df-dv 25706  df-log 26395  df-cxp 26396

This theorem is referenced by: (None)