Theorem ruclem12

Description: Lemma for ruc . The supremum of the increasing sequence 1st o. G is a real number that is not in the range of F . (Contributed by Mario Carneiro, 28-May-2014)

	Ref	Expression
Hypotheses	ruc.1	|- ( ph -> F : NN --> RR )
	ruc.2	|- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )
	ruc.4	|- C = ( { <. 0 , <. 0 , 1 >. >. } u. F )
	ruc.5	|- G = seq 0 ( D , C )
	ruc.6	|- S = sup ( ran ( 1st o. G ) , RR , < )
Assertion	ruclem12	|- ( ph -> S e. ( RR \ ran F ) )

Proof

Step	Hyp	Ref	Expression
1		ruc.1	|- ( ph -> F : NN --> RR )
2		ruc.2	|- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )
3		ruc.4	|- C = ( { <. 0 , <. 0 , 1 >. >. } u. F )
4		ruc.5	|- G = seq 0 ( D , C )
5		ruc.6	|- S = sup ( ran ( 1st o. G ) , RR , < )
6	1 2 3 4	ruclem11	|- ( ph -> ( ran ( 1st o. G ) C_ RR /\ ran ( 1st o. G ) =/= (/) /\ A. z e. ran ( 1st o. G ) z <_ 1 ) )
7	6	simp1d	|- ( ph -> ran ( 1st o. G ) C_ RR )
8	6	simp2d	|- ( ph -> ran ( 1st o. G ) =/= (/) )
9		1re	|- 1 e. RR
10	6	simp3d	|- ( ph -> A. z e. ran ( 1st o. G ) z <_ 1 )
11		brralrspcev	|- ( ( 1 e. RR /\ A. z e. ran ( 1st o. G ) z <_ 1 ) -> E. n e. RR A. z e. ran ( 1st o. G ) z <_ n )
12	9 10 11	sylancr	|- ( ph -> E. n e. RR A. z e. ran ( 1st o. G ) z <_ n )
13	7 8 12	suprcld	|- ( ph -> sup ( ran ( 1st o. G ) , RR , < ) e. RR )
14	5 13	eqeltrid	|- ( ph -> S e. RR )
15	1	adantr	|- ( ( ph /\ n e. NN ) -> F : NN --> RR )
16	2	adantr	|- ( ( ph /\ n e. NN ) -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )
17	1 2 3 4	ruclem6	|- ( ph -> G : NN0 --> ( RR X. RR ) )
18		nnm1nn0	|- ( n e. NN -> ( n - 1 ) e. NN0 )
19		ffvelrn	|- ( ( G : NN0 --> ( RR X. RR ) /\ ( n - 1 ) e. NN0 ) -> ( G ` ( n - 1 ) ) e. ( RR X. RR ) )
20	17 18 19	syl2an	|- ( ( ph /\ n e. NN ) -> ( G ` ( n - 1 ) ) e. ( RR X. RR ) )
21		xp1st	|- ( ( G ` ( n - 1 ) ) e. ( RR X. RR ) -> ( 1st ` ( G ` ( n - 1 ) ) ) e. RR )
22	20 21	syl	|- ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` ( n - 1 ) ) ) e. RR )
23		xp2nd	|- ( ( G ` ( n - 1 ) ) e. ( RR X. RR ) -> ( 2nd ` ( G ` ( n - 1 ) ) ) e. RR )
24	20 23	syl	|- ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` ( n - 1 ) ) ) e. RR )
25	1	ffvelrnda	|- ( ( ph /\ n e. NN ) -> ( F ` n ) e. RR )
26		eqid	|- ( 1st ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) = ( 1st ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) )
27		eqid	|- ( 2nd ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) = ( 2nd ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) )
28	1 2 3 4	ruclem8	|- ( ( ph /\ ( n - 1 ) e. NN0 ) -> ( 1st ` ( G ` ( n - 1 ) ) ) < ( 2nd ` ( G ` ( n - 1 ) ) ) )
29	18 28	sylan2	|- ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` ( n - 1 ) ) ) < ( 2nd ` ( G ` ( n - 1 ) ) ) )
30	15 16 22 24 25 26 27 29	ruclem3	|- ( ( ph /\ n e. NN ) -> ( ( F ` n ) < ( 1st ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) \/ ( 2nd ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) < ( F ` n ) ) )
31	1 2 3 4	ruclem7	|- ( ( ph /\ ( n - 1 ) e. NN0 ) -> ( G ` ( ( n - 1 ) + 1 ) ) = ( ( G ` ( n - 1 ) ) D ( F ` ( ( n - 1 ) + 1 ) ) ) )
32	18 31	sylan2	|- ( ( ph /\ n e. NN ) -> ( G ` ( ( n - 1 ) + 1 ) ) = ( ( G ` ( n - 1 ) ) D ( F ` ( ( n - 1 ) + 1 ) ) ) )
33		nncn	|- ( n e. NN -> n e. CC )
34	33	adantl	|- ( ( ph /\ n e. NN ) -> n e. CC )
35		ax-1cn	|- 1 e. CC
36		npcan	|- ( ( n e. CC /\ 1 e. CC ) -> ( ( n - 1 ) + 1 ) = n )
37	34 35 36	sylancl	|- ( ( ph /\ n e. NN ) -> ( ( n - 1 ) + 1 ) = n )
38	37	fveq2d	|- ( ( ph /\ n e. NN ) -> ( G ` ( ( n - 1 ) + 1 ) ) = ( G ` n ) )
39		1st2nd2	|- ( ( G ` ( n - 1 ) ) e. ( RR X. RR ) -> ( G ` ( n - 1 ) ) = <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. )
40	20 39	syl	|- ( ( ph /\ n e. NN ) -> ( G ` ( n - 1 ) ) = <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. )
41	37	fveq2d	|- ( ( ph /\ n e. NN ) -> ( F ` ( ( n - 1 ) + 1 ) ) = ( F ` n ) )
42	40 41	oveq12d	|- ( ( ph /\ n e. NN ) -> ( ( G ` ( n - 1 ) ) D ( F ` ( ( n - 1 ) + 1 ) ) ) = ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) )
43	32 38 42	3eqtr3d	|- ( ( ph /\ n e. NN ) -> ( G ` n ) = ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) )
44	43	fveq2d	|- ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) = ( 1st ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) )
45	44	breq2d	|- ( ( ph /\ n e. NN ) -> ( ( F ` n ) < ( 1st ` ( G ` n ) ) <-> ( F ` n ) < ( 1st ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) ) )
46	43	fveq2d	|- ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = ( 2nd ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) )
47	46	breq1d	|- ( ( ph /\ n e. NN ) -> ( ( 2nd ` ( G ` n ) ) < ( F ` n ) <-> ( 2nd ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) < ( F ` n ) ) )
48	45 47	orbi12d	|- ( ( ph /\ n e. NN ) -> ( ( ( F ` n ) < ( 1st ` ( G ` n ) ) \/ ( 2nd ` ( G ` n ) ) < ( F ` n ) ) <-> ( ( F ` n ) < ( 1st ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) \/ ( 2nd ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) < ( F ` n ) ) ) )
49	30 48	mpbird	|- ( ( ph /\ n e. NN ) -> ( ( F ` n ) < ( 1st ` ( G ` n ) ) \/ ( 2nd ` ( G ` n ) ) < ( F ` n ) ) )
50	7	adantr	|- ( ( ph /\ n e. NN ) -> ran ( 1st o. G ) C_ RR )
51	8	adantr	|- ( ( ph /\ n e. NN ) -> ran ( 1st o. G ) =/= (/) )
52	12	adantr	|- ( ( ph /\ n e. NN ) -> E. n e. RR A. z e. ran ( 1st o. G ) z <_ n )
53		nnnn0	|- ( n e. NN -> n e. NN0 )
54		fvco3	|- ( ( G : NN0 --> ( RR X. RR ) /\ n e. NN0 ) -> ( ( 1st o. G ) ` n ) = ( 1st ` ( G ` n ) ) )
55	17 53 54	syl2an	|- ( ( ph /\ n e. NN ) -> ( ( 1st o. G ) ` n ) = ( 1st ` ( G ` n ) ) )
56	17	adantr	|- ( ( ph /\ n e. NN ) -> G : NN0 --> ( RR X. RR ) )
57		1stcof	|- ( G : NN0 --> ( RR X. RR ) -> ( 1st o. G ) : NN0 --> RR )
58		ffn	|- ( ( 1st o. G ) : NN0 --> RR -> ( 1st o. G ) Fn NN0 )
59	56 57 58	3syl	|- ( ( ph /\ n e. NN ) -> ( 1st o. G ) Fn NN0 )
60	53	adantl	|- ( ( ph /\ n e. NN ) -> n e. NN0 )
61		fnfvelrn	|- ( ( ( 1st o. G ) Fn NN0 /\ n e. NN0 ) -> ( ( 1st o. G ) ` n ) e. ran ( 1st o. G ) )
62	59 60 61	syl2anc	|- ( ( ph /\ n e. NN ) -> ( ( 1st o. G ) ` n ) e. ran ( 1st o. G ) )
63	55 62	eqeltrrd	|- ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) e. ran ( 1st o. G ) )
64	50 51 52 63	suprubd	|- ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) <_ sup ( ran ( 1st o. G ) , RR , < ) )
65	64 5	breqtrrdi	|- ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) <_ S )
66		ffvelrn	|- ( ( G : NN0 --> ( RR X. RR ) /\ n e. NN0 ) -> ( G ` n ) e. ( RR X. RR ) )
67	17 53 66	syl2an	|- ( ( ph /\ n e. NN ) -> ( G ` n ) e. ( RR X. RR ) )
68		xp1st	|- ( ( G ` n ) e. ( RR X. RR ) -> ( 1st ` ( G ` n ) ) e. RR )
69	67 68	syl	|- ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) e. RR )
70	14	adantr	|- ( ( ph /\ n e. NN ) -> S e. RR )
71		ltletr	|- ( ( ( F ` n ) e. RR /\ ( 1st ` ( G ` n ) ) e. RR /\ S e. RR ) -> ( ( ( F ` n ) < ( 1st ` ( G ` n ) ) /\ ( 1st ` ( G ` n ) ) <_ S ) -> ( F ` n ) < S ) )
72	25 69 70 71	syl3anc	|- ( ( ph /\ n e. NN ) -> ( ( ( F ` n ) < ( 1st ` ( G ` n ) ) /\ ( 1st ` ( G ` n ) ) <_ S ) -> ( F ` n ) < S ) )
73	65 72	mpan2d	|- ( ( ph /\ n e. NN ) -> ( ( F ` n ) < ( 1st ` ( G ` n ) ) -> ( F ` n ) < S ) )
74		fvco3	|- ( ( G : NN0 --> ( RR X. RR ) /\ k e. NN0 ) -> ( ( 1st o. G ) ` k ) = ( 1st ` ( G ` k ) ) )
75	56 74	sylan	|- ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> ( ( 1st o. G ) ` k ) = ( 1st ` ( G ` k ) ) )
76	56	ffvelrnda	|- ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> ( G ` k ) e. ( RR X. RR ) )
77		xp1st	|- ( ( G ` k ) e. ( RR X. RR ) -> ( 1st ` ( G ` k ) ) e. RR )
78	76 77	syl	|- ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> ( 1st ` ( G ` k ) ) e. RR )
79		xp2nd	|- ( ( G ` n ) e. ( RR X. RR ) -> ( 2nd ` ( G ` n ) ) e. RR )
80	67 79	syl	|- ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) e. RR )
81	80	adantr	|- ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> ( 2nd ` ( G ` n ) ) e. RR )
82	15	adantr	|- ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> F : NN --> RR )
83	16	adantr	|- ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )
84		simpr	|- ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> k e. NN0 )
85	60	adantr	|- ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> n e. NN0 )
86	82 83 3 4 84 85	ruclem10	|- ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> ( 1st ` ( G ` k ) ) < ( 2nd ` ( G ` n ) ) )
87	78 81 86	ltled	|- ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> ( 1st ` ( G ` k ) ) <_ ( 2nd ` ( G ` n ) ) )
88	75 87	eqbrtrd	|- ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> ( ( 1st o. G ) ` k ) <_ ( 2nd ` ( G ` n ) ) )
89	88	ralrimiva	|- ( ( ph /\ n e. NN ) -> A. k e. NN0 ( ( 1st o. G ) ` k ) <_ ( 2nd ` ( G ` n ) ) )
90		breq1	|- ( z = ( ( 1st o. G ) ` k ) -> ( z <_ ( 2nd ` ( G ` n ) ) <-> ( ( 1st o. G ) ` k ) <_ ( 2nd ` ( G ` n ) ) ) )
91	90	ralrn	|- ( ( 1st o. G ) Fn NN0 -> ( A. z e. ran ( 1st o. G ) z <_ ( 2nd ` ( G ` n ) ) <-> A. k e. NN0 ( ( 1st o. G ) ` k ) <_ ( 2nd ` ( G ` n ) ) ) )
92	59 91	syl	|- ( ( ph /\ n e. NN ) -> ( A. z e. ran ( 1st o. G ) z <_ ( 2nd ` ( G ` n ) ) <-> A. k e. NN0 ( ( 1st o. G ) ` k ) <_ ( 2nd ` ( G ` n ) ) ) )
93	89 92	mpbird	|- ( ( ph /\ n e. NN ) -> A. z e. ran ( 1st o. G ) z <_ ( 2nd ` ( G ` n ) ) )
94		suprleub	|- ( ( ( ran ( 1st o. G ) C_ RR /\ ran ( 1st o. G ) =/= (/) /\ E. n e. RR A. z e. ran ( 1st o. G ) z <_ n ) /\ ( 2nd ` ( G ` n ) ) e. RR ) -> ( sup ( ran ( 1st o. G ) , RR , < ) <_ ( 2nd ` ( G ` n ) ) <-> A. z e. ran ( 1st o. G ) z <_ ( 2nd ` ( G ` n ) ) ) )
95	50 51 52 80 94	syl31anc	|- ( ( ph /\ n e. NN ) -> ( sup ( ran ( 1st o. G ) , RR , < ) <_ ( 2nd ` ( G ` n ) ) <-> A. z e. ran ( 1st o. G ) z <_ ( 2nd ` ( G ` n ) ) ) )
96	93 95	mpbird	|- ( ( ph /\ n e. NN ) -> sup ( ran ( 1st o. G ) , RR , < ) <_ ( 2nd ` ( G ` n ) ) )
97	5 96	eqbrtrid	|- ( ( ph /\ n e. NN ) -> S <_ ( 2nd ` ( G ` n ) ) )
98		lelttr	|- ( ( S e. RR /\ ( 2nd ` ( G ` n ) ) e. RR /\ ( F ` n ) e. RR ) -> ( ( S <_ ( 2nd ` ( G ` n ) ) /\ ( 2nd ` ( G ` n ) ) < ( F ` n ) ) -> S < ( F ` n ) ) )
99	70 80 25 98	syl3anc	|- ( ( ph /\ n e. NN ) -> ( ( S <_ ( 2nd ` ( G ` n ) ) /\ ( 2nd ` ( G ` n ) ) < ( F ` n ) ) -> S < ( F ` n ) ) )
100	97 99	mpand	|- ( ( ph /\ n e. NN ) -> ( ( 2nd ` ( G ` n ) ) < ( F ` n ) -> S < ( F ` n ) ) )
101	73 100	orim12d	|- ( ( ph /\ n e. NN ) -> ( ( ( F ` n ) < ( 1st ` ( G ` n ) ) \/ ( 2nd ` ( G ` n ) ) < ( F ` n ) ) -> ( ( F ` n ) < S \/ S < ( F ` n ) ) ) )
102	49 101	mpd	|- ( ( ph /\ n e. NN ) -> ( ( F ` n ) < S \/ S < ( F ` n ) ) )
103	25 70	lttri2d	|- ( ( ph /\ n e. NN ) -> ( ( F ` n ) =/= S <-> ( ( F ` n ) < S \/ S < ( F ` n ) ) ) )
104	102 103	mpbird	|- ( ( ph /\ n e. NN ) -> ( F ` n ) =/= S )
105	104	neneqd	|- ( ( ph /\ n e. NN ) -> -. ( F ` n ) = S )
106	105	nrexdv	|- ( ph -> -. E. n e. NN ( F ` n ) = S )
107		risset	|- ( S e. ran F <-> E. z e. ran F z = S )
108		ffn	|- ( F : NN --> RR -> F Fn NN )
109		eqeq1	|- ( z = ( F ` n ) -> ( z = S <-> ( F ` n ) = S ) )
110	109	rexrn	|- ( F Fn NN -> ( E. z e. ran F z = S <-> E. n e. NN ( F ` n ) = S ) )
111	1 108 110	3syl	|- ( ph -> ( E. z e. ran F z = S <-> E. n e. NN ( F ` n ) = S ) )
112	107 111	syl5bb	|- ( ph -> ( S e. ran F <-> E. n e. NN ( F ` n ) = S ) )
113	106 112	mtbird	|- ( ph -> -. S e. ran F )
114	14 113	eldifd	|- ( ph -> S e. ( RR \ ran F ) )