Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem znnen 4930

Description: The set of integers and the set of natural numbers are equinumerous.

**Assertion**
Ref	Expression
znnen	⊢ ℤ ≈ ℕ

**Proof of Theorem znnen**
Step	Hyp	Ref	Expression
1		zex 4571	. . . 4 ⊢ ℤ ∈ V
2		elnn0z 4574	. . . . . . . 8 ⊢ (x ∈ ℕ₀ ↔ (x ∈ ℤ ∧ 0 ≤ x))
3		2nn0 4548	. . . . . . . . 9 ⊢ 2 ∈ ℕ₀
4		nn0mulclt 4554	. . . . . . . . 9 ⊢ ((2 ∈ ℕ₀ ∧ x ∈ ℕ₀) → (2 · x) ∈ ℕ₀)
5	3, 4	mpan 518	. . . . . . . 8 ⊢ (x ∈ ℕ₀ → (2 · x) ∈ ℕ₀)
6	2, 5	sylbir 176	. . . . . . 7 ⊢ ((x ∈ ℤ ∧ 0 ≤ x) → (2 · x) ∈ ℕ₀)
7		iftrue 1780	. . . . . . . . 9 ⊢ (0 ≤ x → if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = (2 · x))
8	7	eleq1d 1155	. . . . . . . 8 ⊢ (0 ≤ x → (if(0 ≤ x, (2 · x), ((-2 · x) + 1)) ∈ ℕ₀ ↔ (2 · x) ∈ ℕ₀))
9	8	adantl 305	. . . . . . 7 ⊢ ((x ∈ ℤ ∧ 0 ≤ x) → (if(0 ≤ x, (2 · x), ((-2 · x) + 1)) ∈ ℕ₀ ↔ (2 · x) ∈ ℕ₀))
10	6, 9	mpbird 171	. . . . . 6 ⊢ ((x ∈ ℤ ∧ 0 ≤ x) → if(0 ≤ x, (2 · x), ((-2 · x) + 1)) ∈ ℕ₀)
11		2z 4585	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
12		znegclt 4588	. . . . . . . . . . . 12 ⊢ (2 ∈ ℤ → -2 ∈ ℤ)
13	11, 12	ax-mp 6	. . . . . . . . . . 11 ⊢ -2 ∈ ℤ
14		zmulclt 4596	. . . . . . . . . . 11 ⊢ ((-2 ∈ ℤ ∧ x ∈ ℤ) → (-2 · x) ∈ ℤ)
15	13, 14	mpan 518	. . . . . . . . . 10 ⊢ (x ∈ ℤ → (-2 · x) ∈ ℤ)
16	15	adantr 306	. . . . . . . . 9 ⊢ ((x ∈ ℤ ∧ ¬ 0 ≤ x) → (-2 · x) ∈ ℤ)
17		zret 4567	. . . . . . . . . . 11 ⊢ (x ∈ ℤ → x ∈ ℝ)
18		renegclt 4172	. . . . . . . . . . . . . 14 ⊢ (x ∈ ℝ → -x ∈ ℝ)
19		2pos 4479	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
20		2re 4470	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
21		axmulgt0 4086	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ ∧ -x ∈ ℝ) → ((0 < 2 ∧ 0 < -x) → 0 < (2 · -x)))
22	20, 21	mpan 518	. . . . . . . . . . . . . . 15 ⊢ (-x ∈ ℝ → ((0 < 2 ∧ 0 < -x) → 0 < (2 · -x)))
23	19, 22	mpani 521	. . . . . . . . . . . . . 14 ⊢ (-x ∈ ℝ → (0 < -x → 0 < (2 · -x)))
24	18, 23	syl 12	. . . . . . . . . . . . 13 ⊢ (x ∈ ℝ → (0 < -x → 0 < (2 · -x)))
25		ax0re 4063	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
26		leltt 4278	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ ∧ x ∈ ℝ) → (0 ≤ x ↔ ¬ x < 0))
27	25, 26	mpan 518	. . . . . . . . . . . . . . 15 ⊢ (x ∈ ℝ → (0 ≤ x ↔ ¬ x < 0))
28	27	bicon2d 404	. . . . . . . . . . . . . 14 ⊢ (x ∈ ℝ → (x < 0 ↔ ¬ 0 ≤ x))
29		lt0neg1t 4370	. . . . . . . . . . . . . 14 ⊢ (x ∈ ℝ → (x < 0 ↔ 0 < -x))
30	28, 29	bitr3d 408	. . . . . . . . . . . . 13 ⊢ (x ∈ ℝ → (¬ 0 ≤ x ↔ 0 < -x))
31		recnt 4097	. . . . . . . . . . . . . . 15 ⊢ (x ∈ ℝ → x ∈ ℂ)
32		2cn 4471	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
33		mulneg12t 4198	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℂ ∧ x ∈ ℂ) → (-2 · x) = (2 · -x))
34	32, 33	mpan 518	. . . . . . . . . . . . . . 15 ⊢ (x ∈ ℂ → (-2 · x) = (2 · -x))
35	31, 34	syl 12	. . . . . . . . . . . . . 14 ⊢ (x ∈ ℝ → (-2 · x) = (2 · -x))
36	35	breq2d 2072	. . . . . . . . . . . . 13 ⊢ (x ∈ ℝ → (0 < (-2 · x) ↔ 0 < (2 · -x)))
37	24, 30, 36	3imtr4d 421	. . . . . . . . . . . 12 ⊢ (x ∈ ℝ → (¬ 0 ≤ x → 0 < (-2 · x)))
38	20	renegcl 4171	. . . . . . . . . . . . . 14 ⊢ -2 ∈ ℝ
39		axmulrcl 4069	. . . . . . . . . . . . . 14 ⊢ ((-2 ∈ ℝ ∧ x ∈ ℝ) → (-2 · x) ∈ ℝ)
40	38, 39	mpan 518	. . . . . . . . . . . . 13 ⊢ (x ∈ ℝ → (-2 · x) ∈ ℝ)
41		ltlet 4286	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (-2 · x) ∈ ℝ) → (0 < (-2 · x) → 0 ≤ (-2 · x)))
42	25, 41	mpan 518	. . . . . . . . . . . . 13 ⊢ ((-2 · x) ∈ ℝ → (0 < (-2 · x) → 0 ≤ (-2 · x)))
43	40, 42	syl 12	. . . . . . . . . . . 12 ⊢ (x ∈ ℝ → (0 < (-2 · x) → 0 ≤ (-2 · x)))
44	37, 43	syld 27	. . . . . . . . . . 11 ⊢ (x ∈ ℝ → (¬ 0 ≤ x → 0 ≤ (-2 · x)))
45	17, 44	syl 12	. . . . . . . . . 10 ⊢ (x ∈ ℤ → (¬ 0 ≤ x → 0 ≤ (-2 · x)))
46	45	imp 277	. . . . . . . . 9 ⊢ ((x ∈ ℤ ∧ ¬ 0 ≤ x) → 0 ≤ (-2 · x))
47	16, 46	jca 236	. . . . . . . 8 ⊢ ((x ∈ ℤ ∧ ¬ 0 ≤ x) → ((-2 · x) ∈ ℤ ∧ 0 ≤ (-2 · x)))
48		elnn0z 4574	. . . . . . . . 9 ⊢ ((-2 · x) ∈ ℕ₀ ↔ ((-2 · x) ∈ ℤ ∧ 0 ≤ (-2 · x)))
49	48	biimpr 134	. . . . . . . 8 ⊢ (((-2 · x) ∈ ℤ ∧ 0 ≤ (-2 · x)) → (-2 · x) ∈ ℕ₀)
50		peano2nn0 4555	. . . . . . . 8 ⊢ ((-2 · x) ∈ ℕ₀ → ((-2 · x) + 1) ∈ ℕ₀)
51	47, 49, 50	3syl 21	. . . . . . 7 ⊢ ((x ∈ ℤ ∧ ¬ 0 ≤ x) → ((-2 · x) + 1) ∈ ℕ₀)
52		iffalse 1781	. . . . . . . . 9 ⊢ (¬ 0 ≤ x → if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = ((-2 · x) + 1))
53	52	eleq1d 1155	. . . . . . . 8 ⊢ (¬ 0 ≤ x → (if(0 ≤ x, (2 · x), ((-2 · x) + 1)) ∈ ℕ₀ ↔ ((-2 · x) + 1) ∈ ℕ₀))
54	53	adantl 305	. . . . . . 7 ⊢ ((x ∈ ℤ ∧ ¬ 0 ≤ x) → (if(0 ≤ x, (2 · x), ((-2 · x) + 1)) ∈ ℕ₀ ↔ ((-2 · x) + 1) ∈ ℕ₀))
55	51, 54	mpbird 171	. . . . . 6 ⊢ ((x ∈ ℤ ∧ ¬ 0 ≤ x) → if(0 ≤ x, (2 · x), ((-2 · x) + 1)) ∈ ℕ₀)
56	10, 55	pm2.61an2 365	. . . . 5 ⊢ (x ∈ ℤ → if(0 ≤ x, (2 · x), ((-2 · x) + 1)) ∈ ℕ₀)
57		iftrue 1780	. . . . . . . . . . 11 ⊢ (0 ≤ y → if(0 ≤ y, (2 · y), ((-2 · y) + 1)) = (2 · y))
58	7, 57	cleqan12d 1116	. . . . . . . . . 10 ⊢ ((0 ≤ x ∧ 0 ≤ y) → (if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1)) ↔ (2 · x) = (2 · y)))
59	20, 19	gt0ne0i 4345	. . . . . . . . . . . . 13 ⊢ 2 ≠ 0
60	59	mulcant 4208	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ x ∈ ℂ ∧ y ∈ ℂ) → ((2 · x) = (2 · y) ↔ x = y))
61	32, 60	mp3an1 639	. . . . . . . . . . 11 ⊢ ((x ∈ ℂ ∧ y ∈ ℂ) → ((2 · x) = (2 · y) ↔ x = y))
62		zcnt 4568	. . . . . . . . . . 11 ⊢ (x ∈ ℤ → x ∈ ℂ)
63		zcnt 4568	. . . . . . . . . . 11 ⊢ (y ∈ ℤ → y ∈ ℂ)
64	61, 62, 63	syl2an 349	. . . . . . . . . 10 ⊢ ((x ∈ ℤ ∧ y ∈ ℤ) → ((2 · x) = (2 · y) ↔ x = y))
65	58, 64	sylan9bb 418	. . . . . . . . 9 ⊢ (((0 ≤ x ∧ 0 ≤ y) ∧ (x ∈ ℤ ∧ y ∈ ℤ)) → (if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1)) ↔ x = y))
66	65	bicomd 399	. . . . . . . 8 ⊢ (((0 ≤ x ∧ 0 ≤ y) ∧ (x ∈ ℤ ∧ y ∈ ℤ)) → (x = y ↔ if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1))))
67	66	exp 291	. . . . . . 7 ⊢ ((0 ≤ x ∧ 0 ≤ y) → ((x ∈ ℤ ∧ y ∈ ℤ) → (x = y ↔ if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1)))))
68		znnenlem 4929	. . . . . . . . . 10 ⊢ (((0 ≤ x ∧ ¬ 0 ≤ y) ∧ (x ∈ ℤ ∧ y ∈ ℤ)) → (y = x ↔ (2 · x) = ((-2 · y) + 1)))
69		eqcomb 812	. . . . . . . . . 10 ⊢ (x = y ↔ y = x)
70	68, 69	syl5bb 410	. . . . . . . . 9 ⊢ (((0 ≤ x ∧ ¬ 0 ≤ y) ∧ (x ∈ ℤ ∧ y ∈ ℤ)) → (x = y ↔ (2 · x) = ((-2 · y) + 1)))
71		iffalse 1781	. . . . . . . . . . 11 ⊢ (¬ 0 ≤ y → if(0 ≤ y, (2 · y), ((-2 · y) + 1)) = ((-2 · y) + 1))
72	7, 71	cleqan12d 1116	. . . . . . . . . 10 ⊢ ((0 ≤ x ∧ ¬ 0 ≤ y) → (if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1)) ↔ (2 · x) = ((-2 · y) + 1)))
73	72	adantr 306	. . . . . . . . 9 ⊢ (((0 ≤ x ∧ ¬ 0 ≤ y) ∧ (x ∈ ℤ ∧ y ∈ ℤ)) → (if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1)) ↔ (2 · x) = ((-2 · y) + 1)))
74	70, 73	bitr4d 409	. . . . . . . 8 ⊢ (((0 ≤ x ∧ ¬ 0 ≤ y) ∧ (x ∈ ℤ ∧ y ∈ ℤ)) → (x = y ↔ if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1))))
75	74	exp 291	. . . . . . 7 ⊢ ((0 ≤ x ∧ ¬ 0 ≤ y) → ((x ∈ ℤ ∧ y ∈ ℤ) → (x = y ↔ if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1)))))
76		znnenlem 4929	. . . . . . . . . . 11 ⊢ (((0 ≤ y ∧ ¬ 0 ≤ x) ∧ (y ∈ ℤ ∧ x ∈ ℤ)) → (x = y ↔ (2 · y) = ((-2 · x) + 1)))
77		ancom 333	. . . . . . . . . . 11 ⊢ ((¬ 0 ≤ x ∧ 0 ≤ y) ↔ (0 ≤ y ∧ ¬ 0 ≤ x))
78		ancom 333	. . . . . . . . . . 11 ⊢ ((x ∈ ℤ ∧ y ∈ ℤ) ↔ (y ∈ ℤ ∧ x ∈ ℤ))
79	76, 77, 78	syl2anb 350	. . . . . . . . . 10 ⊢ (((¬ 0 ≤ x ∧ 0 ≤ y) ∧ (x ∈ ℤ ∧ y ∈ ℤ)) → (x = y ↔ (2 · y) = ((-2 · x) + 1)))
80		cleqcom 1103	. . . . . . . . . 10 ⊢ (((-2 · x) + 1) = (2 · y) ↔ (2 · y) = ((-2 · x) + 1))
81	79, 80	syl6bbr 416	. . . . . . . . 9 ⊢ (((¬ 0 ≤ x ∧ 0 ≤ y) ∧ (x ∈ ℤ ∧ y ∈ ℤ)) → (x = y ↔ ((-2 · x) + 1) = (2 · y)))
82	52, 57	cleqan12d 1116	. . . . . . . . . 10 ⊢ ((¬ 0 ≤ x ∧ 0 ≤ y) → (if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1)) ↔ ((-2 · x) + 1) = (2 · y)))
83	82	adantr 306	. . . . . . . . 9 ⊢ (((¬ 0 ≤ x ∧ 0 ≤ y) ∧ (x ∈ ℤ ∧ y ∈ ℤ)) → (if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1)) ↔ ((-2 · x) + 1) = (2 · y)))
84	81, 83	bitr4d 409	. . . . . . . 8 ⊢ (((¬ 0 ≤ x ∧ 0 ≤ y) ∧ (x ∈ ℤ ∧ y ∈ ℤ)) → (x = y ↔ if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1))))
85	84	exp 291	. . . . . . 7 ⊢ ((¬ 0 ≤ x ∧ 0 ≤ y) → ((x ∈ ℤ ∧ y ∈ ℤ) → (x = y ↔ if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1)))))
86		1cn 4101	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
87		addcan2t 4123	. . . . . . . . . . . . 13 ⊢ (((-2 · x) ∈ ℂ ∧ (-2 · y) ∈ ℂ ∧ 1 ∈ ℂ) → (((-2 · x) + 1) = ((-2 · y) + 1) ↔ (-2 · x) = (-2 · y)))
88	86, 87	mp3an3 641	. . . . . . . . . . . 12 ⊢ (((-2 · x) ∈ ℂ ∧ (-2 · y) ∈ ℂ) → (((-2 · x) + 1) = ((-2 · y) + 1) ↔ (-2 · x) = (-2 · y)))
89	32	negcl 4142	. . . . . . . . . . . . 13 ⊢ -2 ∈ ℂ
90		axmulcl 4068	. . . . . . . . . . . . 13 ⊢ ((-2 ∈ ℂ ∧ x ∈ ℂ) → (-2 · x) ∈ ℂ)
91	89, 90	mpan 518	. . . . . . . . . . . 12 ⊢ (x ∈ ℂ → (-2 · x) ∈ ℂ)
92		axmulcl 4068	. . . . . . . . . . . . 13 ⊢ ((-2 ∈ ℂ ∧ y ∈ ℂ) → (-2 · y) ∈ ℂ)
93	89, 92	mpan 518	. . . . . . . . . . . 12 ⊢ (y ∈ ℂ → (-2 · y) ∈ ℂ)
94	88, 91, 93	syl2an 349	. . . . . . . . . . 11 ⊢ ((x ∈ ℂ ∧ y ∈ ℂ) → (((-2 · x) + 1) = ((-2 · y) + 1) ↔ (-2 · x) = (-2 · y)))
95	32, 59	negn0 4380	. . . . . . . . . . . . 13 ⊢ -2 ≠ 0
96	95	mulcant 4208	. . . . . . . . . . . 12 ⊢ ((-2 ∈ ℂ ∧ x ∈ ℂ ∧ y ∈ ℂ) → ((-2 · x) = (-2 · y) ↔ x = y))
97	89, 96	mp3an1 639	. . . . . . . . . . 11 ⊢ ((x ∈ ℂ ∧ y ∈ ℂ) → ((-2 · x) = (-2 · y) ↔ x = y))
98	94, 97	bitr2d 407	. . . . . . . . . 10 ⊢ ((x ∈ ℂ ∧ y ∈ ℂ) → (x = y ↔ ((-2 · x) + 1) = ((-2 · y) + 1)))
99	98, 62, 63	syl2an 349	. . . . . . . . 9 ⊢ ((x ∈ ℤ ∧ y ∈ ℤ) → (x = y ↔ ((-2 · x) + 1) = ((-2 · y) + 1)))
100	52, 71	cleqan12d 1116	. . . . . . . . . 10 ⊢ ((¬ 0 ≤ x ∧ ¬ 0 ≤ y) → (if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1)) ↔ ((-2 · x) + 1) = ((-2 · y) + 1)))
101	100	bicomd 399	. . . . . . . . 9 ⊢ ((¬ 0 ≤ x ∧ ¬ 0 ≤ y) → (((-2 · x) + 1) = ((-2 · y) + 1) ↔ if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1))))
102	99, 101	sylan9bbr 419	. . . . . . . 8 ⊢ (((¬ 0 ≤ x ∧ ¬ 0 ≤ y) ∧ (x ∈ ℤ ∧ y ∈ ℤ)) → (x = y ↔ if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1))))
103	102	exp 291	. . . . . . 7 ⊢ ((¬ 0 ≤ x ∧ ¬ 0 ≤ y) → ((x ∈ ℤ ∧ y ∈ ℤ) → (x = y ↔ if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1)))))
104	67, 75, 85, 103	4cases 565	. . . . . 6 ⊢ ((x ∈ ℤ ∧ y ∈ ℤ) → (x = y ↔ if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1))))
105	104	bicomd 399	. . . . 5 ⊢ ((x ∈ ℤ ∧ y ∈ ℤ) → (if(0 ≤ x, (2 · x), ((-2 · x) + 1)) = if(0 ≤ y, (2 · y), ((-2 · y) + 1)) ↔ x = y))
106	56, 105	dom2 3308	. . . 4 ⊢ (ℤ ∈ V → ℤ ≼ ℕ₀)
107	1, 106	ax-mp 6	. . 3 ⊢ ℤ ≼ ℕ₀
108		nn0ex 4540	. . . 4 ⊢ ℕ₀ ∈ V
109		nn0ssz 4578	. . . 4 ⊢ ℕ₀ ⊆ ℤ
110		ssdomg 3311	. . . 4 ⊢ (ℕ₀ ∈ V → (ℕ₀ ⊆ ℤ → ℕ₀ ≼ ℤ))
111	108, 109, 110	mp2 43	. . 3 ⊢ ℕ₀ ≼ ℤ
112		sbth 3359	. . 3 ⊢ ((ℤ ≼ ℕ₀ ∧ ℕ₀ ≼ ℤ) → ℤ ≈ ℕ₀)
113	107, 111, 112	mp2an 520	. 2 ⊢ ℤ ≈ ℕ₀
114		nn0ennn 4925	. 2 ⊢ ℕ₀ ≈ ℕ
115	113, 114	entr 3321	1 ⊢ ℤ ≈ ℕ

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∧ wa 196 = weq 797 = wceq 1091 ∈ wcel 1092 Vcvv 1348 ⊆ wss 1487 ifcif 1776 class class class wbr 2054 (class class class)co 3001 ≈ cen 3271 ≼ cdom 3272 ℂcc 4026 ℝcr 4027 0cc0 4028 1c1 4029 + caddc 4031 · cmulc 4032 < clt 4033 -cneg 4090 ≤ cle 4092 ℕcn 4093 ℕ₀cn0 4094 ℤcz 4095 2c2 4454

This theorem is referenced by: qnnen 4931

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-en 3274 df-dom 3275 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-div 4216 df-le 4277 df-n 4423 df-2 4462 df-n0 4535 df-z 4564

metamath.org