ruclem4

Description: Lemma for ruc . Initial value of the interval sequence. (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	ruclem4	⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = ⟨ 0 , 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	4	fveq1i	⊢ ( 𝐺 ‘ 0 ) = ( seq 0 ( 𝐷 , 𝐶 ) ‘ 0 )
6		0z	⊢ 0 ∈ ℤ
7		dfn2	⊢ ℕ = ( ℕ₀ ∖ { 0 } )
8	7	reseq2i	⊢ ( 𝐹 ↾ ℕ ) = ( 𝐹 ↾ ( ℕ₀ ∖ { 0 } ) )
9		ffn	⊢ ( 𝐹 : ℕ ⟶ ℝ → 𝐹 Fn ℕ )
10		fnresdm	⊢ ( 𝐹 Fn ℕ → ( 𝐹 ↾ ℕ ) = 𝐹 )
11	1 9 10	3syl	⊢ ( 𝜑 → ( 𝐹 ↾ ℕ ) = 𝐹 )
12	8 11	syl5reqr	⊢ ( 𝜑 → 𝐹 = ( 𝐹 ↾ ( ℕ₀ ∖ { 0 } ) ) )
13	12	uneq2d	⊢ ( 𝜑 → ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 ) = ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ ( 𝐹 ↾ ( ℕ₀ ∖ { 0 } ) ) ) )
14	3 13	syl5eq	⊢ ( 𝜑 → 𝐶 = ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ ( 𝐹 ↾ ( ℕ₀ ∖ { 0 } ) ) ) )
15	14	fveq1d	⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) = ( ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ ( 𝐹 ↾ ( ℕ₀ ∖ { 0 } ) ) ) ‘ 0 ) )
16		c0ex	⊢ 0 ∈ V
17	16	a1i	⊢ ( ⊤ → 0 ∈ V )
18		opex	⊢ ⟨ 0 , 1 ⟩ ∈ V
19	18	a1i	⊢ ( ⊤ → ⟨ 0 , 1 ⟩ ∈ V )
20		eqid	⊢ ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ ( 𝐹 ↾ ( ℕ₀ ∖ { 0 } ) ) ) = ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ ( 𝐹 ↾ ( ℕ₀ ∖ { 0 } ) ) )
21	17 19 20	fvsnun1	⊢ ( ⊤ → ( ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ ( 𝐹 ↾ ( ℕ₀ ∖ { 0 } ) ) ) ‘ 0 ) = ⟨ 0 , 1 ⟩ )
22	21	mptru	⊢ ( ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ ( 𝐹 ↾ ( ℕ₀ ∖ { 0 } ) ) ) ‘ 0 ) = ⟨ 0 , 1 ⟩
23	15 22	eqtrdi	⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) = ⟨ 0 , 1 ⟩ )
24	6 23	seq1i	⊢ ( 𝜑 → ( seq 0 ( 𝐷 , 𝐶 ) ‘ 0 ) = ⟨ 0 , 1 ⟩ )
25	5 24	syl5eq	⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = ⟨ 0 , 1 ⟩ )

Metamath Proof Explorer

Theorem ruclem4

Proof