Theorem carsgclctunlem2 29151

Description: Lemma for carsgclctun 29153. (Contributed by Thierry Arnoux, 25-May-2020.)

Hypotheses

Ref	Expression
carsgval.1	|- ( ph -> O e. V )
carsgval.2	|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
carsgsiga.1	|- ( ph -> ( M ` (/) ) = 0 )
carsgsiga.2	|- ( ( ph /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )
carsgsiga.3	|- ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
carsgclctunlem2.1	|- ( ph -> Disj k e. NN A )
carsgclctunlem2.2	|- ( ( ph /\ k e. NN ) -> A e. (toCaraSiga ` M ) )
carsgclctunlem2.3	|- ( ph -> E e. ~P O )
carsgclctunlem2.4	|- ( ph -> ( M ` E ) =/= +oo )

Assertion

Ref	Expression
carsgclctunlem2	|- ( ph -> ( ( M ` ( E i^i U_ k e. NN A ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) <_ ( M ` E ) )

Distinct variable groups:   x, A, y   x, E, y   x, M, y   x, O, y   ph, x, y, k   k, E   k, M   k, O   ph, k

Allowed substitution hints:   A( k)   V( x, y, k)

Proof of Theorem carsgclctunlem2

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

Step	Hyp	Ref	Expression
1		iunin2 4342	. . . . 5 |- U_ k e. NN ( E i^i A ) = ( E i^i U_ k e. NN A )
2	1	fveq2i 5868	. . . 4 |- ( M ` U_ k e. NN ( E i^i A ) ) = ( M ` ( E i^i U_ k e. NN A ) )
3		iccssxr 11717	. . . . 5 |- ( 0 [,] +oo ) C_ RR*
4		carsgval.2	. . . . . 6 |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
5		nnex 10615	. . . . . . . 8 |- NN e. _V
6	5	a1i 11	. . . . . . 7 |- ( ph -> NN e. _V )
7		carsgclctunlem2.3	. . . . . . . . 9 |- ( ph -> E e. ~P O )
8	7	adantr 467	. . . . . . . 8 |- ( ( ph /\ k e. NN ) -> E e. ~P O )
9	8	elpwincl1 28154	. . . . . . 7 |- ( ( ph /\ k e. NN ) -> ( E i^i A ) e. ~P O )
10	6, 9	elpwiuncl 28156	. . . . . 6 |- ( ph -> U_ k e. NN ( E i^i A ) e. ~P O )
11	4, 10	ffvelrnd 6023	. . . . 5 |- ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) e. ( 0 [,] +oo ) )
12	3, 11	sseldi 3430	. . . 4 |- ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) e. RR* )
13	2, 12	syl5eqelr 2534	. . 3 |- ( ph -> ( M ` ( E i^i U_ k e. NN A ) ) e. RR* )
14	4, 7	ffvelrnd 6023	. . . . 5 |- ( ph -> ( M ` E ) e. ( 0 [,] +oo ) )
15	3, 14	sseldi 3430	. . . 4 |- ( ph -> ( M ` E ) e. RR* )
16	7	elpwdifcl 28155	. . . . . . 7 |- ( ph -> ( E \ U_ k e. NN A ) e. ~P O )
17	4, 16	ffvelrnd 6023	. . . . . 6 |- ( ph -> ( M ` ( E \ U_ k e. NN A ) ) e. ( 0 [,] +oo ) )
18	3, 17	sseldi 3430	. . . . 5 |- ( ph -> ( M ` ( E \ U_ k e. NN A ) ) e. RR* )
19	18	xnegcld 11586	. . . 4 |- ( ph -> -e ( M ` ( E \ U_ k e. NN A ) ) e. RR* )
20	15, 19	xaddcld 11587	. . 3 |- ( ph -> ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) e. RR* )
21	4	adantr 467	. . . . . . . . 9 |- ( ( ph /\ k e. NN ) -> M : ~P O --> ( 0 [,] +oo ) )
22	21, 9	ffvelrnd 6023	. . . . . . . 8 |- ( ( ph /\ k e. NN ) -> ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) )
23	22	ralrimiva 2802	. . . . . . 7 |- ( ph -> A. k e. NN ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) )
24		nfcv 2592	. . . . . . . 8 |- F/_ k NN
25	24	esumcl 28851	. . . . . . 7 |- ( ( NN e. _V /\ A. k e. NN ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) ) -> Σ* k e. NN ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) )
26	6, 23, 25	syl2anc 667	. . . . . 6 |- ( ph -> Σ* k e. NN ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) )
27	3, 26	sseldi 3430	. . . . 5 |- ( ph -> Σ* k e. NN ( M ` ( E i^i A ) ) e. RR* )
28	9	ralrimiva 2802	. . . . . . . . 9 |- ( ph -> A. k e. NN ( E i^i A ) e. ~P O )
29		dfiun3g 5087	. . . . . . . . 9 |- ( A. k e. NN ( E i^i A ) e. ~P O -> U_ k e. NN ( E i^i A ) = U. ran ( k e. NN |-> ( E i^i A ) ) )
30	28, 29	syl 17	. . . . . . . 8 |- ( ph -> U_ k e. NN ( E i^i A ) = U. ran ( k e. NN |-> ( E i^i A ) ) )
31	30	fveq2d 5869	. . . . . . 7 |- ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) = ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) )
32		nnct 28294	. . . . . . . . . 10 |- NN ~<_ om
33		mptct 28302	. . . . . . . . . 10 |- ( NN ~<_ om -> ( k e. NN |-> ( E i^i A ) ) ~<_ om )
34		rnct 28300	. . . . . . . . . 10 |- ( ( k e. NN |-> ( E i^i A ) ) ~<_ om -> ran ( k e. NN |-> ( E i^i A ) ) ~<_ om )
35	32, 33, 34	mp2b 10	. . . . . . . . 9 |- ran ( k e. NN |-> ( E i^i A ) ) ~<_ om
36	35	a1i 11	. . . . . . . 8 |- ( ph -> ran ( k e. NN |-> ( E i^i A ) ) ~<_ om )
37		eqid 2451	. . . . . . . . . 10 |- ( k e. NN |-> ( E i^i A ) ) = ( k e. NN |-> ( E i^i A ) )
38	37	rnmptss 6052	. . . . . . . . 9 |- ( A. k e. NN ( E i^i A ) e. ~P O -> ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O )
39	28, 38	syl 17	. . . . . . . 8 |- ( ph -> ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O )
40		mptexg 6135	. . . . . . . . . 10 |- ( NN e. _V -> ( k e. NN |-> ( E i^i A ) ) e. _V )
41		rnexg 6725	. . . . . . . . . 10 |- ( ( k e. NN |-> ( E i^i A ) ) e. _V -> ran ( k e. NN |-> ( E i^i A ) ) e. _V )
42	5, 40, 41	mp2b 10	. . . . . . . . 9 |- ran ( k e. NN |-> ( E i^i A ) ) e. _V
43		breq1 4405	. . . . . . . . . . . 12 |- ( x = ran ( k e. NN |-> ( E i^i A ) ) -> ( x ~<_ om <-> ran ( k e. NN |-> ( E i^i A ) ) ~<_ om ) )
44		sseq1 3453	. . . . . . . . . . . 12 |- ( x = ran ( k e. NN |-> ( E i^i A ) ) -> ( x C_ ~P O <-> ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O ) )
45	43, 44	3anbi23d 1342	. . . . . . . . . . 11 |- ( x = ran ( k e. NN |-> ( E i^i A ) ) -> ( ( ph /\ x ~<_ om /\ x C_ ~P O ) <-> ( ph /\ ran ( k e. NN |-> ( E i^i A ) ) ~<_ om /\ ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O ) ) )
46		unieq 4206	. . . . . . . . . . . . 13 |- ( x = ran ( k e. NN |-> ( E i^i A ) ) -> U. x = U. ran ( k e. NN |-> ( E i^i A ) ) )
47	46	fveq2d 5869	. . . . . . . . . . . 12 |- ( x = ran ( k e. NN |-> ( E i^i A ) ) -> ( M ` U. x ) = ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) )
48		esumeq1 28855	. . . . . . . . . . . 12 |- ( x = ran ( k e. NN |-> ( E i^i A ) ) -> Σ* y e. x ( M ` y ) = Σ* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) )
49	47, 48	breq12d 4415	. . . . . . . . . . 11 |- ( x = ran ( k e. NN |-> ( E i^i A ) ) -> ( ( M ` U. x ) <_ Σ* y e. x ( M ` y ) <-> ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) <_ Σ* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) ) )
50	45, 49	imbi12d 322	. . . . . . . . . 10 |- ( x = ran ( k e. NN |-> ( E i^i A ) ) -> ( ( ( ph /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) ) <-> ( ( ph /\ ran ( k e. NN |-> ( E i^i A ) ) ~<_ om /\ ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O ) -> ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) <_ Σ* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) ) ) )
51		carsgsiga.2	. . . . . . . . . 10 |- ( ( ph /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )
52	50, 51	vtoclg 3107	. . . . . . . . 9 |- ( ran ( k e. NN |-> ( E i^i A ) ) e. _V -> ( ( ph /\ ran ( k e. NN |-> ( E i^i A ) ) ~<_ om /\ ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O ) -> ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) <_ Σ* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) ) )
53	42, 52	ax-mp 5	. . . . . . . 8 |- ( ( ph /\ ran ( k e. NN |-> ( E i^i A ) ) ~<_ om /\ ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O ) -> ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) <_ Σ* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) )
54	36, 39, 53	mpd3an23 1366	. . . . . . 7 |- ( ph -> ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) <_ Σ* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) )
55	31, 54	eqbrtrd 4423	. . . . . 6 |- ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) <_ Σ* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) )
56		fveq2 5865	. . . . . . 7 |- ( y = ( E i^i A ) -> ( M ` y ) = ( M ` ( E i^i A ) ) )
57		simpr 463	. . . . . . . . 9 |- ( ( ( ph /\ k e. NN ) /\ ( E i^i A ) = (/) ) -> ( E i^i A ) = (/) )
58	57	fveq2d 5869	. . . . . . . 8 |- ( ( ( ph /\ k e. NN ) /\ ( E i^i A ) = (/) ) -> ( M ` ( E i^i A ) ) = ( M ` (/) ) )
59		carsgsiga.1	. . . . . . . . 9 |- ( ph -> ( M ` (/) ) = 0 )
60	59	ad2antrr 732	. . . . . . . 8 |- ( ( ( ph /\ k e. NN ) /\ ( E i^i A ) = (/) ) -> ( M ` (/) ) = 0 )
61	58, 60	eqtrd 2485	. . . . . . 7 |- ( ( ( ph /\ k e. NN ) /\ ( E i^i A ) = (/) ) -> ( M ` ( E i^i A ) ) = 0 )
62		carsgclctunlem2.1	. . . . . . . . 9 |- ( ph -> Disj k e. NN A )
63		disjin 28196	. . . . . . . . 9 |- (Disj k e. NN A -> Disj k e. NN ( A i^i E ) )
64	62, 63	syl 17	. . . . . . . 8 |- ( ph -> Disj k e. NN ( A i^i E ) )
65		incom 3625	. . . . . . . . . 10 |- ( A i^i E ) = ( E i^i A )
66	65	rgenw 2749	. . . . . . . . 9 |- A. k e. NN ( A i^i E ) = ( E i^i A )
67		disjeq2 4377	. . . . . . . . 9 |- ( A. k e. NN ( A i^i E ) = ( E i^i A ) -> (Disj k e. NN ( A i^i E ) <-> Disj k e. NN ( E i^i A ) ) )
68	66, 67	ax-mp 5	. . . . . . . 8 |- (Disj k e. NN ( A i^i E ) <-> Disj k e. NN ( E i^i A ) )
69	64, 68	sylib 200	. . . . . . 7 |- ( ph -> Disj k e. NN ( E i^i A ) )
70	56, 6, 22, 9, 61, 69	esumrnmpt2 28889	. . . . . 6 |- ( ph -> Σ* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) = Σ* k e. NN ( M ` ( E i^i A ) ) )
71	55, 70	breqtrd 4427	. . . . 5 |- ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) <_ Σ* k e. NN ( M ` ( E i^i A ) ) )
72		carsgval.1	. . . . . . . 8 |- ( ph -> O e. V )
73		difssd 3561	. . . . . . . 8 |- ( ph -> ( E \ U_ k e. NN A ) C_ E )
74		carsgsiga.3	. . . . . . . 8 |- ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
75	72, 4, 73, 7, 74	carsgmon 29146	. . . . . . 7 |- ( ph -> ( M ` ( E \ U_ k e. NN A ) ) <_ ( M ` E ) )
76	14, 17, 75	xrge0subcld 28345	. . . . . 6 |- ( ph -> ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) e. ( 0 [,] +oo ) )
77	4	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> M : ~P O --> ( 0 [,] +oo ) )
78	7	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> E e. ~P O )
79	78	elpwincl1 28154	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( E i^i U_ k e. ( 1 ... n ) A ) e. ~P O )
80	77, 79	ffvelrnd 6023	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) e. ( 0 [,] +oo ) )
81	3, 80	sseldi 3430	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) e. RR* )
82		xrge0neqmnf 11737	. . . . . . . . . . 11 |- ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) e. ( 0 [,] +oo ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) =/= -oo )
83	80, 82	syl 17	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) =/= -oo )
84	78	elpwdifcl 28155	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( E \ U_ k e. ( 1 ... n ) A ) e. ~P O )
85	77, 84	ffvelrnd 6023	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. ( 0 [,] +oo ) )
86	3, 85	sseldi 3430	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* )
87		xrge0neqmnf 11737	. . . . . . . . . . 11 |- ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. ( 0 [,] +oo ) -> ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) =/= -oo )
88	85, 87	syl 17	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) =/= -oo )
89	86	xnegcld 11586	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* )
90		xnegneg 11507	. . . . . . . . . . . . . . . . 17 |- ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* -> -e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) )
91	86, 90	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> -e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) )
92	91	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> -e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) )
93		xnegeq 11500	. . . . . . . . . . . . . . . . 17 |- ( -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo -> -e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -e -oo )
94	93	adantl 468	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> -e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -e -oo )
95		xnegmnf 11503	. . . . . . . . . . . . . . . 16 |- -e -oo = +oo
96	94, 95	syl6eq 2501	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> -e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = +oo )
97	92, 96	eqtr3d 2487	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = +oo )
98	97	oveq2d 6306	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e +oo ) )
99		simpll 760	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ph )
100		fz1ssnn 11830	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 1 ... n ) C_ NN
101	100	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ n e. NN ) -> ( 1 ... n ) C_ NN )
102	101	sselda 3432	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. NN )
103		carsgclctunlem2.2	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. NN ) -> A e. (toCaraSiga ` M ) )
104	99, 102, 103	syl2anc 667	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> A e. (toCaraSiga ` M ) )
105	104	ralrimiva 2802	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. NN ) -> A. k e. ( 1 ... n ) A e. (toCaraSiga ` M ) )
106		dfiun3g 5087	. . . . . . . . . . . . . . . . . . 19 |- ( A. k e. ( 1 ... n ) A e. (toCaraSiga ` M ) -> U_ k e. ( 1 ... n ) A = U. ran ( k e. ( 1 ... n ) |-> A ) )
107	105, 106	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. NN ) -> U_ k e. ( 1 ... n ) A = U. ran ( k e. ( 1 ... n ) |-> A ) )
108	72	adantr 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. NN ) -> O e. V )
109	59	adantr 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. NN ) -> ( M ` (/) ) = 0 )
110	51	3adant1r 1261	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )
111		fzfi 12185	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 ... n ) e. Fin
112		mptfi 7873	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 1 ... n ) e. Fin -> ( k e. ( 1 ... n ) |-> A ) e. Fin )
113		rnfi 7857	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( k e. ( 1 ... n ) |-> A ) e. Fin -> ran ( k e. ( 1 ... n ) |-> A ) e. Fin )
114	111, 112, 113	mp2b 10	. . . . . . . . . . . . . . . . . . . 20 |- ran ( k e. ( 1 ... n ) |-> A ) e. Fin
115	114	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. NN ) -> ran ( k e. ( 1 ... n ) |-> A ) e. Fin )
116		eqid 2451	. . . . . . . . . . . . . . . . . . . . 21 |- ( k e. ( 1 ... n ) |-> A ) = ( k e. ( 1 ... n ) |-> A )
117	116	rnmptss 6052	. . . . . . . . . . . . . . . . . . . 20 |- ( A. k e. ( 1 ... n ) A e. (toCaraSiga ` M ) -> ran ( k e. ( 1 ... n ) |-> A ) C_ (toCaraSiga ` M ) )
118	105, 117	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. NN ) -> ran ( k e. ( 1 ... n ) |-> A ) C_ (toCaraSiga ` M ) )
119	108, 77, 109, 110, 115, 118	fiunelcarsg 29148	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. NN ) -> U. ran ( k e. ( 1 ... n ) |-> A ) e. (toCaraSiga ` M ) )
120	107, 119	eqeltrd 2529	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. NN ) -> U_ k e. ( 1 ... n ) A e. (toCaraSiga ` M ) )
121	108, 77	elcarsg 29137	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. NN ) -> ( U_ k e. ( 1 ... n ) A e. (toCaraSiga ` M ) <-> ( U_ k e. ( 1 ... n ) A C_ O /\ A. e e. ~P O ( ( M ` ( e i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` e ) ) ) )
122	120, 121	mpbid 214	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. NN ) -> ( U_ k e. ( 1 ... n ) A C_ O /\ A. e e. ~P O ( ( M ` ( e i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` e ) ) )
123	122	simprd 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> A. e e. ~P O ( ( M ` ( e i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` e ) )
124		ineq1 3627	. . . . . . . . . . . . . . . . . . 19 |- ( e = E -> ( e i^i U_ k e. ( 1 ... n ) A ) = ( E i^i U_ k e. ( 1 ... n ) A ) )
125	124	fveq2d 5869	. . . . . . . . . . . . . . . . . 18 |- ( e = E -> ( M ` ( e i^i U_ k e. ( 1 ... n ) A ) ) = ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) )
126		difeq1 3544	. . . . . . . . . . . . . . . . . . 19 |- ( e = E -> ( e \ U_ k e. ( 1 ... n ) A ) = ( E \ U_ k e. ( 1 ... n ) A ) )
127	126	fveq2d 5869	. . . . . . . . . . . . . . . . . 18 |- ( e = E -> ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) = ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) )
128	125, 127	oveq12d 6308	. . . . . . . . . . . . . . . . 17 |- ( e = E -> ( ( M ` ( e i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) ) = ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) )
129		fveq2 5865	. . . . . . . . . . . . . . . . 17 |- ( e = E -> ( M ` e ) = ( M ` E ) )
130	128, 129	eqeq12d 2466	. . . . . . . . . . . . . . . 16 |- ( e = E -> ( ( ( M ` ( e i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` e ) <-> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` E ) ) )
131	130	rspcv 3146	. . . . . . . . . . . . . . 15 |- ( E e. ~P O -> ( A. e e. ~P O ( ( M ` ( e i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` e ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` E ) ) )
132	78, 123, 131	sylc 62	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` E ) )
133	132	adantr 467	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` E ) )
134		xaddpnf1 11519	. . . . . . . . . . . . . . 15 |- ( ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) e. RR* /\ ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) =/= -oo ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e +oo ) = +oo )
135	81, 83, 134	syl2anc 667	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e +oo ) = +oo )
136	135	adantr 467	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e +oo ) = +oo )
137	98, 133, 136	3eqtr3d 2493	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> ( M ` E ) = +oo )
138		carsgclctunlem2.4	. . . . . . . . . . . . . 14 |- ( ph -> ( M ` E ) =/= +oo )
139	138	ad2antrr 732	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> ( M ` E ) =/= +oo )
140	139	neneqd 2629	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> -. ( M ` E ) = +oo )
141	137, 140	pm2.65da 580	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> -. -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo )
142	141	neqned 2631	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) =/= -oo )
143		xaddass 11535	. . . . . . . . . 10 |- ( ( ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) e. RR* /\ ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) =/= -oo ) /\ ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* /\ ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) =/= -oo ) /\ ( -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) =/= -oo ) ) -> ( ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) ) )
144	81, 83, 86, 88, 89, 142, 143	syl222anc 1284	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) ) )
145		xnegid 11529	. . . . . . . . . . 11 |- ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* -> ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = 0 )
146	86, 145	syl 17	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = 0 )
147	146	oveq2d 6306	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) ) = ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e 0 ) )
148		xaddid1 11532	. . . . . . . . . 10 |- ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) e. RR* -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e 0 ) = ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) )
149	81, 148	syl 17	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e 0 ) = ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) )
150	144, 147, 149	3eqtrd 2489	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) )
151	132	oveq1d 6305	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) )
152	107	ineq2d 3634	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( E i^i U_ k e. ( 1 ... n ) A ) = ( E i^i U. ran ( k e. ( 1 ... n ) |-> A ) ) )
153	152	fveq2d 5869	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) = ( M ` ( E i^i U. ran ( k e. ( 1 ... n ) |-> A ) ) ) )
154		fmptss 28277	. . . . . . . . . . . . 13 |- ( ( 1 ... n ) C_ NN -> ( k e. ( 1 ... n ) |-> A ) C_ ( k e. NN |-> A ) )
155		rnss 5063	. . . . . . . . . . . . 13 |- ( ( k e. ( 1 ... n ) |-> A ) C_ ( k e. NN |-> A ) -> ran ( k e. ( 1 ... n ) |-> A ) C_ ran ( k e. NN |-> A ) )
156	100, 154, 155	mp2b 10	. . . . . . . . . . . 12 |- ran ( k e. ( 1 ... n ) |-> A ) C_ ran ( k e. NN |-> A )
157	156	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> ran ( k e. ( 1 ... n ) |-> A ) C_ ran ( k e. NN |-> A ) )
158		disjrnmpt 28195	. . . . . . . . . . . . 13 |- (Disj k e. NN A -> Disj y e. ran ( k e. NN |-> A ) y )
159	62, 158	syl 17	. . . . . . . . . . . 12 |- ( ph -> Disj y e. ran ( k e. NN |-> A ) y )
160	159	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> Disj y e. ran ( k e. NN |-> A ) y )
161		disjss1 4379	. . . . . . . . . . 11 |- ( ran ( k e. ( 1 ... n ) |-> A ) C_ ran ( k e. NN |-> A ) -> (Disj y e. ran ( k e. NN |-> A ) y -> Disj y e. ran ( k e. ( 1 ... n ) |-> A ) y ) )
162	157, 160, 161	sylc 62	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> Disj y e. ran ( k e. ( 1 ... n ) |-> A ) y )
163	108, 77, 109, 110, 115, 118, 162, 78	carsgclctunlem1 29149	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U. ran ( k e. ( 1 ... n ) |-> A ) ) ) = Σ* y e. ran ( k e. ( 1 ... n ) |-> A ) ( M ` ( E i^i y ) ) )
164		ineq2 3628	. . . . . . . . . . 11 |- ( y = A -> ( E i^i y ) = ( E i^i A ) )
165	164	fveq2d 5869	. . . . . . . . . 10 |- ( y = A -> ( M ` ( E i^i y ) ) = ( M ` ( E i^i A ) ) )
166	111	elexi 3055	. . . . . . . . . . 11 |- ( 1 ... n ) e. _V
167	166	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( 1 ... n ) e. _V )
168	99, 102, 22	syl2anc 667	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) )
169		inss2 3653	. . . . . . . . . . . . . . 15 |- ( E i^i A ) C_ A
170		sseq2 3454	. . . . . . . . . . . . . . 15 |- ( A = (/) -> ( ( E i^i A ) C_ A <-> ( E i^i A ) C_ (/) ) )
171	169, 170	mpbii 215	. . . . . . . . . . . . . 14 |- ( A = (/) -> ( E i^i A ) C_ (/) )
172		ss0 3765	. . . . . . . . . . . . . 14 |- ( ( E i^i A ) C_ (/) -> ( E i^i A ) = (/) )
173	171, 172	syl 17	. . . . . . . . . . . . 13 |- ( A = (/) -> ( E i^i A ) = (/) )
174	173	adantl 468	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ A = (/) ) -> ( E i^i A ) = (/) )
175	174	fveq2d 5869	. . . . . . . . . . 11 |- ( ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ A = (/) ) -> ( M ` ( E i^i A ) ) = ( M ` (/) ) )
176	109	ad2antrr 732	. . . . . . . . . . 11 |- ( ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ A = (/) ) -> ( M ` (/) ) = 0 )
177	175, 176	eqtrd 2485	. . . . . . . . . 10 |- ( ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ A = (/) ) -> ( M ` ( E i^i A ) ) = 0 )
178	62	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> Disj k e. NN A )
179		disjss1 4379	. . . . . . . . . . 11 |- ( ( 1 ... n ) C_ NN -> (Disj k e. NN A -> Disj k e. ( 1 ... n ) A ) )
180	101, 178, 179	sylc 62	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> Disj k e. ( 1 ... n ) A )
181	165, 167, 168, 104, 177, 180	esumrnmpt2 28889	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> Σ* y e. ran ( k e. ( 1 ... n ) |-> A ) ( M ` ( E i^i y ) ) = Σ* k e. ( 1 ... n ) ( M ` ( E i^i A ) ) )
182	153, 163, 181	3eqtrd 2489	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) = Σ* k e. ( 1 ... n ) ( M ` ( E i^i A ) ) )
183	150, 151, 182	3eqtr3rd 2494	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> Σ* k e. ( 1 ... n ) ( M ` ( E i^i A ) ) = ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) )
184	17	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. NN A ) ) e. ( 0 [,] +oo ) )
185	3, 184	sseldi 3430	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. NN A ) ) e. RR* )
186	185	xnegcld 11586	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> -e ( M ` ( E \ U_ k e. NN A ) ) e. RR* )
187	15	adantr 467	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( M ` E ) e. RR* )
188		iunss1 4290	. . . . . . . . . . . 12 |- ( ( 1 ... n ) C_ NN -> U_ k e. ( 1 ... n ) A C_ U_ k e. NN A )
189	100, 188	mp1i 13	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> U_ k e. ( 1 ... n ) A C_ U_ k e. NN A )
190	189	sscond 3570	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( E \ U_ k e. NN A ) C_ ( E \ U_ k e. ( 1 ... n ) A ) )
191	74	3adant1r 1261	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
192	108, 77, 190, 84, 191	carsgmon 29146	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. NN A ) ) <_ ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) )
193		xleneg 11511	. . . . . . . . . 10 |- ( ( ( M ` ( E \ U_ k e. NN A ) ) e. RR* /\ ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* ) -> ( ( M ` ( E \ U_ k e. NN A ) ) <_ ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) <-> -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) <_ -e ( M ` ( E \ U_ k e. NN A ) ) ) )
194	193	biimpa 487	. . . . . . . . 9 |- ( ( ( ( M ` ( E \ U_ k e. NN A ) ) e. RR* /\ ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* ) /\ ( M ` ( E \ U_ k e. NN A ) ) <_ ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) -> -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) <_ -e ( M ` ( E \ U_ k e. NN A ) ) )
195	185, 86, 192, 194	syl21anc 1267	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) <_ -e ( M ` ( E \ U_ k e. NN A ) ) )
196		xleadd2a 11540	. . . . . . . 8 |- ( ( ( -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* /\ -e ( M ` ( E \ U_ k e. NN A ) ) e. RR* /\ ( M ` E ) e. RR* ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) <_ -e ( M ` ( E \ U_ k e. NN A ) ) ) -> ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) )
197	89, 186, 187, 195, 196	syl31anc 1271	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) )
198	183, 197	eqbrtrd 4423	. . . . . 6 |- ( ( ph /\ n e. NN ) -> Σ* k e. ( 1 ... n ) ( M ` ( E i^i A ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) )
199	76, 22, 198	esumgect 28911	. . . . 5 |- ( ph -> Σ* k e. NN ( M ` ( E i^i A ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) )
200	12, 27, 20, 71, 199	xrletrd 11459	. . . 4 |- ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) )
201	2, 200	syl5eqbrr 4437	. . 3 |- ( ph -> ( M ` ( E i^i U_ k e. NN A ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) )
202		xleadd1a 11539	. . 3 |- ( ( ( ( M ` ( E i^i U_ k e. NN A ) ) e. RR* /\ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) e. RR* /\ ( M ` ( E \ U_ k e. NN A ) ) e. RR* ) /\ ( M ` ( E i^i U_ k e. NN A ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) ) -> ( ( M ` ( E i^i U_ k e. NN A ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) <_ ( ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) )
203	13, 20, 18, 201, 202	syl31anc 1271	. 2 |- ( ph -> ( ( M ` ( E i^i U_ k e. NN A ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) <_ ( ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) )
204		xrge0npcan 28457	. . 3 |- ( ( ( M ` E ) e. ( 0 [,] +oo ) /\ ( M ` ( E \ U_ k e. NN A ) ) e. ( 0 [,] +oo ) /\ ( M ` ( E \ U_ k e. NN A ) ) <_ ( M ` E ) ) -> ( ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) = ( M ` E ) )
205	14, 17, 75, 204	syl3anc 1268	. 2 |- ( ph -> ( ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) = ( M ` E ) )
206	203, 205	breqtrd 4427	1 |- ( ph -> ( ( M ` ( E i^i U_ k e. NN A ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) <_ ( M ` E ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   /\ w3a 985   = wceq 1444   e. wcel 1887   =/= wne 2622   A.wral 2737   _Vcvv 3045   \ cdif 3401   i^i cin 3403   C_ wss 3404   (/)c0 3731   ~Pcpw 3951   U.cuni 4198   U_ciun 4278  Disj wdisj 4373   class class class wbr 4402   |-> cmpt 4461   ran crn 4835   -->wf 5578   ` cfv 5582  (class class class)co 6290   omcom 6692   ~<_ cdom 7567   Fincfn 7569   0cc0 9539   1c1 9540   +oocpnf 9672   -oocmnf 9673   RR*cxr 9674   <_ cle 9676   NNcn 10609   -ecxne 11406   +ecxad 11407   [,]cicc 11638   ...cfz 11784  Σ^*cesum 28848  toCaraSigaccarsg 29133

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-inf2 8146  ax-ac2 8893  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617  ax-addf 9618  ax-mulf 9619

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-fal 1450  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-iin 4281  df-disj 4374  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-se 4794  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-isom 5591  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-of 6531  df-om 6693  df-1st 6793  df-2nd 6794  df-supp 6915  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-2o 7183  df-oadd 7186  df-er 7363  df-map 7474  df-pm 7475  df-ixp 7523  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-fsupp 7884  df-fi 7925  df-sup 7956  df-inf 7957  df-oi 8025  df-card 8373  df-acn 8376  df-ac 8547  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-dec 11052  df-uz 11160  df-q 11265  df-rp 11303  df-xneg 11409  df-xadd 11410  df-xmul 11411  df-ioo 11639  df-ioc 11640  df-ico 11641  df-icc 11642  df-fz 11785  df-fzo 11916  df-fl 12028  df-mod 12097  df-seq 12214  df-exp 12273  df-fac 12460  df-bc 12488  df-hash 12516  df-shft 13130  df-cj 13162  df-re 13163  df-im 13164  df-sqrt 13298  df-abs 13299  df-limsup 13526  df-clim 13552  df-rlim 13553  df-sum 13753  df-ef 14121  df-sin 14123  df-cos 14124  df-pi 14126  df-struct 15123  df-ndx 15124  df-slot 15125  df-base 15126  df-sets 15127  df-ress 15128  df-plusg 15203  df-mulr 15204  df-starv 15205  df-sca 15206  df-vsca 15207  df-ip 15208  df-tset 15209  df-ple 15210  df-ds 15212  df-unif 15213  df-hom 15214  df-cco 15215  df-rest 15321  df-topn 15322  df-0g 15340  df-gsum 15341  df-topgen 15342  df-pt 15343  df-prds 15346  df-ordt 15399  df-xrs 15400  df-qtop 15406  df-imas 15407  df-xps 15410  df-mre 15492  df-mrc 15493  df-acs 15495  df-ps 16446  df-tsr 16447  df-plusf 16487  df-mgm 16488  df-sgrp 16527  df-mnd 16537  df-mhm 16582  df-submnd 16583  df-grp 16673  df-minusg 16674  df-sbg 16675  df-mulg 16676  df-subg 16814  df-cntz 16971  df-cmn 17432  df-abl 17433  df-mgp 17724  df-ur 17736  df-ring 17782  df-cring 17783  df-subrg 18006  df-abv 18045  df-lmod 18093  df-scaf 18094  df-sra 18395  df-rgmod 18396  df-psmet 18962  df-xmet 18963  df-met 18964  df-bl 18965  df-mopn 18966  df-fbas 18967  df-fg 18968  df-cnfld 18971  df-top 19921  df-bases 19922  df-topon 19923  df-topsp 19924  df-cld 20034  df-ntr 20035  df-cls 20036  df-nei 20114  df-lp 20152  df-perf 20153  df-cn 20243  df-cnp 20244  df-haus 20331  df-tx 20577  df-hmeo 20770  df-fil 20861  df-fm 20953  df-flim 20954  df-flf 20955  df-tmd 21087  df-tgp 21088  df-tsms 21141  df-trg 21174  df-xms 21335  df-ms 21336  df-tms 21337  df-nm 21597  df-ngp 21598  df-nrg 21600  df-nlm 21601  df-ii 21909  df-cncf 21910  df-limc 22821  df-dv 22822  df-log 23506  df-esum 28849  df-carsg 29134

This theorem is referenced by:  carsgclctunlem3  29152