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=x2,y1stx+2ndx2/mifm<y1stxmm+2ndx22ndx
ruc.4 C=001F
ruc.5 G=seq0DC
Assertion ruclem11 φran1stGran1stGzran1stGz1

Proof

Step Hyp Ref Expression
1 ruc.1 φF:
2 ruc.2 φD=x2,y1stx+2ndx2/mifm<y1stxmm+2ndx22ndx
3 ruc.4 C=001F
4 ruc.5 G=seq0DC
5 1 2 3 4 ruclem6 φG:02
6 1stcof G:021stG:0
7 5 6 syl φ1stG:0
8 7 frnd φran1stG
9 7 fdmd φdom1stG=0
10 0nn0 00
11 ne0i 000
12 10 11 mp1i φ0
13 9 12 eqnetrd φdom1stG
14 dm0rn0 dom1stG=ran1stG=
15 14 necon3bii dom1stGran1stG
16 13 15 sylib φran1stG
17 fvco3 G:02n01stGn=1stGn
18 5 17 sylan φn01stGn=1stGn
19 1 adantr φn0F:
20 2 adantr φn0D=x2,y1stx+2ndx2/mifm<y1stxmm+2ndx22ndx
21 simpr φn0n0
22 10 a1i φn000
23 19 20 3 4 21 22 ruclem10 φn01stGn<2ndG0
24 1 2 3 4 ruclem4 φG0=01
25 24 fveq2d φ2ndG0=2nd01
26 c0ex 0V
27 1ex 1V
28 26 27 op2nd 2nd01=1
29 25 28 eqtrdi φ2ndG0=1
30 29 adantr φn02ndG0=1
31 23 30 breqtrd φn01stGn<1
32 5 ffvelcdmda φn0Gn2
33 xp1st Gn21stGn
34 32 33 syl φn01stGn
35 1re 1
36 ltle 1stGn11stGn<11stGn1
37 34 35 36 sylancl φn01stGn<11stGn1
38 31 37 mpd φn01stGn1
39 18 38 eqbrtrd φn01stGn1
40 39 ralrimiva φn01stGn1
41 7 ffnd φ1stGFn0
42 breq1 z=1stGnz11stGn1
43 42 ralrn 1stGFn0zran1stGz1n01stGn1
44 41 43 syl φzran1stGz1n01stGn1
45 40 44 mpbird φzran1stGz1
46 8 16 45 3jca φran1stGran1stGzran1stGz1