Theorem facavg 10740

Description: The product of two factorials is greater than or equal to the factorial of (the floor of) their average. (Contributed by NM, 9-Dec-2005.)

Assertion

Ref	Expression
facavg	⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ ((!‘𝑀) · (!‘𝑁)))

Proof of Theorem facavg

Step	Hyp	Ref	Expression
1		nn0addcl 9225	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℕ0)
2	1	nn0zd 9387	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℤ)
3		2nn 9094	. . . . . 6 ⊢ 2 ∈ ℕ
4		znq 9638	. . . . . 6 ⊢ (((𝑀 + 𝑁) ∈ ℤ ∧ 2 ∈ ℕ) → ((𝑀 + 𝑁) / 2) ∈ ℚ)
5	2, 3, 4	sylancl 413	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝑀 + 𝑁) / 2) ∈ ℚ)
6		flqle 10292	. . . . 5 ⊢ (((𝑀 + 𝑁) / 2) ∈ ℚ → (⌊‘((𝑀 + 𝑁) / 2)) ≤ ((𝑀 + 𝑁) / 2))
7	5, 6	syl 14	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (⌊‘((𝑀 + 𝑁) / 2)) ≤ ((𝑀 + 𝑁) / 2))
8	5	flqcld 10291	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (⌊‘((𝑀 + 𝑁) / 2)) ∈ ℤ)
9	8	zred 9389	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (⌊‘((𝑀 + 𝑁) / 2)) ∈ ℝ)
10		nn0readdcl 9249	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℝ)
11	10	rehalfcld 9179	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝑀 + 𝑁) / 2) ∈ ℝ)
12		nn0re 9199	. . . . . 6 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ)
13	12	adantr 276	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ ℝ)
14		letr 8054	. . . . 5 ⊢ (((⌊‘((𝑀 + 𝑁) / 2)) ∈ ℝ ∧ ((𝑀 + 𝑁) / 2) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((⌊‘((𝑀 + 𝑁) / 2)) ≤ ((𝑀 + 𝑁) / 2) ∧ ((𝑀 + 𝑁) / 2) ≤ 𝑀) → (⌊‘((𝑀 + 𝑁) / 2)) ≤ 𝑀))
15	9, 11, 13, 14	syl3anc 1248	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (((⌊‘((𝑀 + 𝑁) / 2)) ≤ ((𝑀 + 𝑁) / 2) ∧ ((𝑀 + 𝑁) / 2) ≤ 𝑀) → (⌊‘((𝑀 + 𝑁) / 2)) ≤ 𝑀))
16	7, 15	mpand 429	. . 3 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (((𝑀 + 𝑁) / 2) ≤ 𝑀 → (⌊‘((𝑀 + 𝑁) / 2)) ≤ 𝑀))
17	1	nn0ge0d 9246	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 0 ≤ (𝑀 + 𝑁))
18		halfnneg2 9165	. . . . . . 7 ⊢ ((𝑀 + 𝑁) ∈ ℝ → (0 ≤ (𝑀 + 𝑁) ↔ 0 ≤ ((𝑀 + 𝑁) / 2)))
19	10, 18	syl 14	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (0 ≤ (𝑀 + 𝑁) ↔ 0 ≤ ((𝑀 + 𝑁) / 2)))
20	17, 19	mpbid 147	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 0 ≤ ((𝑀 + 𝑁) / 2))
21		flqge0nn0 10307	. . . . 5 ⊢ ((((𝑀 + 𝑁) / 2) ∈ ℚ ∧ 0 ≤ ((𝑀 + 𝑁) / 2)) → (⌊‘((𝑀 + 𝑁) / 2)) ∈ ℕ0)
22	5, 20, 21	syl2anc 411	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (⌊‘((𝑀 + 𝑁) / 2)) ∈ ℕ0)
23		simpl 109	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ ℕ0)
24		facwordi 10734	. . . . 5 ⊢ (((⌊‘((𝑀 + 𝑁) / 2)) ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ (⌊‘((𝑀 + 𝑁) / 2)) ≤ 𝑀) → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ (!‘𝑀))
25	24	3exp 1203	. . . 4 ⊢ ((⌊‘((𝑀 + 𝑁) / 2)) ∈ ℕ0 → (𝑀 ∈ ℕ0 → ((⌊‘((𝑀 + 𝑁) / 2)) ≤ 𝑀 → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ (!‘𝑀))))
26	22, 23, 25	sylc 62	. . 3 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((⌊‘((𝑀 + 𝑁) / 2)) ≤ 𝑀 → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ (!‘𝑀)))
27		faccl 10729	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ0 → (!‘𝑀) ∈ ℕ)
28	27	nncnd 8947	. . . . . . 7 ⊢ (𝑀 ∈ ℕ0 → (!‘𝑀) ∈ ℂ)
29	28	mulridd 7988	. . . . . 6 ⊢ (𝑀 ∈ ℕ0 → ((!‘𝑀) · 1) = (!‘𝑀))
30	29	adantr 276	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((!‘𝑀) · 1) = (!‘𝑀))
31		faccl 10729	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
32	31	nnred 8946	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℝ)
33	32	adantl 277	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (!‘𝑁) ∈ ℝ)
34	27	nnred 8946	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ0 → (!‘𝑀) ∈ ℝ)
35	27	nnnn0d 9243	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → (!‘𝑀) ∈ ℕ0)
36	35	nn0ge0d 9246	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ0 → 0 ≤ (!‘𝑀))
37	34, 36	jca 306	. . . . . . 7 ⊢ (𝑀 ∈ ℕ0 → ((!‘𝑀) ∈ ℝ ∧ 0 ≤ (!‘𝑀)))
38	37	adantr 276	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((!‘𝑀) ∈ ℝ ∧ 0 ≤ (!‘𝑀)))
39	31	nnge1d 8976	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → 1 ≤ (!‘𝑁))
40	39	adantl 277	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 1 ≤ (!‘𝑁))
41		1re 7970	. . . . . . 7 ⊢ 1 ∈ ℝ
42		lemul2a 8830	. . . . . . 7 ⊢ (((1 ∈ ℝ ∧ (!‘𝑁) ∈ ℝ ∧ ((!‘𝑀) ∈ ℝ ∧ 0 ≤ (!‘𝑀))) ∧ 1 ≤ (!‘𝑁)) → ((!‘𝑀) · 1) ≤ ((!‘𝑀) · (!‘𝑁)))
43	41, 42	mp3anl1 1341	. . . . . 6 ⊢ ((((!‘𝑁) ∈ ℝ ∧ ((!‘𝑀) ∈ ℝ ∧ 0 ≤ (!‘𝑀))) ∧ 1 ≤ (!‘𝑁)) → ((!‘𝑀) · 1) ≤ ((!‘𝑀) · (!‘𝑁)))
44	33, 38, 40, 43	syl21anc 1247	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((!‘𝑀) · 1) ≤ ((!‘𝑀) · (!‘𝑁)))
45	30, 44	eqbrtrrd 4039	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (!‘𝑀) ≤ ((!‘𝑀) · (!‘𝑁)))
46		faccl 10729	. . . . . . 7 ⊢ ((⌊‘((𝑀 + 𝑁) / 2)) ∈ ℕ0 → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ∈ ℕ)
47	22, 46	syl 14	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ∈ ℕ)
48	47	nnred 8946	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ∈ ℝ)
49	34	adantr 276	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (!‘𝑀) ∈ ℝ)
50		remulcl 7953	. . . . . 6 ⊢ (((!‘𝑀) ∈ ℝ ∧ (!‘𝑁) ∈ ℝ) → ((!‘𝑀) · (!‘𝑁)) ∈ ℝ)
51	34, 32, 50	syl2an 289	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((!‘𝑀) · (!‘𝑁)) ∈ ℝ)
52		letr 8054	. . . . 5 ⊢ (((!‘(⌊‘((𝑀 + 𝑁) / 2))) ∈ ℝ ∧ (!‘𝑀) ∈ ℝ ∧ ((!‘𝑀) · (!‘𝑁)) ∈ ℝ) → (((!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ (!‘𝑀) ∧ (!‘𝑀) ≤ ((!‘𝑀) · (!‘𝑁))) → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ ((!‘𝑀) · (!‘𝑁))))
53	48, 49, 51, 52	syl3anc 1248	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (((!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ (!‘𝑀) ∧ (!‘𝑀) ≤ ((!‘𝑀) · (!‘𝑁))) → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ ((!‘𝑀) · (!‘𝑁))))
54	45, 53	mpan2d 428	. . 3 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ (!‘𝑀) → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ ((!‘𝑀) · (!‘𝑁))))
55	16, 26, 54	3syld 57	. 2 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (((𝑀 + 𝑁) / 2) ≤ 𝑀 → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ ((!‘𝑀) · (!‘𝑁))))
56		nn0re 9199	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
57	56	adantl 277	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℝ)
58		letr 8054	. . . . 5 ⊢ (((⌊‘((𝑀 + 𝑁) / 2)) ∈ ℝ ∧ ((𝑀 + 𝑁) / 2) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((⌊‘((𝑀 + 𝑁) / 2)) ≤ ((𝑀 + 𝑁) / 2) ∧ ((𝑀 + 𝑁) / 2) ≤ 𝑁) → (⌊‘((𝑀 + 𝑁) / 2)) ≤ 𝑁))
59	9, 11, 57, 58	syl3anc 1248	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (((⌊‘((𝑀 + 𝑁) / 2)) ≤ ((𝑀 + 𝑁) / 2) ∧ ((𝑀 + 𝑁) / 2) ≤ 𝑁) → (⌊‘((𝑀 + 𝑁) / 2)) ≤ 𝑁))
60	7, 59	mpand 429	. . 3 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (((𝑀 + 𝑁) / 2) ≤ 𝑁 → (⌊‘((𝑀 + 𝑁) / 2)) ≤ 𝑁))
61		simpr 110	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℕ0)
62		facwordi 10734	. . . . 5 ⊢ (((⌊‘((𝑀 + 𝑁) / 2)) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (⌊‘((𝑀 + 𝑁) / 2)) ≤ 𝑁) → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ (!‘𝑁))
63	62	3exp 1203	. . . 4 ⊢ ((⌊‘((𝑀 + 𝑁) / 2)) ∈ ℕ0 → (𝑁 ∈ ℕ0 → ((⌊‘((𝑀 + 𝑁) / 2)) ≤ 𝑁 → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ (!‘𝑁))))
64	22, 61, 63	sylc 62	. . 3 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((⌊‘((𝑀 + 𝑁) / 2)) ≤ 𝑁 → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ (!‘𝑁)))
65	31	nncnd 8947	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℂ)
66	65	mulid2d 7990	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (1 · (!‘𝑁)) = (!‘𝑁))
67	66	adantl 277	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (1 · (!‘𝑁)) = (!‘𝑁))
68	31	nnnn0d 9243	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ0)
69	68	nn0ge0d 9246	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ (!‘𝑁))
70	32, 69	jca 306	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → ((!‘𝑁) ∈ ℝ ∧ 0 ≤ (!‘𝑁)))
71	70	adantl 277	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((!‘𝑁) ∈ ℝ ∧ 0 ≤ (!‘𝑁)))
72	27	nnge1d 8976	. . . . . . 7 ⊢ (𝑀 ∈ ℕ0 → 1 ≤ (!‘𝑀))
73	72	adantr 276	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 1 ≤ (!‘𝑀))
74		lemul1a 8829	. . . . . . 7 ⊢ (((1 ∈ ℝ ∧ (!‘𝑀) ∈ ℝ ∧ ((!‘𝑁) ∈ ℝ ∧ 0 ≤ (!‘𝑁))) ∧ 1 ≤ (!‘𝑀)) → (1 · (!‘𝑁)) ≤ ((!‘𝑀) · (!‘𝑁)))
75	41, 74	mp3anl1 1341	. . . . . 6 ⊢ ((((!‘𝑀) ∈ ℝ ∧ ((!‘𝑁) ∈ ℝ ∧ 0 ≤ (!‘𝑁))) ∧ 1 ≤ (!‘𝑀)) → (1 · (!‘𝑁)) ≤ ((!‘𝑀) · (!‘𝑁)))
76	49, 71, 73, 75	syl21anc 1247	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (1 · (!‘𝑁)) ≤ ((!‘𝑀) · (!‘𝑁)))
77	67, 76	eqbrtrrd 4039	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (!‘𝑁) ≤ ((!‘𝑀) · (!‘𝑁)))
78		letr 8054	. . . . 5 ⊢ (((!‘(⌊‘((𝑀 + 𝑁) / 2))) ∈ ℝ ∧ (!‘𝑁) ∈ ℝ ∧ ((!‘𝑀) · (!‘𝑁)) ∈ ℝ) → (((!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ (!‘𝑁) ∧ (!‘𝑁) ≤ ((!‘𝑀) · (!‘𝑁))) → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ ((!‘𝑀) · (!‘𝑁))))
79	48, 33, 51, 78	syl3anc 1248	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (((!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ (!‘𝑁) ∧ (!‘𝑁) ≤ ((!‘𝑀) · (!‘𝑁))) → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ ((!‘𝑀) · (!‘𝑁))))
80	77, 79	mpan2d 428	. . 3 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ (!‘𝑁) → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ ((!‘𝑀) · (!‘𝑁))))
81	60, 64, 80	3syld 57	. 2 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (((𝑀 + 𝑁) / 2) ≤ 𝑁 → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ ((!‘𝑀) · (!‘𝑁))))
82	23	nn0zd 9387	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ ℤ)
83		zq 9640	. . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℚ)
84	82, 83	syl 14	. . 3 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ ℚ)
85	61	nn0zd 9387	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℤ)
86		zq 9640	. . . 4 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℚ)
87	85, 86	syl 14	. . 3 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℚ)
88		qavgle 10273	. . 3 ⊢ ((𝑀 ∈ ℚ ∧ 𝑁 ∈ ℚ) → (((𝑀 + 𝑁) / 2) ≤ 𝑀 ∨ ((𝑀 + 𝑁) / 2) ≤ 𝑁))
89	84, 87, 88	syl2anc 411	. 2 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (((𝑀 + 𝑁) / 2) ≤ 𝑀 ∨ ((𝑀 + 𝑁) / 2) ≤ 𝑁))
90	55, 81, 89	mpjaod 719	1 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ ((!‘𝑀) · (!‘𝑁)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 709   = wceq 1363   ∈ wcel 2158   class class class wbr 4015  ‘cfv 5228  (class class class)co 5888  ℝcr 7824  0cc0 7825  1c1 7826   + caddc 7828   · cmul 7830   ≤ cle 8007   / cdiv 8643  ℕcn 8933  2c2 8984  ℕ₀cn0 9190  ℤcz 9267  ℚcq 9633  ⌊cfl 10282  !cfa 10719

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7916  ax-resscn 7917  ax-1cn 7918  ax-1re 7919  ax-icn 7920  ax-addcl 7921  ax-addrcl 7922  ax-mulcl 7923  ax-mulrcl 7924  ax-addcom 7925  ax-mulcom 7926  ax-addass 7927  ax-mulass 7928  ax-distr 7929  ax-i2m1 7930  ax-0lt1 7931  ax-1rid 7932  ax-0id 7933  ax-rnegex 7934  ax-precex 7935  ax-cnre 7936  ax-pre-ltirr 7937  ax-pre-ltwlin 7938  ax-pre-lttrn 7939  ax-pre-apti 7940  ax-pre-ltadd 7941  ax-pre-mulgt0 7942  ax-pre-mulext 7943  ax-arch 7944

This theorem depends on definitions:  df-bi 117  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6155  df-2nd 6156  df-recs 6320  df-frec 6406  df-pnf 8008  df-mnf 8009  df-xr 8010  df-ltxr 8011  df-le 8012  df-sub 8144  df-neg 8145  df-reap 8546  df-ap 8553  df-div 8644  df-inn 8934  df-2 8992  df-n0 9191  df-z 9268  df-uz 9543  df-q 9634  df-rp 9668  df-fl 10284  df-seqfrec 10460  df-fac 10720

This theorem is referenced by: (None)