Metamath Proof Explorer


Theorem ruclem11

Description: Lemma for ruc . Closure lemmas for supremum. (Contributed by Mario Carneiro, 28-May-2014)

Ref Expression
Hypotheses ruc.1 φ F :
ruc.2 φ D = x 2 , y 1 st x + 2 nd x 2 / m if m < y 1 st x m m + 2 nd x 2 2 nd x
ruc.4 C = 0 0 1 F
ruc.5 G = seq 0 D C
Assertion ruclem11 φ ran 1 st G ran 1 st G z ran 1 st G z 1

Proof

Step Hyp Ref Expression
1 ruc.1 φ F :
2 ruc.2 φ D = x 2 , y 1 st x + 2 nd x 2 / m if m < y 1 st x m m + 2 nd x 2 2 nd x
3 ruc.4 C = 0 0 1 F
4 ruc.5 G = seq 0 D C
5 1 2 3 4 ruclem6 φ G : 0 2
6 1stcof G : 0 2 1 st G : 0
7 5 6 syl φ 1 st G : 0
8 7 frnd φ ran 1 st G
9 7 fdmd φ dom 1 st G = 0
10 0nn0 0 0
11 ne0i 0 0 0
12 10 11 mp1i φ 0
13 9 12 eqnetrd φ dom 1 st G
14 dm0rn0 dom 1 st G = ran 1 st G =
15 14 necon3bii dom 1 st G ran 1 st G
16 13 15 sylib φ ran 1 st G
17 fvco3 G : 0 2 n 0 1 st G n = 1 st G n
18 5 17 sylan φ n 0 1 st G n = 1 st G n
19 1 adantr φ n 0 F :
20 2 adantr φ n 0 D = x 2 , y 1 st x + 2 nd x 2 / m if m < y 1 st x m m + 2 nd x 2 2 nd x
21 simpr φ n 0 n 0
22 10 a1i φ n 0 0 0
23 19 20 3 4 21 22 ruclem10 φ n 0 1 st G n < 2 nd G 0
24 1 2 3 4 ruclem4 φ G 0 = 0 1
25 24 fveq2d φ 2 nd G 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 G 0 = 1
30 29 adantr φ n 0 2 nd G 0 = 1
31 23 30 breqtrd φ n 0 1 st G n < 1
32 5 ffvelrnda φ n 0 G n 2
33 xp1st G n 2 1 st G n
34 32 33 syl φ n 0 1 st G n
35 1re 1
36 ltle 1 st G n 1 1 st G n < 1 1 st G n 1
37 34 35 36 sylancl φ n 0 1 st G n < 1 1 st G n 1
38 31 37 mpd φ n 0 1 st G n 1
39 18 38 eqbrtrd φ n 0 1 st G n 1
40 39 ralrimiva φ n 0 1 st G n 1
41 7 ffnd φ 1 st G Fn 0
42 breq1 z = 1 st G n z 1 1 st G n 1
43 42 ralrn 1 st G Fn 0 z ran 1 st G z 1 n 0 1 st G n 1
44 41 43 syl φ z ran 1 st G z 1 n 0 1 st G n 1
45 40 44 mpbird φ z ran 1 st G z 1
46 8 16 45 3jca φ ran 1 st G ran 1 st G z ran 1 st G z 1