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	$⊢ φ \to F : ℕ ⟶ ℝ$
	ruc.2	$⊢ φ \to D = (x \in ℝ^{2}, y \in ℝ ⟼ ⦋ (\frac{1^{st} (x) + 2^{nd} (x)}{2}) / m ⦌ if (m < y, ⟨1^{st} (x), m⟩, ⟨\frac{m + 2^{nd} (x)}{2}, 2^{nd} (x)⟩))$
	ruc.4	$⊢ C = \{⟨0, ⟨0, 1⟩⟩\} \cup F$
	ruc.5	$⊢ G = seq 0 (D, C)$
	ruc.6	$⊢ S = sup (ran (1^{st} \circ G) ℝ <)$
Assertion	ruclem12	$⊢ φ \to S \in (ℝ ∖ ran F)$

Proof

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

Metamath Proof Explorer

Theorem ruclem12

Proof