Metamath Proof Explorer

Theorem itg2cnlem1

Description: Lemma for itgcn . (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Hypotheses itg2cn.1 ⊢φ→F:ℝ⟶0+∞
itg2cn.2 ⊢φ→F∈MblFn
itg2cn.3 ⊢φ→∫2⁡F∈ℝ
Assertion itg2cnlem1 ⊢φ→supran⁡n∈ℕ⟼∫2⁡x∈ℝ⟼ifF⁡x≤nF⁡x0ℝ*<=∫2⁡F

Proof

Step Hyp Ref Expression
1 itg2cn.1 ⊢φ→F:ℝ⟶0+∞
2 itg2cn.2 ⊢φ→F∈MblFn
3 itg2cn.3 ⊢φ→∫2⁡F∈ℝ
4 fvex ⊢F⁡x∈V
5 c0ex ⊢0∈V
6 4 5 ifex ⊢ifF⁡x≤nF⁡x0∈V
7 eqid ⊢x∈ℝ⟼ifF⁡x≤nF⁡x0=x∈ℝ⟼ifF⁡x≤nF⁡x0
8 7 fvmpt2 ⊢x∈ℝ∧ifF⁡x≤nF⁡x0∈V→x∈ℝ⟼ifF⁡x≤nF⁡x0⁡x=ifF⁡x≤nF⁡x0
9 6 8 mpan2 ⊢x∈ℝ→x∈ℝ⟼ifF⁡x≤nF⁡x0⁡x=ifF⁡x≤nF⁡x0
10 9 mpteq2dv ⊢x∈ℝ→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡x=n∈ℕ⟼ifF⁡x≤nF⁡x0
11 10 rneqd ⊢x∈ℝ→ran⁡n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡x=ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0
12 11 supeq1d ⊢x∈ℝ→supran⁡n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡xℝ<=supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<
13 12 mpteq2ia ⊢x∈ℝ⟼supran⁡n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡xℝ<=x∈ℝ⟼supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<
14 nfcv ⊢Ⅎ_ysupran⁡n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡xℝ<
15 nfcv ⊢Ⅎ_xℕ
16 nfmpt1 ⊢Ⅎ_xx∈ℝ⟼ifF⁡x≤nF⁡x0
17 15 16 nfmpt ⊢Ⅎ_xn∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0
18 nfcv ⊢Ⅎ_xm
19 17 18 nffv ⊢Ⅎ_xn∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m
20 nfcv ⊢Ⅎ_xy
21 19 20 nffv ⊢Ⅎ_xn∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡y
22 15 21 nfmpt ⊢Ⅎ_xm∈ℕ⟼n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡y
23 22 nfrn ⊢Ⅎ_xran⁡m∈ℕ⟼n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡y
24 nfcv ⊢Ⅎ_xℝ
25 nfcv ⊢Ⅎ_x<
26 23 24 25 nfsup ⊢Ⅎ_xsupran⁡m∈ℕ⟼n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡yℝ<
27 fveq2 ⊢x=y→x∈ℝ⟼ifF⁡x≤nF⁡x0⁡x=x∈ℝ⟼ifF⁡x≤nF⁡x0⁡y
28 27 mpteq2dv ⊢x=y→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡x=n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡y
29 breq2 ⊢n=m→F⁡x≤n↔F⁡x≤m
30 29 ifbid ⊢n=m→ifF⁡x≤nF⁡x0=ifF⁡x≤mF⁡x0
31 30 mpteq2dv ⊢n=m→x∈ℝ⟼ifF⁡x≤nF⁡x0=x∈ℝ⟼ifF⁡x≤mF⁡x0
32 31 fveq1d ⊢n=m→x∈ℝ⟼ifF⁡x≤nF⁡x0⁡y=x∈ℝ⟼ifF⁡x≤mF⁡x0⁡y
33 32 cbvmptv ⊢n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡y=m∈ℕ⟼x∈ℝ⟼ifF⁡x≤mF⁡x0⁡y
34 eqid ⊢n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0=n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0
35 reex ⊢ℝ∈V
36 35 mptex ⊢x∈ℝ⟼ifF⁡x≤mF⁡x0∈V
37 31 34 36 fvmpt ⊢m∈ℕ→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m=x∈ℝ⟼ifF⁡x≤mF⁡x0
38 37 fveq1d ⊢m∈ℕ→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡y=x∈ℝ⟼ifF⁡x≤mF⁡x0⁡y
39 38 mpteq2ia ⊢m∈ℕ⟼n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡y=m∈ℕ⟼x∈ℝ⟼ifF⁡x≤mF⁡x0⁡y
40 33 39 eqtr4i ⊢n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡y=m∈ℕ⟼n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡y
41 28 40 eqtrdi ⊢x=y→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡x=m∈ℕ⟼n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡y
42 41 rneqd ⊢x=y→ran⁡n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡x=ran⁡m∈ℕ⟼n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡y
43 42 supeq1d ⊢x=y→supran⁡n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡xℝ<=supran⁡m∈ℕ⟼n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡yℝ<
44 14 26 43 cbvmpt ⊢x∈ℝ⟼supran⁡n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡xℝ<=y∈ℝ⟼supran⁡m∈ℕ⟼n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡yℝ<
45 13 44 eqtr3i ⊢x∈ℝ⟼supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<=y∈ℝ⟼supran⁡m∈ℕ⟼n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡yℝ<
46 fveq2 ⊢x=y→F⁡x=F⁡y
47 46 breq1d ⊢x=y→F⁡x≤m↔F⁡y≤m
48 47 46 ifbieq1d ⊢x=y→ifF⁡x≤mF⁡x0=ifF⁡y≤mF⁡y0
49 48 cbvmptv ⊢x∈ℝ⟼ifF⁡x≤mF⁡x0=y∈ℝ⟼ifF⁡y≤mF⁡y0
50 37 adantl ⊢φ∧m∈ℕ→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m=x∈ℝ⟼ifF⁡x≤mF⁡x0
51 nnre ⊢m∈ℕ→m∈ℝ
52 51 ad2antlr ⊢φ∧m∈ℕ∧y∈ℝ→m∈ℝ
53 52 rexrd ⊢φ∧m∈ℕ∧y∈ℝ→m∈ℝ*
54 elioopnf ⊢m∈ℝ*→F⁡y∈m+∞↔F⁡y∈ℝ∧m<F⁡y
55 53 54 syl ⊢φ∧m∈ℕ∧y∈ℝ→F⁡y∈m+∞↔F⁡y∈ℝ∧m<F⁡y
56 simpr ⊢φ∧m∈ℕ∧y∈ℝ→y∈ℝ
57 1 ffnd ⊢φ→FFnℝ
58 57 ad2antrr ⊢φ∧m∈ℕ∧y∈ℝ→FFnℝ
59 elpreima ⊢FFnℝ→y∈F-1m+∞↔y∈ℝ∧F⁡y∈m+∞
60 58 59 syl ⊢φ∧m∈ℕ∧y∈ℝ→y∈F-1m+∞↔y∈ℝ∧F⁡y∈m+∞
61 56 60 mpbirand ⊢φ∧m∈ℕ∧y∈ℝ→y∈F-1m+∞↔F⁡y∈m+∞
62 rge0ssre ⊢0+∞⊆ℝ
63 fss ⊢F:ℝ⟶0+∞∧0+∞⊆ℝ→F:ℝ⟶ℝ
64 1 62 63 sylancl ⊢φ→F:ℝ⟶ℝ
65 64 adantr ⊢φ∧m∈ℕ→F:ℝ⟶ℝ
66 65 ffvelcdmda ⊢φ∧m∈ℕ∧y∈ℝ→F⁡y∈ℝ
67 66 biantrurd ⊢φ∧m∈ℕ∧y∈ℝ→m<F⁡y↔F⁡y∈ℝ∧m<F⁡y
68 55 61 67 3bitr4d ⊢φ∧m∈ℕ∧y∈ℝ→y∈F-1m+∞↔m<F⁡y
69 68 notbid ⊢φ∧m∈ℕ∧y∈ℝ→¬y∈F-1m+∞↔¬m<F⁡y
70 eldif ⊢y∈ℝ∖F-1m+∞↔y∈ℝ∧¬y∈F-1m+∞
71 70 baib ⊢y∈ℝ→y∈ℝ∖F-1m+∞↔¬y∈F-1m+∞
72 71 adantl ⊢φ∧m∈ℕ∧y∈ℝ→y∈ℝ∖F-1m+∞↔¬y∈F-1m+∞
73 66 52 lenltd ⊢φ∧m∈ℕ∧y∈ℝ→F⁡y≤m↔¬m<F⁡y
74 69 72 73 3bitr4d ⊢φ∧m∈ℕ∧y∈ℝ→y∈ℝ∖F-1m+∞↔F⁡y≤m
75 74 ifbid ⊢φ∧m∈ℕ∧y∈ℝ→ify∈ℝ∖F-1m+∞F⁡y0=ifF⁡y≤mF⁡y0
76 75 mpteq2dva ⊢φ∧m∈ℕ→y∈ℝ⟼ify∈ℝ∖F-1m+∞F⁡y0=y∈ℝ⟼ifF⁡y≤mF⁡y0
77 49 50 76 3eqtr4a ⊢φ∧m∈ℕ→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m=y∈ℝ⟼ify∈ℝ∖F-1m+∞F⁡y0
78 difss ⊢ℝ∖F-1m+∞⊆ℝ
79 78 a1i ⊢φ∧m∈ℕ→ℝ∖F-1m+∞⊆ℝ
80 rembl ⊢ℝ∈dom⁡vol
81 80 a1i ⊢φ∧m∈ℕ→ℝ∈dom⁡vol
82 fvex ⊢F⁡y∈V
83 82 5 ifex ⊢ify∈ℝ∖F-1m+∞F⁡y0∈V
84 83 a1i ⊢φ∧m∈ℕ∧y∈ℝ∖F-1m+∞→ify∈ℝ∖F-1m+∞F⁡y0∈V
85 eldifn ⊢y∈ℝ∖ℝ∖F-1m+∞→¬y∈ℝ∖F-1m+∞
86 85 adantl ⊢φ∧m∈ℕ∧y∈ℝ∖ℝ∖F-1m+∞→¬y∈ℝ∖F-1m+∞
87 86 iffalsed ⊢φ∧m∈ℕ∧y∈ℝ∖ℝ∖F-1m+∞→ify∈ℝ∖F-1m+∞F⁡y0=0
88 iftrue ⊢y∈ℝ∖F-1m+∞→ify∈ℝ∖F-1m+∞F⁡y0=F⁡y
89 88 mpteq2ia ⊢y∈ℝ∖F-1m+∞⟼ify∈ℝ∖F-1m+∞F⁡y0=y∈ℝ∖F-1m+∞⟼F⁡y
90 resmpt ⊢ℝ∖F-1m+∞⊆ℝ→y∈ℝ⟼F⁡y↾ℝ∖F-1m+∞=y∈ℝ∖F-1m+∞⟼F⁡y
91 78 90 ax-mp ⊢y∈ℝ⟼F⁡y↾ℝ∖F-1m+∞=y∈ℝ∖F-1m+∞⟼F⁡y
92 89 91 eqtr4i ⊢y∈ℝ∖F-1m+∞⟼ify∈ℝ∖F-1m+∞F⁡y0=y∈ℝ⟼F⁡y↾ℝ∖F-1m+∞
93 1 feqmptd ⊢φ→F=y∈ℝ⟼F⁡y
94 93 2 eqeltrrd ⊢φ→y∈ℝ⟼F⁡y∈MblFn
95 mbfima ⊢F∈MblFn∧F:ℝ⟶ℝ→F-1m+∞∈dom⁡vol
96 2 64 95 syl2anc ⊢φ→F-1m+∞∈dom⁡vol
97 cmmbl ⊢F-1m+∞∈dom⁡vol→ℝ∖F-1m+∞∈dom⁡vol
98 96 97 syl ⊢φ→ℝ∖F-1m+∞∈dom⁡vol
99 mbfres ⊢y∈ℝ⟼F⁡y∈MblFn∧ℝ∖F-1m+∞∈dom⁡vol→y∈ℝ⟼F⁡y↾ℝ∖F-1m+∞∈MblFn
100 94 98 99 syl2anc ⊢φ→y∈ℝ⟼F⁡y↾ℝ∖F-1m+∞∈MblFn
101 92 100 eqeltrid ⊢φ→y∈ℝ∖F-1m+∞⟼ify∈ℝ∖F-1m+∞F⁡y0∈MblFn
102 101 adantr ⊢φ∧m∈ℕ→y∈ℝ∖F-1m+∞⟼ify∈ℝ∖F-1m+∞F⁡y0∈MblFn
103 79 81 84 87 102 mbfss ⊢φ∧m∈ℕ→y∈ℝ⟼ify∈ℝ∖F-1m+∞F⁡y0∈MblFn
104 77 103 eqeltrd ⊢φ∧m∈ℕ→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m∈MblFn
105 1 ffvelcdmda ⊢φ∧x∈ℝ→F⁡x∈0+∞
106 0e0icopnf ⊢0∈0+∞
107 ifcl ⊢F⁡x∈0+∞∧0∈0+∞→ifF⁡x≤mF⁡x0∈0+∞
108 105 106 107 sylancl ⊢φ∧x∈ℝ→ifF⁡x≤mF⁡x0∈0+∞
109 108 adantlr ⊢φ∧m∈ℕ∧x∈ℝ→ifF⁡x≤mF⁡x0∈0+∞
110 50 109 fmpt3d ⊢φ∧m∈ℕ→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m:ℝ⟶0+∞
111 elrege0 ⊢F⁡x∈0+∞↔F⁡x∈ℝ∧0≤F⁡x
112 105 111 sylib ⊢φ∧x∈ℝ→F⁡x∈ℝ∧0≤F⁡x
113 112 simpld ⊢φ∧x∈ℝ→F⁡x∈ℝ
114 113 adantlr ⊢φ∧m∈ℕ∧x∈ℝ→F⁡x∈ℝ
115 114 adantr ⊢φ∧m∈ℕ∧x∈ℝ∧F⁡x≤m→F⁡x∈ℝ
116 115 leidd ⊢φ∧m∈ℕ∧x∈ℝ∧F⁡x≤m→F⁡x≤F⁡x
117 iftrue ⊢F⁡x≤m→ifF⁡x≤mF⁡x0=F⁡x
118 117 adantl ⊢φ∧m∈ℕ∧x∈ℝ∧F⁡x≤m→ifF⁡x≤mF⁡x0=F⁡x
119 51 ad3antlr ⊢φ∧m∈ℕ∧x∈ℝ∧F⁡x≤m→m∈ℝ
120 peano2re ⊢m∈ℝ→m+1∈ℝ
121 119 120 syl ⊢φ∧m∈ℕ∧x∈ℝ∧F⁡x≤m→m+1∈ℝ
122 simpr ⊢φ∧m∈ℕ∧x∈ℝ∧F⁡x≤m→F⁡x≤m
123 119 lep1d ⊢φ∧m∈ℕ∧x∈ℝ∧F⁡x≤m→m≤m+1
124 115 119 121 122 123 letrd ⊢φ∧m∈ℕ∧x∈ℝ∧F⁡x≤m→F⁡x≤m+1
125 124 iftrued ⊢φ∧m∈ℕ∧x∈ℝ∧F⁡x≤m→ifF⁡x≤m+1F⁡x0=F⁡x
126 116 118 125 3brtr4d ⊢φ∧m∈ℕ∧x∈ℝ∧F⁡x≤m→ifF⁡x≤mF⁡x0≤ifF⁡x≤m+1F⁡x0
127 iffalse ⊢¬F⁡x≤m→ifF⁡x≤mF⁡x0=0
128 127 adantl ⊢φ∧m∈ℕ∧x∈ℝ∧¬F⁡x≤m→ifF⁡x≤mF⁡x0=0
129 112 simprd ⊢φ∧x∈ℝ→0≤F⁡x
130 0le0 ⊢0≤0
131 breq2 ⊢F⁡x=ifF⁡x≤m+1F⁡x0→0≤F⁡x↔0≤ifF⁡x≤m+1F⁡x0
132 breq2 ⊢0=ifF⁡x≤m+1F⁡x0→0≤0↔0≤ifF⁡x≤m+1F⁡x0
133 131 132 ifboth ⊢0≤F⁡x∧0≤0→0≤ifF⁡x≤m+1F⁡x0
134 129 130 133 sylancl ⊢φ∧x∈ℝ→0≤ifF⁡x≤m+1F⁡x0
135 134 adantlr ⊢φ∧m∈ℕ∧x∈ℝ→0≤ifF⁡x≤m+1F⁡x0
136 135 adantr ⊢φ∧m∈ℕ∧x∈ℝ∧¬F⁡x≤m→0≤ifF⁡x≤m+1F⁡x0
137 128 136 eqbrtrd ⊢φ∧m∈ℕ∧x∈ℝ∧¬F⁡x≤m→ifF⁡x≤mF⁡x0≤ifF⁡x≤m+1F⁡x0
138 126 137 pm2.61dan ⊢φ∧m∈ℕ∧x∈ℝ→ifF⁡x≤mF⁡x0≤ifF⁡x≤m+1F⁡x0
139 138 ralrimiva ⊢φ∧m∈ℕ→∀x∈ℝifF⁡x≤mF⁡x0≤ifF⁡x≤m+1F⁡x0
140 4 5 ifex ⊢ifF⁡x≤m+1F⁡x0∈V
141 140 a1i ⊢φ∧m∈ℕ∧x∈ℝ→ifF⁡x≤m+1F⁡x0∈V
142 eqidd ⊢φ∧m∈ℕ→x∈ℝ⟼ifF⁡x≤mF⁡x0=x∈ℝ⟼ifF⁡x≤mF⁡x0
143 eqidd ⊢φ∧m∈ℕ→x∈ℝ⟼ifF⁡x≤m+1F⁡x0=x∈ℝ⟼ifF⁡x≤m+1F⁡x0
144 81 109 141 142 143 ofrfval2 ⊢φ∧m∈ℕ→x∈ℝ⟼ifF⁡x≤mF⁡x0≤fx∈ℝ⟼ifF⁡x≤m+1F⁡x0↔∀x∈ℝifF⁡x≤mF⁡x0≤ifF⁡x≤m+1F⁡x0
145 139 144 mpbird ⊢φ∧m∈ℕ→x∈ℝ⟼ifF⁡x≤mF⁡x0≤fx∈ℝ⟼ifF⁡x≤m+1F⁡x0
146 peano2nn ⊢m∈ℕ→m+1∈ℕ
147 146 adantl ⊢φ∧m∈ℕ→m+1∈ℕ
148 breq2 ⊢n=m+1→F⁡x≤n↔F⁡x≤m+1
149 148 ifbid ⊢n=m+1→ifF⁡x≤nF⁡x0=ifF⁡x≤m+1F⁡x0
150 149 mpteq2dv ⊢n=m+1→x∈ℝ⟼ifF⁡x≤nF⁡x0=x∈ℝ⟼ifF⁡x≤m+1F⁡x0
151 35 mptex ⊢x∈ℝ⟼ifF⁡x≤m+1F⁡x0∈V
152 150 34 151 fvmpt ⊢m+1∈ℕ→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m+1=x∈ℝ⟼ifF⁡x≤m+1F⁡x0
153 147 152 syl ⊢φ∧m∈ℕ→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m+1=x∈ℝ⟼ifF⁡x≤m+1F⁡x0
154 145 50 153 3brtr4d ⊢φ∧m∈ℕ→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m≤fn∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m+1
155 64 ffvelcdmda ⊢φ∧y∈ℝ→F⁡y∈ℝ
156 37 adantl ⊢φ∧y∈ℝ∧m∈ℕ→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m=x∈ℝ⟼ifF⁡x≤mF⁡x0
157 156 fveq1d ⊢φ∧y∈ℝ∧m∈ℕ→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡y=x∈ℝ⟼ifF⁡x≤mF⁡x0⁡y
158 113 leidd ⊢φ∧x∈ℝ→F⁡x≤F⁡x
159 breq1 ⊢F⁡x=ifF⁡x≤mF⁡x0→F⁡x≤F⁡x↔ifF⁡x≤mF⁡x0≤F⁡x
160 breq1 ⊢0=ifF⁡x≤mF⁡x0→0≤F⁡x↔ifF⁡x≤mF⁡x0≤F⁡x
161 159 160 ifboth ⊢F⁡x≤F⁡x∧0≤F⁡x→ifF⁡x≤mF⁡x0≤F⁡x
162 158 129 161 syl2anc ⊢φ∧x∈ℝ→ifF⁡x≤mF⁡x0≤F⁡x
163 162 adantlr ⊢φ∧m∈ℕ∧x∈ℝ→ifF⁡x≤mF⁡x0≤F⁡x
164 163 ralrimiva ⊢φ∧m∈ℕ→∀x∈ℝifF⁡x≤mF⁡x0≤F⁡x
165 35 a1i ⊢φ∧m∈ℕ→ℝ∈V
166 4 5 ifex ⊢ifF⁡x≤mF⁡x0∈V
167 166 a1i ⊢φ∧m∈ℕ∧x∈ℝ→ifF⁡x≤mF⁡x0∈V
168 1 feqmptd ⊢φ→F=x∈ℝ⟼F⁡x
169 168 adantr ⊢φ∧m∈ℕ→F=x∈ℝ⟼F⁡x
170 165 167 114 142 169 ofrfval2 ⊢φ∧m∈ℕ→x∈ℝ⟼ifF⁡x≤mF⁡x0≤fF↔∀x∈ℝifF⁡x≤mF⁡x0≤F⁡x
171 164 170 mpbird ⊢φ∧m∈ℕ→x∈ℝ⟼ifF⁡x≤mF⁡x0≤fF
172 167 fmpttd ⊢φ∧m∈ℕ→x∈ℝ⟼ifF⁡x≤mF⁡x0:ℝ⟶V
173 172 ffnd ⊢φ∧m∈ℕ→x∈ℝ⟼ifF⁡x≤mF⁡x0Fnℝ
174 57 adantr ⊢φ∧m∈ℕ→FFnℝ
175 inidm ⊢ℝ∩ℝ=ℝ
176 eqidd ⊢φ∧m∈ℕ∧y∈ℝ→x∈ℝ⟼ifF⁡x≤mF⁡x0⁡y=x∈ℝ⟼ifF⁡x≤mF⁡x0⁡y
177 eqidd ⊢φ∧m∈ℕ∧y∈ℝ→F⁡y=F⁡y
178 173 174 165 165 175 176 177 ofrfval ⊢φ∧m∈ℕ→x∈ℝ⟼ifF⁡x≤mF⁡x0≤fF↔∀y∈ℝx∈ℝ⟼ifF⁡x≤mF⁡x0⁡y≤F⁡y
179 171 178 mpbid ⊢φ∧m∈ℕ→∀y∈ℝx∈ℝ⟼ifF⁡x≤mF⁡x0⁡y≤F⁡y
180 179 r19.21bi ⊢φ∧m∈ℕ∧y∈ℝ→x∈ℝ⟼ifF⁡x≤mF⁡x0⁡y≤F⁡y
181 180 an32s ⊢φ∧y∈ℝ∧m∈ℕ→x∈ℝ⟼ifF⁡x≤mF⁡x0⁡y≤F⁡y
182 157 181 eqbrtrd ⊢φ∧y∈ℝ∧m∈ℕ→n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡y≤F⁡y
183 182 ralrimiva ⊢φ∧y∈ℝ→∀m∈ℕn∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡y≤F⁡y
184 brralrspcev ⊢F⁡y∈ℝ∧∀m∈ℕn∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡y≤F⁡y→∃z∈ℝ∀m∈ℕn∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡y≤z
185 155 183 184 syl2anc ⊢φ∧y∈ℝ→∃z∈ℝ∀m∈ℕn∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m⁡y≤z
186 31 fveq2d ⊢n=m→∫2⁡x∈ℝ⟼ifF⁡x≤nF⁡x0=∫2⁡x∈ℝ⟼ifF⁡x≤mF⁡x0
187 186 cbvmptv ⊢n∈ℕ⟼∫2⁡x∈ℝ⟼ifF⁡x≤nF⁡x0=m∈ℕ⟼∫2⁡x∈ℝ⟼ifF⁡x≤mF⁡x0
188 37 fveq2d ⊢m∈ℕ→∫2⁡n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m=∫2⁡x∈ℝ⟼ifF⁡x≤mF⁡x0
189 188 mpteq2ia ⊢m∈ℕ⟼∫2⁡n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m=m∈ℕ⟼∫2⁡x∈ℝ⟼ifF⁡x≤mF⁡x0
190 187 189 eqtr4i ⊢n∈ℕ⟼∫2⁡x∈ℝ⟼ifF⁡x≤nF⁡x0=m∈ℕ⟼∫2⁡n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m
191 190 rneqi ⊢ran⁡n∈ℕ⟼∫2⁡x∈ℝ⟼ifF⁡x≤nF⁡x0=ran⁡m∈ℕ⟼∫2⁡n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡m
192 191 supeq1i ⊢supran⁡n∈ℕ⟼∫2⁡x∈ℝ⟼ifF⁡x≤nF⁡x0ℝ*<=supran⁡m∈ℕ⟼∫2⁡n∈ℕ⟼x∈ℝ⟼ifF⁡x≤nF⁡x0⁡mℝ*<
193 45 104 110 154 185 192 itg2mono ⊢φ→∫2⁡x∈ℝ⟼supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<=supran⁡n∈ℕ⟼∫2⁡x∈ℝ⟼ifF⁡x≤nF⁡x0ℝ*<
194 eqid ⊢n∈ℕ⟼ifF⁡x≤nF⁡x0=n∈ℕ⟼ifF⁡x≤nF⁡x0
195 30 194 166 fvmpt ⊢m∈ℕ→n∈ℕ⟼ifF⁡x≤nF⁡x0⁡m=ifF⁡x≤mF⁡x0
196 195 adantl ⊢φ∧x∈ℝ∧m∈ℕ→n∈ℕ⟼ifF⁡x≤nF⁡x0⁡m=ifF⁡x≤mF⁡x0
197 162 adantr ⊢φ∧x∈ℝ∧m∈ℕ→ifF⁡x≤mF⁡x0≤F⁡x
198 196 197 eqbrtrd ⊢φ∧x∈ℝ∧m∈ℕ→n∈ℕ⟼ifF⁡x≤nF⁡x0⁡m≤F⁡x
199 198 ralrimiva ⊢φ∧x∈ℝ→∀m∈ℕn∈ℕ⟼ifF⁡x≤nF⁡x0⁡m≤F⁡x
200 6 a1i ⊢φ∧x∈ℝ∧n∈ℕ→ifF⁡x≤nF⁡x0∈V
201 200 fmpttd ⊢φ∧x∈ℝ→n∈ℕ⟼ifF⁡x≤nF⁡x0:ℕ⟶V
202 201 ffnd ⊢φ∧x∈ℝ→n∈ℕ⟼ifF⁡x≤nF⁡x0Fnℕ
203 breq1 ⊢w=n∈ℕ⟼ifF⁡x≤nF⁡x0⁡m→w≤F⁡x↔n∈ℕ⟼ifF⁡x≤nF⁡x0⁡m≤F⁡x
204 203 ralrn ⊢n∈ℕ⟼ifF⁡x≤nF⁡x0Fnℕ→∀w∈ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0w≤F⁡x↔∀m∈ℕn∈ℕ⟼ifF⁡x≤nF⁡x0⁡m≤F⁡x
205 202 204 syl ⊢φ∧x∈ℝ→∀w∈ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0w≤F⁡x↔∀m∈ℕn∈ℕ⟼ifF⁡x≤nF⁡x0⁡m≤F⁡x
206 199 205 mpbird ⊢φ∧x∈ℝ→∀w∈ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0w≤F⁡x
207 113 adantr ⊢φ∧x∈ℝ∧n∈ℕ→F⁡x∈ℝ
208 0re ⊢0∈ℝ
209 ifcl ⊢F⁡x∈ℝ∧0∈ℝ→ifF⁡x≤nF⁡x0∈ℝ
210 207 208 209 sylancl ⊢φ∧x∈ℝ∧n∈ℕ→ifF⁡x≤nF⁡x0∈ℝ
211 210 fmpttd ⊢φ∧x∈ℝ→n∈ℕ⟼ifF⁡x≤nF⁡x0:ℕ⟶ℝ
212 211 frnd ⊢φ∧x∈ℝ→ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0⊆ℝ
213 1nn ⊢1∈ℕ
214 194 210 dmmptd ⊢φ∧x∈ℝ→dom⁡n∈ℕ⟼ifF⁡x≤nF⁡x0=ℕ
215 213 214 eleqtrrid ⊢φ∧x∈ℝ→1∈dom⁡n∈ℕ⟼ifF⁡x≤nF⁡x0
216 n0i ⊢1∈dom⁡n∈ℕ⟼ifF⁡x≤nF⁡x0→¬dom⁡n∈ℕ⟼ifF⁡x≤nF⁡x0=∅
217 dm0rn0 ⊢dom⁡n∈ℕ⟼ifF⁡x≤nF⁡x0=∅↔ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0=∅
218 217 necon3bbii ⊢¬dom⁡n∈ℕ⟼ifF⁡x≤nF⁡x0=∅↔ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0≠∅
219 216 218 sylib ⊢1∈dom⁡n∈ℕ⟼ifF⁡x≤nF⁡x0→ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0≠∅
220 215 219 syl ⊢φ∧x∈ℝ→ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0≠∅
221 brralrspcev ⊢F⁡x∈ℝ∧∀w∈ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0w≤F⁡x→∃z∈ℝ∀w∈ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0w≤z
222 113 206 221 syl2anc ⊢φ∧x∈ℝ→∃z∈ℝ∀w∈ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0w≤z
223 suprleub ⊢ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0⊆ℝ∧ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0≠∅∧∃z∈ℝ∀w∈ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0w≤z∧F⁡x∈ℝ→supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<≤F⁡x↔∀w∈ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0w≤F⁡x
224 212 220 222 113 223 syl31anc ⊢φ∧x∈ℝ→supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<≤F⁡x↔∀w∈ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0w≤F⁡x
225 206 224 mpbird ⊢φ∧x∈ℝ→supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<≤F⁡x
226 arch ⊢F⁡x∈ℝ→∃m∈ℕF⁡x<m
227 113 226 syl ⊢φ∧x∈ℝ→∃m∈ℕF⁡x<m
228 195 ad2antrl ⊢φ∧x∈ℝ∧m∈ℕ∧F⁡x<m→n∈ℕ⟼ifF⁡x≤nF⁡x0⁡m=ifF⁡x≤mF⁡x0
229 ltle ⊢F⁡x∈ℝ∧m∈ℝ→F⁡x<m→F⁡x≤m
230 113 51 229 syl2an ⊢φ∧x∈ℝ∧m∈ℕ→F⁡x<m→F⁡x≤m
231 230 impr ⊢φ∧x∈ℝ∧m∈ℕ∧F⁡x<m→F⁡x≤m
232 231 iftrued ⊢φ∧x∈ℝ∧m∈ℕ∧F⁡x<m→ifF⁡x≤mF⁡x0=F⁡x
233 228 232 eqtrd ⊢φ∧x∈ℝ∧m∈ℕ∧F⁡x<m→n∈ℕ⟼ifF⁡x≤nF⁡x0⁡m=F⁡x
234 202 adantr ⊢φ∧x∈ℝ∧m∈ℕ∧F⁡x<m→n∈ℕ⟼ifF⁡x≤nF⁡x0Fnℕ
235 simprl ⊢φ∧x∈ℝ∧m∈ℕ∧F⁡x<m→m∈ℕ
236 fnfvelrn ⊢n∈ℕ⟼ifF⁡x≤nF⁡x0Fnℕ∧m∈ℕ→n∈ℕ⟼ifF⁡x≤nF⁡x0⁡m∈ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0
237 234 235 236 syl2anc ⊢φ∧x∈ℝ∧m∈ℕ∧F⁡x<m→n∈ℕ⟼ifF⁡x≤nF⁡x0⁡m∈ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0
238 233 237 eqeltrrd ⊢φ∧x∈ℝ∧m∈ℕ∧F⁡x<m→F⁡x∈ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0
239 227 238 rexlimddv ⊢φ∧x∈ℝ→F⁡x∈ran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0
240 212 220 222 239 suprubd ⊢φ∧x∈ℝ→F⁡x≤supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<
241 212 220 222 suprcld ⊢φ∧x∈ℝ→supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<∈ℝ
242 241 113 letri3d ⊢φ∧x∈ℝ→supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<=F⁡x↔supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<≤F⁡x∧F⁡x≤supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<
243 225 240 242 mpbir2and ⊢φ∧x∈ℝ→supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<=F⁡x
244 243 mpteq2dva ⊢φ→x∈ℝ⟼supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<=x∈ℝ⟼F⁡x
245 244 168 eqtr4d ⊢φ→x∈ℝ⟼supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<=F
246 245 fveq2d ⊢φ→∫2⁡x∈ℝ⟼supran⁡n∈ℕ⟼ifF⁡x≤nF⁡x0ℝ<=∫2⁡F
247 193 246 eqtr3d ⊢φ→supran⁡n∈ℕ⟼∫2⁡x∈ℝ⟼ifF⁡x≤nF⁡x0ℝ*<=∫2⁡F