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

Theorem ovolicc2lem3 23333
 Description: Lemma for ovolicc2 23336. (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 fveq2 6229 . . . . 5 (𝑦 = 𝑘 → (𝐾𝑦) = (𝐾𝑘))
21fveq2d 6233 . . . 4 (𝑦 = 𝑘 → (𝐺‘(𝐾𝑦)) = (𝐺‘(𝐾𝑘)))
32fveq2d 6233 . . 3 (𝑦 = 𝑘 → (𝐹‘(𝐺‘(𝐾𝑦))) = (𝐹‘(𝐺‘(𝐾𝑘))))
43fveq2d 6233 . 2 (𝑦 = 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))
5 fveq2 6229 . . . . 5 (𝑦 = 𝑁 → (𝐾𝑦) = (𝐾𝑁))
65fveq2d 6233 . . . 4 (𝑦 = 𝑁 → (𝐺‘(𝐾𝑦)) = (𝐺‘(𝐾𝑁)))
76fveq2d 6233 . . 3 (𝑦 = 𝑁 → (𝐹‘(𝐺‘(𝐾𝑦))) = (𝐹‘(𝐺‘(𝐾𝑁))))
87fveq2d 6233 . 2 (𝑦 = 𝑁 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑁)))))
9 fveq2 6229 . . . . 5 (𝑦 = 𝑃 → (𝐾𝑦) = (𝐾𝑃))
109fveq2d 6233 . . . 4 (𝑦 = 𝑃 → (𝐺‘(𝐾𝑦)) = (𝐺‘(𝐾𝑃)))
1110fveq2d 6233 . . 3 (𝑦 = 𝑃 → (𝐹‘(𝐺‘(𝐾𝑦))) = (𝐹‘(𝐺‘(𝐾𝑃))))
1211fveq2d 6233 . 2 (𝑦 = 𝑃 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑃)))))
13 ssrab2 3720 . . 3 {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ⊆ ℕ
14 nnssre 11062 . . 3 ℕ ⊆ ℝ
1513, 14sstri 3645 . 2 {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ⊆ ℝ
1613sseli 3632 . . 3 (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} → 𝑦 ∈ ℕ)
17 ovolicc2.5 . . . . . . 7 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
18 inss2 3867 . . . . . . 7 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
19 fss 6094 . . . . . . 7 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ × ℝ))
2017, 18, 19sylancl 695 . . . . . 6 (𝜑𝐹:ℕ⟶(ℝ × ℝ))
2120adantr 480 . . . . 5 ((𝜑𝑦 ∈ ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
22 ovolicc2.8 . . . . . . 7 (𝜑𝐺:𝑈⟶ℕ)
2322adantr 480 . . . . . 6 ((𝜑𝑦 ∈ ℕ) → 𝐺:𝑈⟶ℕ)
24 nnuz 11761 . . . . . . . . . 10 ℕ = (ℤ‘1)
25 ovolicc2.15 . . . . . . . . . 10 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))
26 1zzd 11446 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
27 ovolicc2.14 . . . . . . . . . 10 (𝜑𝐶𝑇)
28 ovolicc2.11 . . . . . . . . . 10 (𝜑𝐻:𝑇𝑇)
2924, 25, 26, 27, 28algrf 15333 . . . . . . . . 9 (𝜑𝐾:ℕ⟶𝑇)
3029adantr 480 . . . . . . . 8 ((𝜑𝑦 ∈ ℕ) → 𝐾:ℕ⟶𝑇)
31 ovolicc2.10 . . . . . . . . 9 𝑇 = {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
32 ssrab2 3720 . . . . . . . . 9 {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⊆ 𝑈
3331, 32eqsstri 3668 . . . . . . . 8 𝑇𝑈
34 fss 6094 . . . . . . . 8 ((𝐾:ℕ⟶𝑇𝑇𝑈) → 𝐾:ℕ⟶𝑈)
3530, 33, 34sylancl 695 . . . . . . 7 ((𝜑𝑦 ∈ ℕ) → 𝐾:ℕ⟶𝑈)
36 ffvelrn 6397 . . . . . . 7 ((𝐾:ℕ⟶𝑈𝑦 ∈ ℕ) → (𝐾𝑦) ∈ 𝑈)
3735, 36sylancom 702 . . . . . 6 ((𝜑𝑦 ∈ ℕ) → (𝐾𝑦) ∈ 𝑈)
3823, 37ffvelrnd 6400 . . . . 5 ((𝜑𝑦 ∈ ℕ) → (𝐺‘(𝐾𝑦)) ∈ ℕ)
3921, 38ffvelrnd 6400 . . . 4 ((𝜑𝑦 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾𝑦))) ∈ (ℝ × ℝ))
40 xp2nd 7243 . . . 4 ((𝐹‘(𝐺‘(𝐾𝑦))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) ∈ ℝ)
4139, 40syl 17 . . 3 ((𝜑𝑦 ∈ ℕ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) ∈ ℝ)
4216, 41sylan2 490 . 2 ((𝜑𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚}) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) ∈ ℝ)
4313sseli 3632 . . . 4 (𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} → 𝑘 ∈ ℕ)
4443ad2antll 765 . . 3 ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → 𝑘 ∈ ℕ)
4516anim2i 592 . . . 4 ((𝜑𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚}) → (𝜑𝑦 ∈ ℕ))
4645adantrr 753 . . 3 ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → (𝜑𝑦 ∈ ℕ))
47 breq1 4688 . . . . . . 7 (𝑛 = 𝑘 → (𝑛𝑚𝑘𝑚))
4847ralbidv 3015 . . . . . 6 (𝑛 = 𝑘 → (∀𝑚𝑊 𝑛𝑚 ↔ ∀𝑚𝑊 𝑘𝑚))
4948elrab 3396 . . . . 5 (𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ↔ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 𝑘𝑚))
5049simprbi 479 . . . 4 (𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} → ∀𝑚𝑊 𝑘𝑚)
5150ad2antll 765 . . 3 ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → ∀𝑚𝑊 𝑘𝑚)
52 breq1 4688 . . . . . . 7 (𝑥 = 1 → (𝑥𝑚 ↔ 1 ≤ 𝑚))
5352ralbidv 3015 . . . . . 6 (𝑥 = 1 → (∀𝑚𝑊 𝑥𝑚 ↔ ∀𝑚𝑊 1 ≤ 𝑚))
54 breq2 4689 . . . . . . 7 (𝑥 = 1 → (𝑦 < 𝑥𝑦 < 1))
55 fveq2 6229 . . . . . . . . . . 11 (𝑥 = 1 → (𝐾𝑥) = (𝐾‘1))
5655fveq2d 6233 . . . . . . . . . 10 (𝑥 = 1 → (𝐺‘(𝐾𝑥)) = (𝐺‘(𝐾‘1)))
5756fveq2d 6233 . . . . . . . . 9 (𝑥 = 1 → (𝐹‘(𝐺‘(𝐾𝑥))) = (𝐹‘(𝐺‘(𝐾‘1))))
5857fveq2d 6233 . . . . . . . 8 (𝑥 = 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘1)))))
5958breq2d 4697 . . . . . . 7 (𝑥 = 1 → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥)))) ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1))))))
6054, 59imbi12d 333 . . . . . 6 (𝑥 = 1 → ((𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥))))) ↔ (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1)))))))
6153, 60imbi12d 333 . . . . 5 (𝑥 = 1 → ((∀𝑚𝑊 𝑥𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥)))))) ↔ (∀𝑚𝑊 1 ≤ 𝑚 → (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1))))))))
6261imbi2d 329 . . . 4 (𝑥 = 1 → (((𝜑𝑦 ∈ ℕ) → (∀𝑚𝑊 𝑥𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥))))))) ↔ ((𝜑𝑦 ∈ ℕ) → (∀𝑚𝑊 1 ≤ 𝑚 → (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1)))))))))
63 breq1 4688 . . . . . . 7 (𝑥 = 𝑘 → (𝑥𝑚𝑘𝑚))
6463ralbidv 3015 . . . . . 6 (𝑥 = 𝑘 → (∀𝑚𝑊 𝑥𝑚 ↔ ∀𝑚𝑊 𝑘𝑚))
65 breq2 4689 . . . . . . 7 (𝑥 = 𝑘 → (𝑦 < 𝑥𝑦 < 𝑘))
66 fveq2 6229 . . . . . . . . . . 11 (𝑥 = 𝑘 → (𝐾𝑥) = (𝐾𝑘))
6766fveq2d 6233 . . . . . . . . . 10 (𝑥 = 𝑘 → (𝐺‘(𝐾𝑥)) = (𝐺‘(𝐾𝑘)))
6867fveq2d 6233 . . . . . . . . 9 (𝑥 = 𝑘 → (𝐹‘(𝐺‘(𝐾𝑥))) = (𝐹‘(𝐺‘(𝐾𝑘))))
6968fveq2d 6233 . . . . . . . 8 (𝑥 = 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))
7069breq2d 4697 . . . . . . 7 (𝑥 = 𝑘 → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥)))) ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))))
7165, 70imbi12d 333 . . . . . 6 (𝑥 = 𝑘 → ((𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥))))) ↔ (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))))
7264, 71imbi12d 333 . . . . 5 (𝑥 = 𝑘 → ((∀𝑚𝑊 𝑥𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥)))))) ↔ (∀𝑚𝑊 𝑘𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))))))
7372imbi2d 329 . . . 4 (𝑥 = 𝑘 → (((𝜑𝑦 ∈ ℕ) → (∀𝑚𝑊 𝑥𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥))))))) ↔ ((𝜑𝑦 ∈ ℕ) → (∀𝑚𝑊 𝑘𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))))))
74 breq1 4688 . . . . . . 7 (𝑥 = (𝑘 + 1) → (𝑥𝑚 ↔ (𝑘 + 1) ≤ 𝑚))
7574ralbidv 3015 . . . . . 6 (𝑥 = (𝑘 + 1) → (∀𝑚𝑊 𝑥𝑚 ↔ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚))
76 breq2 4689 . . . . . . 7 (𝑥 = (𝑘 + 1) → (𝑦 < 𝑥𝑦 < (𝑘 + 1)))
77 fveq2 6229 . . . . . . . . . . 11 (𝑥 = (𝑘 + 1) → (𝐾𝑥) = (𝐾‘(𝑘 + 1)))
7877fveq2d 6233 . . . . . . . . . 10 (𝑥 = (𝑘 + 1) → (𝐺‘(𝐾𝑥)) = (𝐺‘(𝐾‘(𝑘 + 1))))
7978fveq2d 6233 . . . . . . . . 9 (𝑥 = (𝑘 + 1) → (𝐹‘(𝐺‘(𝐾𝑥))) = (𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))
8079fveq2d 6233 . . . . . . . 8 (𝑥 = (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))
8180breq2d 4697 . . . . . . 7 (𝑥 = (𝑘 + 1) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥)))) ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))
8276, 81imbi12d 333 . . . . . 6 (𝑥 = (𝑘 + 1) → ((𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥))))) ↔ (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))
8375, 82imbi12d 333 . . . . 5 (𝑥 = (𝑘 + 1) → ((∀𝑚𝑊 𝑥𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥)))))) ↔ (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))))
8483imbi2d 329 . . . 4 (𝑥 = (𝑘 + 1) → (((𝜑𝑦 ∈ ℕ) → (∀𝑚𝑊 𝑥𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥))))))) ↔ ((𝜑𝑦 ∈ ℕ) → (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))))
85 nnnlt1 11088 . . . . . . 7 (𝑦 ∈ ℕ → ¬ 𝑦 < 1)
8685adantl 481 . . . . . 6 ((𝜑𝑦 ∈ ℕ) → ¬ 𝑦 < 1)
8786pm2.21d 118 . . . . 5 ((𝜑𝑦 ∈ ℕ) → (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1))))))
8887a1d 25 . . . 4 ((𝜑𝑦 ∈ ℕ) → (∀𝑚𝑊 1 ≤ 𝑚 → (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1)))))))
89 nnre 11065 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
9089adantr 480 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑚𝑊) → 𝑘 ∈ ℝ)
9190lep1d 10993 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑚𝑊) → 𝑘 ≤ (𝑘 + 1))
92 peano2re 10247 . . . . . . . . . . . . 13 (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
9390, 92syl 17 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑚𝑊) → (𝑘 + 1) ∈ ℝ)
94 ovolicc2.16 . . . . . . . . . . . . . . . 16 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾𝑛)}
95 ssrab2 3720 . . . . . . . . . . . . . . . 16 {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾𝑛)} ⊆ ℕ
9694, 95eqsstri 3668 . . . . . . . . . . . . . . 15 𝑊 ⊆ ℕ
9796, 14sstri 3645 . . . . . . . . . . . . . 14 𝑊 ⊆ ℝ
9897sseli 3632 . . . . . . . . . . . . 13 (𝑚𝑊𝑚 ∈ ℝ)
9998adantl 481 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑚𝑊) → 𝑚 ∈ ℝ)
100 letr 10169 . . . . . . . . . . . 12 ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑚) → 𝑘𝑚))
10190, 93, 99, 100syl3anc 1366 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑚𝑊) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑚) → 𝑘𝑚))
10291, 101mpand 711 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ 𝑚𝑊) → ((𝑘 + 1) ≤ 𝑚𝑘𝑚))
103102ralimdva 2991 . . . . . . . . 9 (𝑘 ∈ ℕ → (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → ∀𝑚𝑊 𝑘𝑚))
104103imim1d 82 . . . . . . . 8 (𝑘 ∈ ℕ → ((∀𝑚𝑊 𝑘𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))) → (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))))))
105104adantl 481 . . . . . . 7 (((𝜑𝑦 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((∀𝑚𝑊 𝑘𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))) → (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))))))
106 simplr 807 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑦 ∈ ℕ)
107 simprl 809 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑘 ∈ ℕ)
108 nnleltp1 11470 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑦𝑘𝑦 < (𝑘 + 1)))
109106, 107, 108syl2anc 694 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦𝑘𝑦 < (𝑘 + 1)))
110106nnred 11073 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑦 ∈ ℝ)
111107nnred 11073 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑘 ∈ ℝ)
112110, 111leloed 10218 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦𝑘 ↔ (𝑦 < 𝑘𝑦 = 𝑘)))
113109, 112bitr3d 270 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 < (𝑘 + 1) ↔ (𝑦 < 𝑘𝑦 = 𝑘)))
114 simpll 805 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝜑)
115 ltp1 10899 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ ℝ → 𝑘 < (𝑘 + 1))
116 ltnle 10155 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘))
11792, 116mpdan 703 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ ℝ → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘))
118115, 117mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℝ → ¬ (𝑘 + 1) ≤ 𝑘)
119111, 118syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → ¬ (𝑘 + 1) ≤ 𝑘)
120 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = 𝑘 → ((𝑘 + 1) ≤ 𝑚 ↔ (𝑘 + 1) ≤ 𝑘))
121120rspccv 3337 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑘𝑊 → (𝑘 + 1) ≤ 𝑘))
122121ad2antll 765 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑘𝑊 → (𝑘 + 1) ≤ 𝑘))
123119, 122mtod 189 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → ¬ 𝑘𝑊)
124 ovolicc.1 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐴 ∈ ℝ)
125 ovolicc.2 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵 ∈ ℝ)
126 ovolicc.3 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐴𝐵)
127 ovolicc2.4 . . . . . . . . . . . . . . . . . . . . . 22 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
128 ovolicc2.6 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
129 ovolicc2.7 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴[,]𝐵) ⊆ 𝑈)
130 ovolicc2.9 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡𝑈) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
131 ovolicc2.12 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
132 ovolicc2.13 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐴𝐶)
133124, 125, 126, 127, 17, 128, 129, 22, 130, 31, 28, 131, 132, 27, 25, 94ovolicc2lem2 23332 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ ¬ 𝑘𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵)
134114, 107, 123, 133syl12anc 1364 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵)
135134iftrued 4127 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))), 𝐵) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))
13629ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐾:ℕ⟶𝑇)
137136, 107ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾𝑘) ∈ 𝑇)
138131ralrimiva 2995 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
139138ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
140 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = (𝐾𝑘) → (𝐺𝑡) = (𝐺‘(𝐾𝑘)))
141140fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = (𝐾𝑘) → (𝐹‘(𝐺𝑡)) = (𝐹‘(𝐺‘(𝐾𝑘))))
142141fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = (𝐾𝑘) → (2nd ‘(𝐹‘(𝐺𝑡))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))
143142breq1d 4695 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = (𝐾𝑘) → ((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵))
144143, 142ifbieq1d 4142 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = (𝐾𝑘) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) = if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))), 𝐵))
145 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = (𝐾𝑘) → (𝐻𝑡) = (𝐻‘(𝐾𝑘)))
146144, 145eleq12d 2724 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = (𝐾𝑘) → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡) ↔ if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))), 𝐵) ∈ (𝐻‘(𝐾𝑘))))
147146rspcv 3336 . . . . . . . . . . . . . . . . . . . 20 ((𝐾𝑘) ∈ 𝑇 → (∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))), 𝐵) ∈ (𝐻‘(𝐾𝑘))))
148137, 139, 147sylc 65 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))), 𝐵) ∈ (𝐻‘(𝐾𝑘)))
149135, 148eqeltrrd 2731 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ (𝐻‘(𝐾𝑘)))
15024, 25, 26, 27, 28algrp1 15334 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐾‘(𝑘 + 1)) = (𝐻‘(𝐾𝑘)))
151150ad2ant2r 798 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾‘(𝑘 + 1)) = (𝐻‘(𝐾𝑘)))
152149, 151eleqtrrd 2733 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ (𝐾‘(𝑘 + 1)))
153136, 33, 34sylancl 695 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐾:ℕ⟶𝑈)
154107peano2nnd 11075 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑘 + 1) ∈ ℕ)
155153, 154ffvelrnd 6400 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾‘(𝑘 + 1)) ∈ 𝑈)
156124, 125, 126, 127, 17, 128, 129, 22, 130ovolicc2lem1 23331 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐾‘(𝑘 + 1)) ∈ 𝑈) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ (𝐾‘(𝑘 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))
157114, 155, 156syl2anc 694 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ (𝐾‘(𝑘 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))
158152, 157mpbid 222 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))
159158simp3d 1095 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))
16041adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) ∈ ℝ)
16120ad2antrr 762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐹:ℕ⟶(ℝ × ℝ))
16222ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐺:𝑈⟶ℕ)
163153, 107ffvelrnd 6400 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾𝑘) ∈ 𝑈)
164162, 163ffvelrnd 6400 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐺‘(𝐾𝑘)) ∈ ℕ)
165161, 164ffvelrnd 6400 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐹‘(𝐺‘(𝐾𝑘))) ∈ (ℝ × ℝ))
166 xp2nd 7243 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝐺‘(𝐾𝑘))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ ℝ)
167165, 166syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ ℝ)
168162, 155ffvelrnd 6400 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐺‘(𝐾‘(𝑘 + 1))) ∈ ℕ)
169161, 168ffvelrnd 6400 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))) ∈ (ℝ × ℝ))
170 xp2nd 7243 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ∈ ℝ)
171169, 170syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ∈ ℝ)
172 lttr 10152 . . . . . . . . . . . . . . . 16 (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) ∈ ℝ ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ ℝ ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ∈ ℝ) → (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))
173160, 167, 171, 172syl3anc 1366 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))
174159, 173mpan2d 710 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))
175174imim2d 57 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))) → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))
176175com23 86 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 < 𝑘 → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))
1774breq1d 4695 . . . . . . . . . . . . . 14 (𝑦 = 𝑘 → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))
178159, 177syl5ibrcom 237 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 = 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))
179178a1dd 50 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 = 𝑘 → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))
180176, 179jaod 394 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → ((𝑦 < 𝑘𝑦 = 𝑘) → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))
181113, 180sylbid 230 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 < (𝑘 + 1) → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))
182181com23 86 . . . . . . . . 9 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))) → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))
183182expr 642 . . . . . . . 8 (((𝜑𝑦 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))) → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))))
184183a2d 29 . . . . . . 7 (((𝜑𝑦 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))) → (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))))
185105, 184syld 47 . . . . . 6 (((𝜑𝑦 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((∀𝑚𝑊 𝑘𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))) → (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))))
186185expcom 450 . . . . 5 (𝑘 ∈ ℕ → ((𝜑𝑦 ∈ ℕ) → ((∀𝑚𝑊 𝑘𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))) → (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))))
187186a2d 29 . . . 4 (𝑘 ∈ ℕ → (((𝜑𝑦 ∈ ℕ) → (∀𝑚𝑊 𝑘𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))))) → ((𝜑𝑦 ∈ ℕ) → (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))))
18862, 73, 84, 73, 88, 187nnind 11076 . . 3 (𝑘 ∈ ℕ → ((𝜑𝑦 ∈ ℕ) → (∀𝑚𝑊 𝑘𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))))))
18944, 46, 51, 188syl3c 66 . 2 ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))))
1904, 8, 12, 15, 42, 189eqord1 10594 1 ((𝜑 ∧ (𝑁 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑃 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → (𝑁 = 𝑃 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑁)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑃))))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  {crab 2945   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  ifcif 4119  𝒫 cpw 4191  {csn 4210  ∪ cuni 4468   class class class wbr 4685   × cxp 5141  ran crn 5144   ∘ ccom 5147  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  Fincfn 7997  ℝcr 9973  1c1 9975   + caddc 9977   < clt 10112   ≤ cle 10113   − cmin 10304  ℕcn 11058  (,)cioo 12213  [,]cicc 12216  seqcseq 12841  abscabs 14018 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-ioo 12217  df-icc 12220  df-fz 12365  df-seq 12842 This theorem is referenced by:  ovolicc2lem4  23334
 Copyright terms: Public domain W3C validator