MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovolicc2lem3 Structured version   Visualization version   GIF version
Theorem ovolicc2lem3 25027
Description: Lemma for ovolicc2 25030. (Contributed by Mario Carneiro, 14-Jun-2014.)
Hypotheses
Ref Expression
ovolicc.1 (πœ‘ β†’ 𝐴 ∈ ℝ)
ovolicc.2 (πœ‘ β†’ 𝐡 ∈ ℝ)
ovolicc.3 (πœ‘ β†’ 𝐴 ≀ 𝐡)
ovolicc2.4 𝑆 = seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐹))
ovolicc2.5 (πœ‘ β†’ 𝐹:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
ovolicc2.6 (πœ‘ β†’ π‘ˆ ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
ovolicc2.7 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† βˆͺ π‘ˆ)
ovolicc2.8 (πœ‘ β†’ 𝐺:π‘ˆβŸΆβ„•)
ovolicc2.9 ((πœ‘ ∧ 𝑑 ∈ π‘ˆ) β†’ (((,) ∘ 𝐹)β€˜(πΊβ€˜π‘‘)) = 𝑑)
ovolicc2.10 𝑇 = {𝑒 ∈ π‘ˆ ∣ (𝑒 ∩ (𝐴[,]𝐡)) β‰  βˆ…}
ovolicc2.11 (πœ‘ β†’ 𝐻:π‘‡βŸΆπ‘‡)
ovolicc2.12 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ if((2nd β€˜(πΉβ€˜(πΊβ€˜π‘‘))) ≀ 𝐡, (2nd β€˜(πΉβ€˜(πΊβ€˜π‘‘))), 𝐡) ∈ (π»β€˜π‘‘))
ovolicc2.13 (πœ‘ β†’ 𝐴 ∈ 𝐢)
ovolicc2.14 (πœ‘ β†’ 𝐢 ∈ 𝑇)
ovolicc2.15 𝐾 = seq1((𝐻 ∘ 1st ), (β„• Γ— {𝐢}))
ovolicc2.16 π‘Š = {𝑛 ∈ β„• ∣ 𝐡 ∈ (πΎβ€˜π‘›)}
Assertion
Ref Expression
ovolicc2lem3 ((πœ‘ ∧ (𝑁 ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š} ∧ 𝑃 ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š})) β†’ (𝑁 = 𝑃 ↔ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘)))) = (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘ƒ))))))
Distinct variable groups:   π‘š,𝑛,𝑑,𝑒,𝐴   𝐡,π‘š,𝑛,𝑑,𝑒   𝑑,𝐻   𝐢,π‘š,𝑛,𝑑   𝑛,𝐹,𝑑   𝑛,𝐾,𝑑,𝑒   𝑛,𝐺,𝑑   π‘š,π‘Š,𝑛   πœ‘,π‘š,𝑛,𝑑   𝑇,𝑛,𝑑   𝑛,𝑁,𝑑,𝑒   π‘ˆ,𝑛,𝑑,𝑒
Allowed substitution hints:   πœ‘(𝑒)   𝐢(𝑒)   𝑃(𝑒,𝑑,π‘š,𝑛)   𝑆(𝑒,𝑑,π‘š,𝑛)   𝑇(𝑒,π‘š)   π‘ˆ(π‘š)   𝐹(𝑒,π‘š)   𝐺(𝑒,π‘š)   𝐻(𝑒,π‘š,𝑛)   𝐾(π‘š)   𝑁(π‘š)   π‘Š(𝑒,𝑑)
Proof of Theorem ovolicc2lem3
Dummy variables π‘˜ π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2fveq3 6893 . . . 4 (𝑦 = π‘˜ β†’ (πΊβ€˜(πΎβ€˜π‘¦)) = (πΊβ€˜(πΎβ€˜π‘˜)))
21fveq2d 6892 . . 3 (𝑦 = π‘˜ β†’ (πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦))) = (πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))
32fveq2d 6892 . 2 (𝑦 = π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) = (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))))
4 2fveq3 6893 . . . 4 (𝑦 = 𝑁 β†’ (πΊβ€˜(πΎβ€˜π‘¦)) = (πΊβ€˜(πΎβ€˜π‘)))
54fveq2d 6892 . . 3 (𝑦 = 𝑁 β†’ (πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦))) = (πΉβ€˜(πΊβ€˜(πΎβ€˜π‘))))
65fveq2d 6892 . 2 (𝑦 = 𝑁 β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) = (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘)))))
7 2fveq3 6893 . . . 4 (𝑦 = 𝑃 β†’ (πΊβ€˜(πΎβ€˜π‘¦)) = (πΊβ€˜(πΎβ€˜π‘ƒ)))
87fveq2d 6892 . . 3 (𝑦 = 𝑃 β†’ (πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦))) = (πΉβ€˜(πΊβ€˜(πΎβ€˜π‘ƒ))))
98fveq2d 6892 . 2 (𝑦 = 𝑃 β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) = (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘ƒ)))))
10 ssrab2 4076 . . 3 {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š} βŠ† β„•
11 nnssre 12212 . . 3 β„• βŠ† ℝ
1210, 11sstri 3990 . 2 {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š} βŠ† ℝ
1310sseli 3977 . . 3 (𝑦 ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š} β†’ 𝑦 ∈ β„•)
14 ovolicc2.5 . . . . . . 7 (πœ‘ β†’ 𝐹:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
15 inss2 4228 . . . . . . 7 ( ≀ ∩ (ℝ Γ— ℝ)) βŠ† (ℝ Γ— ℝ)
16 fss 6731 . . . . . . 7 ((𝐹:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ ( ≀ ∩ (ℝ Γ— ℝ)) βŠ† (ℝ Γ— ℝ)) β†’ 𝐹:β„•βŸΆ(ℝ Γ— ℝ))
1714, 15, 16sylancl 586 . . . . . 6 (πœ‘ β†’ 𝐹:β„•βŸΆ(ℝ Γ— ℝ))
1817adantr 481 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ 𝐹:β„•βŸΆ(ℝ Γ— ℝ))
19 ovolicc2.8 . . . . . . 7 (πœ‘ β†’ 𝐺:π‘ˆβŸΆβ„•)
2019adantr 481 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ 𝐺:π‘ˆβŸΆβ„•)
21 nnuz 12861 . . . . . . . . . 10 β„• = (β„€β‰₯β€˜1)
22 ovolicc2.15 . . . . . . . . . 10 𝐾 = seq1((𝐻 ∘ 1st ), (β„• Γ— {𝐢}))
23 1zzd 12589 . . . . . . . . . 10 (πœ‘ β†’ 1 ∈ β„€)
24 ovolicc2.14 . . . . . . . . . 10 (πœ‘ β†’ 𝐢 ∈ 𝑇)
25 ovolicc2.11 . . . . . . . . . 10 (πœ‘ β†’ 𝐻:π‘‡βŸΆπ‘‡)
2621, 22, 23, 24, 25algrf 16506 . . . . . . . . 9 (πœ‘ β†’ 𝐾:β„•βŸΆπ‘‡)
2726adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ 𝐾:β„•βŸΆπ‘‡)
28 ovolicc2.10 . . . . . . . . 9 𝑇 = {𝑒 ∈ π‘ˆ ∣ (𝑒 ∩ (𝐴[,]𝐡)) β‰  βˆ…}
2928ssrab3 4079 . . . . . . . 8 𝑇 βŠ† π‘ˆ
30 fss 6731 . . . . . . . 8 ((𝐾:β„•βŸΆπ‘‡ ∧ 𝑇 βŠ† π‘ˆ) β†’ 𝐾:β„•βŸΆπ‘ˆ)
3127, 29, 30sylancl 586 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ 𝐾:β„•βŸΆπ‘ˆ)
32 ffvelcdm 7080 . . . . . . 7 ((𝐾:β„•βŸΆπ‘ˆ ∧ 𝑦 ∈ β„•) β†’ (πΎβ€˜π‘¦) ∈ π‘ˆ)
3331, 32sylancom 588 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (πΎβ€˜π‘¦) ∈ π‘ˆ)
3420, 33ffvelcdmd 7084 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (πΊβ€˜(πΎβ€˜π‘¦)) ∈ β„•)
3518, 34ffvelcdmd 7084 . . . 4 ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦))) ∈ (ℝ Γ— ℝ))
36 xp2nd 8004 . . . 4 ((πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦))) ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) ∈ ℝ)
3735, 36syl 17 . . 3 ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) ∈ ℝ)
3813, 37sylan2 593 . 2 ((πœ‘ ∧ 𝑦 ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š}) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) ∈ ℝ)
3910sseli 3977 . . . 4 (π‘˜ ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š} β†’ π‘˜ ∈ β„•)
4039ad2antll 727 . . 3 ((πœ‘ ∧ (𝑦 ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š} ∧ π‘˜ ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š})) β†’ π‘˜ ∈ β„•)
4113anim2i 617 . . . 4 ((πœ‘ ∧ 𝑦 ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š}) β†’ (πœ‘ ∧ 𝑦 ∈ β„•))
4241adantrr 715 . . 3 ((πœ‘ ∧ (𝑦 ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š} ∧ π‘˜ ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š})) β†’ (πœ‘ ∧ 𝑦 ∈ β„•))
43 breq1 5150 . . . . . . 7 (𝑛 = π‘˜ β†’ (𝑛 ≀ π‘š ↔ π‘˜ ≀ π‘š))
4443ralbidv 3177 . . . . . 6 (𝑛 = π‘˜ β†’ (βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š ↔ βˆ€π‘š ∈ π‘Š π‘˜ ≀ π‘š))
4544elrab 3682 . . . . 5 (π‘˜ ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š} ↔ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š π‘˜ ≀ π‘š))
4645simprbi 497 . . . 4 (π‘˜ ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š} β†’ βˆ€π‘š ∈ π‘Š π‘˜ ≀ π‘š)
4746ad2antll 727 . . 3 ((πœ‘ ∧ (𝑦 ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š} ∧ π‘˜ ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š})) β†’ βˆ€π‘š ∈ π‘Š π‘˜ ≀ π‘š)
48 breq1 5150 . . . . . . 7 (π‘₯ = 1 β†’ (π‘₯ ≀ π‘š ↔ 1 ≀ π‘š))
4948ralbidv 3177 . . . . . 6 (π‘₯ = 1 β†’ (βˆ€π‘š ∈ π‘Š π‘₯ ≀ π‘š ↔ βˆ€π‘š ∈ π‘Š 1 ≀ π‘š))
50 breq2 5151 . . . . . . 7 (π‘₯ = 1 β†’ (𝑦 < π‘₯ ↔ 𝑦 < 1))
51 2fveq3 6893 . . . . . . . . . 10 (π‘₯ = 1 β†’ (πΊβ€˜(πΎβ€˜π‘₯)) = (πΊβ€˜(πΎβ€˜1)))
5251fveq2d 6892 . . . . . . . . 9 (π‘₯ = 1 β†’ (πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯))) = (πΉβ€˜(πΊβ€˜(πΎβ€˜1))))
5352fveq2d 6892 . . . . . . . 8 (π‘₯ = 1 β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯)))) = (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜1)))))
5453breq2d 5159 . . . . . . 7 (π‘₯ = 1 β†’ ((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯)))) ↔ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜1))))))
5550, 54imbi12d 344 . . . . . 6 (π‘₯ = 1 β†’ ((𝑦 < π‘₯ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯))))) ↔ (𝑦 < 1 β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜1)))))))
5649, 55imbi12d 344 . . . . 5 (π‘₯ = 1 β†’ ((βˆ€π‘š ∈ π‘Š π‘₯ ≀ π‘š β†’ (𝑦 < π‘₯ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯)))))) ↔ (βˆ€π‘š ∈ π‘Š 1 ≀ π‘š β†’ (𝑦 < 1 β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜1))))))))
5756imbi2d 340 . . . 4 (π‘₯ = 1 β†’ (((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (βˆ€π‘š ∈ π‘Š π‘₯ ≀ π‘š β†’ (𝑦 < π‘₯ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯))))))) ↔ ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (βˆ€π‘š ∈ π‘Š 1 ≀ π‘š β†’ (𝑦 < 1 β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜1)))))))))
58 breq1 5150 . . . . . . 7 (π‘₯ = π‘˜ β†’ (π‘₯ ≀ π‘š ↔ π‘˜ ≀ π‘š))
5958ralbidv 3177 . . . . . 6 (π‘₯ = π‘˜ β†’ (βˆ€π‘š ∈ π‘Š π‘₯ ≀ π‘š ↔ βˆ€π‘š ∈ π‘Š π‘˜ ≀ π‘š))
60 breq2 5151 . . . . . . 7 (π‘₯ = π‘˜ β†’ (𝑦 < π‘₯ ↔ 𝑦 < π‘˜))
61 2fveq3 6893 . . . . . . . . . 10 (π‘₯ = π‘˜ β†’ (πΊβ€˜(πΎβ€˜π‘₯)) = (πΊβ€˜(πΎβ€˜π‘˜)))
6261fveq2d 6892 . . . . . . . . 9 (π‘₯ = π‘˜ β†’ (πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯))) = (πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))
6362fveq2d 6892 . . . . . . . 8 (π‘₯ = π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯)))) = (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))))
6463breq2d 5159 . . . . . . 7 (π‘₯ = π‘˜ β†’ ((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯)))) ↔ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))))
6560, 64imbi12d 344 . . . . . 6 (π‘₯ = π‘˜ β†’ ((𝑦 < π‘₯ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯))))) ↔ (𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))))))
6659, 65imbi12d 344 . . . . 5 (π‘₯ = π‘˜ β†’ ((βˆ€π‘š ∈ π‘Š π‘₯ ≀ π‘š β†’ (𝑦 < π‘₯ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯)))))) ↔ (βˆ€π‘š ∈ π‘Š π‘˜ ≀ π‘š β†’ (𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))))))
6766imbi2d 340 . . . 4 (π‘₯ = π‘˜ β†’ (((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (βˆ€π‘š ∈ π‘Š π‘₯ ≀ π‘š β†’ (𝑦 < π‘₯ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯))))))) ↔ ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (βˆ€π‘š ∈ π‘Š π‘˜ ≀ π‘š β†’ (𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))))))))
68 breq1 5150 . . . . . . 7 (π‘₯ = (π‘˜ + 1) β†’ (π‘₯ ≀ π‘š ↔ (π‘˜ + 1) ≀ π‘š))
6968ralbidv 3177 . . . . . 6 (π‘₯ = (π‘˜ + 1) β†’ (βˆ€π‘š ∈ π‘Š π‘₯ ≀ π‘š ↔ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š))
70 breq2 5151 . . . . . . 7 (π‘₯ = (π‘˜ + 1) β†’ (𝑦 < π‘₯ ↔ 𝑦 < (π‘˜ + 1)))
71 2fveq3 6893 . . . . . . . . . 10 (π‘₯ = (π‘˜ + 1) β†’ (πΊβ€˜(πΎβ€˜π‘₯)) = (πΊβ€˜(πΎβ€˜(π‘˜ + 1))))
7271fveq2d 6892 . . . . . . . . 9 (π‘₯ = (π‘˜ + 1) β†’ (πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯))) = (πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1)))))
7372fveq2d 6892 . . . . . . . 8 (π‘₯ = (π‘˜ + 1) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯)))) = (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))))
7473breq2d 5159 . . . . . . 7 (π‘₯ = (π‘˜ + 1) β†’ ((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯)))) ↔ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1)))))))
7570, 74imbi12d 344 . . . . . 6 (π‘₯ = (π‘˜ + 1) β†’ ((𝑦 < π‘₯ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯))))) ↔ (𝑦 < (π‘˜ + 1) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))))))
7669, 75imbi12d 344 . . . . 5 (π‘₯ = (π‘˜ + 1) β†’ ((βˆ€π‘š ∈ π‘Š π‘₯ ≀ π‘š β†’ (𝑦 < π‘₯ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯)))))) ↔ (βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š β†’ (𝑦 < (π‘˜ + 1) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1)))))))))
7776imbi2d 340 . . . 4 (π‘₯ = (π‘˜ + 1) β†’ (((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (βˆ€π‘š ∈ π‘Š π‘₯ ≀ π‘š β†’ (𝑦 < π‘₯ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘₯))))))) ↔ ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š β†’ (𝑦 < (π‘˜ + 1) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))))))))
78 nnnlt1 12240 . . . . . . 7 (𝑦 ∈ β„• β†’ Β¬ 𝑦 < 1)
7978adantl 482 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ Β¬ 𝑦 < 1)
8079pm2.21d 121 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (𝑦 < 1 β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜1))))))
8180a1d 25 . . . 4 ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (βˆ€π‘š ∈ π‘Š 1 ≀ π‘š β†’ (𝑦 < 1 β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜1)))))))
82 nnre 12215 . . . . . . . . . . 11 (π‘˜ ∈ β„• β†’ π‘˜ ∈ ℝ)
8382adantr 481 . . . . . . . . . 10 ((π‘˜ ∈ β„• ∧ π‘š ∈ π‘Š) β†’ π‘˜ ∈ ℝ)
8483lep1d 12141 . . . . . . . . 9 ((π‘˜ ∈ β„• ∧ π‘š ∈ π‘Š) β†’ π‘˜ ≀ (π‘˜ + 1))
85 peano2re 11383 . . . . . . . . . . 11 (π‘˜ ∈ ℝ β†’ (π‘˜ + 1) ∈ ℝ)
8683, 85syl 17 . . . . . . . . . 10 ((π‘˜ ∈ β„• ∧ π‘š ∈ π‘Š) β†’ (π‘˜ + 1) ∈ ℝ)
87 ovolicc2.16 . . . . . . . . . . . . . 14 π‘Š = {𝑛 ∈ β„• ∣ 𝐡 ∈ (πΎβ€˜π‘›)}
8887ssrab3 4079 . . . . . . . . . . . . 13 π‘Š βŠ† β„•
8988, 11sstri 3990 . . . . . . . . . . . 12 π‘Š βŠ† ℝ
9089sseli 3977 . . . . . . . . . . 11 (π‘š ∈ π‘Š β†’ π‘š ∈ ℝ)
9190adantl 482 . . . . . . . . . 10 ((π‘˜ ∈ β„• ∧ π‘š ∈ π‘Š) β†’ π‘š ∈ ℝ)
92 letr 11304 . . . . . . . . . 10 ((π‘˜ ∈ ℝ ∧ (π‘˜ + 1) ∈ ℝ ∧ π‘š ∈ ℝ) β†’ ((π‘˜ ≀ (π‘˜ + 1) ∧ (π‘˜ + 1) ≀ π‘š) β†’ π‘˜ ≀ π‘š))
9383, 86, 91, 92syl3anc 1371 . . . . . . . . 9 ((π‘˜ ∈ β„• ∧ π‘š ∈ π‘Š) β†’ ((π‘˜ ≀ (π‘˜ + 1) ∧ (π‘˜ + 1) ≀ π‘š) β†’ π‘˜ ≀ π‘š))
9484, 93mpand 693 . . . . . . . 8 ((π‘˜ ∈ β„• ∧ π‘š ∈ π‘Š) β†’ ((π‘˜ + 1) ≀ π‘š β†’ π‘˜ ≀ π‘š))
9594ralimdva 3167 . . . . . . 7 (π‘˜ ∈ β„• β†’ (βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š β†’ βˆ€π‘š ∈ π‘Š π‘˜ ≀ π‘š))
9695imim1d 82 . . . . . 6 (π‘˜ ∈ β„• β†’ ((βˆ€π‘š ∈ π‘Š π‘˜ ≀ π‘š β†’ (𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))))) β†’ (βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š β†’ (𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))))))
9796adantl 482 . . . . 5 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ β„•) β†’ ((βˆ€π‘š ∈ π‘Š π‘˜ ≀ π‘š β†’ (𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))))) β†’ (βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š β†’ (𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))))))
98 simplr 767 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ 𝑦 ∈ β„•)
99 simprl 769 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ π‘˜ ∈ β„•)
100 nnleltp1 12613 . . . . . . . . 9 ((𝑦 ∈ β„• ∧ π‘˜ ∈ β„•) β†’ (𝑦 ≀ π‘˜ ↔ 𝑦 < (π‘˜ + 1)))
10198, 99, 100syl2anc 584 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (𝑦 ≀ π‘˜ ↔ 𝑦 < (π‘˜ + 1)))
10298nnred 12223 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ 𝑦 ∈ ℝ)
10399nnred 12223 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ π‘˜ ∈ ℝ)
104102, 103leloed 11353 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (𝑦 ≀ π‘˜ ↔ (𝑦 < π‘˜ ∨ 𝑦 = π‘˜)))
105101, 104bitr3d 280 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (𝑦 < (π‘˜ + 1) ↔ (𝑦 < π‘˜ ∨ 𝑦 = π‘˜)))
106 simpll 765 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ πœ‘)
107 ltp1 12050 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∈ ℝ β†’ π‘˜ < (π‘˜ + 1))
108 ltnle 11289 . . . . . . . . . . . . . . . . . . . . 21 ((π‘˜ ∈ ℝ ∧ (π‘˜ + 1) ∈ ℝ) β†’ (π‘˜ < (π‘˜ + 1) ↔ Β¬ (π‘˜ + 1) ≀ π‘˜))
10985, 108mpdan 685 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∈ ℝ β†’ (π‘˜ < (π‘˜ + 1) ↔ Β¬ (π‘˜ + 1) ≀ π‘˜))
110107, 109mpbid 231 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ ℝ β†’ Β¬ (π‘˜ + 1) ≀ π‘˜)
111103, 110syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ Β¬ (π‘˜ + 1) ≀ π‘˜)
112 breq2 5151 . . . . . . . . . . . . . . . . . . . 20 (π‘š = π‘˜ β†’ ((π‘˜ + 1) ≀ π‘š ↔ (π‘˜ + 1) ≀ π‘˜))
113112rspccv 3609 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š β†’ (π‘˜ ∈ π‘Š β†’ (π‘˜ + 1) ≀ π‘˜))
114113ad2antll 727 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (π‘˜ ∈ π‘Š β†’ (π‘˜ + 1) ≀ π‘˜))
115111, 114mtod 197 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ Β¬ π‘˜ ∈ π‘Š)
116 ovolicc.1 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐴 ∈ ℝ)
117 ovolicc.2 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐡 ∈ ℝ)
118 ovolicc.3 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐴 ≀ 𝐡)
119 ovolicc2.4 . . . . . . . . . . . . . . . . . 18 𝑆 = seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐹))
120 ovolicc2.6 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ π‘ˆ ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
121 ovolicc2.7 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† βˆͺ π‘ˆ)
122 ovolicc2.9 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑑 ∈ π‘ˆ) β†’ (((,) ∘ 𝐹)β€˜(πΊβ€˜π‘‘)) = 𝑑)
123 ovolicc2.12 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ if((2nd β€˜(πΉβ€˜(πΊβ€˜π‘‘))) ≀ 𝐡, (2nd β€˜(πΉβ€˜(πΊβ€˜π‘‘))), 𝐡) ∈ (π»β€˜π‘‘))
124 ovolicc2.13 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐴 ∈ 𝐢)
125116, 117, 118, 119, 14, 120, 121, 19, 122, 28, 25, 123, 124, 24, 22, 87ovolicc2lem2 25026 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ Β¬ π‘˜ ∈ π‘Š)) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ≀ 𝐡)
126106, 99, 115, 125syl12anc 835 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ≀ 𝐡)
127126iftrued 4535 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ if((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ≀ 𝐡, (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))), 𝐡) = (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))))
128 2fveq3 6893 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = (πΎβ€˜π‘˜) β†’ (πΉβ€˜(πΊβ€˜π‘‘)) = (πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))
129128fveq2d 6892 . . . . . . . . . . . . . . . . . . 19 (𝑑 = (πΎβ€˜π‘˜) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜π‘‘))) = (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))))
130129breq1d 5157 . . . . . . . . . . . . . . . . . 18 (𝑑 = (πΎβ€˜π‘˜) β†’ ((2nd β€˜(πΉβ€˜(πΊβ€˜π‘‘))) ≀ 𝐡 ↔ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ≀ 𝐡))
131130, 129ifbieq1d 4551 . . . . . . . . . . . . . . . . 17 (𝑑 = (πΎβ€˜π‘˜) β†’ if((2nd β€˜(πΉβ€˜(πΊβ€˜π‘‘))) ≀ 𝐡, (2nd β€˜(πΉβ€˜(πΊβ€˜π‘‘))), 𝐡) = if((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ≀ 𝐡, (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))), 𝐡))
132 fveq2 6888 . . . . . . . . . . . . . . . . 17 (𝑑 = (πΎβ€˜π‘˜) β†’ (π»β€˜π‘‘) = (π»β€˜(πΎβ€˜π‘˜)))
133131, 132eleq12d 2827 . . . . . . . . . . . . . . . 16 (𝑑 = (πΎβ€˜π‘˜) β†’ (if((2nd β€˜(πΉβ€˜(πΊβ€˜π‘‘))) ≀ 𝐡, (2nd β€˜(πΉβ€˜(πΊβ€˜π‘‘))), 𝐡) ∈ (π»β€˜π‘‘) ↔ if((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ≀ 𝐡, (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))), 𝐡) ∈ (π»β€˜(πΎβ€˜π‘˜))))
134123ralrimiva 3146 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βˆ€π‘‘ ∈ 𝑇 if((2nd β€˜(πΉβ€˜(πΊβ€˜π‘‘))) ≀ 𝐡, (2nd β€˜(πΉβ€˜(πΊβ€˜π‘‘))), 𝐡) ∈ (π»β€˜π‘‘))
135134ad2antrr 724 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ βˆ€π‘‘ ∈ 𝑇 if((2nd β€˜(πΉβ€˜(πΊβ€˜π‘‘))) ≀ 𝐡, (2nd β€˜(πΉβ€˜(πΊβ€˜π‘‘))), 𝐡) ∈ (π»β€˜π‘‘))
13626ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ 𝐾:β„•βŸΆπ‘‡)
137136, 99ffvelcdmd 7084 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (πΎβ€˜π‘˜) ∈ 𝑇)
138133, 135, 137rspcdva 3613 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ if((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ≀ 𝐡, (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))), 𝐡) ∈ (π»β€˜(πΎβ€˜π‘˜)))
139127, 138eqeltrrd 2834 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∈ (π»β€˜(πΎβ€˜π‘˜)))
14021, 22, 23, 24, 25algrp1 16507 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΎβ€˜(π‘˜ + 1)) = (π»β€˜(πΎβ€˜π‘˜)))
141140ad2ant2r 745 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (πΎβ€˜(π‘˜ + 1)) = (π»β€˜(πΎβ€˜π‘˜)))
142139, 141eleqtrrd 2836 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∈ (πΎβ€˜(π‘˜ + 1)))
143136, 29, 30sylancl 586 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ 𝐾:β„•βŸΆπ‘ˆ)
14499peano2nnd 12225 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (π‘˜ + 1) ∈ β„•)
145143, 144ffvelcdmd 7084 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (πΎβ€˜(π‘˜ + 1)) ∈ π‘ˆ)
146116, 117, 118, 119, 14, 120, 121, 19, 122ovolicc2lem1 25025 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (πΎβ€˜(π‘˜ + 1)) ∈ π‘ˆ) β†’ ((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∈ (πΎβ€˜(π‘˜ + 1)) ↔ ((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∈ ℝ ∧ (1st β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∧ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))))))
147106, 145, 146syl2anc 584 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ ((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∈ (πΎβ€˜(π‘˜ + 1)) ↔ ((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∈ ℝ ∧ (1st β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∧ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))))))
148142, 147mpbid 231 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ ((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∈ ℝ ∧ (1st β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∧ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1)))))))
149148simp3d 1144 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))))
15037adantr 481 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) ∈ ℝ)
15117ad2antrr 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ 𝐹:β„•βŸΆ(ℝ Γ— ℝ))
15219ad2antrr 724 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ 𝐺:π‘ˆβŸΆβ„•)
153143, 99ffvelcdmd 7084 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (πΎβ€˜π‘˜) ∈ π‘ˆ)
154152, 153ffvelcdmd 7084 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (πΊβ€˜(πΎβ€˜π‘˜)) ∈ β„•)
155151, 154ffvelcdmd 7084 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))) ∈ (ℝ Γ— ℝ))
156 xp2nd 8004 . . . . . . . . . . . . 13 ((πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))) ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∈ ℝ)
157155, 156syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∈ ℝ)
158152, 145ffvelcdmd 7084 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (πΊβ€˜(πΎβ€˜(π‘˜ + 1))) ∈ β„•)
159151, 158ffvelcdmd 7084 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1)))) ∈ (ℝ Γ— ℝ))
160 xp2nd 8004 . . . . . . . . . . . . 13 ((πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1)))) ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))) ∈ ℝ)
161159, 160syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))) ∈ ℝ)
162 lttr 11286 . . . . . . . . . . . 12 (((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) ∈ ℝ ∧ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∈ ℝ ∧ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))) ∈ ℝ) β†’ (((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∧ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1)))))) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1)))))))
163150, 157, 161, 162syl3anc 1371 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) ∧ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1)))))) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1)))))))
164149, 163mpan2d 692 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ ((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1)))))))
165164imim2d 57 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ ((𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))) β†’ (𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))))))
166165com23 86 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (𝑦 < π‘˜ β†’ ((𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))))))
1673breq1d 5157 . . . . . . . . . 10 (𝑦 = π‘˜ β†’ ((2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))) ↔ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1)))))))
168149, 167syl5ibrcom 246 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (𝑦 = π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1)))))))
169168a1dd 50 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (𝑦 = π‘˜ β†’ ((𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))))))
170166, 169jaod 857 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ ((𝑦 < π‘˜ ∨ 𝑦 = π‘˜) β†’ ((𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))))))
171105, 170sylbid 239 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ (𝑦 < (π‘˜ + 1) β†’ ((𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))))))
172171com23 86 . . . . 5 (((πœ‘ ∧ 𝑦 ∈ β„•) ∧ (π‘˜ ∈ β„• ∧ βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š)) β†’ ((𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))) β†’ (𝑦 < (π‘˜ + 1) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))))))
17397, 172animpimp2impd 844 . . . 4 (π‘˜ ∈ β„• β†’ (((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (βˆ€π‘š ∈ π‘Š π‘˜ ≀ π‘š β†’ (𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))))) β†’ ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (βˆ€π‘š ∈ π‘Š (π‘˜ + 1) ≀ π‘š β†’ (𝑦 < (π‘˜ + 1) β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜(π‘˜ + 1))))))))))
17457, 67, 77, 67, 81, 173nnind 12226 . . 3 (π‘˜ ∈ β„• β†’ ((πœ‘ ∧ 𝑦 ∈ β„•) β†’ (βˆ€π‘š ∈ π‘Š π‘˜ ≀ π‘š β†’ (𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))))))
17540, 42, 47, 174syl3c 66 . 2 ((πœ‘ ∧ (𝑦 ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š} ∧ π‘˜ ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š})) β†’ (𝑦 < π‘˜ β†’ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘¦)))) < (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘˜))))))
1763, 6, 9, 12, 38, 175eqord1 11738 1 ((πœ‘ ∧ (𝑁 ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š} ∧ 𝑃 ∈ {𝑛 ∈ β„• ∣ βˆ€π‘š ∈ π‘Š 𝑛 ≀ π‘š})) β†’ (𝑁 = 𝑃 ↔ (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘)))) = (2nd β€˜(πΉβ€˜(πΊβ€˜(πΎβ€˜π‘ƒ))))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  {crab 3432   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  ifcif 4527  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907   class class class wbr 5147   Γ— cxp 5673  ran crn 5676   ∘ ccom 5679  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405  1st c1st 7969  2nd c2nd 7970  Fincfn 8935  β„cr 11105  1c1 11107   + caddc 11109   < clt 11244   ≀ cle 11245   βˆ’ cmin 11440  β„•cn 12208  (,)cioo 13320  [,]cicc 13323  seqcseq 13962  abscabs 15177
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-n0 12469  df-z 12555  df-uz 12819  df-ioo 13324  df-icc 13327  df-fz 13481  df-seq 13963
This theorem is referenced by:  ovolicc2lem4  25028
  Copyright terms: Public domain W3C validator