Theorem bclbnd 16319

Description: A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.)

Assertion

Ref	Expression
bclbnd	|- ( N e. ( ZZ>= ` 4 ) -> ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) )

Proof of Theorem bclbnd

Dummy variables x n are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 6096	. . . 4 |- ( x = 4 -> ( 4 ^ x ) = ( 4 ^ 4 ) )
2		id 19	. . . 4 |- ( x = 4 -> x = 4 )
3	1, 2	oveq12d 6106	. . 3 |- ( x = 4 -> ( ( 4 ^ x ) / x ) = ( ( 4 ^ 4 ) / 4 ) )
4		oveq2 6096	. . . 4 |- ( x = 4 -> ( 2 x. x ) = ( 2 x. 4 ) )
5	4, 2	oveq12d 6106	. . 3 |- ( x = 4 -> ( ( 2 x. x ) _C x ) = ( ( 2 x. 4 ) _C 4 ) )
6	3, 5	breq12d 4144	. 2 |- ( x = 4 -> ( ( ( 4 ^ x ) / x ) < ( ( 2 x. x ) _C x ) <-> ( ( 4 ^ 4 ) / 4 ) < ( ( 2 x. 4 ) _C 4 ) ) )
7		oveq2 6096	. . . 4 |- ( x = n -> ( 4 ^ x ) = ( 4 ^ n ) )
8		id 19	. . . 4 |- ( x = n -> x = n )
9	7, 8	oveq12d 6106	. . 3 |- ( x = n -> ( ( 4 ^ x ) / x ) = ( ( 4 ^ n ) / n ) )
10		oveq2 6096	. . . 4 |- ( x = n -> ( 2 x. x ) = ( 2 x. n ) )
11	10, 8	oveq12d 6106	. . 3 |- ( x = n -> ( ( 2 x. x ) _C x ) = ( ( 2 x. n ) _C n ) )
12	9, 11	breq12d 4144	. 2 |- ( x = n -> ( ( ( 4 ^ x ) / x ) < ( ( 2 x. x ) _C x ) <-> ( ( 4 ^ n ) / n ) < ( ( 2 x. n ) _C n ) ) )
13		oveq2 6096	. . . 4 |- ( x = ( n + 1 ) -> ( 4 ^ x ) = ( 4 ^ ( n + 1 ) ) )
14		id 19	. . . 4 |- ( x = ( n + 1 ) -> x = ( n + 1 ) )
15	13, 14	oveq12d 6106	. . 3 |- ( x = ( n + 1 ) -> ( ( 4 ^ x ) / x ) = ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) )
16		oveq2 6096	. . . 4 |- ( x = ( n + 1 ) -> ( 2 x. x ) = ( 2 x. ( n + 1 ) ) )
17	16, 14	oveq12d 6106	. . 3 |- ( x = ( n + 1 ) -> ( ( 2 x. x ) _C x ) = ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) )
18	15, 17	breq12d 4144	. 2 |- ( x = ( n + 1 ) -> ( ( ( 4 ^ x ) / x ) < ( ( 2 x. x ) _C x ) <-> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) < ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) ) )
19		oveq2 6096	. . . 4 |- ( x = N -> ( 4 ^ x ) = ( 4 ^ N ) )
20		id 19	. . . 4 |- ( x = N -> x = N )
21	19, 20	oveq12d 6106	. . 3 |- ( x = N -> ( ( 4 ^ x ) / x ) = ( ( 4 ^ N ) / N ) )
22		oveq2 6096	. . . 4 |- ( x = N -> ( 2 x. x ) = ( 2 x. N ) )
23	22, 20	oveq12d 6106	. . 3 |- ( x = N -> ( ( 2 x. x ) _C x ) = ( ( 2 x. N ) _C N ) )
24	21, 23	breq12d 4144	. 2 |- ( x = N -> ( ( ( 4 ^ x ) / x ) < ( ( 2 x. x ) _C x ) <-> ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) ) )
25		6nn0 9596	. . . 4 |- 6 e. NN0
26		7nn0 9597	. . . 4 |- 7 e. NN0
27		4nn0 9594	. . . 4 |- 4 e. NN0
28		0nn0 9590	. . . 4 |- 0 e. NN0
29		4lt10 9929	. . . 4 |- 4 < ; 1 0
30		6lt7 9501	. . . 4 |- 6 < 7
31	25, 26, 27, 28, 29, 30	decltc 9822	. . 3 |- ; 6 4 < ; 7 0
32		2cn 9385	. . . . . 6 |- 2 e. CC
33		2nn0 9592	. . . . . 6 |- 2 e. NN0
34		3nn0 9593	. . . . . 6 |- 3 e. NN0
35		expmul 11043	. . . . . 6 |- ( ( 2 e. CC /\ 2 e. NN0 /\ 3 e. NN0 ) -> ( 2 ^ ( 2 x. 3 ) ) = ( ( 2 ^ 2 ) ^ 3 ) )
36	32, 33, 34, 35	mp3an 1378	. . . . 5 |- ( 2 ^ ( 2 x. 3 ) ) = ( ( 2 ^ 2 ) ^ 3 )
37		sq2 11094	. . . . . . 7 |- ( 2 ^ 2 ) = 4
38	37	eqcomi 2242	. . . . . 6 |- 4 = ( 2 ^ 2 )
39		4m1e3 9435	. . . . . 6 |- ( 4 - 1 ) = 3
40	38, 39	oveq12i 6100	. . . . 5 |- ( 4 ^ ( 4 - 1 ) ) = ( ( 2 ^ 2 ) ^ 3 )
41	36, 40	eqtr4i 2262	. . . 4 |- ( 2 ^ ( 2 x. 3 ) ) = ( 4 ^ ( 4 - 1 ) )
42		2t3e6 9472	. . . . . 6 |- ( 2 x. 3 ) = 6
43	42	oveq2i 6099	. . . . 5 |- ( 2 ^ ( 2 x. 3 ) ) = ( 2 ^ 6 )
44		2exp6 13243	. . . . 5 |- ( 2 ^ 6 ) = ; 6 4
45	43, 44	eqtri 2259	. . . 4 |- ( 2 ^ ( 2 x. 3 ) ) = ; 6 4
46		4cn 9392	. . . . 5 |- 4 e. CC
47		4ap0 9413	. . . . 5 |- 4 # 0
48		4z 9686	. . . . 5 |- 4 e. ZZ
49		expm1ap 11048	. . . . 5 |- ( ( 4 e. CC /\ 4 # 0 /\ 4 e. ZZ ) -> ( 4 ^ ( 4 - 1 ) ) = ( ( 4 ^ 4 ) / 4 ) )
50	46, 47, 48, 49	mp3an 1378	. . . 4 |- ( 4 ^ ( 4 - 1 ) ) = ( ( 4 ^ 4 ) / 4 )
51	41, 45, 50	3eqtr3ri 2268	. . 3 |- ( ( 4 ^ 4 ) / 4 ) = ; 6 4
52		df-4 9375	. . . . . . 7 |- 4 = ( 3 + 1 )
53	52	oveq2i 6099	. . . . . 6 |- ( 2 x. 4 ) = ( 2 x. ( 3 + 1 ) )
54	53, 52	oveq12i 6100	. . . . 5 |- ( ( 2 x. 4 ) _C 4 ) = ( ( 2 x. ( 3 + 1 ) ) _C ( 3 + 1 ) )
55		bcp1ctr 16318	. . . . . 6 |- ( 3 e. NN0 -> ( ( 2 x. ( 3 + 1 ) ) _C ( 3 + 1 ) ) = ( ( ( 2 x. 3 ) _C 3 ) x. ( 2 x. ( ( ( 2 x. 3 ) + 1 ) / ( 3 + 1 ) ) ) ) )
56	34, 55	ax-mp 5	. . . . 5 |- ( ( 2 x. ( 3 + 1 ) ) _C ( 3 + 1 ) ) = ( ( ( 2 x. 3 ) _C 3 ) x. ( 2 x. ( ( ( 2 x. 3 ) + 1 ) / ( 3 + 1 ) ) ) )
57		df-3 9374	. . . . . . . . 9 |- 3 = ( 2 + 1 )
58	57	oveq2i 6099	. . . . . . . 8 |- ( 2 x. 3 ) = ( 2 x. ( 2 + 1 ) )
59	58, 57	oveq12i 6100	. . . . . . 7 |- ( ( 2 x. 3 ) _C 3 ) = ( ( 2 x. ( 2 + 1 ) ) _C ( 2 + 1 ) )
60		bcp1ctr 16318	. . . . . . . . 9 |- ( 2 e. NN0 -> ( ( 2 x. ( 2 + 1 ) ) _C ( 2 + 1 ) ) = ( ( ( 2 x. 2 ) _C 2 ) x. ( 2 x. ( ( ( 2 x. 2 ) + 1 ) / ( 2 + 1 ) ) ) ) )
61	33, 60	ax-mp 5	. . . . . . . 8 |- ( ( 2 x. ( 2 + 1 ) ) _C ( 2 + 1 ) ) = ( ( ( 2 x. 2 ) _C 2 ) x. ( 2 x. ( ( ( 2 x. 2 ) + 1 ) / ( 2 + 1 ) ) ) )
62		df-2 9373	. . . . . . . . . . . 12 |- 2 = ( 1 + 1 )
63	62	oveq2i 6099	. . . . . . . . . . 11 |- ( 2 x. 2 ) = ( 2 x. ( 1 + 1 ) )
64	63, 62	oveq12i 6100	. . . . . . . . . 10 |- ( ( 2 x. 2 ) _C 2 ) = ( ( 2 x. ( 1 + 1 ) ) _C ( 1 + 1 ) )
65		1nn0 9591	. . . . . . . . . . 11 |- 1 e. NN0
66		bcp1ctr 16318	. . . . . . . . . . 11 |- ( 1 e. NN0 -> ( ( 2 x. ( 1 + 1 ) ) _C ( 1 + 1 ) ) = ( ( ( 2 x. 1 ) _C 1 ) x. ( 2 x. ( ( ( 2 x. 1 ) + 1 ) / ( 1 + 1 ) ) ) ) )
67	65, 66	ax-mp 5	. . . . . . . . . 10 |- ( ( 2 x. ( 1 + 1 ) ) _C ( 1 + 1 ) ) = ( ( ( 2 x. 1 ) _C 1 ) x. ( 2 x. ( ( ( 2 x. 1 ) + 1 ) / ( 1 + 1 ) ) ) )
68		1e0p1 9835	. . . . . . . . . . . . . . 15 |- 1 = ( 0 + 1 )
69	68	oveq2i 6099	. . . . . . . . . . . . . 14 |- ( 2 x. 1 ) = ( 2 x. ( 0 + 1 ) )
70	69, 68	oveq12i 6100	. . . . . . . . . . . . 13 |- ( ( 2 x. 1 ) _C 1 ) = ( ( 2 x. ( 0 + 1 ) ) _C ( 0 + 1 ) )
71		bcp1ctr 16318	. . . . . . . . . . . . . 14 |- ( 0 e. NN0 -> ( ( 2 x. ( 0 + 1 ) ) _C ( 0 + 1 ) ) = ( ( ( 2 x. 0 ) _C 0 ) x. ( 2 x. ( ( ( 2 x. 0 ) + 1 ) / ( 0 + 1 ) ) ) ) )
72	28, 71	ax-mp 5	. . . . . . . . . . . . 13 |- ( ( 2 x. ( 0 + 1 ) ) _C ( 0 + 1 ) ) = ( ( ( 2 x. 0 ) _C 0 ) x. ( 2 x. ( ( ( 2 x. 0 ) + 1 ) / ( 0 + 1 ) ) ) )
73	33, 28	nn0mulcli 9613	. . . . . . . . . . . . . . . 16 |- ( 2 x. 0 ) e. NN0
74		bcn0 11216	. . . . . . . . . . . . . . . 16 |- ( ( 2 x. 0 ) e. NN0 -> ( ( 2 x. 0 ) _C 0 ) = 1 )
75	73, 74	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( ( 2 x. 0 ) _C 0 ) = 1
76		2t0e0 9476	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 x. 0 ) = 0
77	76	oveq1i 6098	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 x. 0 ) + 1 ) = ( 0 + 1 )
78	77, 68	eqtr4i 2262	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 x. 0 ) + 1 ) = 1
79	68	eqcomi 2242	. . . . . . . . . . . . . . . . . . 19 |- ( 0 + 1 ) = 1
80	78, 79	oveq12i 6100	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 2 x. 0 ) + 1 ) / ( 0 + 1 ) ) = ( 1 / 1 )
81		1div1e1 9043	. . . . . . . . . . . . . . . . . 18 |- ( 1 / 1 ) = 1
82	80, 81	eqtri 2259	. . . . . . . . . . . . . . . . 17 |- ( ( ( 2 x. 0 ) + 1 ) / ( 0 + 1 ) ) = 1
83	82	oveq2i 6099	. . . . . . . . . . . . . . . 16 |- ( 2 x. ( ( ( 2 x. 0 ) + 1 ) / ( 0 + 1 ) ) ) = ( 2 x. 1 )
84		2t1e2 9468	. . . . . . . . . . . . . . . 16 |- ( 2 x. 1 ) = 2
85	83, 84	eqtri 2259	. . . . . . . . . . . . . . 15 |- ( 2 x. ( ( ( 2 x. 0 ) + 1 ) / ( 0 + 1 ) ) ) = 2
86	75, 85	oveq12i 6100	. . . . . . . . . . . . . 14 |- ( ( ( 2 x. 0 ) _C 0 ) x. ( 2 x. ( ( ( 2 x. 0 ) + 1 ) / ( 0 + 1 ) ) ) ) = ( 1 x. 2 )
87	32	mullidi 8336	. . . . . . . . . . . . . 14 |- ( 1 x. 2 ) = 2
88	86, 87	eqtri 2259	. . . . . . . . . . . . 13 |- ( ( ( 2 x. 0 ) _C 0 ) x. ( 2 x. ( ( ( 2 x. 0 ) + 1 ) / ( 0 + 1 ) ) ) ) = 2
89	70, 72, 88	3eqtri 2263	. . . . . . . . . . . 12 |- ( ( 2 x. 1 ) _C 1 ) = 2
90	84	oveq1i 6098	. . . . . . . . . . . . . . . 16 |- ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
91	90, 57	eqtr4i 2262	. . . . . . . . . . . . . . 15 |- ( ( 2 x. 1 ) + 1 ) = 3
92	62	eqcomi 2242	. . . . . . . . . . . . . . 15 |- ( 1 + 1 ) = 2
93	91, 92	oveq12i 6100	. . . . . . . . . . . . . 14 |- ( ( ( 2 x. 1 ) + 1 ) / ( 1 + 1 ) ) = ( 3 / 2 )
94	93	oveq2i 6099	. . . . . . . . . . . . 13 |- ( 2 x. ( ( ( 2 x. 1 ) + 1 ) / ( 1 + 1 ) ) ) = ( 2 x. ( 3 / 2 ) )
95		3cn 9389	. . . . . . . . . . . . . 14 |- 3 e. CC
96		2ap0 9407	. . . . . . . . . . . . . 14 |- 2 # 0
97	95, 32, 96	divcanap2i 9094	. . . . . . . . . . . . 13 |- ( 2 x. ( 3 / 2 ) ) = 3
98	94, 97	eqtri 2259	. . . . . . . . . . . 12 |- ( 2 x. ( ( ( 2 x. 1 ) + 1 ) / ( 1 + 1 ) ) ) = 3
99	89, 98	oveq12i 6100	. . . . . . . . . . 11 |- ( ( ( 2 x. 1 ) _C 1 ) x. ( 2 x. ( ( ( 2 x. 1 ) + 1 ) / ( 1 + 1 ) ) ) ) = ( 2 x. 3 )
100	99, 42	eqtri 2259	. . . . . . . . . 10 |- ( ( ( 2 x. 1 ) _C 1 ) x. ( 2 x. ( ( ( 2 x. 1 ) + 1 ) / ( 1 + 1 ) ) ) ) = 6
101	64, 67, 100	3eqtri 2263	. . . . . . . . 9 |- ( ( 2 x. 2 ) _C 2 ) = 6
102		2t2e4 9469	. . . . . . . . . . . . . 14 |- ( 2 x. 2 ) = 4
103	102	oveq1i 6098	. . . . . . . . . . . . 13 |- ( ( 2 x. 2 ) + 1 ) = ( 4 + 1 )
104		df-5 9376	. . . . . . . . . . . . 13 |- 5 = ( 4 + 1 )
105	103, 104	eqtr4i 2262	. . . . . . . . . . . 12 |- ( ( 2 x. 2 ) + 1 ) = 5
106	57	eqcomi 2242	. . . . . . . . . . . 12 |- ( 2 + 1 ) = 3
107	105, 106	oveq12i 6100	. . . . . . . . . . 11 |- ( ( ( 2 x. 2 ) + 1 ) / ( 2 + 1 ) ) = ( 5 / 3 )
108	107	oveq2i 6099	. . . . . . . . . 10 |- ( 2 x. ( ( ( 2 x. 2 ) + 1 ) / ( 2 + 1 ) ) ) = ( 2 x. ( 5 / 3 ) )
109		5cn 9394	. . . . . . . . . . 11 |- 5 e. CC
110		3ap0 9410	. . . . . . . . . . 11 |- 3 # 0
111	32, 109, 95, 110	divassapi 9107	. . . . . . . . . 10 |- ( ( 2 x. 5 ) / 3 ) = ( 2 x. ( 5 / 3 ) )
112	108, 111	eqtr4i 2262	. . . . . . . . 9 |- ( 2 x. ( ( ( 2 x. 2 ) + 1 ) / ( 2 + 1 ) ) ) = ( ( 2 x. 5 ) / 3 )
113	101, 112	oveq12i 6100	. . . . . . . 8 |- ( ( ( 2 x. 2 ) _C 2 ) x. ( 2 x. ( ( ( 2 x. 2 ) + 1 ) / ( 2 + 1 ) ) ) ) = ( 6 x. ( ( 2 x. 5 ) / 3 ) )
114	61, 113	eqtri 2259	. . . . . . 7 |- ( ( 2 x. ( 2 + 1 ) ) _C ( 2 + 1 ) ) = ( 6 x. ( ( 2 x. 5 ) / 3 ) )
115		6cn 9396	. . . . . . . . 9 |- 6 e. CC
116		2nn 9478	. . . . . . . . . . 11 |- 2 e. NN
117		5nn 9481	. . . . . . . . . . 11 |- 5 e. NN
118	116, 117	nnmulcli 9336	. . . . . . . . . 10 |- ( 2 x. 5 ) e. NN
119	118	nncni 9324	. . . . . . . . 9 |- ( 2 x. 5 ) e. CC
120	95, 110	pm3.2i 272	. . . . . . . . 9 |- ( 3 e. CC /\ 3 # 0 )
121		div12ap 9033	. . . . . . . . 9 |- ( ( 6 e. CC /\ ( 2 x. 5 ) e. CC /\ ( 3 e. CC /\ 3 # 0 ) ) -> ( 6 x. ( ( 2 x. 5 ) / 3 ) ) = ( ( 2 x. 5 ) x. ( 6 / 3 ) ) )
122	115, 119, 120, 121	mp3an 1378	. . . . . . . 8 |- ( 6 x. ( ( 2 x. 5 ) / 3 ) ) = ( ( 2 x. 5 ) x. ( 6 / 3 ) )
123		5t2e10 9893	. . . . . . . . . 10 |- ( 5 x. 2 ) = ; 1 0
124	109, 32, 123	mulcomli 8340	. . . . . . . . 9 |- ( 2 x. 5 ) = ; 1 0
125		3t2e6 9471	. . . . . . . . . 10 |- ( 3 x. 2 ) = 6
126	115, 95, 32, 110	divmulapi 9105	. . . . . . . . . 10 |- ( ( 6 / 3 ) = 2 <-> ( 3 x. 2 ) = 6 )
127	125, 126	mpbir 146	. . . . . . . . 9 |- ( 6 / 3 ) = 2
128	124, 127	oveq12i 6100	. . . . . . . 8 |- ( ( 2 x. 5 ) x. ( 6 / 3 ) ) = (; 1 0 x. 2 )
129	122, 128	eqtri 2259	. . . . . . 7 |- ( 6 x. ( ( 2 x. 5 ) / 3 ) ) = (; 1 0 x. 2 )
130	59, 114, 129	3eqtri 2263	. . . . . 6 |- ( ( 2 x. 3 ) _C 3 ) = (; 1 0 x. 2 )
131	42	oveq1i 6098	. . . . . . . . 9 |- ( ( 2 x. 3 ) + 1 ) = ( 6 + 1 )
132		df-7 9378	. . . . . . . . 9 |- 7 = ( 6 + 1 )
133	131, 132	eqtr4i 2262	. . . . . . . 8 |- ( ( 2 x. 3 ) + 1 ) = 7
134		3p1e4 9450	. . . . . . . 8 |- ( 3 + 1 ) = 4
135	133, 134	oveq12i 6100	. . . . . . 7 |- ( ( ( 2 x. 3 ) + 1 ) / ( 3 + 1 ) ) = ( 7 / 4 )
136	135	oveq2i 6099	. . . . . 6 |- ( 2 x. ( ( ( 2 x. 3 ) + 1 ) / ( 3 + 1 ) ) ) = ( 2 x. ( 7 / 4 ) )
137	130, 136	oveq12i 6100	. . . . 5 |- ( ( ( 2 x. 3 ) _C 3 ) x. ( 2 x. ( ( ( 2 x. 3 ) + 1 ) / ( 3 + 1 ) ) ) ) = ( (; 1 0 x. 2 ) x. ( 2 x. ( 7 / 4 ) ) )
138	54, 56, 137	3eqtri 2263	. . . 4 |- ( ( 2 x. 4 ) _C 4 ) = ( (; 1 0 x. 2 ) x. ( 2 x. ( 7 / 4 ) ) )
139		10nn 9808	. . . . . . 7 |- ; 1 0 e. NN
140	139	nncni 9324	. . . . . 6 |- ; 1 0 e. CC
141		7cn 9398	. . . . . . . 8 |- 7 e. CC
142	141, 46, 47	divclapi 9093	. . . . . . 7 |- ( 7 / 4 ) e. CC
143	32, 142	mulcli 8338	. . . . . 6 |- ( 2 x. ( 7 / 4 ) ) e. CC
144	140, 32, 143	mulassi 8342	. . . . 5 |- ( (; 1 0 x. 2 ) x. ( 2 x. ( 7 / 4 ) ) ) = (; 1 0 x. ( 2 x. ( 2 x. ( 7 / 4 ) ) ) )
145	102	oveq1i 6098	. . . . . . 7 |- ( ( 2 x. 2 ) x. ( 7 / 4 ) ) = ( 4 x. ( 7 / 4 ) )
146	32, 32, 142	mulassi 8342	. . . . . . 7 |- ( ( 2 x. 2 ) x. ( 7 / 4 ) ) = ( 2 x. ( 2 x. ( 7 / 4 ) ) )
147	141, 46, 47	divcanap2i 9094	. . . . . . 7 |- ( 4 x. ( 7 / 4 ) ) = 7
148	145, 146, 147	3eqtr3i 2267	. . . . . 6 |- ( 2 x. ( 2 x. ( 7 / 4 ) ) ) = 7
149	148	oveq2i 6099	. . . . 5 |- (; 1 0 x. ( 2 x. ( 2 x. ( 7 / 4 ) ) ) ) = (; 1 0 x. 7 )
150	144, 149	eqtri 2259	. . . 4 |- ( (; 1 0 x. 2 ) x. ( 2 x. ( 7 / 4 ) ) ) = (; 1 0 x. 7 )
151	26	dec0u 9814	. . . 4 |- (; 1 0 x. 7 ) = ; 7 0
152	138, 150, 151	3eqtri 2263	. . 3 |- ( ( 2 x. 4 ) _C 4 ) = ; 7 0
153	31, 51, 152	3brtr4i 4161	. 2 |- ( ( 4 ^ 4 ) / 4 ) < ( ( 2 x. 4 ) _C 4 )
154		eluz4nn 9986	. . 3 |- ( n e. ( ZZ>= ` 4 ) -> n e. NN )
155		4nn 9480	. . . . . . . . . 10 |- 4 e. NN
156		nnnn0 9582	. . . . . . . . . 10 |- ( n e. NN -> n e. NN0 )
157		nnexpcl 11011	. . . . . . . . . 10 |- ( ( 4 e. NN /\ n e. NN0 ) -> ( 4 ^ n ) e. NN )
158	155, 156, 157	sylancr 418	. . . . . . . . 9 |- ( n e. NN -> ( 4 ^ n ) e. NN )
159	158	nnrpd 10113	. . . . . . . 8 |- ( n e. NN -> ( 4 ^ n ) e. RR+ )
160		nnrp 10082	. . . . . . . 8 |- ( n e. NN -> n e. RR+ )
161	159, 160	rpdivcld 10133	. . . . . . 7 |- ( n e. NN -> ( ( 4 ^ n ) / n ) e. RR+ )
162	161	rpred 10115	. . . . . 6 |- ( n e. NN -> ( ( 4 ^ n ) / n ) e. RR )
163		nnmulcl 9335	. . . . . . . . . 10 |- ( ( 2 e. NN /\ n e. NN ) -> ( 2 x. n ) e. NN )
164	116, 163	mpan 428	. . . . . . . . 9 |- ( n e. NN -> ( 2 x. n ) e. NN )
165	164	nnnn0d 9632	. . . . . . . 8 |- ( n e. NN -> ( 2 x. n ) e. NN0 )
166		nnz 9675	. . . . . . . 8 |- ( n e. NN -> n e. ZZ )
167		bccl 11228	. . . . . . . 8 |- ( ( ( 2 x. n ) e. NN0 /\ n e. ZZ ) -> ( ( 2 x. n ) _C n ) e. NN0 )
168	165, 166, 167	syl2anc 415	. . . . . . 7 |- ( n e. NN -> ( ( 2 x. n ) _C n ) e. NN0 )
169	168	nn0red 9633	. . . . . 6 |- ( n e. NN -> ( ( 2 x. n ) _C n ) e. RR )
170		2rp 10077	. . . . . . 7 |- 2 e. RR+
171	164	peano2nnd 9329	. . . . . . . . 9 |- ( n e. NN -> ( ( 2 x. n ) + 1 ) e. NN )
172	171	nnrpd 10113	. . . . . . . 8 |- ( n e. NN -> ( ( 2 x. n ) + 1 ) e. RR+ )
173		peano2nn 9326	. . . . . . . . 9 |- ( n e. NN -> ( n + 1 ) e. NN )
174	173	nnrpd 10113	. . . . . . . 8 |- ( n e. NN -> ( n + 1 ) e. RR+ )
175	172, 174	rpdivcld 10133	. . . . . . 7 |- ( n e. NN -> ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) e. RR+ )
176		rpmulcl 10097	. . . . . . 7 |- ( ( 2 e. RR+ /\ ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) e. RR+ ) -> ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) e. RR+ )
177	170, 175, 176	sylancr 418	. . . . . 6 |- ( n e. NN -> ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) e. RR+ )
178	162, 169, 177	ltmul1d 10157	. . . . 5 |- ( n e. NN -> ( ( ( 4 ^ n ) / n ) < ( ( 2 x. n ) _C n ) <-> ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) < ( ( ( 2 x. n ) _C n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) ) )
179		bcp1ctr 16318	. . . . . . 7 |- ( n e. NN0 -> ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) = ( ( ( 2 x. n ) _C n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) )
180	156, 179	syl 14	. . . . . 6 |- ( n e. NN -> ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) = ( ( ( 2 x. n ) _C n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) )
181	180	breq2d 4143	. . . . 5 |- ( n e. NN -> ( ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) < ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) <-> ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) < ( ( ( 2 x. n ) _C n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) ) )
182	178, 181	bitr4d 191	. . . 4 |- ( n e. NN -> ( ( ( 4 ^ n ) / n ) < ( ( 2 x. n ) _C n ) <-> ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) < ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) ) )
183		2re 9384	. . . . . . . 8 |- 2 e. RR
184	183	a1i 9	. . . . . . 7 |- ( n e. NN -> 2 e. RR )
185	172, 160	rpdivcld 10133	. . . . . . . 8 |- ( n e. NN -> ( ( ( 2 x. n ) + 1 ) / n ) e. RR+ )
186	185	rpred 10115	. . . . . . 7 |- ( n e. NN -> ( ( ( 2 x. n ) + 1 ) / n ) e. RR )
187		nnmulcl 9335	. . . . . . . . . 10 |- ( ( ( 4 ^ n ) e. NN /\ 2 e. NN ) -> ( ( 4 ^ n ) x. 2 ) e. NN )
188	158, 116, 187	sylancl 417	. . . . . . . . 9 |- ( n e. NN -> ( ( 4 ^ n ) x. 2 ) e. NN )
189	188	nnrpd 10113	. . . . . . . 8 |- ( n e. NN -> ( ( 4 ^ n ) x. 2 ) e. RR+ )
190	189, 174	rpdivcld 10133	. . . . . . 7 |- ( n e. NN -> ( ( ( 4 ^ n ) x. 2 ) / ( n + 1 ) ) e. RR+ )
191	160	rpreccld 10126	. . . . . . . . 9 |- ( n e. NN -> ( 1 / n ) e. RR+ )
192		ltaddrp 10110	. . . . . . . . 9 |- ( ( 2 e. RR /\ ( 1 / n ) e. RR+ ) -> 2 < ( 2 + ( 1 / n ) ) )
193	183, 191, 192	sylancr 418	. . . . . . . 8 |- ( n e. NN -> 2 < ( 2 + ( 1 / n ) ) )
194	164	nncnd 9328	. . . . . . . . . 10 |- ( n e. NN -> ( 2 x. n ) e. CC )
195		1cnd 8349	. . . . . . . . . 10 |- ( n e. NN -> 1 e. CC )
196		nncn 9322	. . . . . . . . . 10 |- ( n e. NN -> n e. CC )
197		nnap0 9343	. . . . . . . . . 10 |- ( n e. NN -> n # 0 )
198	194, 195, 196, 197	divdirapd 9168	. . . . . . . . 9 |- ( n e. NN -> ( ( ( 2 x. n ) + 1 ) / n ) = ( ( ( 2 x. n ) / n ) + ( 1 / n ) ) )
199		2cnd 9387	. . . . . . . . . . 11 |- ( n e. NN -> 2 e. CC )
200	199, 196, 197	divcanap4d 9135	. . . . . . . . . 10 |- ( n e. NN -> ( ( 2 x. n ) / n ) = 2 )
201	200	oveq1d 6103	. . . . . . . . 9 |- ( n e. NN -> ( ( ( 2 x. n ) / n ) + ( 1 / n ) ) = ( 2 + ( 1 / n ) ) )
202	198, 201	eqtr2d 2272	. . . . . . . 8 |- ( n e. NN -> ( 2 + ( 1 / n ) ) = ( ( ( 2 x. n ) + 1 ) / n ) )
203	193, 202	breqtrd 4157	. . . . . . 7 |- ( n e. NN -> 2 < ( ( ( 2 x. n ) + 1 ) / n ) )
204	184, 186, 190, 203	ltmul2dd 10172	. . . . . 6 |- ( n e. NN -> ( ( ( ( 4 ^ n ) x. 2 ) / ( n + 1 ) ) x. 2 ) < ( ( ( ( 4 ^ n ) x. 2 ) / ( n + 1 ) ) x. ( ( ( 2 x. n ) + 1 ) / n ) ) )
205		expp1 11005	. . . . . . . . . 10 |- ( ( 4 e. CC /\ n e. NN0 ) -> ( 4 ^ ( n + 1 ) ) = ( ( 4 ^ n ) x. 4 ) )
206	46, 156, 205	sylancr 418	. . . . . . . . 9 |- ( n e. NN -> ( 4 ^ ( n + 1 ) ) = ( ( 4 ^ n ) x. 4 ) )
207	158	nncnd 9328	. . . . . . . . . . 11 |- ( n e. NN -> ( 4 ^ n ) e. CC )
208	207, 199, 199	mulassd 8356	. . . . . . . . . 10 |- ( n e. NN -> ( ( ( 4 ^ n ) x. 2 ) x. 2 ) = ( ( 4 ^ n ) x. ( 2 x. 2 ) ) )
209	102	oveq2i 6099	. . . . . . . . . 10 |- ( ( 4 ^ n ) x. ( 2 x. 2 ) ) = ( ( 4 ^ n ) x. 4 )
210	208, 209	eqtrdi 2287	. . . . . . . . 9 |- ( n e. NN -> ( ( ( 4 ^ n ) x. 2 ) x. 2 ) = ( ( 4 ^ n ) x. 4 ) )
211	206, 210	eqtr4d 2274	. . . . . . . 8 |- ( n e. NN -> ( 4 ^ ( n + 1 ) ) = ( ( ( 4 ^ n ) x. 2 ) x. 2 ) )
212	211	oveq1d 6103	. . . . . . 7 |- ( n e. NN -> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) = ( ( ( ( 4 ^ n ) x. 2 ) x. 2 ) / ( n + 1 ) ) )
213	188	nncnd 9328	. . . . . . . 8 |- ( n e. NN -> ( ( 4 ^ n ) x. 2 ) e. CC )
214	173	nncnd 9328	. . . . . . . 8 |- ( n e. NN -> ( n + 1 ) e. CC )
215	173	nnap0d 9360	. . . . . . . 8 |- ( n e. NN -> ( n + 1 ) # 0 )
216	213, 199, 214, 215	div23apd 9167	. . . . . . 7 |- ( n e. NN -> ( ( ( ( 4 ^ n ) x. 2 ) x. 2 ) / ( n + 1 ) ) = ( ( ( ( 4 ^ n ) x. 2 ) / ( n + 1 ) ) x. 2 ) )
217	212, 216	eqtrd 2271	. . . . . 6 |- ( n e. NN -> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) = ( ( ( ( 4 ^ n ) x. 2 ) / ( n + 1 ) ) x. 2 ) )
218	207, 199, 196, 197	div23apd 9167	. . . . . . . 8 |- ( n e. NN -> ( ( ( 4 ^ n ) x. 2 ) / n ) = ( ( ( 4 ^ n ) / n ) x. 2 ) )
219	218	oveq1d 6103	. . . . . . 7 |- ( n e. NN -> ( ( ( ( 4 ^ n ) x. 2 ) / n ) x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) = ( ( ( ( 4 ^ n ) / n ) x. 2 ) x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) )
220	171	nncnd 9328	. . . . . . . 8 |- ( n e. NN -> ( ( 2 x. n ) + 1 ) e. CC )
221	196, 197	jca 306	. . . . . . . 8 |- ( n e. NN -> ( n e. CC /\ n # 0 ) )
222	214, 215	jca 306	. . . . . . . 8 |- ( n e. NN -> ( ( n + 1 ) e. CC /\ ( n + 1 ) # 0 ) )
223		divmul24ap 9055	. . . . . . . 8 |- ( ( ( ( ( 4 ^ n ) x. 2 ) e. CC /\ ( ( 2 x. n ) + 1 ) e. CC ) /\ ( ( n e. CC /\ n # 0 ) /\ ( ( n + 1 ) e. CC /\ ( n + 1 ) # 0 ) ) ) -> ( ( ( ( 4 ^ n ) x. 2 ) / n ) x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) = ( ( ( ( 4 ^ n ) x. 2 ) / ( n + 1 ) ) x. ( ( ( 2 x. n ) + 1 ) / n ) ) )
224	213, 220, 221, 222, 223	syl22anc 1279	. . . . . . 7 |- ( n e. NN -> ( ( ( ( 4 ^ n ) x. 2 ) / n ) x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) = ( ( ( ( 4 ^ n ) x. 2 ) / ( n + 1 ) ) x. ( ( ( 2 x. n ) + 1 ) / n ) ) )
225	161	rpcnd 10117	. . . . . . . 8 |- ( n e. NN -> ( ( 4 ^ n ) / n ) e. CC )
226	175	rpcnd 10117	. . . . . . . 8 |- ( n e. NN -> ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) e. CC )
227	225, 199, 226	mulassd 8356	. . . . . . 7 |- ( n e. NN -> ( ( ( ( 4 ^ n ) / n ) x. 2 ) x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) = ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) )
228	219, 224, 227	3eqtr3rd 2280	. . . . . 6 |- ( n e. NN -> ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) = ( ( ( ( 4 ^ n ) x. 2 ) / ( n + 1 ) ) x. ( ( ( 2 x. n ) + 1 ) / n ) ) )
229	204, 217, 228	3brtr4d 4163	. . . . 5 |- ( n e. NN -> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) < ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) )
230	173	nnnn0d 9632	. . . . . . . . . 10 |- ( n e. NN -> ( n + 1 ) e. NN0 )
231		nnexpcl 11011	. . . . . . . . . 10 |- ( ( 4 e. NN /\ ( n + 1 ) e. NN0 ) -> ( 4 ^ ( n + 1 ) ) e. NN )
232	155, 230, 231	sylancr 418	. . . . . . . . 9 |- ( n e. NN -> ( 4 ^ ( n + 1 ) ) e. NN )
233	232	nnrpd 10113	. . . . . . . 8 |- ( n e. NN -> ( 4 ^ ( n + 1 ) ) e. RR+ )
234	233, 174	rpdivcld 10133	. . . . . . 7 |- ( n e. NN -> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) e. RR+ )
235	234	rpred 10115	. . . . . 6 |- ( n e. NN -> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) e. RR )
236	177	rpred 10115	. . . . . . 7 |- ( n e. NN -> ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) e. RR )
237	162, 236	remulcld 8363	. . . . . 6 |- ( n e. NN -> ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) e. RR )
238		nn0mulcl 9611	. . . . . . . . 9 |- ( ( 2 e. NN0 /\ ( n + 1 ) e. NN0 ) -> ( 2 x. ( n + 1 ) ) e. NN0 )
239	33, 230, 238	sylancr 418	. . . . . . . 8 |- ( n e. NN -> ( 2 x. ( n + 1 ) ) e. NN0 )
240	173	nnzd 9779	. . . . . . . 8 |- ( n e. NN -> ( n + 1 ) e. ZZ )
241		bccl 11228	. . . . . . . 8 |- ( ( ( 2 x. ( n + 1 ) ) e. NN0 /\ ( n + 1 ) e. ZZ ) -> ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) e. NN0 )
242	239, 240, 241	syl2anc 415	. . . . . . 7 |- ( n e. NN -> ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) e. NN0 )
243	242	nn0red 9633	. . . . . 6 |- ( n e. NN -> ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) e. RR )
244		lttr 8406	. . . . . 6 |- ( ( ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) e. RR /\ ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) e. RR /\ ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) e. RR ) -> ( ( ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) < ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) /\ ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) < ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) ) -> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) < ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) ) )
245	235, 237, 243, 244	syl3anc 1278	. . . . 5 |- ( n e. NN -> ( ( ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) < ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) /\ ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) < ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) ) -> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) < ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) ) )
246	229, 245	mpand 433	. . . 4 |- ( n e. NN -> ( ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) < ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) -> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) < ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) ) )
247	182, 246	sylbid 150	. . 3 |- ( n e. NN -> ( ( ( 4 ^ n ) / n ) < ( ( 2 x. n ) _C n ) -> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) < ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) ) )
248	154, 247	syl 14	. 2 |- ( n e. ( ZZ>= ` 4 ) -> ( ( ( 4 ^ n ) / n ) < ( ( 2 x. n ) _C n ) -> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) < ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) ) )
249	6, 12, 18, 24, 153, 248	uzind4i 10009	1 |- ( N e. ( ZZ>= ` 4 ) -> ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209   class class class wbr 4131   ` cfv 5380  (class class class)co 6088   CCcc 8184   RRcr 8185   0cc0 8186   1c1 8187   + caddc 8189   x. cmul 8191   < clt 8367   - cmin 8505   # cap 8918   / cdiv 9011   NNcn 9314   2c2 9365   3c3 9366   4c4 9367   5c5 9368   6c6 9369   7c7 9370   NN0cn0 9575   ZZcz 9656  ;cdc 9789   ZZ>=cuz 9938   RR+crp 10072   ^cexp 10997   _C cbc 11208

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 4248  ax-sep 4251  ax-nul 4261  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-iinf 4737  ax-cnex 8277  ax-resscn 8278  ax-1cn 8279  ax-1re 8280  ax-icn 8281  ax-addcl 8282  ax-addrcl 8283  ax-mulcl 8284  ax-mulrcl 8285  ax-addcom 8286  ax-mulcom 8287  ax-addass 8288  ax-mulass 8289  ax-distr 8290  ax-i2m1 8291  ax-0lt1 8292  ax-1rid 8293  ax-0id 8294  ax-rnegex 8295  ax-precex 8296  ax-cnre 8297  ax-pre-ltirr 8298  ax-pre-ltwlin 8299  ax-pre-lttrn 8300  ax-pre-apti 8301  ax-pre-ltadd 8302  ax-pre-mulgt0 8303  ax-pre-mulext 8304

This proof depends on definitions:  df-bi 117  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 4132  df-opab 4194  df-mpt 4195  df-tr 4232  df-id 4440  df-po 4443  df-iso 4444  df-iord 4513  df-on 4515  df-ilim 4516  df-suc 4518  df-iom 4740  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-f1 5385  df-fo 5386  df-f1o 5387  df-fv 5388  df-riota 6041  df-ov 6091  df-oprab 6092  df-mpo 6093  df-1st 6378  df-2nd 6379  df-recs 6580  df-frec 6666  df-pnf 8369  df-mnf 8370  df-xr 8371  df-ltxr 8372  df-le 8373  df-sub 8507  df-neg 8508  df-reap 8912  df-ap 8919  df-div 9012  df-inn 9315  df-2 9373  df-3 9374  df-4 9375  df-5 9376  df-6 9377  df-7 9378  df-8 9379  df-9 9380  df-n0 9576  df-z 9657  df-dec 9790  df-uz 9939  df-q 10037  df-rp 10073  df-fz 10430  df-seqfrec 10907  df-exp 10998  df-fac 11187  df-bc 11209

This theorem is used by:  bposlem6  16328