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 ⟶ ( ℝ × ℝ ) ) |