MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovolunlem1a Structured version   Visualization version   GIF version

Theorem ovolunlem1a 24883
Description: Lemma for ovolun 24886. (Contributed by Mario Carneiro, 7-May-2015.)
Hypotheses
Ref Expression
ovolun.a (πœ‘ β†’ (𝐴 βŠ† ℝ ∧ (vol*β€˜π΄) ∈ ℝ))
ovolun.b (πœ‘ β†’ (𝐡 βŠ† ℝ ∧ (vol*β€˜π΅) ∈ ℝ))
ovolun.c (πœ‘ β†’ 𝐢 ∈ ℝ+)
ovolun.s 𝑆 = seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐹))
ovolun.t 𝑇 = seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐺))
ovolun.u π‘ˆ = seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))
ovolun.f1 (πœ‘ β†’ 𝐹 ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
ovolun.f2 (πœ‘ β†’ 𝐴 βŠ† βˆͺ ran ((,) ∘ 𝐹))
ovolun.f3 (πœ‘ β†’ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐢 / 2)))
ovolun.g1 (πœ‘ β†’ 𝐺 ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
ovolun.g2 (πœ‘ β†’ 𝐡 βŠ† βˆͺ ran ((,) ∘ 𝐺))
ovolun.g3 (πœ‘ β†’ sup(ran 𝑇, ℝ*, < ) ≀ ((vol*β€˜π΅) + (𝐢 / 2)))
ovolun.h 𝐻 = (𝑛 ∈ β„• ↦ if((𝑛 / 2) ∈ β„•, (πΊβ€˜(𝑛 / 2)), (πΉβ€˜((𝑛 + 1) / 2))))
Assertion
Ref Expression
ovolunlem1a ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘ˆβ€˜π‘˜) ≀ (((vol*β€˜π΄) + (vol*β€˜π΅)) + 𝐢))
Distinct variable groups:   π‘˜,𝑛,𝐢   π‘˜,𝐹,𝑛   π‘˜,𝐻   𝐴,π‘˜,𝑛   𝐡,π‘˜,𝑛   𝑆,π‘˜   𝑇,π‘˜   π‘˜,𝐺,𝑛   πœ‘,π‘˜,𝑛   π‘ˆ,π‘˜
Allowed substitution hints:   𝑆(𝑛)   𝑇(𝑛)   π‘ˆ(𝑛)   𝐻(𝑛)

Proof of Theorem ovolunlem1a
Dummy variables 𝑧 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovolun.g1 . . . . . . . . . 10 (πœ‘ β†’ 𝐺 ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
2 elovolmlem 24861 . . . . . . . . . 10 (𝐺 ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•) ↔ 𝐺:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
31, 2sylib 217 . . . . . . . . 9 (πœ‘ β†’ 𝐺:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
43adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐺:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
54ffvelcdmda 7039 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ (𝑛 / 2) ∈ β„•) β†’ (πΊβ€˜(𝑛 / 2)) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
6 nneo 12595 . . . . . . . . . . 11 (𝑛 ∈ β„• β†’ ((𝑛 / 2) ∈ β„• ↔ Β¬ ((𝑛 + 1) / 2) ∈ β„•))
76adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((𝑛 / 2) ∈ β„• ↔ Β¬ ((𝑛 + 1) / 2) ∈ β„•))
87con2bid 355 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((𝑛 + 1) / 2) ∈ β„• ↔ Β¬ (𝑛 / 2) ∈ β„•))
98biimpar 479 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ Β¬ (𝑛 / 2) ∈ β„•) β†’ ((𝑛 + 1) / 2) ∈ β„•)
10 ovolun.f1 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹 ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
11 elovolmlem 24861 . . . . . . . . . . 11 (𝐹 ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•) ↔ 𝐹:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
1210, 11sylib 217 . . . . . . . . . 10 (πœ‘ β†’ 𝐹:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
1312adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐹:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
1413ffvelcdmda 7039 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ ((𝑛 + 1) / 2) ∈ β„•) β†’ (πΉβ€˜((𝑛 + 1) / 2)) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
159, 14syldan 592 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ Β¬ (𝑛 / 2) ∈ β„•) β†’ (πΉβ€˜((𝑛 + 1) / 2)) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
165, 15ifclda 4525 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ if((𝑛 / 2) ∈ β„•, (πΊβ€˜(𝑛 / 2)), (πΉβ€˜((𝑛 + 1) / 2))) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
17 ovolun.h . . . . . 6 𝐻 = (𝑛 ∈ β„• ↦ if((𝑛 / 2) ∈ β„•, (πΊβ€˜(𝑛 / 2)), (πΉβ€˜((𝑛 + 1) / 2))))
1816, 17fmptd 7066 . . . . 5 (πœ‘ β†’ 𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
19 eqid 2733 . . . . . 6 ((abs ∘ βˆ’ ) ∘ 𝐻) = ((abs ∘ βˆ’ ) ∘ 𝐻)
20 ovolun.u . . . . . 6 π‘ˆ = seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))
2119, 20ovolsf 24859 . . . . 5 (𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) β†’ π‘ˆ:β„•βŸΆ(0[,)+∞))
2218, 21syl 17 . . . 4 (πœ‘ β†’ π‘ˆ:β„•βŸΆ(0[,)+∞))
23 rge0ssre 13382 . . . 4 (0[,)+∞) βŠ† ℝ
24 fss 6689 . . . 4 ((π‘ˆ:β„•βŸΆ(0[,)+∞) ∧ (0[,)+∞) βŠ† ℝ) β†’ π‘ˆ:β„•βŸΆβ„)
2522, 23, 24sylancl 587 . . 3 (πœ‘ β†’ π‘ˆ:β„•βŸΆβ„)
2625ffvelcdmda 7039 . 2 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘ˆβ€˜π‘˜) ∈ ℝ)
27 2nn 12234 . . . 4 2 ∈ β„•
28 peano2nn 12173 . . . . . . . . 9 (π‘˜ ∈ β„• β†’ (π‘˜ + 1) ∈ β„•)
2928adantl 483 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„•)
3029nnred 12176 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ ℝ)
3130rehalfcld 12408 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) / 2) ∈ ℝ)
3231flcld 13712 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (βŒŠβ€˜((π‘˜ + 1) / 2)) ∈ β„€)
33 ax-1cn 11117 . . . . . . . . 9 1 ∈ β„‚
34332timesi 12299 . . . . . . . 8 (2 Β· 1) = (1 + 1)
35 nnge1 12189 . . . . . . . . . 10 (π‘˜ ∈ β„• β†’ 1 ≀ π‘˜)
3635adantl 483 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 1 ≀ π‘˜)
37 nnre 12168 . . . . . . . . . . 11 (π‘˜ ∈ β„• β†’ π‘˜ ∈ ℝ)
3837adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ ℝ)
39 1re 11163 . . . . . . . . . . 11 1 ∈ ℝ
40 leadd1 11631 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ π‘˜ ∈ ℝ ∧ 1 ∈ ℝ) β†’ (1 ≀ π‘˜ ↔ (1 + 1) ≀ (π‘˜ + 1)))
4139, 39, 40mp3an13 1453 . . . . . . . . . 10 (π‘˜ ∈ ℝ β†’ (1 ≀ π‘˜ ↔ (1 + 1) ≀ (π‘˜ + 1)))
4238, 41syl 17 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 ≀ π‘˜ ↔ (1 + 1) ≀ (π‘˜ + 1)))
4336, 42mpbid 231 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 + 1) ≀ (π‘˜ + 1))
4434, 43eqbrtrid 5144 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2 Β· 1) ≀ (π‘˜ + 1))
45 2re 12235 . . . . . . . . . 10 2 ∈ ℝ
46 2pos 12264 . . . . . . . . . 10 0 < 2
4745, 46pm3.2i 472 . . . . . . . . 9 (2 ∈ ℝ ∧ 0 < 2)
48 lemuldiv2 12044 . . . . . . . . 9 ((1 ∈ ℝ ∧ (π‘˜ + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) β†’ ((2 Β· 1) ≀ (π‘˜ + 1) ↔ 1 ≀ ((π‘˜ + 1) / 2)))
4939, 47, 48mp3an13 1453 . . . . . . . 8 ((π‘˜ + 1) ∈ ℝ β†’ ((2 Β· 1) ≀ (π‘˜ + 1) ↔ 1 ≀ ((π‘˜ + 1) / 2)))
5030, 49syl 17 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· 1) ≀ (π‘˜ + 1) ↔ 1 ≀ ((π‘˜ + 1) / 2)))
5144, 50mpbid 231 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 1 ≀ ((π‘˜ + 1) / 2))
52 1z 12541 . . . . . . 7 1 ∈ β„€
53 flge 13719 . . . . . . 7 ((((π‘˜ + 1) / 2) ∈ ℝ ∧ 1 ∈ β„€) β†’ (1 ≀ ((π‘˜ + 1) / 2) ↔ 1 ≀ (βŒŠβ€˜((π‘˜ + 1) / 2))))
5431, 52, 53sylancl 587 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 ≀ ((π‘˜ + 1) / 2) ↔ 1 ≀ (βŒŠβ€˜((π‘˜ + 1) / 2))))
5551, 54mpbid 231 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 1 ≀ (βŒŠβ€˜((π‘˜ + 1) / 2)))
56 elnnz1 12537 . . . . 5 ((βŒŠβ€˜((π‘˜ + 1) / 2)) ∈ β„• ↔ ((βŒŠβ€˜((π‘˜ + 1) / 2)) ∈ β„€ ∧ 1 ≀ (βŒŠβ€˜((π‘˜ + 1) / 2))))
5732, 55, 56sylanbrc 584 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (βŒŠβ€˜((π‘˜ + 1) / 2)) ∈ β„•)
58 nnmulcl 12185 . . . 4 ((2 ∈ β„• ∧ (βŒŠβ€˜((π‘˜ + 1) / 2)) ∈ β„•) β†’ (2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ β„•)
5927, 57, 58sylancr 588 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ β„•)
6025ffvelcdmda 7039 . . 3 ((πœ‘ ∧ (2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ β„•) β†’ (π‘ˆβ€˜(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))) ∈ ℝ)
6159, 60syldan 592 . 2 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘ˆβ€˜(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))) ∈ ℝ)
62 ovolun.a . . . . . 6 (πœ‘ β†’ (𝐴 βŠ† ℝ ∧ (vol*β€˜π΄) ∈ ℝ))
6362simprd 497 . . . . 5 (πœ‘ β†’ (vol*β€˜π΄) ∈ ℝ)
64 ovolun.b . . . . . 6 (πœ‘ β†’ (𝐡 βŠ† ℝ ∧ (vol*β€˜π΅) ∈ ℝ))
6564simprd 497 . . . . 5 (πœ‘ β†’ (vol*β€˜π΅) ∈ ℝ)
6663, 65readdcld 11192 . . . 4 (πœ‘ β†’ ((vol*β€˜π΄) + (vol*β€˜π΅)) ∈ ℝ)
67 ovolun.c . . . . 5 (πœ‘ β†’ 𝐢 ∈ ℝ+)
6867rpred 12965 . . . 4 (πœ‘ β†’ 𝐢 ∈ ℝ)
6966, 68readdcld 11192 . . 3 (πœ‘ β†’ (((vol*β€˜π΄) + (vol*β€˜π΅)) + 𝐢) ∈ ℝ)
7069adantr 482 . 2 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((vol*β€˜π΄) + (vol*β€˜π΅)) + 𝐢) ∈ ℝ)
71 simpr 486 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
72 nnuz 12814 . . . . 5 β„• = (β„€β‰₯β€˜1)
7371, 72eleqtrdi 2844 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ (β„€β‰₯β€˜1))
74 nnz 12528 . . . . . . 7 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„€)
7574adantl 483 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„€)
76 flhalf 13744 . . . . . 6 (π‘˜ ∈ β„€ β†’ π‘˜ ≀ (2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))))
7775, 76syl 17 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ≀ (2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))))
78 nnz 12528 . . . . . . 7 ((2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ β„• β†’ (2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ β„€)
79 eluz 12785 . . . . . . 7 ((π‘˜ ∈ β„€ ∧ (2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ β„€) β†’ ((2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ (β„€β‰₯β€˜π‘˜) ↔ π‘˜ ≀ (2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))))
8074, 78, 79syl2an 597 . . . . . 6 ((π‘˜ ∈ β„• ∧ (2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ β„•) β†’ ((2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ (β„€β‰₯β€˜π‘˜) ↔ π‘˜ ≀ (2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))))
8171, 59, 80syl2anc 585 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ (β„€β‰₯β€˜π‘˜) ↔ π‘˜ ≀ (2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))))
8277, 81mpbird 257 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ (β„€β‰₯β€˜π‘˜))
83 elfznn 13479 . . . . 5 (𝑗 ∈ (1...(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))) β†’ 𝑗 ∈ β„•)
8419ovolfsf 24858 . . . . . . . . . 10 (𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) β†’ ((abs ∘ βˆ’ ) ∘ 𝐻):β„•βŸΆ(0[,)+∞))
8518, 84syl 17 . . . . . . . . 9 (πœ‘ β†’ ((abs ∘ βˆ’ ) ∘ 𝐻):β„•βŸΆ(0[,)+∞))
8685adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((abs ∘ βˆ’ ) ∘ 𝐻):β„•βŸΆ(0[,)+∞))
8786ffvelcdmda 7039 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘—) ∈ (0[,)+∞))
88 elrege0 13380 . . . . . . 7 ((((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘—) ∈ (0[,)+∞) ↔ ((((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘—) ∈ ℝ ∧ 0 ≀ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘—)))
8987, 88sylib 217 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ ((((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘—) ∈ ℝ ∧ 0 ≀ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘—)))
9089simpld 496 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘—) ∈ ℝ)
9183, 90sylan2 594 . . . 4 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))))) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘—) ∈ ℝ)
92 elfzuz 13446 . . . . . 6 (𝑗 ∈ ((π‘˜ + 1)...(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))) β†’ 𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1)))
93 eluznn 12851 . . . . . 6 (((π‘˜ + 1) ∈ β„• ∧ 𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))) β†’ 𝑗 ∈ β„•)
9429, 92, 93syl2an 597 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ ((π‘˜ + 1)...(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))))) β†’ 𝑗 ∈ β„•)
9589simprd 497 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ 0 ≀ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘—))
9694, 95syldan 592 . . . 4 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ ((π‘˜ + 1)...(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))))) β†’ 0 ≀ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘—))
9773, 82, 91, 96sermono 13949 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜π‘˜) ≀ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))))
9820fveq1i 6847 . . 3 (π‘ˆβ€˜π‘˜) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜π‘˜)
9920fveq1i 6847 . . 3 (π‘ˆβ€˜(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))))
10097, 98, 993brtr4g 5143 . 2 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘ˆβ€˜π‘˜) ≀ (π‘ˆβ€˜(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))))
101 eqid 2733 . . . . . . . . . 10 ((abs ∘ βˆ’ ) ∘ 𝐹) = ((abs ∘ βˆ’ ) ∘ 𝐹)
102 ovolun.s . . . . . . . . . 10 𝑆 = seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐹))
103101, 102ovolsf 24859 . . . . . . . . 9 (𝐹:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) β†’ 𝑆:β„•βŸΆ(0[,)+∞))
10412, 103syl 17 . . . . . . . 8 (πœ‘ β†’ 𝑆:β„•βŸΆ(0[,)+∞))
105104frnd 6680 . . . . . . 7 (πœ‘ β†’ ran 𝑆 βŠ† (0[,)+∞))
106105, 23sstrdi 3960 . . . . . 6 (πœ‘ β†’ ran 𝑆 βŠ† ℝ)
107106adantr 482 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ran 𝑆 βŠ† ℝ)
108104ffnd 6673 . . . . . 6 (πœ‘ β†’ 𝑆 Fn β„•)
109 fnfvelrn 7035 . . . . . 6 ((𝑆 Fn β„• ∧ (βŒŠβ€˜((π‘˜ + 1) / 2)) ∈ β„•) β†’ (π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ ran 𝑆)
110108, 57, 109syl2an2r 684 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ ran 𝑆)
111107, 110sseldd 3949 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ ℝ)
112 eqid 2733 . . . . . . . . . 10 ((abs ∘ βˆ’ ) ∘ 𝐺) = ((abs ∘ βˆ’ ) ∘ 𝐺)
113 ovolun.t . . . . . . . . . 10 𝑇 = seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐺))
114112, 113ovolsf 24859 . . . . . . . . 9 (𝐺:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) β†’ 𝑇:β„•βŸΆ(0[,)+∞))
1153, 114syl 17 . . . . . . . 8 (πœ‘ β†’ 𝑇:β„•βŸΆ(0[,)+∞))
116115frnd 6680 . . . . . . 7 (πœ‘ β†’ ran 𝑇 βŠ† (0[,)+∞))
117116, 23sstrdi 3960 . . . . . 6 (πœ‘ β†’ ran 𝑇 βŠ† ℝ)
118117adantr 482 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ran 𝑇 βŠ† ℝ)
119115ffnd 6673 . . . . . 6 (πœ‘ β†’ 𝑇 Fn β„•)
120 fnfvelrn 7035 . . . . . 6 ((𝑇 Fn β„• ∧ (βŒŠβ€˜((π‘˜ + 1) / 2)) ∈ β„•) β†’ (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ ran 𝑇)
121119, 57, 120syl2an2r 684 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ ran 𝑇)
122118, 121sseldd 3949 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ ℝ)
12368rehalfcld 12408 . . . . . 6 (πœ‘ β†’ (𝐢 / 2) ∈ ℝ)
12463, 123readdcld 11192 . . . . 5 (πœ‘ β†’ ((vol*β€˜π΄) + (𝐢 / 2)) ∈ ℝ)
125124adantr 482 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((vol*β€˜π΄) + (𝐢 / 2)) ∈ ℝ)
12665, 123readdcld 11192 . . . . 5 (πœ‘ β†’ ((vol*β€˜π΅) + (𝐢 / 2)) ∈ ℝ)
127126adantr 482 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((vol*β€˜π΅) + (𝐢 / 2)) ∈ ℝ)
128 ressxr 11207 . . . . . . . . 9 ℝ βŠ† ℝ*
129106, 128sstrdi 3960 . . . . . . . 8 (πœ‘ β†’ ran 𝑆 βŠ† ℝ*)
130 supxrcl 13243 . . . . . . . 8 (ran 𝑆 βŠ† ℝ* β†’ sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
131129, 130syl 17 . . . . . . 7 (πœ‘ β†’ sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
132 1nn 12172 . . . . . . . . . . 11 1 ∈ β„•
133104fdmd 6683 . . . . . . . . . . 11 (πœ‘ β†’ dom 𝑆 = β„•)
134132, 133eleqtrrid 2841 . . . . . . . . . 10 (πœ‘ β†’ 1 ∈ dom 𝑆)
135134ne0d 4299 . . . . . . . . 9 (πœ‘ β†’ dom 𝑆 β‰  βˆ…)
136 dm0rn0 5884 . . . . . . . . . 10 (dom 𝑆 = βˆ… ↔ ran 𝑆 = βˆ…)
137136necon3bii 2993 . . . . . . . . 9 (dom 𝑆 β‰  βˆ… ↔ ran 𝑆 β‰  βˆ…)
138135, 137sylib 217 . . . . . . . 8 (πœ‘ β†’ ran 𝑆 β‰  βˆ…)
139 supxrgtmnf 13257 . . . . . . . 8 ((ran 𝑆 βŠ† ℝ ∧ ran 𝑆 β‰  βˆ…) β†’ -∞ < sup(ran 𝑆, ℝ*, < ))
140106, 138, 139syl2anc 585 . . . . . . 7 (πœ‘ β†’ -∞ < sup(ran 𝑆, ℝ*, < ))
141 ovolun.f3 . . . . . . 7 (πœ‘ β†’ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐢 / 2)))
142 xrre 13097 . . . . . . 7 (((sup(ran 𝑆, ℝ*, < ) ∈ ℝ* ∧ ((vol*β€˜π΄) + (𝐢 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑆, ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐢 / 2)))) β†’ sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
143131, 124, 140, 141, 142syl22anc 838 . . . . . 6 (πœ‘ β†’ sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
144143adantr 482 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
145 supxrub 13252 . . . . . 6 ((ran 𝑆 βŠ† ℝ* ∧ (π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ ran 𝑆) β†’ (π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) ≀ sup(ran 𝑆, ℝ*, < ))
146129, 110, 145syl2an2r 684 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) ≀ sup(ran 𝑆, ℝ*, < ))
147141adantr 482 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐢 / 2)))
148111, 144, 125, 146, 147letrd 11320 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) ≀ ((vol*β€˜π΄) + (𝐢 / 2)))
149117, 128sstrdi 3960 . . . . . . . 8 (πœ‘ β†’ ran 𝑇 βŠ† ℝ*)
150 supxrcl 13243 . . . . . . . 8 (ran 𝑇 βŠ† ℝ* β†’ sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
151149, 150syl 17 . . . . . . 7 (πœ‘ β†’ sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
152115fdmd 6683 . . . . . . . . . . 11 (πœ‘ β†’ dom 𝑇 = β„•)
153132, 152eleqtrrid 2841 . . . . . . . . . 10 (πœ‘ β†’ 1 ∈ dom 𝑇)
154153ne0d 4299 . . . . . . . . 9 (πœ‘ β†’ dom 𝑇 β‰  βˆ…)
155 dm0rn0 5884 . . . . . . . . . 10 (dom 𝑇 = βˆ… ↔ ran 𝑇 = βˆ…)
156155necon3bii 2993 . . . . . . . . 9 (dom 𝑇 β‰  βˆ… ↔ ran 𝑇 β‰  βˆ…)
157154, 156sylib 217 . . . . . . . 8 (πœ‘ β†’ ran 𝑇 β‰  βˆ…)
158 supxrgtmnf 13257 . . . . . . . 8 ((ran 𝑇 βŠ† ℝ ∧ ran 𝑇 β‰  βˆ…) β†’ -∞ < sup(ran 𝑇, ℝ*, < ))
159117, 157, 158syl2anc 585 . . . . . . 7 (πœ‘ β†’ -∞ < sup(ran 𝑇, ℝ*, < ))
160 ovolun.g3 . . . . . . 7 (πœ‘ β†’ sup(ran 𝑇, ℝ*, < ) ≀ ((vol*β€˜π΅) + (𝐢 / 2)))
161 xrre 13097 . . . . . . 7 (((sup(ran 𝑇, ℝ*, < ) ∈ ℝ* ∧ ((vol*β€˜π΅) + (𝐢 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑇, ℝ*, < ) ∧ sup(ran 𝑇, ℝ*, < ) ≀ ((vol*β€˜π΅) + (𝐢 / 2)))) β†’ sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
162151, 126, 159, 160, 161syl22anc 838 . . . . . 6 (πœ‘ β†’ sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
163162adantr 482 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
164 supxrub 13252 . . . . . 6 ((ran 𝑇 βŠ† ℝ* ∧ (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) ∈ ran 𝑇) β†’ (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) ≀ sup(ran 𝑇, ℝ*, < ))
165149, 121, 164syl2an2r 684 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) ≀ sup(ran 𝑇, ℝ*, < ))
166160adantr 482 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ sup(ran 𝑇, ℝ*, < ) ≀ ((vol*β€˜π΅) + (𝐢 / 2)))
167122, 163, 127, 165, 166letrd 11320 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) ≀ ((vol*β€˜π΅) + (𝐢 / 2)))
168111, 122, 125, 127, 148, 167le2addd 11782 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) + (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2)))) ≀ (((vol*β€˜π΄) + (𝐢 / 2)) + ((vol*β€˜π΅) + (𝐢 / 2))))
169 oveq2 7369 . . . . . . . . 9 (𝑧 = 1 β†’ (2 Β· 𝑧) = (2 Β· 1))
170169fveq2d 6850 . . . . . . . 8 (𝑧 = 1 β†’ (π‘ˆβ€˜(2 Β· 𝑧)) = (π‘ˆβ€˜(2 Β· 1)))
171 fveq2 6846 . . . . . . . . 9 (𝑧 = 1 β†’ (π‘†β€˜π‘§) = (π‘†β€˜1))
172 fveq2 6846 . . . . . . . . 9 (𝑧 = 1 β†’ (π‘‡β€˜π‘§) = (π‘‡β€˜1))
173171, 172oveq12d 7379 . . . . . . . 8 (𝑧 = 1 β†’ ((π‘†β€˜π‘§) + (π‘‡β€˜π‘§)) = ((π‘†β€˜1) + (π‘‡β€˜1)))
174170, 173eqeq12d 2749 . . . . . . 7 (𝑧 = 1 β†’ ((π‘ˆβ€˜(2 Β· 𝑧)) = ((π‘†β€˜π‘§) + (π‘‡β€˜π‘§)) ↔ (π‘ˆβ€˜(2 Β· 1)) = ((π‘†β€˜1) + (π‘‡β€˜1))))
175174imbi2d 341 . . . . . 6 (𝑧 = 1 β†’ ((πœ‘ β†’ (π‘ˆβ€˜(2 Β· 𝑧)) = ((π‘†β€˜π‘§) + (π‘‡β€˜π‘§))) ↔ (πœ‘ β†’ (π‘ˆβ€˜(2 Β· 1)) = ((π‘†β€˜1) + (π‘‡β€˜1)))))
176 oveq2 7369 . . . . . . . . 9 (𝑧 = π‘˜ β†’ (2 Β· 𝑧) = (2 Β· π‘˜))
177176fveq2d 6850 . . . . . . . 8 (𝑧 = π‘˜ β†’ (π‘ˆβ€˜(2 Β· 𝑧)) = (π‘ˆβ€˜(2 Β· π‘˜)))
178 fveq2 6846 . . . . . . . . 9 (𝑧 = π‘˜ β†’ (π‘†β€˜π‘§) = (π‘†β€˜π‘˜))
179 fveq2 6846 . . . . . . . . 9 (𝑧 = π‘˜ β†’ (π‘‡β€˜π‘§) = (π‘‡β€˜π‘˜))
180178, 179oveq12d 7379 . . . . . . . 8 (𝑧 = π‘˜ β†’ ((π‘†β€˜π‘§) + (π‘‡β€˜π‘§)) = ((π‘†β€˜π‘˜) + (π‘‡β€˜π‘˜)))
181177, 180eqeq12d 2749 . . . . . . 7 (𝑧 = π‘˜ β†’ ((π‘ˆβ€˜(2 Β· 𝑧)) = ((π‘†β€˜π‘§) + (π‘‡β€˜π‘§)) ↔ (π‘ˆβ€˜(2 Β· π‘˜)) = ((π‘†β€˜π‘˜) + (π‘‡β€˜π‘˜))))
182181imbi2d 341 . . . . . 6 (𝑧 = π‘˜ β†’ ((πœ‘ β†’ (π‘ˆβ€˜(2 Β· 𝑧)) = ((π‘†β€˜π‘§) + (π‘‡β€˜π‘§))) ↔ (πœ‘ β†’ (π‘ˆβ€˜(2 Β· π‘˜)) = ((π‘†β€˜π‘˜) + (π‘‡β€˜π‘˜)))))
183 oveq2 7369 . . . . . . . . 9 (𝑧 = (π‘˜ + 1) β†’ (2 Β· 𝑧) = (2 Β· (π‘˜ + 1)))
184183fveq2d 6850 . . . . . . . 8 (𝑧 = (π‘˜ + 1) β†’ (π‘ˆβ€˜(2 Β· 𝑧)) = (π‘ˆβ€˜(2 Β· (π‘˜ + 1))))
185 fveq2 6846 . . . . . . . . 9 (𝑧 = (π‘˜ + 1) β†’ (π‘†β€˜π‘§) = (π‘†β€˜(π‘˜ + 1)))
186 fveq2 6846 . . . . . . . . 9 (𝑧 = (π‘˜ + 1) β†’ (π‘‡β€˜π‘§) = (π‘‡β€˜(π‘˜ + 1)))
187185, 186oveq12d 7379 . . . . . . . 8 (𝑧 = (π‘˜ + 1) β†’ ((π‘†β€˜π‘§) + (π‘‡β€˜π‘§)) = ((π‘†β€˜(π‘˜ + 1)) + (π‘‡β€˜(π‘˜ + 1))))
188184, 187eqeq12d 2749 . . . . . . 7 (𝑧 = (π‘˜ + 1) β†’ ((π‘ˆβ€˜(2 Β· 𝑧)) = ((π‘†β€˜π‘§) + (π‘‡β€˜π‘§)) ↔ (π‘ˆβ€˜(2 Β· (π‘˜ + 1))) = ((π‘†β€˜(π‘˜ + 1)) + (π‘‡β€˜(π‘˜ + 1)))))
189188imbi2d 341 . . . . . 6 (𝑧 = (π‘˜ + 1) β†’ ((πœ‘ β†’ (π‘ˆβ€˜(2 Β· 𝑧)) = ((π‘†β€˜π‘§) + (π‘‡β€˜π‘§))) ↔ (πœ‘ β†’ (π‘ˆβ€˜(2 Β· (π‘˜ + 1))) = ((π‘†β€˜(π‘˜ + 1)) + (π‘‡β€˜(π‘˜ + 1))))))
190 oveq2 7369 . . . . . . . . 9 (𝑧 = (βŒŠβ€˜((π‘˜ + 1) / 2)) β†’ (2 Β· 𝑧) = (2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2))))
191190fveq2d 6850 . . . . . . . 8 (𝑧 = (βŒŠβ€˜((π‘˜ + 1) / 2)) β†’ (π‘ˆβ€˜(2 Β· 𝑧)) = (π‘ˆβ€˜(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))))
192 fveq2 6846 . . . . . . . . 9 (𝑧 = (βŒŠβ€˜((π‘˜ + 1) / 2)) β†’ (π‘†β€˜π‘§) = (π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))))
193 fveq2 6846 . . . . . . . . 9 (𝑧 = (βŒŠβ€˜((π‘˜ + 1) / 2)) β†’ (π‘‡β€˜π‘§) = (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))))
194192, 193oveq12d 7379 . . . . . . . 8 (𝑧 = (βŒŠβ€˜((π‘˜ + 1) / 2)) β†’ ((π‘†β€˜π‘§) + (π‘‡β€˜π‘§)) = ((π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) + (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2)))))
195191, 194eqeq12d 2749 . . . . . . 7 (𝑧 = (βŒŠβ€˜((π‘˜ + 1) / 2)) β†’ ((π‘ˆβ€˜(2 Β· 𝑧)) = ((π‘†β€˜π‘§) + (π‘‡β€˜π‘§)) ↔ (π‘ˆβ€˜(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))) = ((π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) + (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))))))
196195imbi2d 341 . . . . . 6 (𝑧 = (βŒŠβ€˜((π‘˜ + 1) / 2)) β†’ ((πœ‘ β†’ (π‘ˆβ€˜(2 Β· 𝑧)) = ((π‘†β€˜π‘§) + (π‘‡β€˜π‘§))) ↔ (πœ‘ β†’ (π‘ˆβ€˜(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))) = ((π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) + (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2)))))))
19720fveq1i 6847 . . . . . . . 8 (π‘ˆβ€˜(2 Β· 1)) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜(2 Β· 1))
198132a1i 11 . . . . . . . . 9 (πœ‘ β†’ 1 ∈ β„•)
19919ovolfsval 24857 . . . . . . . . . . . 12 ((𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ 1 ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜1) = ((2nd β€˜(π»β€˜1)) βˆ’ (1st β€˜(π»β€˜1))))
20018, 132, 199sylancl 587 . . . . . . . . . . 11 (πœ‘ β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜1) = ((2nd β€˜(π»β€˜1)) βˆ’ (1st β€˜(π»β€˜1))))
201 halfnz 12589 . . . . . . . . . . . . . . . . . 18 Β¬ (1 / 2) ∈ β„€
202 nnz 12528 . . . . . . . . . . . . . . . . . . 19 ((𝑛 / 2) ∈ β„• β†’ (𝑛 / 2) ∈ β„€)
203 oveq1 7368 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 β†’ (𝑛 / 2) = (1 / 2))
204203eleq1d 2819 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 β†’ ((𝑛 / 2) ∈ β„€ ↔ (1 / 2) ∈ β„€))
205202, 204imbitrid 243 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 β†’ ((𝑛 / 2) ∈ β„• β†’ (1 / 2) ∈ β„€))
206201, 205mtoi 198 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 β†’ Β¬ (𝑛 / 2) ∈ β„•)
207206iffalsed 4501 . . . . . . . . . . . . . . . 16 (𝑛 = 1 β†’ if((𝑛 / 2) ∈ β„•, (πΊβ€˜(𝑛 / 2)), (πΉβ€˜((𝑛 + 1) / 2))) = (πΉβ€˜((𝑛 + 1) / 2)))
208 oveq1 7368 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 β†’ (𝑛 + 1) = (1 + 1))
209 df-2 12224 . . . . . . . . . . . . . . . . . . . 20 2 = (1 + 1)
210208, 209eqtr4di 2791 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 β†’ (𝑛 + 1) = 2)
211210oveq1d 7376 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 β†’ ((𝑛 + 1) / 2) = (2 / 2))
212 2div2e1 12302 . . . . . . . . . . . . . . . . . 18 (2 / 2) = 1
213211, 212eqtrdi 2789 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 β†’ ((𝑛 + 1) / 2) = 1)
214213fveq2d 6850 . . . . . . . . . . . . . . . 16 (𝑛 = 1 β†’ (πΉβ€˜((𝑛 + 1) / 2)) = (πΉβ€˜1))
215207, 214eqtrd 2773 . . . . . . . . . . . . . . 15 (𝑛 = 1 β†’ if((𝑛 / 2) ∈ β„•, (πΊβ€˜(𝑛 / 2)), (πΉβ€˜((𝑛 + 1) / 2))) = (πΉβ€˜1))
216 fvex 6859 . . . . . . . . . . . . . . 15 (πΉβ€˜1) ∈ V
217215, 17, 216fvmpt 6952 . . . . . . . . . . . . . 14 (1 ∈ β„• β†’ (π»β€˜1) = (πΉβ€˜1))
218132, 217ax-mp 5 . . . . . . . . . . . . 13 (π»β€˜1) = (πΉβ€˜1)
219218fveq2i 6849 . . . . . . . . . . . 12 (2nd β€˜(π»β€˜1)) = (2nd β€˜(πΉβ€˜1))
220218fveq2i 6849 . . . . . . . . . . . 12 (1st β€˜(π»β€˜1)) = (1st β€˜(πΉβ€˜1))
221219, 220oveq12i 7373 . . . . . . . . . . 11 ((2nd β€˜(π»β€˜1)) βˆ’ (1st β€˜(π»β€˜1))) = ((2nd β€˜(πΉβ€˜1)) βˆ’ (1st β€˜(πΉβ€˜1)))
222200, 221eqtrdi 2789 . . . . . . . . . 10 (πœ‘ β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜1) = ((2nd β€˜(πΉβ€˜1)) βˆ’ (1st β€˜(πΉβ€˜1))))
22352, 222seq1i 13929 . . . . . . . . 9 (πœ‘ β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜1) = ((2nd β€˜(πΉβ€˜1)) βˆ’ (1st β€˜(πΉβ€˜1))))
224 2t1e2 12324 . . . . . . . . . . 11 (2 Β· 1) = 2
225224fveq2i 6849 . . . . . . . . . 10 (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜(2 Β· 1)) = (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜2)
22619ovolfsval 24857 . . . . . . . . . . . 12 ((𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ 2 ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜2) = ((2nd β€˜(π»β€˜2)) βˆ’ (1st β€˜(π»β€˜2))))
22718, 27, 226sylancl 587 . . . . . . . . . . 11 (πœ‘ β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜2) = ((2nd β€˜(π»β€˜2)) βˆ’ (1st β€˜(π»β€˜2))))
228 oveq1 7368 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 2 β†’ (𝑛 / 2) = (2 / 2))
229228, 212eqtrdi 2789 . . . . . . . . . . . . . . . . . 18 (𝑛 = 2 β†’ (𝑛 / 2) = 1)
230229, 132eqeltrdi 2842 . . . . . . . . . . . . . . . . 17 (𝑛 = 2 β†’ (𝑛 / 2) ∈ β„•)
231230iftrued 4498 . . . . . . . . . . . . . . . 16 (𝑛 = 2 β†’ if((𝑛 / 2) ∈ β„•, (πΊβ€˜(𝑛 / 2)), (πΉβ€˜((𝑛 + 1) / 2))) = (πΊβ€˜(𝑛 / 2)))
232229fveq2d 6850 . . . . . . . . . . . . . . . 16 (𝑛 = 2 β†’ (πΊβ€˜(𝑛 / 2)) = (πΊβ€˜1))
233231, 232eqtrd 2773 . . . . . . . . . . . . . . 15 (𝑛 = 2 β†’ if((𝑛 / 2) ∈ β„•, (πΊβ€˜(𝑛 / 2)), (πΉβ€˜((𝑛 + 1) / 2))) = (πΊβ€˜1))
234 fvex 6859 . . . . . . . . . . . . . . 15 (πΊβ€˜1) ∈ V
235233, 17, 234fvmpt 6952 . . . . . . . . . . . . . 14 (2 ∈ β„• β†’ (π»β€˜2) = (πΊβ€˜1))
23627, 235ax-mp 5 . . . . . . . . . . . . 13 (π»β€˜2) = (πΊβ€˜1)
237236fveq2i 6849 . . . . . . . . . . . 12 (2nd β€˜(π»β€˜2)) = (2nd β€˜(πΊβ€˜1))
238236fveq2i 6849 . . . . . . . . . . . 12 (1st β€˜(π»β€˜2)) = (1st β€˜(πΊβ€˜1))
239237, 238oveq12i 7373 . . . . . . . . . . 11 ((2nd β€˜(π»β€˜2)) βˆ’ (1st β€˜(π»β€˜2))) = ((2nd β€˜(πΊβ€˜1)) βˆ’ (1st β€˜(πΊβ€˜1)))
240227, 239eqtrdi 2789 . . . . . . . . . 10 (πœ‘ β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜2) = ((2nd β€˜(πΊβ€˜1)) βˆ’ (1st β€˜(πΊβ€˜1))))
241225, 240eqtrid 2785 . . . . . . . . 9 (πœ‘ β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜(2 Β· 1)) = ((2nd β€˜(πΊβ€˜1)) βˆ’ (1st β€˜(πΊβ€˜1))))
24272, 198, 34, 223, 241seqp1d 13932 . . . . . . . 8 (πœ‘ β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜(2 Β· 1)) = (((2nd β€˜(πΉβ€˜1)) βˆ’ (1st β€˜(πΉβ€˜1))) + ((2nd β€˜(πΊβ€˜1)) βˆ’ (1st β€˜(πΊβ€˜1)))))
243197, 242eqtrid 2785 . . . . . . 7 (πœ‘ β†’ (π‘ˆβ€˜(2 Β· 1)) = (((2nd β€˜(πΉβ€˜1)) βˆ’ (1st β€˜(πΉβ€˜1))) + ((2nd β€˜(πΊβ€˜1)) βˆ’ (1st β€˜(πΊβ€˜1)))))
244102fveq1i 6847 . . . . . . . . 9 (π‘†β€˜1) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐹))β€˜1)
245101ovolfsval 24857 . . . . . . . . . . 11 ((𝐹:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ 1 ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜1) = ((2nd β€˜(πΉβ€˜1)) βˆ’ (1st β€˜(πΉβ€˜1))))
24612, 132, 245sylancl 587 . . . . . . . . . 10 (πœ‘ β†’ (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜1) = ((2nd β€˜(πΉβ€˜1)) βˆ’ (1st β€˜(πΉβ€˜1))))
24752, 246seq1i 13929 . . . . . . . . 9 (πœ‘ β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐹))β€˜1) = ((2nd β€˜(πΉβ€˜1)) βˆ’ (1st β€˜(πΉβ€˜1))))
248244, 247eqtrid 2785 . . . . . . . 8 (πœ‘ β†’ (π‘†β€˜1) = ((2nd β€˜(πΉβ€˜1)) βˆ’ (1st β€˜(πΉβ€˜1))))
249113fveq1i 6847 . . . . . . . . 9 (π‘‡β€˜1) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐺))β€˜1)
250112ovolfsval 24857 . . . . . . . . . . 11 ((𝐺:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ 1 ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜1) = ((2nd β€˜(πΊβ€˜1)) βˆ’ (1st β€˜(πΊβ€˜1))))
2513, 132, 250sylancl 587 . . . . . . . . . 10 (πœ‘ β†’ (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜1) = ((2nd β€˜(πΊβ€˜1)) βˆ’ (1st β€˜(πΊβ€˜1))))
25252, 251seq1i 13929 . . . . . . . . 9 (πœ‘ β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐺))β€˜1) = ((2nd β€˜(πΊβ€˜1)) βˆ’ (1st β€˜(πΊβ€˜1))))
253249, 252eqtrid 2785 . . . . . . . 8 (πœ‘ β†’ (π‘‡β€˜1) = ((2nd β€˜(πΊβ€˜1)) βˆ’ (1st β€˜(πΊβ€˜1))))
254248, 253oveq12d 7379 . . . . . . 7 (πœ‘ β†’ ((π‘†β€˜1) + (π‘‡β€˜1)) = (((2nd β€˜(πΉβ€˜1)) βˆ’ (1st β€˜(πΉβ€˜1))) + ((2nd β€˜(πΊβ€˜1)) βˆ’ (1st β€˜(πΊβ€˜1)))))
255243, 254eqtr4d 2776 . . . . . 6 (πœ‘ β†’ (π‘ˆβ€˜(2 Β· 1)) = ((π‘†β€˜1) + (π‘‡β€˜1)))
256 oveq1 7368 . . . . . . . . 9 ((π‘ˆβ€˜(2 Β· π‘˜)) = ((π‘†β€˜π‘˜) + (π‘‡β€˜π‘˜)) β†’ ((π‘ˆβ€˜(2 Β· π‘˜)) + ((((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)))) = (((π‘†β€˜π‘˜) + (π‘‡β€˜π‘˜)) + ((((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)))))
25734oveq2i 7372 . . . . . . . . . . . . 13 ((2 Β· π‘˜) + (2 Β· 1)) = ((2 Β· π‘˜) + (1 + 1))
258 2cnd 12239 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 2 ∈ β„‚)
25938recnd 11191 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„‚)
260 1cnd 11158 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 1 ∈ β„‚)
261258, 259, 260adddid 11187 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2 Β· (π‘˜ + 1)) = ((2 Β· π‘˜) + (2 Β· 1)))
262 nnmulcl 12185 . . . . . . . . . . . . . . . . 17 ((2 ∈ β„• ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) ∈ β„•)
26327, 262mpan 689 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„• β†’ (2 Β· π‘˜) ∈ β„•)
264263adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) ∈ β„•)
265264nncnd 12177 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) ∈ β„‚)
266265, 260, 260addassd 11185 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((2 Β· π‘˜) + 1) + 1) = ((2 Β· π‘˜) + (1 + 1)))
267257, 261, 2663eqtr4a 2799 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2 Β· (π‘˜ + 1)) = (((2 Β· π‘˜) + 1) + 1))
268267fveq2d 6850 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘ˆβ€˜(2 Β· (π‘˜ + 1))) = (π‘ˆβ€˜(((2 Β· π‘˜) + 1) + 1)))
26920fveq1i 6847 . . . . . . . . . . . 12 (π‘ˆβ€˜(((2 Β· π‘˜) + 1) + 1)) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜(((2 Β· π‘˜) + 1) + 1))
270264peano2nnd 12178 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) + 1) ∈ β„•)
271270, 72eleqtrdi 2844 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) + 1) ∈ (β„€β‰₯β€˜1))
272 seqp1 13930 . . . . . . . . . . . . . 14 (((2 Β· π‘˜) + 1) ∈ (β„€β‰₯β€˜1) β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜(((2 Β· π‘˜) + 1) + 1)) = ((seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜((2 Β· π‘˜) + 1)) + (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜(((2 Β· π‘˜) + 1) + 1))))
273271, 272syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜(((2 Β· π‘˜) + 1) + 1)) = ((seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜((2 Β· π‘˜) + 1)) + (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜(((2 Β· π‘˜) + 1) + 1))))
274264, 72eleqtrdi 2844 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) ∈ (β„€β‰₯β€˜1))
275 seqp1 13930 . . . . . . . . . . . . . . . 16 ((2 Β· π‘˜) ∈ (β„€β‰₯β€˜1) β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜((2 Β· π‘˜) + 1)) = ((seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜(2 Β· π‘˜)) + (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜((2 Β· π‘˜) + 1))))
276274, 275syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜((2 Β· π‘˜) + 1)) = ((seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜(2 Β· π‘˜)) + (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜((2 Β· π‘˜) + 1))))
27720fveq1i 6847 . . . . . . . . . . . . . . . . 17 (π‘ˆβ€˜(2 Β· π‘˜)) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜(2 Β· π‘˜))
278277a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘ˆβ€˜(2 Β· π‘˜)) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜(2 Β· π‘˜)))
279 oveq1 7368 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = ((2 Β· π‘˜) + 1) β†’ (𝑛 / 2) = (((2 Β· π‘˜) + 1) / 2))
280279eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 Β· π‘˜) + 1) β†’ ((𝑛 / 2) ∈ β„• ↔ (((2 Β· π‘˜) + 1) / 2) ∈ β„•))
281279fveq2d 6850 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 Β· π‘˜) + 1) β†’ (πΊβ€˜(𝑛 / 2)) = (πΊβ€˜(((2 Β· π‘˜) + 1) / 2)))
282 oveq1 7368 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = ((2 Β· π‘˜) + 1) β†’ (𝑛 + 1) = (((2 Β· π‘˜) + 1) + 1))
283282fvoveq1d 7383 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 Β· π‘˜) + 1) β†’ (πΉβ€˜((𝑛 + 1) / 2)) = (πΉβ€˜((((2 Β· π‘˜) + 1) + 1) / 2)))
284280, 281, 283ifbieq12d 4518 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = ((2 Β· π‘˜) + 1) β†’ if((𝑛 / 2) ∈ β„•, (πΊβ€˜(𝑛 / 2)), (πΉβ€˜((𝑛 + 1) / 2))) = if((((2 Β· π‘˜) + 1) / 2) ∈ β„•, (πΊβ€˜(((2 Β· π‘˜) + 1) / 2)), (πΉβ€˜((((2 Β· π‘˜) + 1) + 1) / 2))))
285 fvex 6859 . . . . . . . . . . . . . . . . . . . . . . 23 (πΊβ€˜(((2 Β· π‘˜) + 1) / 2)) ∈ V
286 fvex 6859 . . . . . . . . . . . . . . . . . . . . . . 23 (πΉβ€˜((((2 Β· π‘˜) + 1) + 1) / 2)) ∈ V
287285, 286ifex 4540 . . . . . . . . . . . . . . . . . . . . . 22 if((((2 Β· π‘˜) + 1) / 2) ∈ β„•, (πΊβ€˜(((2 Β· π‘˜) + 1) / 2)), (πΉβ€˜((((2 Β· π‘˜) + 1) + 1) / 2))) ∈ V
288284, 17, 287fvmpt 6952 . . . . . . . . . . . . . . . . . . . . 21 (((2 Β· π‘˜) + 1) ∈ β„• β†’ (π»β€˜((2 Β· π‘˜) + 1)) = if((((2 Β· π‘˜) + 1) / 2) ∈ β„•, (πΊβ€˜(((2 Β· π‘˜) + 1) / 2)), (πΉβ€˜((((2 Β· π‘˜) + 1) + 1) / 2))))
289270, 288syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π»β€˜((2 Β· π‘˜) + 1)) = if((((2 Β· π‘˜) + 1) / 2) ∈ β„•, (πΊβ€˜(((2 Β· π‘˜) + 1) / 2)), (πΉβ€˜((((2 Β· π‘˜) + 1) + 1) / 2))))
290 2ne0 12265 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 β‰  0
291290a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 2 β‰  0)
292259, 258, 291divcan3d 11944 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) / 2) = π‘˜)
293292, 71eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) / 2) ∈ β„•)
294 nneo 12595 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 Β· π‘˜) ∈ β„• β†’ (((2 Β· π‘˜) / 2) ∈ β„• ↔ Β¬ (((2 Β· π‘˜) + 1) / 2) ∈ β„•))
295264, 294syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((2 Β· π‘˜) / 2) ∈ β„• ↔ Β¬ (((2 Β· π‘˜) + 1) / 2) ∈ β„•))
296293, 295mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ Β¬ (((2 Β· π‘˜) + 1) / 2) ∈ β„•)
297296iffalsed 4501 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ if((((2 Β· π‘˜) + 1) / 2) ∈ β„•, (πΊβ€˜(((2 Β· π‘˜) + 1) / 2)), (πΉβ€˜((((2 Β· π‘˜) + 1) + 1) / 2))) = (πΉβ€˜((((2 Β· π‘˜) + 1) + 1) / 2)))
298267oveq1d 7376 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· (π‘˜ + 1)) / 2) = ((((2 Β· π‘˜) + 1) + 1) / 2))
29929nncnd 12177 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„‚)
300 2cn 12236 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ β„‚
301 divcan3 11847 . . . . . . . . . . . . . . . . . . . . . . . 24 (((π‘˜ + 1) ∈ β„‚ ∧ 2 ∈ β„‚ ∧ 2 β‰  0) β†’ ((2 Β· (π‘˜ + 1)) / 2) = (π‘˜ + 1))
302300, 290, 301mp3an23 1454 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘˜ + 1) ∈ β„‚ β†’ ((2 Β· (π‘˜ + 1)) / 2) = (π‘˜ + 1))
303299, 302syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· (π‘˜ + 1)) / 2) = (π‘˜ + 1))
304298, 303eqtr3d 2775 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((((2 Β· π‘˜) + 1) + 1) / 2) = (π‘˜ + 1))
305304fveq2d 6850 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜((((2 Β· π‘˜) + 1) + 1) / 2)) = (πΉβ€˜(π‘˜ + 1)))
306289, 297, 3053eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π»β€˜((2 Β· π‘˜) + 1)) = (πΉβ€˜(π‘˜ + 1)))
307306fveq2d 6850 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2nd β€˜(π»β€˜((2 Β· π‘˜) + 1))) = (2nd β€˜(πΉβ€˜(π‘˜ + 1))))
308306fveq2d 6850 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1st β€˜(π»β€˜((2 Β· π‘˜) + 1))) = (1st β€˜(πΉβ€˜(π‘˜ + 1))))
309307, 308oveq12d 7379 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((2nd β€˜(π»β€˜((2 Β· π‘˜) + 1))) βˆ’ (1st β€˜(π»β€˜((2 Β· π‘˜) + 1)))) = ((2nd β€˜(πΉβ€˜(π‘˜ + 1))) βˆ’ (1st β€˜(πΉβ€˜(π‘˜ + 1)))))
31019ovolfsval 24857 . . . . . . . . . . . . . . . . . 18 ((𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ ((2 Β· π‘˜) + 1) ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜((2 Β· π‘˜) + 1)) = ((2nd β€˜(π»β€˜((2 Β· π‘˜) + 1))) βˆ’ (1st β€˜(π»β€˜((2 Β· π‘˜) + 1)))))
31118, 270, 310syl2an2r 684 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜((2 Β· π‘˜) + 1)) = ((2nd β€˜(π»β€˜((2 Β· π‘˜) + 1))) βˆ’ (1st β€˜(π»β€˜((2 Β· π‘˜) + 1)))))
312101ovolfsval 24857 . . . . . . . . . . . . . . . . . 18 ((𝐹:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ (π‘˜ + 1) ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) = ((2nd β€˜(πΉβ€˜(π‘˜ + 1))) βˆ’ (1st β€˜(πΉβ€˜(π‘˜ + 1)))))
31312, 28, 312syl2an 597 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) = ((2nd β€˜(πΉβ€˜(π‘˜ + 1))) βˆ’ (1st β€˜(πΉβ€˜(π‘˜ + 1)))))
314309, 311, 3133eqtr4rd 2784 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) = (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜((2 Β· π‘˜) + 1)))
315278, 314oveq12d 7379 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘ˆβ€˜(2 Β· π‘˜)) + (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1))) = ((seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜(2 Β· π‘˜)) + (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜((2 Β· π‘˜) + 1))))
316276, 315eqtr4d 2776 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜((2 Β· π‘˜) + 1)) = ((π‘ˆβ€˜(2 Β· π‘˜)) + (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1))))
317267fveq2d 6850 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π»β€˜(2 Β· (π‘˜ + 1))) = (π»β€˜(((2 Β· π‘˜) + 1) + 1)))
318270peano2nnd 12178 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((2 Β· π‘˜) + 1) + 1) ∈ β„•)
319267, 318eqeltrd 2834 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2 Β· (π‘˜ + 1)) ∈ β„•)
320 oveq1 7368 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = (2 Β· (π‘˜ + 1)) β†’ (𝑛 / 2) = ((2 Β· (π‘˜ + 1)) / 2))
321320eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 Β· (π‘˜ + 1)) β†’ ((𝑛 / 2) ∈ β„• ↔ ((2 Β· (π‘˜ + 1)) / 2) ∈ β„•))
322320fveq2d 6850 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 Β· (π‘˜ + 1)) β†’ (πΊβ€˜(𝑛 / 2)) = (πΊβ€˜((2 Β· (π‘˜ + 1)) / 2)))
323 oveq1 7368 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = (2 Β· (π‘˜ + 1)) β†’ (𝑛 + 1) = ((2 Β· (π‘˜ + 1)) + 1))
324323fvoveq1d 7383 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 Β· (π‘˜ + 1)) β†’ (πΉβ€˜((𝑛 + 1) / 2)) = (πΉβ€˜(((2 Β· (π‘˜ + 1)) + 1) / 2)))
325321, 322, 324ifbieq12d 4518 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = (2 Β· (π‘˜ + 1)) β†’ if((𝑛 / 2) ∈ β„•, (πΊβ€˜(𝑛 / 2)), (πΉβ€˜((𝑛 + 1) / 2))) = if(((2 Β· (π‘˜ + 1)) / 2) ∈ β„•, (πΊβ€˜((2 Β· (π‘˜ + 1)) / 2)), (πΉβ€˜(((2 Β· (π‘˜ + 1)) + 1) / 2))))
326 fvex 6859 . . . . . . . . . . . . . . . . . . . . . 22 (πΊβ€˜((2 Β· (π‘˜ + 1)) / 2)) ∈ V
327 fvex 6859 . . . . . . . . . . . . . . . . . . . . . 22 (πΉβ€˜(((2 Β· (π‘˜ + 1)) + 1) / 2)) ∈ V
328326, 327ifex 4540 . . . . . . . . . . . . . . . . . . . . 21 if(((2 Β· (π‘˜ + 1)) / 2) ∈ β„•, (πΊβ€˜((2 Β· (π‘˜ + 1)) / 2)), (πΉβ€˜(((2 Β· (π‘˜ + 1)) + 1) / 2))) ∈ V
329325, 17, 328fvmpt 6952 . . . . . . . . . . . . . . . . . . . 20 ((2 Β· (π‘˜ + 1)) ∈ β„• β†’ (π»β€˜(2 Β· (π‘˜ + 1))) = if(((2 Β· (π‘˜ + 1)) / 2) ∈ β„•, (πΊβ€˜((2 Β· (π‘˜ + 1)) / 2)), (πΉβ€˜(((2 Β· (π‘˜ + 1)) + 1) / 2))))
330319, 329syl 17 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π»β€˜(2 Β· (π‘˜ + 1))) = if(((2 Β· (π‘˜ + 1)) / 2) ∈ β„•, (πΊβ€˜((2 Β· (π‘˜ + 1)) / 2)), (πΉβ€˜(((2 Β· (π‘˜ + 1)) + 1) / 2))))
331303, 29eqeltrd 2834 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· (π‘˜ + 1)) / 2) ∈ β„•)
332331iftrued 4498 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ if(((2 Β· (π‘˜ + 1)) / 2) ∈ β„•, (πΊβ€˜((2 Β· (π‘˜ + 1)) / 2)), (πΉβ€˜(((2 Β· (π‘˜ + 1)) + 1) / 2))) = (πΊβ€˜((2 Β· (π‘˜ + 1)) / 2)))
333303fveq2d 6850 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΊβ€˜((2 Β· (π‘˜ + 1)) / 2)) = (πΊβ€˜(π‘˜ + 1)))
334330, 332, 3333eqtrd 2777 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π»β€˜(2 Β· (π‘˜ + 1))) = (πΊβ€˜(π‘˜ + 1)))
335317, 334eqtr3d 2775 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π»β€˜(((2 Β· π‘˜) + 1) + 1)) = (πΊβ€˜(π‘˜ + 1)))
336335fveq2d 6850 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2nd β€˜(π»β€˜(((2 Β· π‘˜) + 1) + 1))) = (2nd β€˜(πΊβ€˜(π‘˜ + 1))))
337335fveq2d 6850 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1st β€˜(π»β€˜(((2 Β· π‘˜) + 1) + 1))) = (1st β€˜(πΊβ€˜(π‘˜ + 1))))
338336, 337oveq12d 7379 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((2nd β€˜(π»β€˜(((2 Β· π‘˜) + 1) + 1))) βˆ’ (1st β€˜(π»β€˜(((2 Β· π‘˜) + 1) + 1)))) = ((2nd β€˜(πΊβ€˜(π‘˜ + 1))) βˆ’ (1st β€˜(πΊβ€˜(π‘˜ + 1)))))
33919ovolfsval 24857 . . . . . . . . . . . . . . . 16 ((𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ (((2 Β· π‘˜) + 1) + 1) ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜(((2 Β· π‘˜) + 1) + 1)) = ((2nd β€˜(π»β€˜(((2 Β· π‘˜) + 1) + 1))) βˆ’ (1st β€˜(π»β€˜(((2 Β· π‘˜) + 1) + 1)))))
34018, 318, 339syl2an2r 684 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜(((2 Β· π‘˜) + 1) + 1)) = ((2nd β€˜(π»β€˜(((2 Β· π‘˜) + 1) + 1))) βˆ’ (1st β€˜(π»β€˜(((2 Β· π‘˜) + 1) + 1)))))
341112ovolfsval 24857 . . . . . . . . . . . . . . . 16 ((𝐺:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ (π‘˜ + 1) ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)) = ((2nd β€˜(πΊβ€˜(π‘˜ + 1))) βˆ’ (1st β€˜(πΊβ€˜(π‘˜ + 1)))))
3423, 28, 341syl2an 597 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)) = ((2nd β€˜(πΊβ€˜(π‘˜ + 1))) βˆ’ (1st β€˜(πΊβ€˜(π‘˜ + 1)))))
343338, 340, 3423eqtr4d 2783 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜(((2 Β· π‘˜) + 1) + 1)) = (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)))
344316, 343oveq12d 7379 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜((2 Β· π‘˜) + 1)) + (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜(((2 Β· π‘˜) + 1) + 1))) = (((π‘ˆβ€˜(2 Β· π‘˜)) + (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1))) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1))))
345273, 344eqtrd 2773 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜(((2 Β· π‘˜) + 1) + 1)) = (((π‘ˆβ€˜(2 Β· π‘˜)) + (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1))) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1))))
346269, 345eqtrid 2785 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘ˆβ€˜(((2 Β· π‘˜) + 1) + 1)) = (((π‘ˆβ€˜(2 Β· π‘˜)) + (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1))) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1))))
347 ffvelcdm 7036 . . . . . . . . . . . . . . 15 ((π‘ˆ:β„•βŸΆ(0[,)+∞) ∧ (2 Β· π‘˜) ∈ β„•) β†’ (π‘ˆβ€˜(2 Β· π‘˜)) ∈ (0[,)+∞))
34822, 263, 347syl2an 597 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘ˆβ€˜(2 Β· π‘˜)) ∈ (0[,)+∞))
34923, 348sselid 3946 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘ˆβ€˜(2 Β· π‘˜)) ∈ ℝ)
350349recnd 11191 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘ˆβ€˜(2 Β· π‘˜)) ∈ β„‚)
351101ovolfsf 24858 . . . . . . . . . . . . . . . 16 (𝐹:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) β†’ ((abs ∘ βˆ’ ) ∘ 𝐹):β„•βŸΆ(0[,)+∞))
35212, 351syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((abs ∘ βˆ’ ) ∘ 𝐹):β„•βŸΆ(0[,)+∞))
353 ffvelcdm 7036 . . . . . . . . . . . . . . 15 ((((abs ∘ βˆ’ ) ∘ 𝐹):β„•βŸΆ(0[,)+∞) ∧ (π‘˜ + 1) ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) ∈ (0[,)+∞))
354352, 28, 353syl2an 597 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) ∈ (0[,)+∞))
35523, 354sselid 3946 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) ∈ ℝ)
356355recnd 11191 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) ∈ β„‚)
357112ovolfsf 24858 . . . . . . . . . . . . . . . 16 (𝐺:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) β†’ ((abs ∘ βˆ’ ) ∘ 𝐺):β„•βŸΆ(0[,)+∞))
3583, 357syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((abs ∘ βˆ’ ) ∘ 𝐺):β„•βŸΆ(0[,)+∞))
359 ffvelcdm 7036 . . . . . . . . . . . . . . 15 ((((abs ∘ βˆ’ ) ∘ 𝐺):β„•βŸΆ(0[,)+∞) ∧ (π‘˜ + 1) ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)) ∈ (0[,)+∞))
360358, 28, 359syl2an 597 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)) ∈ (0[,)+∞))
36123, 360sselid 3946 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)) ∈ ℝ)
362361recnd 11191 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)) ∈ β„‚)
363350, 356, 362addassd 11185 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((π‘ˆβ€˜(2 Β· π‘˜)) + (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1))) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1))) = ((π‘ˆβ€˜(2 Β· π‘˜)) + ((((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)))))
364268, 346, 3633eqtrd 2777 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘ˆβ€˜(2 Β· (π‘˜ + 1))) = ((π‘ˆβ€˜(2 Β· π‘˜)) + ((((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)))))
365 seqp1 13930 . . . . . . . . . . . . . 14 (π‘˜ ∈ (β„€β‰₯β€˜1) β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐹))β€˜(π‘˜ + 1)) = ((seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐹))β€˜π‘˜) + (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1))))
36673, 365syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐹))β€˜(π‘˜ + 1)) = ((seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐹))β€˜π‘˜) + (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1))))
367102fveq1i 6847 . . . . . . . . . . . . 13 (π‘†β€˜(π‘˜ + 1)) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐹))β€˜(π‘˜ + 1))
368102fveq1i 6847 . . . . . . . . . . . . . 14 (π‘†β€˜π‘˜) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐹))β€˜π‘˜)
369368oveq1i 7371 . . . . . . . . . . . . 13 ((π‘†β€˜π‘˜) + (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1))) = ((seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐹))β€˜π‘˜) + (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)))
370366, 367, 3693eqtr4g 2798 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘†β€˜(π‘˜ + 1)) = ((π‘†β€˜π‘˜) + (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1))))
371 seqp1 13930 . . . . . . . . . . . . . 14 (π‘˜ ∈ (β„€β‰₯β€˜1) β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐺))β€˜(π‘˜ + 1)) = ((seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐺))β€˜π‘˜) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1))))
37273, 371syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐺))β€˜(π‘˜ + 1)) = ((seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐺))β€˜π‘˜) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1))))
373113fveq1i 6847 . . . . . . . . . . . . 13 (π‘‡β€˜(π‘˜ + 1)) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐺))β€˜(π‘˜ + 1))
374113fveq1i 6847 . . . . . . . . . . . . . 14 (π‘‡β€˜π‘˜) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐺))β€˜π‘˜)
375374oveq1i 7371 . . . . . . . . . . . . 13 ((π‘‡β€˜π‘˜) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1))) = ((seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐺))β€˜π‘˜) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)))
376372, 373, 3753eqtr4g 2798 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘‡β€˜(π‘˜ + 1)) = ((π‘‡β€˜π‘˜) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1))))
377370, 376oveq12d 7379 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘†β€˜(π‘˜ + 1)) + (π‘‡β€˜(π‘˜ + 1))) = (((π‘†β€˜π‘˜) + (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1))) + ((π‘‡β€˜π‘˜) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)))))
378104ffvelcdmda 7039 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘†β€˜π‘˜) ∈ (0[,)+∞))
37923, 378sselid 3946 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘†β€˜π‘˜) ∈ ℝ)
380379recnd 11191 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘†β€˜π‘˜) ∈ β„‚)
381115ffvelcdmda 7039 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘‡β€˜π‘˜) ∈ (0[,)+∞))
38223, 381sselid 3946 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘‡β€˜π‘˜) ∈ ℝ)
383382recnd 11191 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘‡β€˜π‘˜) ∈ β„‚)
384380, 356, 383, 362add4d 11391 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((π‘†β€˜π‘˜) + (((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1))) + ((π‘‡β€˜π‘˜) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)))) = (((π‘†β€˜π‘˜) + (π‘‡β€˜π‘˜)) + ((((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)))))
385377, 384eqtrd 2773 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘†β€˜(π‘˜ + 1)) + (π‘‡β€˜(π‘˜ + 1))) = (((π‘†β€˜π‘˜) + (π‘‡β€˜π‘˜)) + ((((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)))))
386364, 385eqeq12d 2749 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘ˆβ€˜(2 Β· (π‘˜ + 1))) = ((π‘†β€˜(π‘˜ + 1)) + (π‘‡β€˜(π‘˜ + 1))) ↔ ((π‘ˆβ€˜(2 Β· π‘˜)) + ((((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1)))) = (((π‘†β€˜π‘˜) + (π‘‡β€˜π‘˜)) + ((((abs ∘ βˆ’ ) ∘ 𝐹)β€˜(π‘˜ + 1)) + (((abs ∘ βˆ’ ) ∘ 𝐺)β€˜(π‘˜ + 1))))))
387256, 386syl5ibr 246 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘ˆβ€˜(2 Β· π‘˜)) = ((π‘†β€˜π‘˜) + (π‘‡β€˜π‘˜)) β†’ (π‘ˆβ€˜(2 Β· (π‘˜ + 1))) = ((π‘†β€˜(π‘˜ + 1)) + (π‘‡β€˜(π‘˜ + 1)))))
388387expcom 415 . . . . . . 7 (π‘˜ ∈ β„• β†’ (πœ‘ β†’ ((π‘ˆβ€˜(2 Β· π‘˜)) = ((π‘†β€˜π‘˜) + (π‘‡β€˜π‘˜)) β†’ (π‘ˆβ€˜(2 Β· (π‘˜ + 1))) = ((π‘†β€˜(π‘˜ + 1)) + (π‘‡β€˜(π‘˜ + 1))))))
389388a2d 29 . . . . . 6 (π‘˜ ∈ β„• β†’ ((πœ‘ β†’ (π‘ˆβ€˜(2 Β· π‘˜)) = ((π‘†β€˜π‘˜) + (π‘‡β€˜π‘˜))) β†’ (πœ‘ β†’ (π‘ˆβ€˜(2 Β· (π‘˜ + 1))) = ((π‘†β€˜(π‘˜ + 1)) + (π‘‡β€˜(π‘˜ + 1))))))
390175, 182, 189, 196, 255, 389nnind 12179 . . . . 5 ((βŒŠβ€˜((π‘˜ + 1) / 2)) ∈ β„• β†’ (πœ‘ β†’ (π‘ˆβ€˜(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))) = ((π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) + (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))))))
391390impcom 409 . . . 4 ((πœ‘ ∧ (βŒŠβ€˜((π‘˜ + 1) / 2)) ∈ β„•) β†’ (π‘ˆβ€˜(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))) = ((π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) + (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2)))))
39257, 391syldan 592 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘ˆβ€˜(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))) = ((π‘†β€˜(βŒŠβ€˜((π‘˜ + 1) / 2))) + (π‘‡β€˜(βŒŠβ€˜((π‘˜ + 1) / 2)))))
39363adantr 482 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (vol*β€˜π΄) ∈ ℝ)
394393recnd 11191 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (vol*β€˜π΄) ∈ β„‚)
39568adantr 482 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐢 ∈ ℝ)
396395rehalfcld 12408 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝐢 / 2) ∈ ℝ)
397396recnd 11191 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝐢 / 2) ∈ β„‚)
39865adantr 482 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (vol*β€˜π΅) ∈ ℝ)
399398recnd 11191 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (vol*β€˜π΅) ∈ β„‚)
400394, 397, 399, 397add4d 11391 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((vol*β€˜π΄) + (𝐢 / 2)) + ((vol*β€˜π΅) + (𝐢 / 2))) = (((vol*β€˜π΄) + (vol*β€˜π΅)) + ((𝐢 / 2) + (𝐢 / 2))))
401395recnd 11191 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐢 ∈ β„‚)
4024012halvesd 12407 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((𝐢 / 2) + (𝐢 / 2)) = 𝐢)
403402oveq2d 7377 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((vol*β€˜π΄) + (vol*β€˜π΅)) + ((𝐢 / 2) + (𝐢 / 2))) = (((vol*β€˜π΄) + (vol*β€˜π΅)) + 𝐢))
404400, 403eqtr2d 2774 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((vol*β€˜π΄) + (vol*β€˜π΅)) + 𝐢) = (((vol*β€˜π΄) + (𝐢 / 2)) + ((vol*β€˜π΅) + (𝐢 / 2))))
405168, 392, 4043brtr4d 5141 . 2 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘ˆβ€˜(2 Β· (βŒŠβ€˜((π‘˜ + 1) / 2)))) ≀ (((vol*β€˜π΄) + (vol*β€˜π΅)) + 𝐢))
40626, 61, 70, 100, 405letrd 11320 1 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘ˆβ€˜π‘˜) ≀ (((vol*β€˜π΄) + (vol*β€˜π΅)) + 𝐢))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2940   ∩ cin 3913   βŠ† wss 3914  βˆ…c0 4286  ifcif 4490  βˆͺ cuni 4869   class class class wbr 5109   ↦ cmpt 5192   Γ— cxp 5635  dom cdm 5637  ran crn 5638   ∘ ccom 5641   Fn wfn 6495  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361  1st c1st 7923  2nd c2nd 7924   ↑m cmap 8771  supcsup 9384  β„‚cc 11057  β„cr 11058  0cc0 11059  1c1 11060   + caddc 11062   Β· cmul 11064  +∞cpnf 11194  -∞cmnf 11195  β„*cxr 11196   < clt 11197   ≀ cle 11198   βˆ’ cmin 11393   / cdiv 11820  β„•cn 12161  2c2 12216  β„€cz 12507  β„€β‰₯cuz 12771  β„+crp 12923  (,)cioo 13273  [,)cico 13275  ...cfz 13433  βŒŠcfl 13704  seqcseq 13915  abscabs 15128  vol*covol 24849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-1st 7925  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-er 8654  df-map 8773  df-en 8890  df-dom 8891  df-sdom 8892  df-sup 9386  df-inf 9387  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-3 12225  df-n0 12422  df-z 12508  df-uz 12772  df-rp 12924  df-ico 13279  df-fz 13434  df-fl 13706  df-seq 13916  df-exp 13977  df-cj 14993  df-re 14994  df-im 14995  df-sqrt 15129  df-abs 15130
This theorem is referenced by:  ovolunlem1  24884
  Copyright terms: Public domain W3C validator