Theorem carsgclctunlem2 28527

Description: Lemma for carsgclctun 28529. (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 4379	. . . . 5 |- U_ k e. NN ( E i^i A ) = ( E i^i U_ k e. NN A )
2	1	fveq2i 5851	. . . 4 |- ( M ` U_ k e. NN ( E i^i A ) ) = ( M ` ( E i^i U_ k e. NN A ) )
3		iccssxr 11610	. . . . 5 |- ( 0 [,] +oo ) C_ RR*
4		carsgval.2	. . . . . 6 |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
5		nnex 10537	. . . . . . . 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 463	. . . . . . . 8 |- ( ( ph /\ k e. NN ) -> E e. ~P O )
9	8	elpwincl1 27620	. . . . . . 7 |- ( ( ph /\ k e. NN ) -> ( E i^i A ) e. ~P O )
10	6, 9	elpwiuncl 27622	. . . . . 6 |- ( ph -> U_ k e. NN ( E i^i A ) e. ~P O )
11	4, 10	ffvelrnd 6008	. . . . 5 |- ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) e. ( 0 [,] +oo ) )
12	3, 11	sseldi 3487	. . . 4 |- ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) e. RR* )
13	2, 12	syl5eqelr 2547	. . 3 |- ( ph -> ( M ` ( E i^i U_ k e. NN A ) ) e. RR* )
14	4, 7	ffvelrnd 6008	. . . . 5 |- ( ph -> ( M ` E ) e. ( 0 [,] +oo ) )
15	3, 14	sseldi 3487	. . . 4 |- ( ph -> ( M ` E ) e. RR* )
16	7	elpwdifcl 27621	. . . . . . 7 |- ( ph -> ( E \ U_ k e. NN A ) e. ~P O )
17	4, 16	ffvelrnd 6008	. . . . . 6 |- ( ph -> ( M ` ( E \ U_ k e. NN A ) ) e. ( 0 [,] +oo ) )
18	3, 17	sseldi 3487	. . . . 5 |- ( ph -> ( M ` ( E \ U_ k e. NN A ) ) e. RR* )
19	18	xnegcld 11495	. . . 4 |- ( ph -> -e ( M ` ( E \ U_ k e. NN A ) ) e. RR* )
20	15, 19	xaddcld 11496	. . 3 |- ( ph -> ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) e. RR* )
21	4	adantr 463	. . . . . . . . 9 |- ( ( ph /\ k e. NN ) -> M : ~P O --> ( 0 [,] +oo ) )
22	21, 9	ffvelrnd 6008	. . . . . . . 8 |- ( ( ph /\ k e. NN ) -> ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) )
23	22	ralrimiva 2868	. . . . . . 7 |- ( ph -> A. k e. NN ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) )
24		nfcv 2616	. . . . . . . 8 |- F/_ k NN
25	24	esumcl 28259	. . . . . . 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 659	. . . . . 6 |- ( ph -> Σ* k e. NN ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) )
27	3, 26	sseldi 3487	. . . . 5 |- ( ph -> Σ* k e. NN ( M ` ( E i^i A ) ) e. RR* )
28	9	ralrimiva 2868	. . . . . . . . 9 |- ( ph -> A. k e. NN ( E i^i A ) e. ~P O )
29		dfiun3g 5244	. . . . . . . . 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 16	. . . . . . . 8 |- ( ph -> U_ k e. NN ( E i^i A ) = U. ran ( k e. NN |-> ( E i^i A ) ) )
31	30	fveq2d 5852	. . . . . . 7 |- ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) = ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) )
32		nnct 27759	. . . . . . . . . 10 |- NN ~<_ om
33		mptct 27771	. . . . . . . . . 10 |- ( NN ~<_ om -> ( k e. NN |-> ( E i^i A ) ) ~<_ om )
34		rnct 27769	. . . . . . . . . 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 2454	. . . . . . . . . 10 |- ( k e. NN |-> ( E i^i A ) ) = ( k e. NN |-> ( E i^i A ) )
38	37	rnmptss 6036	. . . . . . . . 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 16	. . . . . . . 8 |- ( ph -> ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O )
40		mptexg 6117	. . . . . . . . . 10 |- ( NN e. _V -> ( k e. NN |-> ( E i^i A ) ) e. _V )
41		rnexg 6705	. . . . . . . . . 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 4442	. . . . . . . . . . . 12 |- ( x = ran ( k e. NN |-> ( E i^i A ) ) -> ( x ~<_ om <-> ran ( k e. NN |-> ( E i^i A ) ) ~<_ om ) )
44		sseq1 3510	. . . . . . . . . . . 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 1300	. . . . . . . . . . 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 4243	. . . . . . . . . . . . 13 |- ( x = ran ( k e. NN |-> ( E i^i A ) ) -> U. x = U. ran ( k e. NN |-> ( E i^i A ) ) )
47	46	fveq2d 5852	. . . . . . . . . . . 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 28263	. . . . . . . . . . . 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 4452	. . . . . . . . . . 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 318	. . . . . . . . . 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 3164	. . . . . . . . 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 1324	. . . . . . 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 4459	. . . . . 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 5848	. . . . . . 7 |- ( y = ( E i^i A ) -> ( M ` y ) = ( M ` ( E i^i A ) ) )
57		simpr 459	. . . . . . . . 9 |- ( ( ( ph /\ k e. NN ) /\ ( E i^i A ) = (/) ) -> ( E i^i A ) = (/) )
58	57	fveq2d 5852	. . . . . . . 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 723	. . . . . . . 8 |- ( ( ( ph /\ k e. NN ) /\ ( E i^i A ) = (/) ) -> ( M ` (/) ) = 0 )
61	58, 60	eqtrd 2495	. . . . . . 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 27657	. . . . . . . . 9 |- (Disj k e. NN A -> Disj k e. NN ( A i^i E ) )
64	62, 63	syl 16	. . . . . . . 8 |- ( ph -> Disj k e. NN ( A i^i E ) )
65		incom 3677	. . . . . . . . . 10 |- ( A i^i E ) = ( E i^i A )
66	65	rgenw 2815	. . . . . . . . 9 |- A. k e. NN ( A i^i E ) = ( E i^i A )
67		disjeq2 4414	. . . . . . . . 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 196	. . . . . . 7 |- ( ph -> Disj k e. NN ( E i^i A ) )
70	56, 6, 22, 9, 61, 69	esumrnmpt2 28297	. . . . . 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 4463	. . . . 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 3618	. . . . . . . 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 28522	. . . . . . 7 |- ( ph -> ( M ` ( E \ U_ k e. NN A ) ) <_ ( M ` E ) )
76	14, 17, 75	xrge0subcld 27814	. . . . . 6 |- ( ph -> ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) e. ( 0 [,] +oo ) )
77	4	adantr 463	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> M : ~P O --> ( 0 [,] +oo ) )
78	7	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> E e. ~P O )
79	78	elpwincl1 27620	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( E i^i U_ k e. ( 1 ... n ) A ) e. ~P O )
80	77, 79	ffvelrnd 6008	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) e. ( 0 [,] +oo ) )
81	3, 80	sseldi 3487	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) e. RR* )
82		xrge0neqmnf 27913	. . . . . . . . . . 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 16	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) =/= -oo )
84	78	elpwdifcl 27621	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( E \ U_ k e. ( 1 ... n ) A ) e. ~P O )
85	77, 84	ffvelrnd 6008	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. ( 0 [,] +oo ) )
86	3, 85	sseldi 3487	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* )
87		xrge0neqmnf 27913	. . . . . . . . . . 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 16	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) =/= -oo )
89	86	xnegcld 11495	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* )
90		xnegneg 11416	. . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . 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 11409	. . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . 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 11412	. . . . . . . . . . . . . . . 16 |- -e -oo = +oo
96	94, 95	syl6eq 2511	. . . . . . . . . . . . . . 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 2497	. . . . . . . . . . . . . 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 6286	. . . . . . . . . . . . 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 751	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ph )
100		fz1ssnn 11719	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 1 ... n ) C_ NN
101	100	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ n e. NN ) -> ( 1 ... n ) C_ NN )
102	101	sselda 3489	. . . . . . . . . . . . . . . . . . . . 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 659	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> A e. (toCaraSiga ` M ) )
105	104	ralrimiva 2868	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. NN ) -> A. k e. ( 1 ... n ) A e. (toCaraSiga ` M ) )
106		dfiun3g 5244	. . . . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. NN ) -> U_ k e. ( 1 ... n ) A = U. ran ( k e. ( 1 ... n ) |-> A ) )
108	72	adantr 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. NN ) -> O e. V )
109	59	adantr 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. NN ) -> ( M ` (/) ) = 0 )
110	51	3adant1r 1219	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )
111		fzfi 12064	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 ... n ) e. Fin
112		mptfi 7811	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 1 ... n ) e. Fin -> ( k e. ( 1 ... n ) |-> A ) e. Fin )
113		rnfi 7797	. . . . . . . . . . . . . . . . . . . . 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 2454	. . . . . . . . . . . . . . . . . . . . 21 |- ( k e. ( 1 ... n ) |-> A ) = ( k e. ( 1 ... n ) |-> A )
117	116	rnmptss 6036	. . . . . . . . . . . . . . . . . . . 20 |- ( A. k e. ( 1 ... n ) A e. (toCaraSiga ` M ) -> ran ( k e. ( 1 ... n ) |-> A ) C_ (toCaraSiga ` M ) )
118	105, 117	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. NN ) -> ran ( k e. ( 1 ... n ) |-> A ) C_ (toCaraSiga ` M ) )
119	108, 77, 109, 110, 115, 118	fiunelcarsg 28524	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. NN ) -> U. ran ( k e. ( 1 ... n ) |-> A ) e. (toCaraSiga ` M ) )
120	107, 119	eqeltrd 2542	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. NN ) -> U_ k e. ( 1 ... n ) A e. (toCaraSiga ` M ) )
121	108, 77	elcarsg 28513	. . . . . . . . . . . . . . . . 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 210	. . . . . . . . . . . . . . . 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 461	. . . . . . . . . . . . . . 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 3679	. . . . . . . . . . . . . . . . . . 19 |- ( e = E -> ( e i^i U_ k e. ( 1 ... n ) A ) = ( E i^i U_ k e. ( 1 ... n ) A ) )
125	124	fveq2d 5852	. . . . . . . . . . . . . . . . . 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 3601	. . . . . . . . . . . . . . . . . . 19 |- ( e = E -> ( e \ U_ k e. ( 1 ... n ) A ) = ( E \ U_ k e. ( 1 ... n ) A ) )
127	126	fveq2d 5852	. . . . . . . . . . . . . . . . . 18 |- ( e = E -> ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) = ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) )
128	125, 127	oveq12d 6288	. . . . . . . . . . . . . . . . 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 5848	. . . . . . . . . . . . . . . . 17 |- ( e = E -> ( M ` e ) = ( M ` E ) )
130	128, 129	eqeq12d 2476	. . . . . . . . . . . . . . . 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 3203	. . . . . . . . . . . . . . 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 60	. . . . . . . . . . . . . 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 463	. . . . . . . . . . . . 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 11428	. . . . . . . . . . . . . . 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 659	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. NN ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e +oo ) = +oo )
136	135	adantr 463	. . . . . . . . . . . . 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 2503	. . . . . . . . . . . 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 723	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> ( M ` E ) =/= +oo )
140	139	neneqd 2656	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> -. ( M ` E ) = +oo )
141	137, 140	pm2.65da 574	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> -. -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo )
142	141	neqned 2657	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) =/= -oo )
143		xaddass 11444	. . . . . . . . . 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 1242	. . . . . . . . 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 11438	. . . . . . . . . . 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 16	. . . . . . . . . 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 6286	. . . . . . . . 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 11441	. . . . . . . . . 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 16	. . . . . . . . 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 2499	. . . . . . . 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 6285	. . . . . . . 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 3686	. . . . . . . . . 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 5852	. . . . . . . . 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 27743	. . . . . . . . . . . . 13 |- ( ( 1 ... n ) C_ NN -> ( k e. ( 1 ... n ) |-> A ) C_ ( k e. NN |-> A ) )
155		rnss 5220	. . . . . . . . . . . . 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 27656	. . . . . . . . . . . . 13 |- (Disj k e. NN A -> Disj y e. ran ( k e. NN |-> A ) y )
159	62, 158	syl 16	. . . . . . . . . . . 12 |- ( ph -> Disj y e. ran ( k e. NN |-> A ) y )
160	159	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> Disj y e. ran ( k e. NN |-> A ) y )
161		disjss1 4416	. . . . . . . . . . 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 60	. . . . . . . . . 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 28525	. . . . . . . . 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 3680	. . . . . . . . . . 11 |- ( y = A -> ( E i^i y ) = ( E i^i A ) )
165	164	fveq2d 5852	. . . . . . . . . 10 |- ( y = A -> ( M ` ( E i^i y ) ) = ( M ` ( E i^i A ) ) )
166	111	elexi 3116	. . . . . . . . . . 11 |- ( 1 ... n ) e. _V
167	166	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( 1 ... n ) e. _V )
168	99, 102, 22	syl2anc 659	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) )
169		inss2 3705	. . . . . . . . . . . . . . 15 |- ( E i^i A ) C_ A
170		sseq2 3511	. . . . . . . . . . . . . . 15 |- ( A = (/) -> ( ( E i^i A ) C_ A <-> ( E i^i A ) C_ (/) ) )
171	169, 170	mpbii 211	. . . . . . . . . . . . . 14 |- ( A = (/) -> ( E i^i A ) C_ (/) )
172		ss0 3815	. . . . . . . . . . . . . 14 |- ( ( E i^i A ) C_ (/) -> ( E i^i A ) = (/) )
173	171, 172	syl 16	. . . . . . . . . . . . 13 |- ( A = (/) -> ( E i^i A ) = (/) )
174	173	adantl 464	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ A = (/) ) -> ( E i^i A ) = (/) )
175	174	fveq2d 5852	. . . . . . . . . . 11 |- ( ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ A = (/) ) -> ( M ` ( E i^i A ) ) = ( M ` (/) ) )
176	109	ad2antrr 723	. . . . . . . . . . 11 |- ( ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ A = (/) ) -> ( M ` (/) ) = 0 )
177	175, 176	eqtrd 2495	. . . . . . . . . 10 |- ( ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ A = (/) ) -> ( M ` ( E i^i A ) ) = 0 )
178	62	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> Disj k e. NN A )
179		disjss1 4416	. . . . . . . . . . 11 |- ( ( 1 ... n ) C_ NN -> (Disj k e. NN A -> Disj k e. ( 1 ... n ) A ) )
180	101, 178, 179	sylc 60	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> Disj k e. ( 1 ... n ) A )
181	165, 167, 168, 104, 177, 180	esumrnmpt2 28297	. . . . . . . . 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 2499	. . . . . . . 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 2504	. . . . . . 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 463	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. NN A ) ) e. ( 0 [,] +oo ) )
185	3, 184	sseldi 3487	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. NN A ) ) e. RR* )
186	185	xnegcld 11495	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> -e ( M ` ( E \ U_ k e. NN A ) ) e. RR* )
187	15	adantr 463	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( M ` E ) e. RR* )
188		iunss1 4327	. . . . . . . . . . . 12 |- ( ( 1 ... n ) C_ NN -> U_ k e. ( 1 ... n ) A C_ U_ k e. NN A )
189	100, 188	mp1i 12	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> U_ k e. ( 1 ... n ) A C_ U_ k e. NN A )
190	189	sscond 3627	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( E \ U_ k e. NN A ) C_ ( E \ U_ k e. ( 1 ... n ) A ) )
191	74	3adant1r 1219	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
192	108, 77, 190, 84, 191	carsgmon 28522	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. NN A ) ) <_ ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) )
193		xleneg 11420	. . . . . . . . . 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 482	. . . . . . . . 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 1225	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) <_ -e ( M ` ( E \ U_ k e. NN A ) ) )
196		xleadd2a 11449	. . . . . . . 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 1229	. . . . . . 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 4459	. . . . . 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 28319	. . . . 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 11368	. . . 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 4473	. . 3 |- ( ph -> ( M ` ( E i^i U_ k e. NN A ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) )
202		xleadd1a 11448	. . 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 1229	. 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 27918	. . 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 1226	. 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 4463	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 184   /\ wa 367   /\ w3a 971   = wceq 1398   e. wcel 1823   =/= wne 2649   A.wral 2804   _Vcvv 3106   \ cdif 3458   i^i cin 3460   C_ wss 3461   (/)c0 3783   ~Pcpw 3999   U.cuni 4235   U_ciun 4315  Disj wdisj 4410   class class class wbr 4439   |-> cmpt 4497   ran crn 4989   -->wf 5566   ` cfv 5570  (class class class)co 6270   omcom 6673   ~<_ cdom 7507   Fincfn 7509   0cc0 9481   1c1 9482   +oocpnf 9614   -oocmnf 9615   RR*cxr 9616   <_ cle 9618   NNcn 10531   -ecxne 11318   +ecxad 11319   [,]cicc 11535   ...cfz 11675  Σ^*cesum 28256  toCaraSigaccarsg 28509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-inf2 8049  ax-ac2 8834  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558  ax-pre-sup 9559  ax-addf 9560  ax-mulf 9561

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-fal 1404  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-iin 4318  df-disj 4411  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-se 4828  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-isom 5579  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-of 6513  df-om 6674  df-1st 6773  df-2nd 6774  df-supp 6892  df-recs 7034  df-rdg 7068  df-1o 7122  df-2o 7123  df-oadd 7126  df-er 7303  df-map 7414  df-pm 7415  df-ixp 7463  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513  df-fsupp 7822  df-fi 7863  df-sup 7893  df-oi 7927  df-card 8311  df-acn 8314  df-ac 8488  df-cda 8539  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-div 10203  df-nn 10532  df-2 10590  df-3 10591  df-4 10592  df-5 10593  df-6 10594  df-7 10595  df-8 10596  df-9 10597  df-10 10598  df-n0 10792  df-z 10861  df-dec 10977  df-uz 11083  df-q 11184  df-rp 11222  df-xneg 11321  df-xadd 11322  df-xmul 11323  df-ioo 11536  df-ioc 11537  df-ico 11538  df-icc 11539  df-fz 11676  df-fzo 11800  df-fl 11910  df-mod 11979  df-seq 12090  df-exp 12149  df-fac 12336  df-bc 12363  df-hash 12388  df-shft 12982  df-cj 13014  df-re 13015  df-im 13016  df-sqrt 13150  df-abs 13151  df-limsup 13376  df-clim 13393  df-rlim 13394  df-sum 13591  df-ef 13885  df-sin 13887  df-cos 13888  df-pi 13890  df-struct 14718  df-ndx 14719  df-slot 14720  df-base 14721  df-sets 14722  df-ress 14723  df-plusg 14797  df-mulr 14798  df-starv 14799  df-sca 14800  df-vsca 14801  df-ip 14802  df-tset 14803  df-ple 14804  df-ds 14806  df-unif 14807  df-hom 14808  df-cco 14809  df-rest 14912  df-topn 14913  df-0g 14931  df-gsum 14932  df-topgen 14933  df-pt 14934  df-prds 14937  df-ordt 14990  df-xrs 14991  df-qtop 14996  df-imas 14997  df-xps 14999  df-mre 15075  df-mrc 15076  df-acs 15078  df-ps 16029  df-tsr 16030  df-plusf 16070  df-mgm 16071  df-sgrp 16110  df-mnd 16120  df-mhm 16165  df-submnd 16166  df-grp 16256  df-minusg 16257  df-sbg 16258  df-mulg 16259  df-subg 16397  df-cntz 16554  df-cmn 16999  df-abl 17000  df-mgp 17337  df-ur 17349  df-ring 17395  df-cring 17396  df-subrg 17622  df-abv 17661  df-lmod 17709  df-scaf 17710  df-sra 18013  df-rgmod 18014  df-psmet 18606  df-xmet 18607  df-met 18608  df-bl 18609  df-mopn 18610  df-fbas 18611  df-fg 18612  df-cnfld 18616  df-top 19566  df-bases 19568  df-topon 19569  df-topsp 19570  df-cld 19687  df-ntr 19688  df-cls 19689  df-nei 19766  df-lp 19804  df-perf 19805  df-cn 19895  df-cnp 19896  df-haus 19983  df-tx 20229  df-hmeo 20422  df-fil 20513  df-fm 20605  df-flim 20606  df-flf 20607  df-tmd 20737  df-tgp 20738  df-tsms 20791  df-trg 20828  df-xms 20989  df-ms 20990  df-tms 20991  df-nm 21269  df-ngp 21270  df-nrg 21272  df-nlm 21273  df-ii 21547  df-cncf 21548  df-limc 22436  df-dv 22437  df-log 23110  df-esum 28257  df-carsg 28510

This theorem is referenced by:  carsgclctunlem3  28528