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

Theorem ovolicc2lem3 23483
Description: Lemma for ovolicc2 23486. (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 6348 . . . . 5 (𝑦 = 𝑘 → (𝐾𝑦) = (𝐾𝑘))
21fveq2d 6352 . . . 4 (𝑦 = 𝑘 → (𝐺‘(𝐾𝑦)) = (𝐺‘(𝐾𝑘)))
32fveq2d 6352 . . 3 (𝑦 = 𝑘 → (𝐹‘(𝐺‘(𝐾𝑦))) = (𝐹‘(𝐺‘(𝐾𝑘))))
43fveq2d 6352 . 2 (𝑦 = 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))
5 fveq2 6348 . . . . 5 (𝑦 = 𝑁 → (𝐾𝑦) = (𝐾𝑁))
65fveq2d 6352 . . . 4 (𝑦 = 𝑁 → (𝐺‘(𝐾𝑦)) = (𝐺‘(𝐾𝑁)))
76fveq2d 6352 . . 3 (𝑦 = 𝑁 → (𝐹‘(𝐺‘(𝐾𝑦))) = (𝐹‘(𝐺‘(𝐾𝑁))))
87fveq2d 6352 . 2 (𝑦 = 𝑁 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑁)))))
9 fveq2 6348 . . . . 5 (𝑦 = 𝑃 → (𝐾𝑦) = (𝐾𝑃))
109fveq2d 6352 . . . 4 (𝑦 = 𝑃 → (𝐺‘(𝐾𝑦)) = (𝐺‘(𝐾𝑃)))
1110fveq2d 6352 . . 3 (𝑦 = 𝑃 → (𝐹‘(𝐺‘(𝐾𝑦))) = (𝐹‘(𝐺‘(𝐾𝑃))))
1211fveq2d 6352 . 2 (𝑦 = 𝑃 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑃)))))
13 ssrab2 3824 . . 3 {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ⊆ ℕ
14 nnssre 11212 . . 3 ℕ ⊆ ℝ
1513, 14sstri 3749 . 2 {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ⊆ ℝ
1613sseli 3736 . . 3 (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} → 𝑦 ∈ ℕ)
17 ovolicc2.5 . . . . . . 7 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
18 inss2 3973 . . . . . . 7 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
19 fss 6213 . . . . . . 7 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ × ℝ))
2017, 18, 19sylancl 697 . . . . . 6 (𝜑𝐹:ℕ⟶(ℝ × ℝ))
2120adantr 472 . . . . 5 ((𝜑𝑦 ∈ ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
22 ovolicc2.8 . . . . . . 7 (𝜑𝐺:𝑈⟶ℕ)
2322adantr 472 . . . . . 6 ((𝜑𝑦 ∈ ℕ) → 𝐺:𝑈⟶ℕ)
24 nnuz 11912 . . . . . . . . . 10 ℕ = (ℤ‘1)
25 ovolicc2.15 . . . . . . . . . 10 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))
26 1zzd 11596 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
27 ovolicc2.14 . . . . . . . . . 10 (𝜑𝐶𝑇)
28 ovolicc2.11 . . . . . . . . . 10 (𝜑𝐻:𝑇𝑇)
2924, 25, 26, 27, 28algrf 15484 . . . . . . . . 9 (𝜑𝐾:ℕ⟶𝑇)
3029adantr 472 . . . . . . . 8 ((𝜑𝑦 ∈ ℕ) → 𝐾:ℕ⟶𝑇)
31 ovolicc2.10 . . . . . . . . 9 𝑇 = {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
32 ssrab2 3824 . . . . . . . . 9 {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⊆ 𝑈
3331, 32eqsstri 3772 . . . . . . . 8 𝑇𝑈
34 fss 6213 . . . . . . . 8 ((𝐾:ℕ⟶𝑇𝑇𝑈) → 𝐾:ℕ⟶𝑈)
3530, 33, 34sylancl 697 . . . . . . 7 ((𝜑𝑦 ∈ ℕ) → 𝐾:ℕ⟶𝑈)
36 ffvelrn 6516 . . . . . . 7 ((𝐾:ℕ⟶𝑈𝑦 ∈ ℕ) → (𝐾𝑦) ∈ 𝑈)
3735, 36sylancom 704 . . . . . 6 ((𝜑𝑦 ∈ ℕ) → (𝐾𝑦) ∈ 𝑈)
3823, 37ffvelrnd 6519 . . . . 5 ((𝜑𝑦 ∈ ℕ) → (𝐺‘(𝐾𝑦)) ∈ ℕ)
3921, 38ffvelrnd 6519 . . . 4 ((𝜑𝑦 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾𝑦))) ∈ (ℝ × ℝ))
40 xp2nd 7362 . . . 4 ((𝐹‘(𝐺‘(𝐾𝑦))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) ∈ ℝ)
4139, 40syl 17 . . 3 ((𝜑𝑦 ∈ ℕ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) ∈ ℝ)
4216, 41sylan2 492 . 2 ((𝜑𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚}) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) ∈ ℝ)
4313sseli 3736 . . . 4 (𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} → 𝑘 ∈ ℕ)
4443ad2antll 767 . . 3 ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → 𝑘 ∈ ℕ)
4516anim2i 594 . . . 4 ((𝜑𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚}) → (𝜑𝑦 ∈ ℕ))
4645adantrr 755 . . 3 ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → (𝜑𝑦 ∈ ℕ))
47 breq1 4803 . . . . . . 7 (𝑛 = 𝑘 → (𝑛𝑚𝑘𝑚))
4847ralbidv 3120 . . . . . 6 (𝑛 = 𝑘 → (∀𝑚𝑊 𝑛𝑚 ↔ ∀𝑚𝑊 𝑘𝑚))
4948elrab 3500 . . . . 5 (𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ↔ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 𝑘𝑚))
5049simprbi 483 . . . 4 (𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} → ∀𝑚𝑊 𝑘𝑚)
5150ad2antll 767 . . 3 ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → ∀𝑚𝑊 𝑘𝑚)
52 breq1 4803 . . . . . . 7 (𝑥 = 1 → (𝑥𝑚 ↔ 1 ≤ 𝑚))
5352ralbidv 3120 . . . . . 6 (𝑥 = 1 → (∀𝑚𝑊 𝑥𝑚 ↔ ∀𝑚𝑊 1 ≤ 𝑚))
54 breq2 4804 . . . . . . 7 (𝑥 = 1 → (𝑦 < 𝑥𝑦 < 1))
55 fveq2 6348 . . . . . . . . . . 11 (𝑥 = 1 → (𝐾𝑥) = (𝐾‘1))
5655fveq2d 6352 . . . . . . . . . 10 (𝑥 = 1 → (𝐺‘(𝐾𝑥)) = (𝐺‘(𝐾‘1)))
5756fveq2d 6352 . . . . . . . . 9 (𝑥 = 1 → (𝐹‘(𝐺‘(𝐾𝑥))) = (𝐹‘(𝐺‘(𝐾‘1))))
5857fveq2d 6352 . . . . . . . 8 (𝑥 = 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘1)))))
5958breq2d 4812 . . . . . . 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 4803 . . . . . . 7 (𝑥 = 𝑘 → (𝑥𝑚𝑘𝑚))
6463ralbidv 3120 . . . . . 6 (𝑥 = 𝑘 → (∀𝑚𝑊 𝑥𝑚 ↔ ∀𝑚𝑊 𝑘𝑚))
65 breq2 4804 . . . . . . 7 (𝑥 = 𝑘 → (𝑦 < 𝑥𝑦 < 𝑘))
66 fveq2 6348 . . . . . . . . . . 11 (𝑥 = 𝑘 → (𝐾𝑥) = (𝐾𝑘))
6766fveq2d 6352 . . . . . . . . . 10 (𝑥 = 𝑘 → (𝐺‘(𝐾𝑥)) = (𝐺‘(𝐾𝑘)))
6867fveq2d 6352 . . . . . . . . 9 (𝑥 = 𝑘 → (𝐹‘(𝐺‘(𝐾𝑥))) = (𝐹‘(𝐺‘(𝐾𝑘))))
6968fveq2d 6352 . . . . . . . 8 (𝑥 = 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))
7069breq2d 4812 . . . . . . 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 4803 . . . . . . 7 (𝑥 = (𝑘 + 1) → (𝑥𝑚 ↔ (𝑘 + 1) ≤ 𝑚))
7574ralbidv 3120 . . . . . 6 (𝑥 = (𝑘 + 1) → (∀𝑚𝑊 𝑥𝑚 ↔ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚))
76 breq2 4804 . . . . . . 7 (𝑥 = (𝑘 + 1) → (𝑦 < 𝑥𝑦 < (𝑘 + 1)))
77 fveq2 6348 . . . . . . . . . . 11 (𝑥 = (𝑘 + 1) → (𝐾𝑥) = (𝐾‘(𝑘 + 1)))
7877fveq2d 6352 . . . . . . . . . 10 (𝑥 = (𝑘 + 1) → (𝐺‘(𝐾𝑥)) = (𝐺‘(𝐾‘(𝑘 + 1))))
7978fveq2d 6352 . . . . . . . . 9 (𝑥 = (𝑘 + 1) → (𝐹‘(𝐺‘(𝐾𝑥))) = (𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))
8079fveq2d 6352 . . . . . . . 8 (𝑥 = (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑥)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))
8180breq2d 4812 . . . . . . 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 11238 . . . . . . 7 (𝑦 ∈ ℕ → ¬ 𝑦 < 1)
8685adantl 473 . . . . . 6 ((𝜑𝑦 ∈ ℕ) → ¬ 𝑦 < 1)
8786pm2.21d 118 . . . . 5 ((𝜑𝑦 ∈ ℕ) → (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1))))))
8887a1d 25 . . . 4 ((𝜑𝑦 ∈ ℕ) → (∀𝑚𝑊 1 ≤ 𝑚 → (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1)))))))
89 nnre 11215 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
9089adantr 472 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑚𝑊) → 𝑘 ∈ ℝ)
9190lep1d 11143 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑚𝑊) → 𝑘 ≤ (𝑘 + 1))
92 peano2re 10397 . . . . . . . . . . . . 13 (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
9390, 92syl 17 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑚𝑊) → (𝑘 + 1) ∈ ℝ)
94 ovolicc2.16 . . . . . . . . . . . . . . . 16 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾𝑛)}
95 ssrab2 3824 . . . . . . . . . . . . . . . 16 {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾𝑛)} ⊆ ℕ
9694, 95eqsstri 3772 . . . . . . . . . . . . . . 15 𝑊 ⊆ ℕ
9796, 14sstri 3749 . . . . . . . . . . . . . 14 𝑊 ⊆ ℝ
9897sseli 3736 . . . . . . . . . . . . 13 (𝑚𝑊𝑚 ∈ ℝ)
9998adantl 473 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑚𝑊) → 𝑚 ∈ ℝ)
100 letr 10319 . . . . . . . . . . . 12 ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑚) → 𝑘𝑚))
10190, 93, 99, 100syl3anc 1477 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑚𝑊) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑚) → 𝑘𝑚))
10291, 101mpand 713 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ 𝑚𝑊) → ((𝑘 + 1) ≤ 𝑚𝑘𝑚))
103102ralimdva 3096 . . . . . . . . 9 (𝑘 ∈ ℕ → (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → ∀𝑚𝑊 𝑘𝑚))
104103imim1d 82 . . . . . . . 8 (𝑘 ∈ ℕ → ((∀𝑚𝑊 𝑘𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))) → (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))))))
105104adantl 473 . . . . . . 7 (((𝜑𝑦 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((∀𝑚𝑊 𝑘𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))) → (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))))))
106 simplr 809 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑦 ∈ ℕ)
107 simprl 811 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑘 ∈ ℕ)
108 nnleltp1 11620 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑦𝑘𝑦 < (𝑘 + 1)))
109106, 107, 108syl2anc 696 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦𝑘𝑦 < (𝑘 + 1)))
110106nnred 11223 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑦 ∈ ℝ)
111107nnred 11223 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑘 ∈ ℝ)
112110, 111leloed 10368 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦𝑘 ↔ (𝑦 < 𝑘𝑦 = 𝑘)))
113109, 112bitr3d 270 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 < (𝑘 + 1) ↔ (𝑦 < 𝑘𝑦 = 𝑘)))
114 simpll 807 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝜑)
115 ltp1 11049 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ ℝ → 𝑘 < (𝑘 + 1))
116 ltnle 10305 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘))
11792, 116mpdan 705 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ ℝ → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘))
118115, 117mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℝ → ¬ (𝑘 + 1) ≤ 𝑘)
119111, 118syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → ¬ (𝑘 + 1) ≤ 𝑘)
120 breq2 4804 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = 𝑘 → ((𝑘 + 1) ≤ 𝑚 ↔ (𝑘 + 1) ≤ 𝑘))
121120rspccv 3442 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑘𝑊 → (𝑘 + 1) ≤ 𝑘))
122121ad2antll 767 . . . . . . . . . . . . . . . . . . . . . 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 23482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ ¬ 𝑘𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵)
134114, 107, 123, 133syl12anc 1475 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵)
135134iftrued 4234 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))), 𝐵) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))
13629ad2antrr 764 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐾:ℕ⟶𝑇)
137136, 107ffvelrnd 6519 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾𝑘) ∈ 𝑇)
138131ralrimiva 3100 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
139138ad2antrr 764 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
140 fveq2 6348 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = (𝐾𝑘) → (𝐺𝑡) = (𝐺‘(𝐾𝑘)))
141140fveq2d 6352 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = (𝐾𝑘) → (𝐹‘(𝐺𝑡)) = (𝐹‘(𝐺‘(𝐾𝑘))))
142141fveq2d 6352 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = (𝐾𝑘) → (2nd ‘(𝐹‘(𝐺𝑡))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))))
143142breq1d 4810 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = (𝐾𝑘) → ((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵))
144143, 142ifbieq1d 4249 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = (𝐾𝑘) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) = if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))), 𝐵))
145 fveq2 6348 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = (𝐾𝑘) → (𝐻𝑡) = (𝐻‘(𝐾𝑘)))
146144, 145eleq12d 2829 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = (𝐾𝑘) → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡) ↔ if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))), 𝐵) ∈ (𝐻‘(𝐾𝑘))))
147146rspcv 3441 . . . . . . . . . . . . . . . . . . . 20 ((𝐾𝑘) ∈ 𝑇 → (∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))), 𝐵) ∈ (𝐻‘(𝐾𝑘))))
148137, 139, 147sylc 65 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))), 𝐵) ∈ (𝐻‘(𝐾𝑘)))
149135, 148eqeltrrd 2836 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ (𝐻‘(𝐾𝑘)))
15024, 25, 26, 27, 28algrp1 15485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐾‘(𝑘 + 1)) = (𝐻‘(𝐾𝑘)))
151150ad2ant2r 800 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾‘(𝑘 + 1)) = (𝐻‘(𝐾𝑘)))
152149, 151eleqtrrd 2838 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ (𝐾‘(𝑘 + 1)))
153136, 33, 34sylancl 697 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐾:ℕ⟶𝑈)
154107peano2nnd 11225 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑘 + 1) ∈ ℕ)
155153, 154ffvelrnd 6519 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾‘(𝑘 + 1)) ∈ 𝑈)
156124, 125, 126, 127, 17, 128, 129, 22, 130ovolicc2lem1 23481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐾‘(𝑘 + 1)) ∈ 𝑈) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ (𝐾‘(𝑘 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))
157114, 155, 156syl2anc 696 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ (𝐾‘(𝑘 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))
158152, 157mpbid 222 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))
159158simp3d 1139 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))
16041adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) ∈ ℝ)
16120ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐹:ℕ⟶(ℝ × ℝ))
16222ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐺:𝑈⟶ℕ)
163153, 107ffvelrnd 6519 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾𝑘) ∈ 𝑈)
164162, 163ffvelrnd 6519 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐺‘(𝐾𝑘)) ∈ ℕ)
165161, 164ffvelrnd 6519 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐹‘(𝐺‘(𝐾𝑘))) ∈ (ℝ × ℝ))
166 xp2nd 7362 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝐺‘(𝐾𝑘))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ ℝ)
167165, 166syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ ℝ)
168162, 155ffvelrnd 6519 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐺‘(𝐾‘(𝑘 + 1))) ∈ ℕ)
169161, 168ffvelrnd 6519 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))) ∈ (ℝ × ℝ))
170 xp2nd 7362 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ∈ ℝ)
171169, 170syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ∈ ℝ)
172 lttr 10302 . . . . . . . . . . . . . . . 16 (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) ∈ ℝ ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∈ ℝ ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ∈ ℝ) → (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))
173160, 167, 171, 172syl3anc 1477 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚𝑊 (𝑘 + 1) ≤ 𝑚)) → (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))
174159, 173mpan2d 712 . . . . . . . . . . . . . 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 4810 . . . . . . . . . . . . . 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 644 . . . . . . . 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 11226 . . 3 (𝑘 ∈ ℕ → ((𝜑𝑦 ∈ ℕ) → (∀𝑚𝑊 𝑘𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))))))
18944, 46, 51, 188syl3c 66 . 2 ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑘))))))
1904, 8, 12, 15, 42, 189eqord1 10744 1 ((𝜑 ∧ (𝑁 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑃 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → (𝑁 = 𝑃 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑁)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑃))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1628  wcel 2135  wne 2928  wral 3046  {crab 3050  cin 3710  wss 3711  c0 4054  ifcif 4226  𝒫 cpw 4298  {csn 4317   cuni 4584   class class class wbr 4800   × cxp 5260  ran crn 5263  ccom 5266  wf 6041  cfv 6045  (class class class)co 6809  1st c1st 7327  2nd c2nd 7328  Fincfn 8117  cr 10123  1c1 10125   + caddc 10127   < clt 10262  cle 10263  cmin 10454  cn 11208  (,)cioo 12364  [,]cicc 12367  seqcseq 12991  abscabs 14169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-cnex 10180  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-mulcom 10188  ax-addass 10189  ax-mulass 10190  ax-distr 10191  ax-i2m1 10192  ax-1ne0 10193  ax-1rid 10194  ax-rnegex 10195  ax-rrecex 10196  ax-cnre 10197  ax-pre-lttri 10198  ax-pre-lttrn 10199  ax-pre-ltadd 10200  ax-pre-mulgt0 10201
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-reu 3053  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-1st 7329  df-2nd 7330  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-er 7907  df-en 8118  df-dom 8119  df-sdom 8120  df-pnf 10264  df-mnf 10265  df-xr 10266  df-ltxr 10267  df-le 10268  df-sub 10456  df-neg 10457  df-nn 11209  df-n0 11481  df-z 11566  df-uz 11876  df-ioo 12368  df-icc 12371  df-fz 12516  df-seq 12992
This theorem is referenced by:  ovolicc2lem4  23484
  Copyright terms: Public domain W3C validator