ruclem11

Description: Lemma for ruc . Closure lemmas for supremum. (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 ( 𝐷 , 𝐶 )
Assertion	ruclem11	⊢ ( 𝜑 → ( ran ( 1^st ∘ 𝐺 ) ⊆ ℝ ∧ ran ( 1^st ∘ 𝐺 ) ≠ ∅ ∧ ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ 1 ) )

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	1 2 3 4	ruclem6	⊢ ( 𝜑 → 𝐺 : ℕ₀ ⟶ ( ℝ × ℝ ) )
6		1stcof	⊢ ( 𝐺 : ℕ₀ ⟶ ( ℝ × ℝ ) → ( 1^st ∘ 𝐺 ) : ℕ₀ ⟶ ℝ )
7	5 6	syl	⊢ ( 𝜑 → ( 1^st ∘ 𝐺 ) : ℕ₀ ⟶ ℝ )
8	7	frnd	⊢ ( 𝜑 → ran ( 1^st ∘ 𝐺 ) ⊆ ℝ )
9	7	fdmd	⊢ ( 𝜑 → dom ( 1^st ∘ 𝐺 ) = ℕ₀ )
10		0nn0	⊢ 0 ∈ ℕ₀
11		ne0i	⊢ ( 0 ∈ ℕ₀ → ℕ₀ ≠ ∅ )
12	10 11	mp1i	⊢ ( 𝜑 → ℕ₀ ≠ ∅ )
13	9 12	eqnetrd	⊢ ( 𝜑 → dom ( 1^st ∘ 𝐺 ) ≠ ∅ )
14		dm0rn0	⊢ ( dom ( 1^st ∘ 𝐺 ) = ∅ ↔ ran ( 1^st ∘ 𝐺 ) = ∅ )
15	14	necon3bii	⊢ ( dom ( 1^st ∘ 𝐺 ) ≠ ∅ ↔ ran ( 1^st ∘ 𝐺 ) ≠ ∅ )
16	13 15	sylib	⊢ ( 𝜑 → ran ( 1^st ∘ 𝐺 ) ≠ ∅ )
17		fvco3	⊢ ( ( 𝐺 : ℕ₀ ⟶ ( ℝ × ℝ ) ∧ 𝑛 ∈ ℕ₀ ) → ( ( 1^st ∘ 𝐺 ) ‘ 𝑛 ) = ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) )
18	5 17	sylan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( ( 1^st ∘ 𝐺 ) ‘ 𝑛 ) = ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) )
19	1	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → 𝐹 : ℕ ⟶ ℝ )
20	2	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1^st ‘ 𝑥 ) + ( 2^nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1^st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2^nd ‘ 𝑥 ) ) / 2 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) ) )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → 𝑛 ∈ ℕ₀ )
22	10	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → 0 ∈ ℕ₀ )
23	19 20 3 4 21 22	ruclem10	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 0 ) ) )
24	1 2 3 4	ruclem4	⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = ⟨ 0 , 1 ⟩ )
25	24	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐺 ‘ 0 ) ) = ( 2^nd ‘ ⟨ 0 , 1 ⟩ ) )
26		c0ex	⊢ 0 ∈ V
27		1ex	⊢ 1 ∈ V
28	26 27	op2nd	⊢ ( 2^nd ‘ ⟨ 0 , 1 ⟩ ) = 1
29	25 28	eqtrdi	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐺 ‘ 0 ) ) = 1 )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( 2^nd ‘ ( 𝐺 ‘ 0 ) ) = 1 )
31	23 30	breqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 1 )
32	5	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) )
33		xp1st	⊢ ( ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
34	32 33	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
35		1re	⊢ 1 ∈ ℝ
36		ltle	⊢ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 1 → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 1 ) )
37	34 35 36	sylancl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 1 → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 1 ) )
38	31 37	mpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 1 )
39	18 38	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( ( 1^st ∘ 𝐺 ) ‘ 𝑛 ) ≤ 1 )
40	39	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ₀ ( ( 1^st ∘ 𝐺 ) ‘ 𝑛 ) ≤ 1 )
41	7	ffnd	⊢ ( 𝜑 → ( 1^st ∘ 𝐺 ) Fn ℕ₀ )
42		breq1	⊢ ( 𝑧 = ( ( 1^st ∘ 𝐺 ) ‘ 𝑛 ) → ( 𝑧 ≤ 1 ↔ ( ( 1^st ∘ 𝐺 ) ‘ 𝑛 ) ≤ 1 ) )
43	42	ralrn	⊢ ( ( 1^st ∘ 𝐺 ) Fn ℕ₀ → ( ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ 1 ↔ ∀ 𝑛 ∈ ℕ₀ ( ( 1^st ∘ 𝐺 ) ‘ 𝑛 ) ≤ 1 ) )
44	41 43	syl	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ 1 ↔ ∀ 𝑛 ∈ ℕ₀ ( ( 1^st ∘ 𝐺 ) ‘ 𝑛 ) ≤ 1 ) )
45	40 44	mpbird	⊢ ( 𝜑 → ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ 1 )
46	8 16 45	3jca	⊢ ( 𝜑 → ( ran ( 1^st ∘ 𝐺 ) ⊆ ℝ ∧ ran ( 1^st ∘ 𝐺 ) ≠ ∅ ∧ ∀ 𝑧 ∈ ran ( 1^st ∘ 𝐺 ) 𝑧 ≤ 1 ) )

Metamath Proof Explorer

Theorem ruclem11

Proof