Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . 5
⊢ (𝑦 = 𝑘 → (𝐾‘𝑦) = (𝐾‘𝑘)) |
2 | 1 | fveq2d 6195 |
. . . 4
⊢ (𝑦 = 𝑘 → (𝐺‘(𝐾‘𝑦)) = (𝐺‘(𝐾‘𝑘))) |
3 | 2 | fveq2d 6195 |
. . 3
⊢ (𝑦 = 𝑘 → (𝐹‘(𝐺‘(𝐾‘𝑦))) = (𝐹‘(𝐺‘(𝐾‘𝑘)))) |
4 | 3 | fveq2d 6195 |
. 2
⊢ (𝑦 = 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) |
5 | | fveq2 6191 |
. . . . 5
⊢ (𝑦 = 𝑁 → (𝐾‘𝑦) = (𝐾‘𝑁)) |
6 | 5 | fveq2d 6195 |
. . . 4
⊢ (𝑦 = 𝑁 → (𝐺‘(𝐾‘𝑦)) = (𝐺‘(𝐾‘𝑁))) |
7 | 6 | fveq2d 6195 |
. . 3
⊢ (𝑦 = 𝑁 → (𝐹‘(𝐺‘(𝐾‘𝑦))) = (𝐹‘(𝐺‘(𝐾‘𝑁)))) |
8 | 7 | fveq2d 6195 |
. 2
⊢ (𝑦 = 𝑁 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁))))) |
9 | | fveq2 6191 |
. . . . 5
⊢ (𝑦 = 𝑃 → (𝐾‘𝑦) = (𝐾‘𝑃)) |
10 | 9 | fveq2d 6195 |
. . . 4
⊢ (𝑦 = 𝑃 → (𝐺‘(𝐾‘𝑦)) = (𝐺‘(𝐾‘𝑃))) |
11 | 10 | fveq2d 6195 |
. . 3
⊢ (𝑦 = 𝑃 → (𝐹‘(𝐺‘(𝐾‘𝑦))) = (𝐹‘(𝐺‘(𝐾‘𝑃)))) |
12 | 11 | fveq2d 6195 |
. 2
⊢ (𝑦 = 𝑃 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑃))))) |
13 | | ssrab2 3687 |
. . 3
⊢ {𝑛 ∈ ℕ ∣
∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ⊆ ℕ |
14 | | nnssre 11024 |
. . 3
⊢ ℕ
⊆ ℝ |
15 | 13, 14 | sstri 3612 |
. 2
⊢ {𝑛 ∈ ℕ ∣
∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ⊆ ℝ |
16 | 13 | sseli 3599 |
. . 3
⊢ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} → 𝑦 ∈ ℕ) |
17 | | ovolicc2.5 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
18 | | inss2 3834 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
19 | | fss 6056 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
20 | 17, 18, 19 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
21 | 20 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
22 | | ovolicc2.8 |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝑈⟶ℕ) |
23 | 22 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → 𝐺:𝑈⟶ℕ) |
24 | | nnuz 11723 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
25 | | ovolicc2.15 |
. . . . . . . . . 10
⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ ×
{𝐶})) |
26 | | 1zzd 11408 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℤ) |
27 | | ovolicc2.14 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ 𝑇) |
28 | | ovolicc2.11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻:𝑇⟶𝑇) |
29 | 24, 25, 26, 27, 28 | algrf 15286 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾:ℕ⟶𝑇) |
30 | 29 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → 𝐾:ℕ⟶𝑇) |
31 | | ovolicc2.10 |
. . . . . . . . 9
⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} |
32 | | ssrab2 3687 |
. . . . . . . . 9
⊢ {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⊆ 𝑈 |
33 | 31, 32 | eqsstri 3635 |
. . . . . . . 8
⊢ 𝑇 ⊆ 𝑈 |
34 | | fss 6056 |
. . . . . . . 8
⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑇 ⊆ 𝑈) → 𝐾:ℕ⟶𝑈) |
35 | 30, 33, 34 | sylancl 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → 𝐾:ℕ⟶𝑈) |
36 | | ffvelrn 6357 |
. . . . . . 7
⊢ ((𝐾:ℕ⟶𝑈 ∧ 𝑦 ∈ ℕ) → (𝐾‘𝑦) ∈ 𝑈) |
37 | 35, 36 | sylancom 701 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (𝐾‘𝑦) ∈ 𝑈) |
38 | 23, 37 | ffvelrnd 6360 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (𝐺‘(𝐾‘𝑦)) ∈ ℕ) |
39 | 21, 38 | ffvelrnd 6360 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘𝑦))) ∈ (ℝ ×
ℝ)) |
40 | | xp2nd 7199 |
. . . 4
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑦))) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) ∈ ℝ) |
41 | 39, 40 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) ∈ ℝ) |
42 | 16, 41 | sylan2 491 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) ∈ ℝ) |
43 | 13 | sseli 3599 |
. . . 4
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} → 𝑘 ∈ ℕ) |
44 | 43 | ad2antll 765 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → 𝑘 ∈ ℕ) |
45 | 16 | anim2i 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) → (𝜑 ∧ 𝑦 ∈ ℕ)) |
46 | 45 | adantrr 753 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝜑 ∧ 𝑦 ∈ ℕ)) |
47 | | breq1 4656 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑛 ≤ 𝑚 ↔ 𝑘 ≤ 𝑚)) |
48 | 47 | ralbidv 2986 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 ↔ ∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚)) |
49 | 48 | elrab 3363 |
. . . . 5
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ↔ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚)) |
50 | 49 | simprbi 480 |
. . . 4
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} → ∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚) |
51 | 50 | ad2antll 765 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → ∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚) |
52 | | breq1 4656 |
. . . . . . 7
⊢ (𝑥 = 1 → (𝑥 ≤ 𝑚 ↔ 1 ≤ 𝑚)) |
53 | 52 | ralbidv 2986 |
. . . . . 6
⊢ (𝑥 = 1 → (∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 ↔ ∀𝑚 ∈ 𝑊 1 ≤ 𝑚)) |
54 | | breq2 4657 |
. . . . . . 7
⊢ (𝑥 = 1 → (𝑦 < 𝑥 ↔ 𝑦 < 1)) |
55 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝐾‘𝑥) = (𝐾‘1)) |
56 | 55 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (𝐺‘(𝐾‘𝑥)) = (𝐺‘(𝐾‘1))) |
57 | 56 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (𝐹‘(𝐺‘(𝐾‘𝑥))) = (𝐹‘(𝐺‘(𝐾‘1)))) |
58 | 57 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = 1 → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑥)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘1))))) |
59 | 58 | breq2d 4665 |
. . . . . . 7
⊢ (𝑥 = 1 → ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))) ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1)))))) |
60 | 54, 59 | imbi12d 334 |
. . . . . 6
⊢ (𝑥 = 1 → ((𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥))))) ↔ (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1))))))) |
61 | 53, 60 | imbi12d 334 |
. . . . 5
⊢ (𝑥 = 1 → ((∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))))) ↔ (∀𝑚 ∈ 𝑊 1 ≤ 𝑚 → (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1)))))))) |
62 | 61 | imbi2d 330 |
. . . 4
⊢ (𝑥 = 1 → (((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥))))))) ↔ ((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 1 ≤ 𝑚 → (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1))))))))) |
63 | | breq1 4656 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑥 ≤ 𝑚 ↔ 𝑘 ≤ 𝑚)) |
64 | 63 | ralbidv 2986 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 ↔ ∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚)) |
65 | | breq2 4657 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑦 < 𝑥 ↔ 𝑦 < 𝑘)) |
66 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → (𝐾‘𝑥) = (𝐾‘𝑘)) |
67 | 66 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑘 → (𝐺‘(𝐾‘𝑥)) = (𝐺‘(𝐾‘𝑘))) |
68 | 67 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = 𝑘 → (𝐹‘(𝐺‘(𝐾‘𝑥))) = (𝐹‘(𝐺‘(𝐾‘𝑘)))) |
69 | 68 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) |
70 | 69 | breq2d 4665 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))) ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))) |
71 | 65, 70 | imbi12d 334 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥))))) ↔ (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))))) |
72 | 64, 71 | imbi12d 334 |
. . . . 5
⊢ (𝑥 = 𝑘 → ((∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))))) ↔ (∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))))) |
73 | 72 | imbi2d 330 |
. . . 4
⊢ (𝑥 = 𝑘 → (((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥))))))) ↔ ((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))))))) |
74 | | breq1 4656 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (𝑥 ≤ 𝑚 ↔ (𝑘 + 1) ≤ 𝑚)) |
75 | 74 | ralbidv 2986 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → (∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 ↔ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) |
76 | | breq2 4657 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (𝑦 < 𝑥 ↔ 𝑦 < (𝑘 + 1))) |
77 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑘 + 1) → (𝐾‘𝑥) = (𝐾‘(𝑘 + 1))) |
78 | 77 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑘 + 1) → (𝐺‘(𝐾‘𝑥)) = (𝐺‘(𝐾‘(𝑘 + 1)))) |
79 | 78 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = (𝑘 + 1) → (𝐹‘(𝐺‘(𝐾‘𝑥))) = (𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) |
80 | 79 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))) |
81 | 80 | breq2d 4665 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))) ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))) |
82 | 76, 81 | imbi12d 334 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → ((𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥))))) ↔ (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
83 | 75, 82 | imbi12d 334 |
. . . . 5
⊢ (𝑥 = (𝑘 + 1) → ((∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))))) ↔ (∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))) |
84 | 83 | imbi2d 330 |
. . . 4
⊢ (𝑥 = (𝑘 + 1) → (((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥))))))) ↔ ((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))))) |
85 | | nnnlt1 11050 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → ¬
𝑦 < 1) |
86 | 85 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → ¬ 𝑦 < 1) |
87 | 86 | pm2.21d 118 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1)))))) |
88 | 87 | a1d 25 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 1 ≤ 𝑚 → (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1))))))) |
89 | | nnre 11027 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
90 | 89 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊) → 𝑘 ∈ ℝ) |
91 | 90 | lep1d 10955 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊) → 𝑘 ≤ (𝑘 + 1)) |
92 | | peano2re 10209 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) |
93 | 90, 92 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊) → (𝑘 + 1) ∈ ℝ) |
94 | | ovolicc2.16 |
. . . . . . . . . . . . . . . 16
⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} |
95 | | ssrab2 3687 |
. . . . . . . . . . . . . . . 16
⊢ {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} ⊆ ℕ |
96 | 94, 95 | eqsstri 3635 |
. . . . . . . . . . . . . . 15
⊢ 𝑊 ⊆
ℕ |
97 | 96, 14 | sstri 3612 |
. . . . . . . . . . . . . 14
⊢ 𝑊 ⊆
ℝ |
98 | 97 | sseli 3599 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ 𝑊 → 𝑚 ∈ ℝ) |
99 | 98 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊) → 𝑚 ∈ ℝ) |
100 | | letr 10131 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑚) → 𝑘 ≤ 𝑚)) |
101 | 90, 93, 99, 100 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑚) → 𝑘 ≤ 𝑚)) |
102 | 91, 101 | mpand 711 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊) → ((𝑘 + 1) ≤ 𝑚 → 𝑘 ≤ 𝑚)) |
103 | 102 | ralimdva 2962 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ →
(∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → ∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚)) |
104 | 103 | imim1d 82 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ →
((∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))) → (∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))))) |
105 | 104 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))) → (∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))))) |
106 | | simplr 792 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑦 ∈ ℕ) |
107 | | simprl 794 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑘 ∈ ℕ) |
108 | | nnleltp1 11432 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑦 ≤ 𝑘 ↔ 𝑦 < (𝑘 + 1))) |
109 | 106, 107,
108 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 ≤ 𝑘 ↔ 𝑦 < (𝑘 + 1))) |
110 | 106 | nnred 11035 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑦 ∈ ℝ) |
111 | 107 | nnred 11035 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑘 ∈ ℝ) |
112 | 110, 111 | leloed 10180 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 ≤ 𝑘 ↔ (𝑦 < 𝑘 ∨ 𝑦 = 𝑘))) |
113 | 109, 112 | bitr3d 270 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 < (𝑘 + 1) ↔ (𝑦 < 𝑘 ∨ 𝑦 = 𝑘))) |
114 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝜑) |
115 | | ltp1 10861 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ ℝ → 𝑘 < (𝑘 + 1)) |
116 | | ltnle 10117 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) →
(𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘)) |
117 | 92, 116 | mpdan 702 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ ℝ → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘)) |
118 | 115, 117 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℝ → ¬
(𝑘 + 1) ≤ 𝑘) |
119 | 111, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ¬ (𝑘 + 1) ≤ 𝑘) |
120 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = 𝑘 → ((𝑘 + 1) ≤ 𝑚 ↔ (𝑘 + 1) ≤ 𝑘)) |
121 | 120 | rspccv 3306 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑚 ∈
𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑘 ∈ 𝑊 → (𝑘 + 1) ≤ 𝑘)) |
122 | 121 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑘 ∈ 𝑊 → (𝑘 + 1) ≤ 𝑘)) |
123 | 119, 122 | mtod 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
⊢ (𝜑 → 𝐴 ∈ 𝐶) |
133 | 124, 125,
126, 127, 17, 128, 129, 22, 130, 31, 28, 131, 132, 27, 25, 94 | ovolicc2lem2 23286 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵) |
134 | 114, 107,
123, 133 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵) |
135 | 134 | iftrued 4094 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))), 𝐵) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) |
136 | 29 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐾:ℕ⟶𝑇) |
137 | 136, 107 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾‘𝑘) ∈ 𝑇) |
138 | 131 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) |
139 | 138 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) |
140 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = (𝐾‘𝑘) → (𝐺‘𝑡) = (𝐺‘(𝐾‘𝑘))) |
141 | 140 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = (𝐾‘𝑘) → (𝐹‘(𝐺‘𝑡)) = (𝐹‘(𝐺‘(𝐾‘𝑘)))) |
142 | 141 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = (𝐾‘𝑘) → (2nd ‘(𝐹‘(𝐺‘𝑡))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) |
143 | 142 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = (𝐾‘𝑘) → ((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵)) |
144 | 143, 142 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = (𝐾‘𝑘) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) = if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))), 𝐵)) |
145 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = (𝐾‘𝑘) → (𝐻‘𝑡) = (𝐻‘(𝐾‘𝑘))) |
146 | 144, 145 | eleq12d 2695 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = (𝐾‘𝑘) → (if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡) ↔ if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑘)))) |
147 | 146 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾‘𝑘) ∈ 𝑇 → (∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡) → if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑘)))) |
148 | 137, 139,
147 | sylc 65 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑘))) |
149 | 135, 148 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ (𝐻‘(𝐾‘𝑘))) |
150 | 24, 25, 26, 27, 28 | algrp1 15287 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐾‘(𝑘 + 1)) = (𝐻‘(𝐾‘𝑘))) |
151 | 150 | ad2ant2r 783 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾‘(𝑘 + 1)) = (𝐻‘(𝐾‘𝑘))) |
152 | 149, 151 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ (𝐾‘(𝑘 + 1))) |
153 | 136, 33, 34 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐾:ℕ⟶𝑈) |
154 | 107 | peano2nnd 11037 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑘 + 1) ∈ ℕ) |
155 | 153, 154 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾‘(𝑘 + 1)) ∈ 𝑈) |
156 | 124, 125,
126, 127, 17, 128, 129, 22, 130 | ovolicc2lem1 23285 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝐾‘(𝑘 + 1)) ∈ 𝑈) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ (𝐾‘(𝑘 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
157 | 114, 155,
156 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ (𝐾‘(𝑘 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
158 | 152, 157 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))) |
159 | 158 | simp3d 1075 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))) |
160 | 41 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) ∈ ℝ) |
161 | 20 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
162 | 22 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐺:𝑈⟶ℕ) |
163 | 153, 107 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾‘𝑘) ∈ 𝑈) |
164 | 162, 163 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐺‘(𝐾‘𝑘)) ∈ ℕ) |
165 | 161, 164 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐹‘(𝐺‘(𝐾‘𝑘))) ∈ (ℝ ×
ℝ)) |
166 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑘))) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ ℝ) |
167 | 165, 166 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ ℝ) |
168 | 162, 155 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐺‘(𝐾‘(𝑘 + 1))) ∈ ℕ) |
169 | 161, 168 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))) ∈ (ℝ ×
ℝ)) |
170 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))) ∈ (ℝ × ℝ)
→ (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ∈ ℝ) |
171 | 169, 170 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ∈ ℝ) |
172 | | lttr 10114 |
. . . . . . . . . . . . . . . 16
⊢
(((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) ∈ ℝ ∧ (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ ℝ ∧ (2nd
‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ∈ ℝ) →
(((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))) |
173 | 160, 167,
171, 172 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))) |
174 | 159, 173 | mpan2d 710 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))) |
175 | 174 | imim2d 57 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
176 | 175 | com23 86 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 < 𝑘 → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
177 | 4 | breq1d 4663 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑘 → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ↔ (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))) |
178 | 159, 177 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 = 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))) |
179 | 178 | a1dd 50 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 = 𝑘 → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
180 | 176, 179 | jaod 395 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ((𝑦 < 𝑘 ∨ 𝑦 = 𝑘) → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
181 | 113, 180 | sylbid 230 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 < (𝑘 + 1) → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
182 | 181 | com23 86 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
183 | 182 | expr 643 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))) |
184 | 183 | a2d 29 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))) → (∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))) |
185 | 105, 184 | syld 47 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))) → (∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))) |
186 | 185 | expcom 451 |
. . . . 5
⊢ (𝑘 ∈ ℕ → ((𝜑 ∧ 𝑦 ∈ ℕ) → ((∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))) → (∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))))) |
187 | 186 | a2d 29 |
. . . 4
⊢ (𝑘 ∈ ℕ → (((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))))) → ((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))))) |
188 | 62, 73, 84, 73, 88, 187 | nnind 11038 |
. . 3
⊢ (𝑘 ∈ ℕ → ((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))))) |
189 | 44, 46, 51, 188 | syl3c 66 |
. 2
⊢ ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))) |
190 | 4, 8, 12, 15, 42, 189 | eqord1 10556 |
1
⊢ ((𝜑 ∧ (𝑁 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑃 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑁 = 𝑃 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑃)))))) |