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