Theorem stirlinglem8 30023

Description: If A converges to C, then F converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.)

Hypotheses

Ref	Expression
stirlinglem8.1	|- F/ n ph
stirlinglem8.2	|- F/_ n A
stirlinglem8.3	|- F/_ n D
stirlinglem8.4	|- D = ( n e. NN |-> ( A ` ( 2 x. n ) ) )
stirlinglem8.5	|- ( ph -> A : NN --> RR+ )
stirlinglem8.6	|- F = ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
stirlinglem8.7	|- L = ( n e. NN |-> ( ( A ` n ) ^ 4 ) )
stirlinglem8.8	|- M = ( n e. NN |-> ( ( D ` n ) ^ 2 ) )
stirlinglem8.9	|- ( ( ph /\ n e. NN ) -> ( D ` n ) e. RR+ )
stirlinglem8.10	|- ( ph -> C e. RR+ )
stirlinglem8.11	|- ( ph -> A ~~> C )

Assertion

Ref	Expression
stirlinglem8	|- ( ph -> F ~~> ( C ^ 2 ) )

Proof of Theorem stirlinglem8

Dummy variable k is distinct from all other variables.

Step	Hyp	Ref	Expression
1		stirlinglem8.1	. . 3 |- F/ n ph
2		stirlinglem8.7	. . . 4 |- L = ( n e. NN |-> ( ( A ` n ) ^ 4 ) )
3		nfmpt1 4488	. . . 4 |- F/_ n ( n e. NN |-> ( ( A ` n ) ^ 4 ) )
4	2, 3	nfcxfr 2614	. . 3 |- F/_ n L
5		stirlinglem8.8	. . . 4 |- M = ( n e. NN |-> ( ( D ` n ) ^ 2 ) )
6		nfmpt1 4488	. . . 4 |- F/_ n ( n e. NN |-> ( ( D ` n ) ^ 2 ) )
7	5, 6	nfcxfr 2614	. . 3 |- F/_ n M
8		stirlinglem8.6	. . . 4 |- F = ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
9		nfmpt1 4488	. . . 4 |- F/_ n ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
10	8, 9	nfcxfr 2614	. . 3 |- F/_ n F
11		nnuz 11006	. . 3 |- NN = ( ZZ>= ` 1 )
12		1z 10786	. . . 4 |- 1 e. ZZ
13	12	a1i 11	. . 3 |- ( ph -> 1 e. ZZ )
14		stirlinglem8.2	. . . 4 |- F/_ n A
15		stirlinglem8.5	. . . . 5 |- ( ph -> A : NN --> RR+ )
16		rrpsscn 29916	. . . . 5 |- RR+ C_ CC
17		fss 5674	. . . . 5 |- ( ( A : NN --> RR+ /\ RR+ C_ CC ) -> A : NN --> CC )
18	15, 16, 17	sylancl 662	. . . 4 |- ( ph -> A : NN --> CC )
19		stirlinglem8.11	. . . 4 |- ( ph -> A ~~> C )
20		4nn0 10708	. . . . 5 |- 4 e. NN0
21	20	a1i 11	. . . 4 |- ( ph -> 4 e. NN0 )
22		nnex 10438	. . . . . . 7 |- NN e. _V
23	22	mptex 6056	. . . . . 6 |- ( n e. NN |-> ( ( A ` n ) ^ 4 ) ) e. _V
24	2, 23	eqeltri 2538	. . . . 5 |- L e. _V
25	24	a1i 11	. . . 4 |- ( ph -> L e. _V )
26		simpr 461	. . . . 5 |- ( ( ph /\ n e. NN ) -> n e. NN )
27	15	ffvelrnda 5951	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ( A ` n ) e. RR+ )
28	27	rpcnd 11139	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( A ` n ) e. CC )
29	20	a1i 11	. . . . . 6 |- ( ( ph /\ n e. NN ) -> 4 e. NN0 )
30	28, 29	expcld 12124	. . . . 5 |- ( ( ph /\ n e. NN ) -> ( ( A ` n ) ^ 4 ) e. CC )
31	2	fvmpt2 5889	. . . . 5 |- ( ( n e. NN /\ ( ( A ` n ) ^ 4 ) e. CC ) -> ( L ` n ) = ( ( A ` n ) ^ 4 ) )
32	26, 30, 31	syl2anc 661	. . . 4 |- ( ( ph /\ n e. NN ) -> ( L ` n ) = ( ( A ` n ) ^ 4 ) )
33	1, 14, 4, 11, 13, 18, 19, 21, 25, 32	climexp 29925	. . 3 |- ( ph -> L ~~> ( C ^ 4 ) )
34	22	mptex 6056	. . . . 5 |- ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) ) e. _V
35	8, 34	eqeltri 2538	. . . 4 |- F e. _V
36	35	a1i 11	. . 3 |- ( ph -> F e. _V )
37		stirlinglem8.3	. . . 4 |- F/_ n D
38	18	adantr 465	. . . . . 6 |- ( ( ph /\ n e. NN ) -> A : NN --> CC )
39		2nn 10589	. . . . . . . . 9 |- 2 e. NN
40	39	a1i 11	. . . . . . . 8 |- ( n e. NN -> 2 e. NN )
41		id 22	. . . . . . . 8 |- ( n e. NN -> n e. NN )
42	40, 41	nnmulcld 10479	. . . . . . 7 |- ( n e. NN -> ( 2 x. n ) e. NN )
43	42	adantl 466	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( 2 x. n ) e. NN )
44	38, 43	ffvelrnd 5952	. . . . 5 |- ( ( ph /\ n e. NN ) -> ( A ` ( 2 x. n ) ) e. CC )
45		stirlinglem8.4	. . . . 5 |- D = ( n e. NN |-> ( A ` ( 2 x. n ) ) )
46	1, 44, 45	fmptdf 5976	. . . 4 |- ( ph -> D : NN --> CC )
47		nfmpt1 4488	. . . . 5 |- F/_ n ( n e. NN |-> ( 2 x. n ) )
48		fex 6058	. . . . . 6 |- ( ( A : NN --> CC /\ NN e. _V ) -> A e. _V )
49	18, 22, 48	sylancl 662	. . . . 5 |- ( ph -> A e. _V )
50		1nn 10443	. . . . . . 7 |- 1 e. NN
51		2cnd 10504	. . . . . . . 8 |- ( ph -> 2 e. CC )
52		ax-1cn 9450	. . . . . . . . 9 |- 1 e. CC
53	52	a1i 11	. . . . . . . 8 |- ( ph -> 1 e. CC )
54	51, 53	mulcld 9516	. . . . . . 7 |- ( ph -> ( 2 x. 1 ) e. CC )
55		oveq2 6207	. . . . . . . 8 |- ( n = 1 -> ( 2 x. n ) = ( 2 x. 1 ) )
56		eqid 2454	. . . . . . . 8 |- ( n e. NN |-> ( 2 x. n ) ) = ( n e. NN |-> ( 2 x. n ) )
57	55, 56	fvmptg 5880	. . . . . . 7 |- ( ( 1 e. NN /\ ( 2 x. 1 ) e. CC ) -> ( ( n e. NN |-> ( 2 x. n ) ) ` 1 ) = ( 2 x. 1 ) )
58	50, 54, 57	sylancr 663	. . . . . 6 |- ( ph -> ( ( n e. NN |-> ( 2 x. n ) ) ` 1 ) = ( 2 x. 1 ) )
59	39	a1i 11	. . . . . . 7 |- ( ph -> 2 e. NN )
60	50	a1i 11	. . . . . . 7 |- ( ph -> 1 e. NN )
61	59, 60	nnmulcld 10479	. . . . . 6 |- ( ph -> ( 2 x. 1 ) e. NN )
62	58, 61	eqeltrd 2542	. . . . 5 |- ( ph -> ( ( n e. NN |-> ( 2 x. n ) ) ` 1 ) e. NN )
63		1re 9495	. . . . . . . . . 10 |- 1 e. RR
64	63	a1i 11	. . . . . . . . 9 |- ( n e. NN -> 1 e. RR )
65	40	nnred 10447	. . . . . . . . 9 |- ( n e. NN -> 2 e. RR )
66	42	nnred 10447	. . . . . . . . 9 |- ( n e. NN -> ( 2 x. n ) e. RR )
67	40	nnge1d 10474	. . . . . . . . 9 |- ( n e. NN -> 1 <_ 2 )
68	64, 65, 66, 67	leadd2dd 10064	. . . . . . . 8 |- ( n e. NN -> ( ( 2 x. n ) + 1 ) <_ ( ( 2 x. n ) + 2 ) )
69	56	fvmpt2 5889	. . . . . . . . . 10 |- ( ( n e. NN /\ ( 2 x. n ) e. NN ) -> ( ( n e. NN |-> ( 2 x. n ) ) ` n ) = ( 2 x. n ) )
70	42, 69	mpdan 668	. . . . . . . . 9 |- ( n e. NN -> ( ( n e. NN |-> ( 2 x. n ) ) ` n ) = ( 2 x. n ) )
71	70	oveq1d 6214	. . . . . . . 8 |- ( n e. NN -> ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) = ( ( 2 x. n ) + 1 ) )
72		oveq2 6207	. . . . . . . . . . . 12 |- ( n = k -> ( 2 x. n ) = ( 2 x. k ) )
73	72	cbvmptv 4490	. . . . . . . . . . 11 |- ( n e. NN |-> ( 2 x. n ) ) = ( k e. NN |-> ( 2 x. k ) )
74	73	a1i 11	. . . . . . . . . 10 |- ( n e. NN -> ( n e. NN |-> ( 2 x. n ) ) = ( k e. NN |-> ( 2 x. k ) ) )
75		simpr 461	. . . . . . . . . . 11 |- ( ( n e. NN /\ k = ( n + 1 ) ) -> k = ( n + 1 ) )
76	75	oveq2d 6215	. . . . . . . . . 10 |- ( ( n e. NN /\ k = ( n + 1 ) ) -> ( 2 x. k ) = ( 2 x. ( n + 1 ) ) )
77		peano2nn 10444	. . . . . . . . . 10 |- ( n e. NN -> ( n + 1 ) e. NN )
78	40, 77	nnmulcld 10479	. . . . . . . . . 10 |- ( n e. NN -> ( 2 x. ( n + 1 ) ) e. NN )
79	74, 76, 77, 78	fvmptd 5887	. . . . . . . . 9 |- ( n e. NN -> ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) = ( 2 x. ( n + 1 ) ) )
80		2cnd 10504	. . . . . . . . . 10 |- ( n e. NN -> 2 e. CC )
81		nncn 10440	. . . . . . . . . 10 |- ( n e. NN -> n e. CC )
82	52	a1i 11	. . . . . . . . . 10 |- ( n e. NN -> 1 e. CC )
83	80, 81, 82	adddid 9520	. . . . . . . . 9 |- ( n e. NN -> ( 2 x. ( n + 1 ) ) = ( ( 2 x. n ) + ( 2 x. 1 ) ) )
84	80	mulid1d 9513	. . . . . . . . . 10 |- ( n e. NN -> ( 2 x. 1 ) = 2 )
85	84	oveq2d 6215	. . . . . . . . 9 |- ( n e. NN -> ( ( 2 x. n ) + ( 2 x. 1 ) ) = ( ( 2 x. n ) + 2 ) )
86	79, 83, 85	3eqtrd 2499	. . . . . . . 8 |- ( n e. NN -> ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) = ( ( 2 x. n ) + 2 ) )
87	68, 71, 86	3brtr4d 4429	. . . . . . 7 |- ( n e. NN -> ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) <_ ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) )
88	42	nnzd 10856	. . . . . . . . . 10 |- ( n e. NN -> ( 2 x. n ) e. ZZ )
89	70, 88	eqeltrd 2542	. . . . . . . . 9 |- ( n e. NN -> ( ( n e. NN |-> ( 2 x. n ) ) ` n ) e. ZZ )
90	89	peano2zd 10860	. . . . . . . 8 |- ( n e. NN -> ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) e. ZZ )
91	78	nnzd 10856	. . . . . . . . 9 |- ( n e. NN -> ( 2 x. ( n + 1 ) ) e. ZZ )
92	79, 91	eqeltrd 2542	. . . . . . . 8 |- ( n e. NN -> ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) e. ZZ )
93		eluz 10984	. . . . . . . 8 |- ( ( ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) e. ZZ /\ ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) e. ZZ ) -> ( ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) e. ( ZZ>= ` ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) ) <-> ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) <_ ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) ) )
94	90, 92, 93	syl2anc 661	. . . . . . 7 |- ( n e. NN -> ( ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) e. ( ZZ>= ` ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) ) <-> ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) <_ ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) ) )
95	87, 94	mpbird 232	. . . . . 6 |- ( n e. NN -> ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) e. ( ZZ>= ` ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) ) )
96	95	adantl 466	. . . . 5 |- ( ( ph /\ n e. NN ) -> ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) e. ( ZZ>= ` ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) ) )
97	22	mptex 6056	. . . . . . 7 |- ( n e. NN |-> ( A ` ( 2 x. n ) ) ) e. _V
98	45, 97	eqeltri 2538	. . . . . 6 |- D e. _V
99	98	a1i 11	. . . . 5 |- ( ph -> D e. _V )
100	45	fvmpt2 5889	. . . . . . 7 |- ( ( n e. NN /\ ( A ` ( 2 x. n ) ) e. CC ) -> ( D ` n ) = ( A ` ( 2 x. n ) ) )
101	26, 44, 100	syl2anc 661	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( D ` n ) = ( A ` ( 2 x. n ) ) )
102	70	adantl 466	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( ( n e. NN |-> ( 2 x. n ) ) ` n ) = ( 2 x. n ) )
103	102	eqcomd 2462	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ( 2 x. n ) = ( ( n e. NN |-> ( 2 x. n ) ) ` n ) )
104	103	fveq2d 5802	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( A ` ( 2 x. n ) ) = ( A ` ( ( n e. NN |-> ( 2 x. n ) ) ` n ) ) )
105	101, 104	eqtrd 2495	. . . . 5 |- ( ( ph /\ n e. NN ) -> ( D ` n ) = ( A ` ( ( n e. NN |-> ( 2 x. n ) ) ` n ) ) )
106	1, 14, 37, 47, 11, 13, 49, 28, 19, 62, 96, 99, 105	climsuse 29928	. . . 4 |- ( ph -> D ~~> C )
107		2nn0 10706	. . . . 5 |- 2 e. NN0
108	107	a1i 11	. . . 4 |- ( ph -> 2 e. NN0 )
109	22	mptex 6056	. . . . . 6 |- ( n e. NN |-> ( ( D ` n ) ^ 2 ) ) e. _V
110	5, 109	eqeltri 2538	. . . . 5 |- M e. _V
111	110	a1i 11	. . . 4 |- ( ph -> M e. _V )
112		stirlinglem8.9	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ( D ` n ) e. RR+ )
113	112	rpcnd 11139	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( D ` n ) e. CC )
114	113	sqcld 12122	. . . . 5 |- ( ( ph /\ n e. NN ) -> ( ( D ` n ) ^ 2 ) e. CC )
115	5	fvmpt2 5889	. . . . 5 |- ( ( n e. NN /\ ( ( D ` n ) ^ 2 ) e. CC ) -> ( M ` n ) = ( ( D ` n ) ^ 2 ) )
116	26, 114, 115	syl2anc 661	. . . 4 |- ( ( ph /\ n e. NN ) -> ( M ` n ) = ( ( D ` n ) ^ 2 ) )
117	1, 37, 7, 11, 13, 46, 106, 108, 111, 116	climexp 29925	. . 3 |- ( ph -> M ~~> ( C ^ 2 ) )
118		stirlinglem8.10	. . . . 5 |- ( ph -> C e. RR+ )
119	118	rpcnd 11139	. . . 4 |- ( ph -> C e. CC )
120	118	rpne0d 11142	. . . 4 |- ( ph -> C =/= 0 )
121		2z 10788	. . . . 5 |- 2 e. ZZ
122	121	a1i 11	. . . 4 |- ( ph -> 2 e. ZZ )
123	119, 120, 122	expne0d 12130	. . 3 |- ( ph -> ( C ^ 2 ) =/= 0 )
124	1, 30, 2	fmptdf 5976	. . . 4 |- ( ph -> L : NN --> CC )
125	124	ffvelrnda 5951	. . 3 |- ( ( ph /\ n e. NN ) -> ( L ` n ) e. CC )
126	116, 114	eqeltrd 2542	. . . 4 |- ( ( ph /\ n e. NN ) -> ( M ` n ) e. CC )
127	101	oveq1d 6214	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( ( D ` n ) ^ 2 ) = ( ( A ` ( 2 x. n ) ) ^ 2 ) )
128	116, 127	eqtrd 2495	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( M ` n ) = ( ( A ` ( 2 x. n ) ) ^ 2 ) )
129	101, 112	eqeltrrd 2543	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( A ` ( 2 x. n ) ) e. RR+ )
130	121	a1i 11	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> 2 e. ZZ )
131	129, 130	rpexpcld 12147	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( ( A ` ( 2 x. n ) ) ^ 2 ) e. RR+ )
132	128, 131	eqeltrd 2542	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ( M ` n ) e. RR+ )
133	132	rpne0d 11142	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( M ` n ) =/= 0 )
134	133	neneqd 2654	. . . . 5 |- ( ( ph /\ n e. NN ) -> -. ( M ` n ) = 0 )
135		0cn 9488	. . . . . 6 |- 0 e. CC
136		elsnc2g 4014	. . . . . 6 |- ( 0 e. CC -> ( ( M ` n ) e. { 0 } <-> ( M ` n ) = 0 ) )
137	135, 136	ax-mp 5	. . . . 5 |- ( ( M ` n ) e. { 0 } <-> ( M ` n ) = 0 )
138	134, 137	sylnibr 305	. . . 4 |- ( ( ph /\ n e. NN ) -> -. ( M ` n ) e. { 0 } )
139	126, 138	eldifd 3446	. . 3 |- ( ( ph /\ n e. NN ) -> ( M ` n ) e. ( CC \ { 0 } ) )
140	29	nn0zd 10855	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> 4 e. ZZ )
141	27, 140	rpexpcld 12147	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( ( A ` n ) ^ 4 ) e. RR+ )
142	112, 130	rpexpcld 12147	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( ( D ` n ) ^ 2 ) e. RR+ )
143	141, 142	rpdivcld 11154	. . . . 5 |- ( ( ph /\ n e. NN ) -> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) e. RR+ )
144	8	fvmpt2 5889	. . . . 5 |- ( ( n e. NN /\ ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) e. RR+ ) -> ( F ` n ) = ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
145	26, 143, 144	syl2anc 661	. . . 4 |- ( ( ph /\ n e. NN ) -> ( F ` n ) = ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
146	2	fvmpt2 5889	. . . . . 6 |- ( ( n e. NN /\ ( ( A ` n ) ^ 4 ) e. RR+ ) -> ( L ` n ) = ( ( A ` n ) ^ 4 ) )
147	26, 141, 146	syl2anc 661	. . . . 5 |- ( ( ph /\ n e. NN ) -> ( L ` n ) = ( ( A ` n ) ^ 4 ) )
148	147, 116	oveq12d 6217	. . . 4 |- ( ( ph /\ n e. NN ) -> ( ( L ` n ) / ( M ` n ) ) = ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
149	145, 148	eqtr4d 2498	. . 3 |- ( ( ph /\ n e. NN ) -> ( F ` n ) = ( ( L ` n ) / ( M ` n ) ) )
150	1, 4, 7, 10, 11, 13, 33, 36, 117, 123, 125, 139, 149	climdivf 29932	. 2 |- ( ph -> F ~~> ( ( C ^ 4 ) / ( C ^ 2 ) ) )
151		4cn 10509	. . . . . . 7 |- 4 e. CC
152		2cn 10502	. . . . . . 7 |- 2 e. CC
153		2p2e4 10549	. . . . . . 7 |- ( 2 + 2 ) = 4
154	151, 152, 152, 153	subaddrii 9807	. . . . . 6 |- ( 4 - 2 ) = 2
155	154	eqcomi 2467	. . . . 5 |- 2 = ( 4 - 2 )
156	155	a1i 11	. . . 4 |- ( ph -> 2 = ( 4 - 2 ) )
157	156	oveq2d 6215	. . 3 |- ( ph -> ( C ^ 2 ) = ( C ^ ( 4 - 2 ) ) )
158	21	nn0zd 10855	. . . 4 |- ( ph -> 4 e. ZZ )
159	119, 120, 122, 158	expsubd 12135	. . 3 |- ( ph -> ( C ^ ( 4 - 2 ) ) = ( ( C ^ 4 ) / ( C ^ 2 ) ) )
160	157, 159	eqtrd 2495	. 2 |- ( ph -> ( C ^ 2 ) = ( ( C ^ 4 ) / ( C ^ 2 ) ) )
161	150, 160	breqtrrd 4425	1 |- ( ph -> F ~~> ( C ^ 2 ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1370   F/wnf 1590   e. wcel 1758   F/_wnfc 2602   _Vcvv 3076   C_ wss 3435   {csn 3984   class class class wbr 4399   |-> cmpt 4457   -->wf 5521   ` cfv 5525  (class class class)co 6199   CCcc 9390   RRcr 9391   0cc0 9392   1c1 9393   + caddc 9395   x. cmul 9397   <_ cle 9529   - cmin 9705   / cdiv 10103   NNcn 10432   2c2 10481   4c4 10483   NN0cn0 10689   ZZcz 10756   ZZ>=cuz 10971   RR+crp 11101   ^cexp 11981   ~~> cli 13079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4510  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-inf2 7957  ax-cnex 9448  ax-resscn 9449  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-mulcom 9456  ax-addass 9457  ax-mulass 9458  ax-distr 9459  ax-i2m1 9460  ax-1ne0 9461  ax-1rid 9462  ax-rnegex 9463  ax-rrecex 9464  ax-cnre 9465  ax-pre-lttri 9466  ax-pre-lttrn 9467  ax-pre-ltadd 9468  ax-pre-mulgt0 9469  ax-pre-sup 9470  ax-mulf 9472

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-nel 2650  df-ral 2803  df-rex 2804  df-reu 2805  df-rmo 2806  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-int 4236  df-iun 4280  df-iin 4281  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-se 4787  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-isom 5534  df-riota 6160  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-of 6429  df-om 6586  df-1st 6686  df-2nd 6687  df-supp 6800  df-recs 6941  df-rdg 6975  df-1o 7029  df-2o 7030  df-oadd 7033  df-er 7210  df-map 7325  df-ixp 7373  df-en 7420  df-dom 7421  df-sdom 7422  df-fin 7423  df-fsupp 7731  df-fi 7771  df-sup 7801  df-oi 7834  df-card 8219  df-cda 8447  df-pnf 9530  df-mnf 9531  df-xr 9532  df-ltxr 9533  df-le 9534  df-sub 9707  df-neg 9708  df-div 10104  df-nn 10433  df-2 10490  df-3 10491  df-4 10492  df-5 10493  df-6 10494  df-7 10495  df-8 10496  df-9 10497  df-10 10498  df-n0 10690  df-z 10757  df-dec 10866  df-uz 10972  df-q 11064  df-rp 11102  df-xneg 11199  df-xadd 11200  df-xmul 11201  df-icc 11417  df-fz 11554  df-fzo 11665  df-seq 11923  df-exp 11982  df-hash 12220  df-cj 12705  df-re 12706  df-im 12707  df-sqr 12841  df-abs 12842  df-clim 13083  df-struct 14293  df-ndx 14294  df-slot 14295  df-base 14296  df-sets 14297  df-ress 14298  df-plusg 14369  df-mulr 14370  df-starv 14371  df-sca 14372  df-vsca 14373  df-ip 14374  df-tset 14375  df-ple 14376  df-ds 14378  df-unif 14379  df-hom 14380  df-cco 14381  df-rest 14479  df-topn 14480  df-0g 14498  df-gsum 14499  df-topgen 14500  df-pt 14501  df-prds 14504  df-xrs 14558  df-qtop 14563  df-imas 14564  df-xps 14566  df-mre 14642  df-mrc 14643  df-acs 14645  df-mnd 15533  df-submnd 15583  df-mulg 15666  df-cntz 15953  df-cmn 16399  df-psmet 17933  df-xmet 17934  df-met 17935  df-bl 17936  df-mopn 17937  df-cnfld 17943  df-top 18634  df-bases 18636  df-topon 18637  df-topsp 18638  df-cn 18962  df-cnp 18963  df-tx 19266  df-hmeo 19459  df-xms 20026  df-ms 20027  df-tms 20028  df-cncf 20585

This theorem is referenced by:  stirlinglem15  30030