Metamath Proof Explorer


Theorem stoweidlem56

Description: This theorem proves Lemma 1 in BrosowskiDeutsh p. 90. Here Z is used to represent t_0 in the paper, v is used to represent V in the paper, and e is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem56.1 _ t U
stoweidlem56.2 t φ
stoweidlem56.3 K = topGen ran .
stoweidlem56.4 φ J Comp
stoweidlem56.5 T = J
stoweidlem56.6 C = J Cn K
stoweidlem56.7 φ A C
stoweidlem56.8 φ f A g A t T f t + g t A
stoweidlem56.9 φ f A g A t T f t g t A
stoweidlem56.10 φ y t T y A
stoweidlem56.11 φ r T t T r t q A q r q t
stoweidlem56.12 φ U J
stoweidlem56.13 φ Z U
Assertion stoweidlem56 φ v J Z v v U e + x A t T 0 x t x t 1 t v x t < e t T U 1 e < x t

Proof

Step Hyp Ref Expression
1 stoweidlem56.1 _ t U
2 stoweidlem56.2 t φ
3 stoweidlem56.3 K = topGen ran .
4 stoweidlem56.4 φ J Comp
5 stoweidlem56.5 T = J
6 stoweidlem56.6 C = J Cn K
7 stoweidlem56.7 φ A C
8 stoweidlem56.8 φ f A g A t T f t + g t A
9 stoweidlem56.9 φ f A g A t T f t g t A
10 stoweidlem56.10 φ y t T y A
11 stoweidlem56.11 φ r T t T r t q A q r q t
12 stoweidlem56.12 φ U J
13 stoweidlem56.13 φ Z U
14 eqid h A | h Z = 0 t T 0 h t h t 1 = h A | h Z = 0 t T 0 h t h t 1
15 eqid w J | h h A | h Z = 0 t T 0 h t h t 1 w = t T | 0 < h t = w J | h h A | h Z = 0 t T 0 h t h t 1 w = t T | 0 < h t
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 stoweidlem55 φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t
17 df-rex p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t p p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t
18 16 17 sylib φ p p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t
19 simpl φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t φ
20 simprl φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t p A
21 simprr3 φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t t T U 0 < p t
22 nfv t p A
23 nfra1 t t T U 0 < p t
24 2 22 23 nf3an t φ p A t T U 0 < p t
25 4 3ad2ant1 φ p A t T U 0 < p t J Comp
26 7 sselda φ p A p C
27 26 6 syl6eleq φ p A p J Cn K
28 27 3adant3 φ p A t T U 0 < p t p J Cn K
29 simp3 φ p A t T U 0 < p t t T U 0 < p t
30 12 3ad2ant1 φ p A t T U 0 < p t U J
31 1 24 3 5 25 28 29 30 stoweidlem28 φ p A t T U 0 < p t d d + d < 1 t T U d p t
32 19 20 21 31 syl3anc φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t d d + d < 1 t T U d p t
33 simpr1 φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t d + d < 1 t T U d p t d +
34 simpr2 φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t d + d < 1 t T U d p t d < 1
35 simplrl φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t d + d < 1 t T U d p t p A
36 simprr1 φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t t T 0 p t p t 1
37 36 adantr φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t d + d < 1 t T U d p t t T 0 p t p t 1
38 simprr2 φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t p Z = 0
39 38 adantr φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t d + d < 1 t T U d p t p Z = 0
40 simpr3 φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t d + d < 1 t T U d p t t T U d p t
41 37 39 40 3jca φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t d + d < 1 t T U d p t t T 0 p t p t 1 p Z = 0 t T U d p t
42 35 41 jca φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t d + d < 1 t T U d p t p A t T 0 p t p t 1 p Z = 0 t T U d p t
43 33 34 42 3jca φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t d + d < 1 t T U d p t d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t
44 43 ex φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t d + d < 1 t T U d p t d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t
45 44 eximdv φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t d d + d < 1 t T U d p t d d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t
46 32 45 mpd φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t d d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t
47 46 ex φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t d d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t
48 47 eximdv φ p p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t p d d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t
49 18 48 mpd φ p d d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t
50 nfv t d +
51 nfv t d < 1
52 nfra1 t t T 0 p t p t 1
53 nfv t p Z = 0
54 nfra1 t t T U d p t
55 52 53 54 nf3an t t T 0 p t p t 1 p Z = 0 t T U d p t
56 22 55 nfan t p A t T 0 p t p t 1 p Z = 0 t T U d p t
57 50 51 56 nf3an t d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t
58 2 57 nfan t φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t
59 nfcv _ t p
60 eqid t T | p t < d 2 = t T | p t < d 2
61 7 adantr φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t A C
62 8 3adant1r φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t f A g A t T f t + g t A
63 9 3adant1r φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t f A g A t T f t g t A
64 10 adantlr φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t y t T y A
65 simpr1 φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t d +
66 simpr2 φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t d < 1
67 12 adantr φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t U J
68 13 adantr φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t Z U
69 simpr3l φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t p A
70 simp3r1 d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t t T 0 p t p t 1
71 70 adantl φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t t T 0 p t p t 1
72 simp3r2 d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t p Z = 0
73 72 adantl φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t p Z = 0
74 simp3r3 d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t t T U d p t
75 74 adantl φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t t T U d p t
76 1 58 59 3 60 5 6 61 62 63 64 65 66 67 68 69 71 73 75 stoweidlem52 φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t v J Z v v U e + x A t T 0 x t x t 1 t v x t < e t T U 1 e < x t
77 76 ex φ d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t v J Z v v U e + x A t T 0 x t x t 1 t v x t < e t T U 1 e < x t
78 77 exlimdvv φ p d d + d < 1 p A t T 0 p t p t 1 p Z = 0 t T U d p t v J Z v v U e + x A t T 0 x t x t 1 t v x t < e t T U 1 e < x t
79 49 78 mpd φ v J Z v v U e + x A t T 0 x t x t 1 t v x t < e t T U 1 e < x t