Metamath Proof Explorer

Theorem ruclem7

Description: Lemma for ruc . Successor value for the interval sequence. (Contributed by Mario Carneiro, 28-May-2014)

Ref Expression
Hypotheses ruc.1 ⊢φ→F:ℕ⟶ℝ
ruc.2 ⊢φ→D=x∈ℝ2,y∈ℝ⟼⦋1st⁡x+2nd⁡x2/m⦌ifm<y1st⁡xmm+2nd⁡x22nd⁡x
ruc.4 ⊢C=001∪F
ruc.5 ⊢G=seq0DC
Assertion ruclem7 ⊢φ∧N∈ℕ0→G⁡N+1=G⁡NDF⁡N+1

Proof

Step Hyp Ref Expression
1 ruc.1 ⊢φ→F:ℕ⟶ℝ
2 ruc.2 ⊢φ→D=x∈ℝ2,y∈ℝ⟼⦋1st⁡x+2nd⁡x2/m⦌ifm<y1st⁡xmm+2nd⁡x22nd⁡x
3 ruc.4 ⊢C=001∪F
4 ruc.5 ⊢G=seq0DC
5 simpr ⊢φ∧N∈ℕ0→N∈ℕ0
6 nn0uz ⊢ℕ0=ℤ≥0
7 5 6 eleqtrdi ⊢φ∧N∈ℕ0→N∈ℤ≥0
8 seqp1 ⊢N∈ℤ≥0→seq0DC⁡N+1=seq0DC⁡NDC⁡N+1
9 7 8 syl ⊢φ∧N∈ℕ0→seq0DC⁡N+1=seq0DC⁡NDC⁡N+1
10 4 fveq1i ⊢G⁡N+1=seq0DC⁡N+1
11 4 fveq1i ⊢G⁡N=seq0DC⁡N
12 11 oveq1i ⊢G⁡NDC⁡N+1=seq0DC⁡NDC⁡N+1
13 9 10 12 3eqtr4g ⊢φ∧N∈ℕ0→G⁡N+1=G⁡NDC⁡N+1
14 nn0p1nn ⊢N∈ℕ0→N+1∈ℕ
15 14 adantl ⊢φ∧N∈ℕ0→N+1∈ℕ
16 15 nnne0d ⊢φ∧N∈ℕ0→N+1≠0
17 16 necomd ⊢φ∧N∈ℕ0→0≠N+1
18 3 equncomi ⊢C=F∪001
19 18 fveq1i ⊢C⁡N+1=F∪001⁡N+1
20 fvunsn ⊢0≠N+1→F∪001⁡N+1=F⁡N+1
21 19 20 eqtrid ⊢0≠N+1→C⁡N+1=F⁡N+1
22 17 21 syl ⊢φ∧N∈ℕ0→C⁡N+1=F⁡N+1
23 22 oveq2d ⊢φ∧N∈ℕ0→G⁡NDC⁡N+1=G⁡NDF⁡N+1
24 13 23 eqtrd ⊢φ∧N∈ℕ0→G⁡N+1=G⁡NDF⁡N+1