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	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
	ruc.2	⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1^st ‘ 𝑥 ) + ( 2^nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1^st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2^nd ‘ 𝑥 ) ) / 2 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) ) )
	ruc.4	⊢ 𝐶 = ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 )
	ruc.5	⊢ 𝐺 = seq 0 ( 𝐷 , 𝐶 )
	ruc.6	⊢ 𝑆 = sup ( ran ( 1^st ∘ 𝐺 ) , ℝ , < )
Assertion	ruclem12	⊢ ( 𝜑 → 𝑆 ∈ ( ℝ ∖ ran 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		ruc.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
2		ruc.2	⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1^st ‘ 𝑥 ) + ( 2^nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1^st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2^nd ‘ 𝑥 ) ) / 2 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) ) )
3		ruc.4	⊢ 𝐶 = ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 )
4		ruc.5	⊢ 𝐺 = seq 0 ( 𝐷 , 𝐶 )
5		ruc.6	⊢ 𝑆 = sup ( ran ( 1^st ∘ 𝐺 ) , ℝ , < )
6	1 2 3 4	ruclem11	⊢ ( 𝜑 → ( ran ( 1^st ∘ 𝐺 ) ⊆ ℝ ∧ ran ( 1^st ∘ 𝐺 ) ≠ ∅ ∧ ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ 1 ) )
7	6	simp1d	⊢ ( 𝜑 → ran ( 1^st ∘ 𝐺 ) ⊆ ℝ )
8	6	simp2d	⊢ ( 𝜑 → ran ( 1^st ∘ 𝐺 ) ≠ ∅ )
9		1re	⊢ 1 ∈ ℝ
10	6	simp3d	⊢ ( 𝜑 → ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ 1 )
11		brralrspcev	⊢ ( ( 1 ∈ ℝ ∧ ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ 1 ) → ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ 𝑛 )
12	9 10 11	sylancr	⊢ ( 𝜑 → ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ 𝑛 )
13	7 8 12	suprcld	⊢ ( 𝜑 → sup ( ran ( 1^st ∘ 𝐺 ) , ℝ , < ) ∈ ℝ )
14	5 13	eqeltrid	⊢ ( 𝜑 → 𝑆 ∈ ℝ )
15	1	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐹 : ℕ ⟶ ℝ )
16	2	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1^st ‘ 𝑥 ) + ( 2^nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1^st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2^nd ‘ 𝑥 ) ) / 2 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) ) )
17	1 2 3 4	ruclem6	⊢ ( 𝜑 → 𝐺 : ℕ₀ ⟶ ( ℝ × ℝ ) )
18		nnm1nn0	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ₀ )
19		ffvelcdm	⊢ ( ( 𝐺 : ℕ₀ ⟶ ( ℝ × ℝ ) ∧ ( 𝑛 − 1 ) ∈ ℕ₀ ) → ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∈ ( ℝ × ℝ ) )
20	17 18 19	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∈ ( ℝ × ℝ ) )
21		xp1st	⊢ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ∈ ℝ )
22	20 21	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ∈ ℝ )
23		xp2nd	⊢ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ∈ ℝ )
24	20 23	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ∈ ℝ )
25	1	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
26		eqid	⊢ ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ 𝐷 ( 𝐹 ‘ 𝑛 ) ) ) = ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ 𝐷 ( 𝐹 ‘ 𝑛 ) ) )
27		eqid	⊢ ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ 𝐷 ( 𝐹 ‘ 𝑛 ) ) ) = ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ 𝐷 ( 𝐹 ‘ 𝑛 ) ) )
28	1 2 3 4	ruclem8	⊢ ( ( 𝜑 ∧ ( 𝑛 − 1 ) ∈ ℕ₀ ) → ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) < ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) )
29	18 28	sylan2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) < ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) )
30	15 16 22 24 25 26 27 29	ruclem3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) < ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ 𝐷 ( 𝐹 ‘ 𝑛 ) ) ) ∨ ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ 𝐷 ( 𝐹 ‘ 𝑛 ) ) ) < ( 𝐹 ‘ 𝑛 ) ) )
31	1 2 3 4	ruclem7	⊢ ( ( 𝜑 ∧ ( 𝑛 − 1 ) ∈ ℕ₀ ) → ( 𝐺 ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) 𝐷 ( 𝐹 ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) )
32	18 31	sylan2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) 𝐷 ( 𝐹 ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) )
33		nncn	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
34	33	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
35		ax-1cn	⊢ 1 ∈ ℂ
36		npcan	⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
37	34 35 36	sylancl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
38	37	fveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( 𝐺 ‘ 𝑛 ) )
39		1st2nd2	⊢ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∈ ( ℝ × ℝ ) → ( 𝐺 ‘ ( 𝑛 − 1 ) ) = ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ )
40	20 39	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑛 − 1 ) ) = ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ )
41	37	fveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( 𝐹 ‘ 𝑛 ) )
42	40 41	oveq12d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) 𝐷 ( 𝐹 ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) = ( ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ 𝐷 ( 𝐹 ‘ 𝑛 ) ) )
43	32 38 42	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) = ( ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ 𝐷 ( 𝐹 ‘ 𝑛 ) ) )
44	43	fveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ 𝐷 ( 𝐹 ‘ 𝑛 ) ) ) )
45	44	breq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) < ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ ( 𝐹 ‘ 𝑛 ) < ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ 𝐷 ( 𝐹 ‘ 𝑛 ) ) ) ) )
46	43	fveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ 𝐷 ( 𝐹 ‘ 𝑛 ) ) ) )
47	46	breq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 𝐹 ‘ 𝑛 ) ↔ ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ 𝐷 ( 𝐹 ‘ 𝑛 ) ) ) < ( 𝐹 ‘ 𝑛 ) ) )
48	45 47	orbi12d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑛 ) < ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∨ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( 𝐹 ‘ 𝑛 ) < ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ 𝐷 ( 𝐹 ‘ 𝑛 ) ) ) ∨ ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) , ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ⟩ 𝐷 ( 𝐹 ‘ 𝑛 ) ) ) < ( 𝐹 ‘ 𝑛 ) ) ) )
49	30 48	mpbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) < ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∨ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 𝐹 ‘ 𝑛 ) ) )
50	7	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ran ( 1^st ∘ 𝐺 ) ⊆ ℝ )
51	8	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ran ( 1^st ∘ 𝐺 ) ≠ ∅ )
52	12	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ 𝑛 )
53		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀ )
54		fvco3	⊢ ( ( 𝐺 : ℕ₀ ⟶ ( ℝ × ℝ ) ∧ 𝑛 ∈ ℕ₀ ) → ( ( 1^st ∘ 𝐺 ) ‘ 𝑛 ) = ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) )
55	17 53 54	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ∘ 𝐺 ) ‘ 𝑛 ) = ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) )
56	17	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 : ℕ₀ ⟶ ( ℝ × ℝ ) )
57		1stcof	⊢ ( 𝐺 : ℕ₀ ⟶ ( ℝ × ℝ ) → ( 1^st ∘ 𝐺 ) : ℕ₀ ⟶ ℝ )
58		ffn	⊢ ( ( 1^st ∘ 𝐺 ) : ℕ₀ ⟶ ℝ → ( 1^st ∘ 𝐺 ) Fn ℕ₀ )
59	56 57 58	3syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ∘ 𝐺 ) Fn ℕ₀ )
60	53	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ₀ )
61		fnfvelrn	⊢ ( ( ( 1^st ∘ 𝐺 ) Fn ℕ₀ ∧ 𝑛 ∈ ℕ₀ ) → ( ( 1^st ∘ 𝐺 ) ‘ 𝑛 ) ∈ ran ( 1^st ∘ 𝐺 ) )
62	59 60 61	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ∘ 𝐺 ) ‘ 𝑛 ) ∈ ran ( 1^st ∘ 𝐺 ) )
63	55 62	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ran ( 1^st ∘ 𝐺 ) )
64	50 51 52 63	suprubd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ sup ( ran ( 1^st ∘ 𝐺 ) , ℝ , < ) )
65	64 5	breqtrrdi	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑆 )
66		ffvelcdm	⊢ ( ( 𝐺 : ℕ₀ ⟶ ( ℝ × ℝ ) ∧ 𝑛 ∈ ℕ₀ ) → ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) )
67	17 53 66	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) )
68		xp1st	⊢ ( ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
69	67 68	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
70	14	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑆 ∈ ℝ )
71		ltletr	⊢ ( ( ( 𝐹 ‘ 𝑛 ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ ∧ 𝑆 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑛 ) < ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑆 ) → ( 𝐹 ‘ 𝑛 ) < 𝑆 ) )
72	25 69 70 71	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑛 ) < ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑆 ) → ( 𝐹 ‘ 𝑛 ) < 𝑆 ) )
73	65 72	mpan2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) < ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑛 ) < 𝑆 ) )
74		fvco3	⊢ ( ( 𝐺 : ℕ₀ ⟶ ( ℝ × ℝ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 1^st ∘ 𝐺 ) ‘ 𝑘 ) = ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) )
75	56 74	sylan	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 1^st ∘ 𝐺 ) ‘ 𝑘 ) = ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) )
76	56	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ℝ × ℝ ) )
77		xp1st	⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
78	76 77	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ₀ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
79		xp2nd	⊢ ( ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
80	67 79	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
81	80	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ₀ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
82	15	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝐹 : ℕ ⟶ ℝ )
83	16	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1^st ‘ 𝑥 ) + ( 2^nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1^st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2^nd ‘ 𝑥 ) ) / 2 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) ) )
84		simpr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑘 ∈ ℕ₀ )
85	60	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑛 ∈ ℕ₀ )
86	82 83 3 4 84 85	ruclem10	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ₀ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
87	78 81 86	ltled	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ₀ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
88	75 87	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 1^st ∘ 𝐺 ) ‘ 𝑘 ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
89	88	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑘 ∈ ℕ₀ ( ( 1^st ∘ 𝐺 ) ‘ 𝑘 ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
90		breq1	⊢ ( 𝑧 = ( ( 1^st ∘ 𝐺 ) ‘ 𝑘 ) → ( 𝑧 ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ ( ( 1^st ∘ 𝐺 ) ‘ 𝑘 ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
91	90	ralrn	⊢ ( ( 1^st ∘ 𝐺 ) Fn ℕ₀ → ( ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ ∀ 𝑘 ∈ ℕ₀ ( ( 1^st ∘ 𝐺 ) ‘ 𝑘 ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
92	59 91	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ ∀ 𝑘 ∈ ℕ₀ ( ( 1^st ∘ 𝐺 ) ‘ 𝑘 ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
93	89 92	mpbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
94		suprleub	⊢ ( ( ( ran ( 1^st ∘ 𝐺 ) ⊆ ℝ ∧ ran ( 1^st ∘ 𝐺 ) ≠ ∅ ∧ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ 𝑛 ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ ) → ( sup ( ran ( 1^st ∘ 𝐺 ) , ℝ , < ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
95	50 51 52 80 94	syl31anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( sup ( ran ( 1^st ∘ 𝐺 ) , ℝ , < ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
96	93 95	mpbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → sup ( ran ( 1^st ∘ 𝐺 ) , ℝ , < ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
97	5 96	eqbrtrid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑆 ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
98		lelttr	⊢ ( ( 𝑆 ∈ ℝ ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑛 ) ∈ ℝ ) → ( ( 𝑆 ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 𝐹 ‘ 𝑛 ) ) → 𝑆 < ( 𝐹 ‘ 𝑛 ) ) )
99	70 80 25 98	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑆 ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 𝐹 ‘ 𝑛 ) ) → 𝑆 < ( 𝐹 ‘ 𝑛 ) ) )
100	97 99	mpand	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 𝐹 ‘ 𝑛 ) → 𝑆 < ( 𝐹 ‘ 𝑛 ) ) )
101	73 100	orim12d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑛 ) < ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∨ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 𝐹 ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑛 ) < 𝑆 ∨ 𝑆 < ( 𝐹 ‘ 𝑛 ) ) ) )
102	49 101	mpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) < 𝑆 ∨ 𝑆 < ( 𝐹 ‘ 𝑛 ) ) )
103	25 70	lttri2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑆 ↔ ( ( 𝐹 ‘ 𝑛 ) < 𝑆 ∨ 𝑆 < ( 𝐹 ‘ 𝑛 ) ) ) )
104	102 103	mpbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ≠ 𝑆 )
105	104	neneqd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ¬ ( 𝐹 ‘ 𝑛 ) = 𝑆 )
106	105	nrexdv	⊢ ( 𝜑 → ¬ ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = 𝑆 )
107		risset	⊢ ( 𝑆 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ ran 𝐹 𝑧 = 𝑆 )
108		ffn	⊢ ( 𝐹 : ℕ ⟶ ℝ → 𝐹 Fn ℕ )
109		eqeq1	⊢ ( 𝑧 = ( 𝐹 ‘ 𝑛 ) → ( 𝑧 = 𝑆 ↔ ( 𝐹 ‘ 𝑛 ) = 𝑆 ) )
110	109	rexrn	⊢ ( 𝐹 Fn ℕ → ( ∃ 𝑧 ∈ ran 𝐹 𝑧 = 𝑆 ↔ ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = 𝑆 ) )
111	1 108 110	3syl	⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ran 𝐹 𝑧 = 𝑆 ↔ ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = 𝑆 ) )
112	107 111	bitrid	⊢ ( 𝜑 → ( 𝑆 ∈ ran 𝐹 ↔ ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = 𝑆 ) )
113	106 112	mtbird	⊢ ( 𝜑 → ¬ 𝑆 ∈ ran 𝐹 )
114	14 113	eldifd	⊢ ( 𝜑 → 𝑆 ∈ ( ℝ ∖ ran 𝐹 ) )

Metamath Proof Explorer

Theorem ruclem12

Proof