Theorem ruclem6

Description: Lemma for ruc . Domain and range of the interval sequence. (Contributed by Mario Carneiro, 28-May-2014)

	Ref	Expression
Hypotheses	ruc.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
	ruc.2	⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) )
	ruc.4	⊢ 𝐶 = ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 )
	ruc.5	⊢ 𝐺 = seq 0 ( 𝐷 , 𝐶 )
Assertion	ruclem6	⊢ ( 𝜑 → 𝐺 : ℕ0 ⟶ ( ℝ × ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		ruc.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
2		ruc.2	⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) )
3		ruc.4	⊢ 𝐶 = ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 )
4		ruc.5	⊢ 𝐺 = seq 0 ( 𝐷 , 𝐶 )
5	4	fveq1i	⊢ ( 𝐺 ‘ 0 ) = ( seq 0 ( 𝐷 , 𝐶 ) ‘ 0 )
6		0z	⊢ 0 ∈ ℤ
7		seq1	⊢ ( 0 ∈ ℤ → ( seq 0 ( 𝐷 , 𝐶 ) ‘ 0 ) = ( 𝐶 ‘ 0 ) )
8	6 7	ax-mp	⊢ ( seq 0 ( 𝐷 , 𝐶 ) ‘ 0 ) = ( 𝐶 ‘ 0 )
9	5 8	eqtri	⊢ ( 𝐺 ‘ 0 ) = ( 𝐶 ‘ 0 )
10	1 2 3 4	ruclem4	⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = ⟨ 0 , 1 ⟩ )
11	9 10	syl5eqr	⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) = ⟨ 0 , 1 ⟩ )
12		0re	⊢ 0 ∈ ℝ
13		1re	⊢ 1 ∈ ℝ
14		opelxpi	⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → ⟨ 0 , 1 ⟩ ∈ ( ℝ × ℝ ) )
15	12 13 14	mp2an	⊢ ⟨ 0 , 1 ⟩ ∈ ( ℝ × ℝ )
16	11 15	eqeltrdi	⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ∈ ( ℝ × ℝ ) )
17		1st2nd2	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → 𝑧 = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ )
18	17	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ℝ ) ) → 𝑧 = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ )
19	18	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ℝ ) ) → ( 𝑧 𝐷 𝑤 ) = ( ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ 𝐷 𝑤 ) )
20	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ℝ ) ) → 𝐹 : ℕ ⟶ ℝ )
21	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ℝ ) ) → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) )
22		xp1st	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 1st ‘ 𝑧 ) ∈ ℝ )
23	22	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ℝ ) ) → ( 1st ‘ 𝑧 ) ∈ ℝ )
24		xp2nd	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 2nd ‘ 𝑧 ) ∈ ℝ )
25	24	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ℝ ) ) → ( 2nd ‘ 𝑧 ) ∈ ℝ )
26		simprr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ℝ ) ) → 𝑤 ∈ ℝ )
27		eqid	⊢ ( 1st ‘ ( ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ 𝐷 𝑤 ) ) = ( 1st ‘ ( ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ 𝐷 𝑤 ) )
28		eqid	⊢ ( 2nd ‘ ( ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ 𝐷 𝑤 ) ) = ( 2nd ‘ ( ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ 𝐷 𝑤 ) )
29	20 21 23 25 26 27 28	ruclem1	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ℝ ) ) → ( ( ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ 𝐷 𝑤 ) ∈ ( ℝ × ℝ ) ∧ ( 1st ‘ ( ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ 𝐷 𝑤 ) ) = if ( ( ( ( 1st ‘ 𝑧 ) + ( 2nd ‘ 𝑧 ) ) / 2 ) < 𝑤 , ( 1st ‘ 𝑧 ) , ( ( ( ( ( 1st ‘ 𝑧 ) + ( 2nd ‘ 𝑧 ) ) / 2 ) + ( 2nd ‘ 𝑧 ) ) / 2 ) ) ∧ ( 2nd ‘ ( ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ 𝐷 𝑤 ) ) = if ( ( ( ( 1st ‘ 𝑧 ) + ( 2nd ‘ 𝑧 ) ) / 2 ) < 𝑤 , ( ( ( 1st ‘ 𝑧 ) + ( 2nd ‘ 𝑧 ) ) / 2 ) , ( 2nd ‘ 𝑧 ) ) ) )
30	29	simp1d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ℝ ) ) → ( ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ 𝐷 𝑤 ) ∈ ( ℝ × ℝ ) )
31	19 30	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ℝ ) ) → ( 𝑧 𝐷 𝑤 ) ∈ ( ℝ × ℝ ) )
32		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
33		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
34		0p1e1	⊢ ( 0 + 1 ) = 1
35	34	fveq2i	⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ( ℤ≥ ‘ 1 )
36		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
37	35 36	eqtr4i	⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ℕ
38	37	eleq2i	⊢ ( 𝑧 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ↔ 𝑧 ∈ ℕ )
39	3	equncomi	⊢ 𝐶 = ( 𝐹 ∪ { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } )
40	39	fveq1i	⊢ ( 𝐶 ‘ 𝑧 ) = ( ( 𝐹 ∪ { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ) ‘ 𝑧 )
41		nnne0	⊢ ( 𝑧 ∈ ℕ → 𝑧 ≠ 0 )
42	41	necomd	⊢ ( 𝑧 ∈ ℕ → 0 ≠ 𝑧 )
43		fvunsn	⊢ ( 0 ≠ 𝑧 → ( ( 𝐹 ∪ { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
44	42 43	syl	⊢ ( 𝑧 ∈ ℕ → ( ( 𝐹 ∪ { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
45	40 44	syl5eq	⊢ ( 𝑧 ∈ ℕ → ( 𝐶 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
46	45	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) → ( 𝐶 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
47	1	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
48	46 47	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) → ( 𝐶 ‘ 𝑧 ) ∈ ℝ )
49	38 48	sylan2b	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ) → ( 𝐶 ‘ 𝑧 ) ∈ ℝ )
50	16 31 32 33 49	seqf2	⊢ ( 𝜑 → seq 0 ( 𝐷 , 𝐶 ) : ℕ0 ⟶ ( ℝ × ℝ ) )
51	4	feq1i	⊢ ( 𝐺 : ℕ0 ⟶ ( ℝ × ℝ ) ↔ seq 0 ( 𝐷 , 𝐶 ) : ℕ0 ⟶ ( ℝ × ℝ ) )
52	50 51	sylibr	⊢ ( 𝜑 → 𝐺 : ℕ0 ⟶ ( ℝ × ℝ ) )