Theorem bclbnd 16127

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 6093	. . . 4 |- ( x = 4 -> ( 4 ^ x ) = ( 4 ^ 4 ) )
2		id 19	. . . 4 |- ( x = 4 -> x = 4 )
3	1, 2	oveq12d 6103	. . 3 |- ( x = 4 -> ( ( 4 ^ x ) / x ) = ( ( 4 ^ 4 ) / 4 ) )
4		oveq2 6093	. . . 4 |- ( x = 4 -> ( 2 x. x ) = ( 2 x. 4 ) )
5	4, 2	oveq12d 6103	. . 3 |- ( x = 4 -> ( ( 2 x. x ) _C x ) = ( ( 2 x. 4 ) _C 4 ) )
6	3, 5	breq12d 4143	. 2 |- ( x = 4 -> ( ( ( 4 ^ x ) / x ) < ( ( 2 x. x ) _C x ) <-> ( ( 4 ^ 4 ) / 4 ) < ( ( 2 x. 4 ) _C 4 ) ) )
7		oveq2 6093	. . . 4 |- ( x = n -> ( 4 ^ x ) = ( 4 ^ n ) )
8		id 19	. . . 4 |- ( x = n -> x = n )
9	7, 8	oveq12d 6103	. . 3 |- ( x = n -> ( ( 4 ^ x ) / x ) = ( ( 4 ^ n ) / n ) )
10		oveq2 6093	. . . 4 |- ( x = n -> ( 2 x. x ) = ( 2 x. n ) )
11	10, 8	oveq12d 6103	. . 3 |- ( x = n -> ( ( 2 x. x ) _C x ) = ( ( 2 x. n ) _C n ) )
12	9, 11	breq12d 4143	. 2 |- ( x = n -> ( ( ( 4 ^ x ) / x ) < ( ( 2 x. x ) _C x ) <-> ( ( 4 ^ n ) / n ) < ( ( 2 x. n ) _C n ) ) )
13		oveq2 6093	. . . 4 |- ( x = ( n + 1 ) -> ( 4 ^ x ) = ( 4 ^ ( n + 1 ) ) )
14		id 19	. . . 4 |- ( x = ( n + 1 ) -> x = ( n + 1 ) )
15	13, 14	oveq12d 6103	. . 3 |- ( x = ( n + 1 ) -> ( ( 4 ^ x ) / x ) = ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) )
16		oveq2 6093	. . . 4 |- ( x = ( n + 1 ) -> ( 2 x. x ) = ( 2 x. ( n + 1 ) ) )
17	16, 14	oveq12d 6103	. . 3 |- ( x = ( n + 1 ) -> ( ( 2 x. x ) _C x ) = ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) )
18	15, 17	breq12d 4143	. 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 6093	. . . 4 |- ( x = N -> ( 4 ^ x ) = ( 4 ^ N ) )
20		id 19	. . . 4 |- ( x = N -> x = N )
21	19, 20	oveq12d 6103	. . 3 |- ( x = N -> ( ( 4 ^ x ) / x ) = ( ( 4 ^ N ) / N ) )
22		oveq2 6093	. . . 4 |- ( x = N -> ( 2 x. x ) = ( 2 x. N ) )
23	22, 20	oveq12d 6103	. . 3 |- ( x = N -> ( ( 2 x. x ) _C x ) = ( ( 2 x. N ) _C N ) )
24	21, 23	breq12d 4143	. 2 |- ( x = N -> ( ( ( 4 ^ x ) / x ) < ( ( 2 x. x ) _C x ) <-> ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) ) )
25		6nn0 9586	. . . 4 |- 6 e. NN0
26		7nn0 9587	. . . 4 |- 7 e. NN0
27		4nn0 9584	. . . 4 |- 4 e. NN0
28		0nn0 9580	. . . 4 |- 0 e. NN0
29		4lt10 9914	. . . 4 |- 4 < ; 1 0
30		6lt7 9491	. . . 4 |- 6 < 7
31	25, 26, 27, 28, 29, 30	decltc 9807	. . 3 |- ; 6 4 < ; 7 0
32		2cn 9376	. . . . . 6 |- 2 e. CC
33		2nn0 9582	. . . . . 6 |- 2 e. NN0
34		3nn0 9583	. . . . . 6 |- 3 e. NN0
35		expmul 11023	. . . . . 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 11074	. . . . . . 7 |- ( 2 ^ 2 ) = 4
38	37	eqcomi 2242	. . . . . 6 |- 4 = ( 2 ^ 2 )
39		4m1e3 9426	. . . . . 6 |- ( 4 - 1 ) = 3
40	38, 39	oveq12i 6097	. . . . 5 |- ( 4 ^ ( 4 - 1 ) ) = ( ( 2 ^ 2 ) ^ 3 )
41	36, 40	eqtr4i 2262	. . . 4 |- ( 2 ^ ( 2 x. 3 ) ) = ( 4 ^ ( 4 - 1 ) )
42		2t3e6 9463	. . . . . 6 |- ( 2 x. 3 ) = 6
43	42	oveq2i 6096	. . . . 5 |- ( 2 ^ ( 2 x. 3 ) ) = ( 2 ^ 6 )
44		2exp6 13214	. . . . 5 |- ( 2 ^ 6 ) = ; 6 4
45	43, 44	eqtri 2259	. . . 4 |- ( 2 ^ ( 2 x. 3 ) ) = ; 6 4
46		4cn 9383	. . . . 5 |- 4 e. CC
47		4ap0 9404	. . . . 5 |- 4 # 0
48		4z 9676	. . . . 5 |- 4 e. ZZ
49		expm1ap 11028	. . . . 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 9366	. . . . . . 7 |- 4 = ( 3 + 1 )
53	52	oveq2i 6096	. . . . . 6 |- ( 2 x. 4 ) = ( 2 x. ( 3 + 1 ) )
54	53, 52	oveq12i 6097	. . . . 5 |- ( ( 2 x. 4 ) _C 4 ) = ( ( 2 x. ( 3 + 1 ) ) _C ( 3 + 1 ) )
55		bcp1ctr 16126	. . . . . 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 9365	. . . . . . . . 9 |- 3 = ( 2 + 1 )
58	57	oveq2i 6096	. . . . . . . 8 |- ( 2 x. 3 ) = ( 2 x. ( 2 + 1 ) )
59	58, 57	oveq12i 6097	. . . . . . 7 |- ( ( 2 x. 3 ) _C 3 ) = ( ( 2 x. ( 2 + 1 ) ) _C ( 2 + 1 ) )
60		bcp1ctr 16126	. . . . . . . . 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 9364	. . . . . . . . . . . 12 |- 2 = ( 1 + 1 )
63	62	oveq2i 6096	. . . . . . . . . . 11 |- ( 2 x. 2 ) = ( 2 x. ( 1 + 1 ) )
64	63, 62	oveq12i 6097	. . . . . . . . . 10 |- ( ( 2 x. 2 ) _C 2 ) = ( ( 2 x. ( 1 + 1 ) ) _C ( 1 + 1 ) )
65		1nn0 9581	. . . . . . . . . . 11 |- 1 e. NN0
66		bcp1ctr 16126	. . . . . . . . . . 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 9820	. . . . . . . . . . . . . . 15 |- 1 = ( 0 + 1 )
69	68	oveq2i 6096	. . . . . . . . . . . . . 14 |- ( 2 x. 1 ) = ( 2 x. ( 0 + 1 ) )
70	69, 68	oveq12i 6097	. . . . . . . . . . . . 13 |- ( ( 2 x. 1 ) _C 1 ) = ( ( 2 x. ( 0 + 1 ) ) _C ( 0 + 1 ) )
71		bcp1ctr 16126	. . . . . . . . . . . . . 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 9603	. . . . . . . . . . . . . . . 16 |- ( 2 x. 0 ) e. NN0
74		bcn0 11195	. . . . . . . . . . . . . . . 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 9466	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 x. 0 ) = 0
77	76	oveq1i 6095	. . . . . . . . . . . . . . . . . . . 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 6097	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 2 x. 0 ) + 1 ) / ( 0 + 1 ) ) = ( 1 / 1 )
81		1div1e1 9035	. . . . . . . . . . . . . . . . . 18 |- ( 1 / 1 ) = 1
82	80, 81	eqtri 2259	. . . . . . . . . . . . . . . . 17 |- ( ( ( 2 x. 0 ) + 1 ) / ( 0 + 1 ) ) = 1
83	82	oveq2i 6096	. . . . . . . . . . . . . . . 16 |- ( 2 x. ( ( ( 2 x. 0 ) + 1 ) / ( 0 + 1 ) ) ) = ( 2 x. 1 )
84		2t1e2 9459	. . . . . . . . . . . . . . . 16 |- ( 2 x. 1 ) = 2
85	83, 84	eqtri 2259	. . . . . . . . . . . . . . 15 |- ( 2 x. ( ( ( 2 x. 0 ) + 1 ) / ( 0 + 1 ) ) ) = 2
86	75, 85	oveq12i 6097	. . . . . . . . . . . . . 14 |- ( ( ( 2 x. 0 ) _C 0 ) x. ( 2 x. ( ( ( 2 x. 0 ) + 1 ) / ( 0 + 1 ) ) ) ) = ( 1 x. 2 )
87	32	mullidi 8329	. . . . . . . . . . . . . 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 6095	. . . . . . . . . . . . . . . 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 6097	. . . . . . . . . . . . . 14 |- ( ( ( 2 x. 1 ) + 1 ) / ( 1 + 1 ) ) = ( 3 / 2 )
94	93	oveq2i 6096	. . . . . . . . . . . . 13 |- ( 2 x. ( ( ( 2 x. 1 ) + 1 ) / ( 1 + 1 ) ) ) = ( 2 x. ( 3 / 2 ) )
95		3cn 9380	. . . . . . . . . . . . . 14 |- 3 e. CC
96		2ap0 9398	. . . . . . . . . . . . . 14 |- 2 # 0
97	95, 32, 96	divcanap2i 9086	. . . . . . . . . . . . 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 6097	. . . . . . . . . . 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 9460	. . . . . . . . . . . . . 14 |- ( 2 x. 2 ) = 4
103	102	oveq1i 6095	. . . . . . . . . . . . 13 |- ( ( 2 x. 2 ) + 1 ) = ( 4 + 1 )
104		df-5 9367	. . . . . . . . . . . . 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 6097	. . . . . . . . . . 11 |- ( ( ( 2 x. 2 ) + 1 ) / ( 2 + 1 ) ) = ( 5 / 3 )
108	107	oveq2i 6096	. . . . . . . . . 10 |- ( 2 x. ( ( ( 2 x. 2 ) + 1 ) / ( 2 + 1 ) ) ) = ( 2 x. ( 5 / 3 ) )
109		5cn 9385	. . . . . . . . . . 11 |- 5 e. CC
110		3ap0 9401	. . . . . . . . . . 11 |- 3 # 0
111	32, 109, 95, 110	divassapi 9099	. . . . . . . . . 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 6097	. . . . . . . 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 9387	. . . . . . . . 9 |- 6 e. CC
116		2nn 9468	. . . . . . . . . . 11 |- 2 e. NN
117		5nn 9471	. . . . . . . . . . 11 |- 5 e. NN
118	116, 117	nnmulcli 9327	. . . . . . . . . 10 |- ( 2 x. 5 ) e. NN
119	118	nncni 9315	. . . . . . . . 9 |- ( 2 x. 5 ) e. CC
120	95, 110	pm3.2i 272	. . . . . . . . 9 |- ( 3 e. CC /\ 3 # 0 )
121		div12ap 9025	. . . . . . . . 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 9878	. . . . . . . . . 10 |- ( 5 x. 2 ) = ; 1 0
124	109, 32, 123	mulcomli 8333	. . . . . . . . 9 |- ( 2 x. 5 ) = ; 1 0
125		3t2e6 9462	. . . . . . . . . 10 |- ( 3 x. 2 ) = 6
126	115, 95, 32, 110	divmulapi 9097	. . . . . . . . . 10 |- ( ( 6 / 3 ) = 2 <-> ( 3 x. 2 ) = 6 )
127	125, 126	mpbir 146	. . . . . . . . 9 |- ( 6 / 3 ) = 2
128	124, 127	oveq12i 6097	. . . . . . . 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 6095	. . . . . . . . 9 |- ( ( 2 x. 3 ) + 1 ) = ( 6 + 1 )
132		df-7 9369	. . . . . . . . 9 |- 7 = ( 6 + 1 )
133	131, 132	eqtr4i 2262	. . . . . . . 8 |- ( ( 2 x. 3 ) + 1 ) = 7
134		3p1e4 9441	. . . . . . . 8 |- ( 3 + 1 ) = 4
135	133, 134	oveq12i 6097	. . . . . . 7 |- ( ( ( 2 x. 3 ) + 1 ) / ( 3 + 1 ) ) = ( 7 / 4 )
136	135	oveq2i 6096	. . . . . 6 |- ( 2 x. ( ( ( 2 x. 3 ) + 1 ) / ( 3 + 1 ) ) ) = ( 2 x. ( 7 / 4 ) )
137	130, 136	oveq12i 6097	. . . . 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 9794	. . . . . . 7 |- ; 1 0 e. NN
140	139	nncni 9315	. . . . . 6 |- ; 1 0 e. CC
141		7cn 9389	. . . . . . . 8 |- 7 e. CC
142	141, 46, 47	divclapi 9085	. . . . . . 7 |- ( 7 / 4 ) e. CC
143	32, 142	mulcli 8331	. . . . . 6 |- ( 2 x. ( 7 / 4 ) ) e. CC
144	140, 32, 143	mulassi 8335	. . . . 5 |- ( (; 1 0 x. 2 ) x. ( 2 x. ( 7 / 4 ) ) ) = (; 1 0 x. ( 2 x. ( 2 x. ( 7 / 4 ) ) ) )
145	102	oveq1i 6095	. . . . . . 7 |- ( ( 2 x. 2 ) x. ( 7 / 4 ) ) = ( 4 x. ( 7 / 4 ) )
146	32, 32, 142	mulassi 8335	. . . . . . 7 |- ( ( 2 x. 2 ) x. ( 7 / 4 ) ) = ( 2 x. ( 2 x. ( 7 / 4 ) ) )
147	141, 46, 47	divcanap2i 9086	. . . . . . 7 |- ( 4 x. ( 7 / 4 ) ) = 7
148	145, 146, 147	3eqtr3i 2267	. . . . . 6 |- ( 2 x. ( 2 x. ( 7 / 4 ) ) ) = 7
149	148	oveq2i 6096	. . . . 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 9799	. . . 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 4160	. 2 |- ( ( 4 ^ 4 ) / 4 ) < ( ( 2 x. 4 ) _C 4 )
154		eluz4nn 9971	. . 3 |- ( n e. ( ZZ>= ` 4 ) -> n e. NN )
155		4nn 9470	. . . . . . . . . 10 |- 4 e. NN
156		nnnn0 9572	. . . . . . . . . 10 |- ( n e. NN -> n e. NN0 )
157		nnexpcl 10991	. . . . . . . . . 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 10097	. . . . . . . 8 |- ( n e. NN -> ( 4 ^ n ) e. RR+ )
160		nnrp 10066	. . . . . . . 8 |- ( n e. NN -> n e. RR+ )
161	159, 160	rpdivcld 10117	. . . . . . 7 |- ( n e. NN -> ( ( 4 ^ n ) / n ) e. RR+ )
162	161	rpred 10099	. . . . . 6 |- ( n e. NN -> ( ( 4 ^ n ) / n ) e. RR )
163		nnmulcl 9326	. . . . . . . . . 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 9622	. . . . . . . 8 |- ( n e. NN -> ( 2 x. n ) e. NN0 )
166		nnz 9665	. . . . . . . 8 |- ( n e. NN -> n e. ZZ )
167		bccl 11207	. . . . . . . 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 9623	. . . . . 6 |- ( n e. NN -> ( ( 2 x. n ) _C n ) e. RR )
170		2rp 10061	. . . . . . 7 |- 2 e. RR+
171	164	peano2nnd 9320	. . . . . . . . 9 |- ( n e. NN -> ( ( 2 x. n ) + 1 ) e. NN )
172	171	nnrpd 10097	. . . . . . . 8 |- ( n e. NN -> ( ( 2 x. n ) + 1 ) e. RR+ )
173		peano2nn 9317	. . . . . . . . 9 |- ( n e. NN -> ( n + 1 ) e. NN )
174	173	nnrpd 10097	. . . . . . . 8 |- ( n e. NN -> ( n + 1 ) e. RR+ )
175	172, 174	rpdivcld 10117	. . . . . . 7 |- ( n e. NN -> ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) e. RR+ )
176		rpmulcl 10081	. . . . . . 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 10141	. . . . 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 16126	. . . . . . 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 4142	. . . . 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 9375	. . . . . . . 8 |- 2 e. RR
184	183	a1i 9	. . . . . . 7 |- ( n e. NN -> 2 e. RR )
185	172, 160	rpdivcld 10117	. . . . . . . 8 |- ( n e. NN -> ( ( ( 2 x. n ) + 1 ) / n ) e. RR+ )
186	185	rpred 10099	. . . . . . 7 |- ( n e. NN -> ( ( ( 2 x. n ) + 1 ) / n ) e. RR )
187		nnmulcl 9326	. . . . . . . . . 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 10097	. . . . . . . 8 |- ( n e. NN -> ( ( 4 ^ n ) x. 2 ) e. RR+ )
190	189, 174	rpdivcld 10117	. . . . . . 7 |- ( n e. NN -> ( ( ( 4 ^ n ) x. 2 ) / ( n + 1 ) ) e. RR+ )
191	160	rpreccld 10110	. . . . . . . . 9 |- ( n e. NN -> ( 1 / n ) e. RR+ )
192		ltaddrp 10094	. . . . . . . . 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 9319	. . . . . . . . . 10 |- ( n e. NN -> ( 2 x. n ) e. CC )
195		1cnd 8342	. . . . . . . . . 10 |- ( n e. NN -> 1 e. CC )
196		nncn 9313	. . . . . . . . . 10 |- ( n e. NN -> n e. CC )
197		nnap0 9334	. . . . . . . . . 10 |- ( n e. NN -> n # 0 )
198	194, 195, 196, 197	divdirapd 9160	. . . . . . . . 9 |- ( n e. NN -> ( ( ( 2 x. n ) + 1 ) / n ) = ( ( ( 2 x. n ) / n ) + ( 1 / n ) ) )
199		2cnd 9378	. . . . . . . . . . 11 |- ( n e. NN -> 2 e. CC )
200	199, 196, 197	divcanap4d 9127	. . . . . . . . . 10 |- ( n e. NN -> ( ( 2 x. n ) / n ) = 2 )
201	200	oveq1d 6100	. . . . . . . . 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 4156	. . . . . . 7 |- ( n e. NN -> 2 < ( ( ( 2 x. n ) + 1 ) / n ) )
204	184, 186, 190, 203	ltmul2dd 10156	. . . . . 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 10985	. . . . . . . . . 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 9319	. . . . . . . . . . 11 |- ( n e. NN -> ( 4 ^ n ) e. CC )
208	207, 199, 199	mulassd 8349	. . . . . . . . . 10 |- ( n e. NN -> ( ( ( 4 ^ n ) x. 2 ) x. 2 ) = ( ( 4 ^ n ) x. ( 2 x. 2 ) ) )
209	102	oveq2i 6096	. . . . . . . . . 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 6100	. . . . . . 7 |- ( n e. NN -> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) = ( ( ( ( 4 ^ n ) x. 2 ) x. 2 ) / ( n + 1 ) ) )
213	188	nncnd 9319	. . . . . . . 8 |- ( n e. NN -> ( ( 4 ^ n ) x. 2 ) e. CC )
214	173	nncnd 9319	. . . . . . . 8 |- ( n e. NN -> ( n + 1 ) e. CC )
215	173	nnap0d 9351	. . . . . . . 8 |- ( n e. NN -> ( n + 1 ) # 0 )
216	213, 199, 214, 215	div23apd 9159	. . . . . . 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 9159	. . . . . . . 8 |- ( n e. NN -> ( ( ( 4 ^ n ) x. 2 ) / n ) = ( ( ( 4 ^ n ) / n ) x. 2 ) )
219	218	oveq1d 6100	. . . . . . 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 9319	. . . . . . . 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 9047	. . . . . . . 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 10101	. . . . . . . 8 |- ( n e. NN -> ( ( 4 ^ n ) / n ) e. CC )
226	175	rpcnd 10101	. . . . . . . 8 |- ( n e. NN -> ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) e. CC )
227	225, 199, 226	mulassd 8349	. . . . . . 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 4162	. . . . 5 |- ( n e. NN -> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) < ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) )
230	173	nnnn0d 9622	. . . . . . . . . 10 |- ( n e. NN -> ( n + 1 ) e. NN0 )
231		nnexpcl 10991	. . . . . . . . . 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 10097	. . . . . . . 8 |- ( n e. NN -> ( 4 ^ ( n + 1 ) ) e. RR+ )
234	233, 174	rpdivcld 10117	. . . . . . 7 |- ( n e. NN -> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) e. RR+ )
235	234	rpred 10099	. . . . . 6 |- ( n e. NN -> ( ( 4 ^ ( n + 1 ) ) / ( n + 1 ) ) e. RR )
236	177	rpred 10099	. . . . . . 7 |- ( n e. NN -> ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) e. RR )
237	162, 236	remulcld 8356	. . . . . 6 |- ( n e. NN -> ( ( ( 4 ^ n ) / n ) x. ( 2 x. ( ( ( 2 x. n ) + 1 ) / ( n + 1 ) ) ) ) e. RR )
238		nn0mulcl 9601	. . . . . . . . 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 9769	. . . . . . . 8 |- ( n e. NN -> ( n + 1 ) e. ZZ )
241		bccl 11207	. . . . . . . 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 9623	. . . . . 6 |- ( n e. NN -> ( ( 2 x. ( n + 1 ) ) _C ( n + 1 ) ) e. RR )
244		lttr 8399	. . . . . 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 9994	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 4130   ` cfv 5377  (class class class)co 6085   CCcc 8177   RRcr 8178   0cc0 8179   1c1 8180   + caddc 8182   x. cmul 8184   < clt 8360   - cmin 8497   # cap 8910   / cdiv 9003   NNcn 9305   2c2 9356   3c3 9357   4c4 9358   5c5 9359   6c6 9360   7c7 9361   NN0cn0 9565   ZZcz 9646  ;cdc 9779   ZZ>=cuz 9923   RR+crp 10056   ^cexp 10977   _C cbc 11187

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 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735  ax-cnex 8270  ax-resscn 8271  ax-1cn 8272  ax-1re 8273  ax-icn 8274  ax-addcl 8275  ax-addrcl 8276  ax-mulcl 8277  ax-mulrcl 8278  ax-addcom 8279  ax-mulcom 8280  ax-addass 8281  ax-mulass 8282  ax-distr 8283  ax-i2m1 8284  ax-0lt1 8285  ax-1rid 8286  ax-0id 8287  ax-rnegex 8288  ax-precex 8289  ax-cnre 8290  ax-pre-ltirr 8291  ax-pre-ltwlin 8292  ax-pre-lttrn 8293  ax-pre-apti 8294  ax-pre-ltadd 8295  ax-pre-mulgt0 8296  ax-pre-mulext 8297

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 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-id 4438  df-po 4441  df-iso 4442  df-iord 4511  df-on 4513  df-ilim 4514  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-1st 6374  df-2nd 6375  df-recs 6576  df-frec 6662  df-pnf 8362  df-mnf 8363  df-xr 8364  df-ltxr 8365  df-le 8366  df-sub 8499  df-neg 8500  df-reap 8904  df-ap 8911  df-div 9004  df-inn 9306  df-2 9364  df-3 9365  df-4 9366  df-5 9367  df-6 9368  df-7 9369  df-8 9370  df-9 9371  df-n0 9566  df-z 9647  df-dec 9780  df-uz 9924  df-q 10022  df-rp 10057  df-fz 10414  df-seqfrec 10887  df-exp 10978  df-fac 11166  df-bc 11188

This theorem is used by: (None)