Step | Hyp | Ref
| Expression |
1 | | 2fveq3 6776 |
. . . 4
⊢ (𝑦 = 𝑘 → (𝐺‘(𝐾‘𝑦)) = (𝐺‘(𝐾‘𝑘))) |
2 | 1 | fveq2d 6775 |
. . 3
⊢ (𝑦 = 𝑘 → (𝐹‘(𝐺‘(𝐾‘𝑦))) = (𝐹‘(𝐺‘(𝐾‘𝑘)))) |
3 | 2 | fveq2d 6775 |
. 2
⊢ (𝑦 = 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) |
4 | | 2fveq3 6776 |
. . . 4
⊢ (𝑦 = 𝑁 → (𝐺‘(𝐾‘𝑦)) = (𝐺‘(𝐾‘𝑁))) |
5 | 4 | fveq2d 6775 |
. . 3
⊢ (𝑦 = 𝑁 → (𝐹‘(𝐺‘(𝐾‘𝑦))) = (𝐹‘(𝐺‘(𝐾‘𝑁)))) |
6 | 5 | fveq2d 6775 |
. 2
⊢ (𝑦 = 𝑁 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁))))) |
7 | | 2fveq3 6776 |
. . . 4
⊢ (𝑦 = 𝑃 → (𝐺‘(𝐾‘𝑦)) = (𝐺‘(𝐾‘𝑃))) |
8 | 7 | fveq2d 6775 |
. . 3
⊢ (𝑦 = 𝑃 → (𝐹‘(𝐺‘(𝐾‘𝑦))) = (𝐹‘(𝐺‘(𝐾‘𝑃)))) |
9 | 8 | fveq2d 6775 |
. 2
⊢ (𝑦 = 𝑃 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑃))))) |
10 | | ssrab2 4018 |
. . 3
⊢ {𝑛 ∈ ℕ ∣
∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ⊆ ℕ |
11 | | nnssre 11977 |
. . 3
⊢ ℕ
⊆ ℝ |
12 | 10, 11 | sstri 3935 |
. 2
⊢ {𝑛 ∈ ℕ ∣
∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ⊆ ℝ |
13 | 10 | sseli 3922 |
. . 3
⊢ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} → 𝑦 ∈ ℕ) |
14 | | ovolicc2.5 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
15 | | inss2 4169 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
16 | | fss 6615 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
17 | 14, 15, 16 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
18 | 17 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
19 | | ovolicc2.8 |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝑈⟶ℕ) |
20 | 19 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → 𝐺:𝑈⟶ℕ) |
21 | | nnuz 12620 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
22 | | ovolicc2.15 |
. . . . . . . . . 10
⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ ×
{𝐶})) |
23 | | 1zzd 12351 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℤ) |
24 | | ovolicc2.14 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ 𝑇) |
25 | | ovolicc2.11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻:𝑇⟶𝑇) |
26 | 21, 22, 23, 24, 25 | algrf 16276 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾:ℕ⟶𝑇) |
27 | 26 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → 𝐾:ℕ⟶𝑇) |
28 | | ovolicc2.10 |
. . . . . . . . 9
⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} |
29 | 28 | ssrab3 4020 |
. . . . . . . 8
⊢ 𝑇 ⊆ 𝑈 |
30 | | fss 6615 |
. . . . . . . 8
⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑇 ⊆ 𝑈) → 𝐾:ℕ⟶𝑈) |
31 | 27, 29, 30 | sylancl 586 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → 𝐾:ℕ⟶𝑈) |
32 | | ffvelrn 6956 |
. . . . . . 7
⊢ ((𝐾:ℕ⟶𝑈 ∧ 𝑦 ∈ ℕ) → (𝐾‘𝑦) ∈ 𝑈) |
33 | 31, 32 | sylancom 588 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (𝐾‘𝑦) ∈ 𝑈) |
34 | 20, 33 | ffvelrnd 6959 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (𝐺‘(𝐾‘𝑦)) ∈ ℕ) |
35 | 18, 34 | ffvelrnd 6959 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘𝑦))) ∈ (ℝ ×
ℝ)) |
36 | | xp2nd 7857 |
. . . 4
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑦))) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) ∈ ℝ) |
37 | 35, 36 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) ∈ ℝ) |
38 | 13, 37 | sylan2 593 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) ∈ ℝ) |
39 | 10 | sseli 3922 |
. . . 4
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} → 𝑘 ∈ ℕ) |
40 | 39 | ad2antll 726 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → 𝑘 ∈ ℕ) |
41 | 13 | anim2i 617 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) → (𝜑 ∧ 𝑦 ∈ ℕ)) |
42 | 41 | adantrr 714 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝜑 ∧ 𝑦 ∈ ℕ)) |
43 | | breq1 5082 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑛 ≤ 𝑚 ↔ 𝑘 ≤ 𝑚)) |
44 | 43 | ralbidv 3123 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 ↔ ∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚)) |
45 | 44 | elrab 3626 |
. . . . 5
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ↔ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚)) |
46 | 45 | simprbi 497 |
. . . 4
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} → ∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚) |
47 | 46 | ad2antll 726 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → ∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚) |
48 | | breq1 5082 |
. . . . . . 7
⊢ (𝑥 = 1 → (𝑥 ≤ 𝑚 ↔ 1 ≤ 𝑚)) |
49 | 48 | ralbidv 3123 |
. . . . . 6
⊢ (𝑥 = 1 → (∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 ↔ ∀𝑚 ∈ 𝑊 1 ≤ 𝑚)) |
50 | | breq2 5083 |
. . . . . . 7
⊢ (𝑥 = 1 → (𝑦 < 𝑥 ↔ 𝑦 < 1)) |
51 | | 2fveq3 6776 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (𝐺‘(𝐾‘𝑥)) = (𝐺‘(𝐾‘1))) |
52 | 51 | fveq2d 6775 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (𝐹‘(𝐺‘(𝐾‘𝑥))) = (𝐹‘(𝐺‘(𝐾‘1)))) |
53 | 52 | fveq2d 6775 |
. . . . . . . 8
⊢ (𝑥 = 1 → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑥)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘1))))) |
54 | 53 | breq2d 5091 |
. . . . . . 7
⊢ (𝑥 = 1 → ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))) ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1)))))) |
55 | 50, 54 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = 1 → ((𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥))))) ↔ (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1))))))) |
56 | 49, 55 | imbi12d 345 |
. . . . 5
⊢ (𝑥 = 1 → ((∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))))) ↔ (∀𝑚 ∈ 𝑊 1 ≤ 𝑚 → (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1)))))))) |
57 | 56 | imbi2d 341 |
. . . 4
⊢ (𝑥 = 1 → (((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥))))))) ↔ ((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 1 ≤ 𝑚 → (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1))))))))) |
58 | | breq1 5082 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑥 ≤ 𝑚 ↔ 𝑘 ≤ 𝑚)) |
59 | 58 | ralbidv 3123 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 ↔ ∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚)) |
60 | | breq2 5083 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑦 < 𝑥 ↔ 𝑦 < 𝑘)) |
61 | | 2fveq3 6776 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑘 → (𝐺‘(𝐾‘𝑥)) = (𝐺‘(𝐾‘𝑘))) |
62 | 61 | fveq2d 6775 |
. . . . . . . . 9
⊢ (𝑥 = 𝑘 → (𝐹‘(𝐺‘(𝐾‘𝑥))) = (𝐹‘(𝐺‘(𝐾‘𝑘)))) |
63 | 62 | fveq2d 6775 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) |
64 | 63 | breq2d 5091 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))) ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))) |
65 | 60, 64 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥))))) ↔ (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))))) |
66 | 59, 65 | imbi12d 345 |
. . . . 5
⊢ (𝑥 = 𝑘 → ((∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))))) ↔ (∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))))) |
67 | 66 | imbi2d 341 |
. . . 4
⊢ (𝑥 = 𝑘 → (((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥))))))) ↔ ((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))))))) |
68 | | breq1 5082 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (𝑥 ≤ 𝑚 ↔ (𝑘 + 1) ≤ 𝑚)) |
69 | 68 | ralbidv 3123 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → (∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 ↔ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) |
70 | | breq2 5083 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (𝑦 < 𝑥 ↔ 𝑦 < (𝑘 + 1))) |
71 | | 2fveq3 6776 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑘 + 1) → (𝐺‘(𝐾‘𝑥)) = (𝐺‘(𝐾‘(𝑘 + 1)))) |
72 | 71 | fveq2d 6775 |
. . . . . . . . 9
⊢ (𝑥 = (𝑘 + 1) → (𝐹‘(𝐺‘(𝐾‘𝑥))) = (𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) |
73 | 72 | fveq2d 6775 |
. . . . . . . 8
⊢ (𝑥 = (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))) |
74 | 73 | breq2d 5091 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))) ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))) |
75 | 70, 74 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → ((𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥))))) ↔ (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
76 | 69, 75 | imbi12d 345 |
. . . . 5
⊢ (𝑥 = (𝑘 + 1) → ((∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥)))))) ↔ (∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))))) |
77 | 76 | imbi2d 341 |
. . . 4
⊢ (𝑥 = (𝑘 + 1) → (((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → (𝑦 < 𝑥 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑥))))))) ↔ ((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))))) |
78 | | nnnlt1 12005 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → ¬
𝑦 < 1) |
79 | 78 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → ¬ 𝑦 < 1) |
80 | 79 | pm2.21d 121 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1)))))) |
81 | 80 | a1d 25 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 1 ≤ 𝑚 → (𝑦 < 1 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘1))))))) |
82 | | nnre 11980 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
83 | 82 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊) → 𝑘 ∈ ℝ) |
84 | 83 | lep1d 11906 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊) → 𝑘 ≤ (𝑘 + 1)) |
85 | | peano2re 11148 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) |
86 | 83, 85 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊) → (𝑘 + 1) ∈ ℝ) |
87 | | ovolicc2.16 |
. . . . . . . . . . . . . 14
⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} |
88 | 87 | ssrab3 4020 |
. . . . . . . . . . . . 13
⊢ 𝑊 ⊆
ℕ |
89 | 88, 11 | sstri 3935 |
. . . . . . . . . . . 12
⊢ 𝑊 ⊆
ℝ |
90 | 89 | sseli 3922 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ 𝑊 → 𝑚 ∈ ℝ) |
91 | 90 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊) → 𝑚 ∈ ℝ) |
92 | | letr 11069 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑚) → 𝑘 ≤ 𝑚)) |
93 | 83, 86, 91, 92 | syl3anc 1370 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑚) → 𝑘 ≤ 𝑚)) |
94 | 84, 93 | mpand 692 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊) → ((𝑘 + 1) ≤ 𝑚 → 𝑘 ≤ 𝑚)) |
95 | 94 | ralimdva 3105 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ →
(∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → ∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚)) |
96 | 95 | imim1d 82 |
. . . . . 6
⊢ (𝑘 ∈ ℕ →
((∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))) → (∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))))) |
97 | 96 | adantl 482 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))) → (∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))))) |
98 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑦 ∈ ℕ) |
99 | | simprl 768 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑘 ∈ ℕ) |
100 | | nnleltp1 12375 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑦 ≤ 𝑘 ↔ 𝑦 < (𝑘 + 1))) |
101 | 98, 99, 100 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 ≤ 𝑘 ↔ 𝑦 < (𝑘 + 1))) |
102 | 98 | nnred 11988 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑦 ∈ ℝ) |
103 | 99 | nnred 11988 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝑘 ∈ ℝ) |
104 | 102, 103 | leloed 11118 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 ≤ 𝑘 ↔ (𝑦 < 𝑘 ∨ 𝑦 = 𝑘))) |
105 | 101, 104 | bitr3d 280 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 < (𝑘 + 1) ↔ (𝑦 < 𝑘 ∨ 𝑦 = 𝑘))) |
106 | | simpll 764 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝜑) |
107 | | ltp1 11815 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℝ → 𝑘 < (𝑘 + 1)) |
108 | | ltnle 11055 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) →
(𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘)) |
109 | 85, 108 | mpdan 684 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℝ → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘)) |
110 | 107, 109 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℝ → ¬
(𝑘 + 1) ≤ 𝑘) |
111 | 103, 110 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ¬ (𝑘 + 1) ≤ 𝑘) |
112 | | breq2 5083 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑘 → ((𝑘 + 1) ≤ 𝑚 ↔ (𝑘 + 1) ≤ 𝑘)) |
113 | 112 | rspccv 3558 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑚 ∈
𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑘 ∈ 𝑊 → (𝑘 + 1) ≤ 𝑘)) |
114 | 113 | ad2antll 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑘 ∈ 𝑊 → (𝑘 + 1) ≤ 𝑘)) |
115 | 111, 114 | mtod 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
⊢ (𝜑 → 𝐴 ∈ 𝐶) |
125 | 116, 117,
118, 119, 14, 120, 121, 19, 122, 28, 25, 123, 124, 24, 22, 87 | ovolicc2lem2 24680 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵) |
126 | 106, 99, 115, 125 | syl12anc 834 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵) |
127 | 126 | iftrued 4473 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))), 𝐵) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) |
128 | | 2fveq3 6776 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = (𝐾‘𝑘) → (𝐹‘(𝐺‘𝑡)) = (𝐹‘(𝐺‘(𝐾‘𝑘)))) |
129 | 128 | fveq2d 6775 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = (𝐾‘𝑘) → (2nd ‘(𝐹‘(𝐺‘𝑡))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) |
130 | 129 | breq1d 5089 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (𝐾‘𝑘) → ((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵)) |
131 | 130, 129 | ifbieq1d 4489 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (𝐾‘𝑘) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) = if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))), 𝐵)) |
132 | | fveq2 6771 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (𝐾‘𝑘) → (𝐻‘𝑡) = (𝐻‘(𝐾‘𝑘))) |
133 | 131, 132 | eleq12d 2835 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (𝐾‘𝑘) → (if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡) ↔ if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑘)))) |
134 | 123 | ralrimiva 3110 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) |
135 | 134 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) |
136 | 26 | ad2antrr 723 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐾:ℕ⟶𝑇) |
137 | 136, 99 | ffvelrnd 6959 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾‘𝑘) ∈ 𝑇) |
138 | 133, 135,
137 | rspcdva 3563 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑘))) |
139 | 127, 138 | eqeltrrd 2842 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ (𝐻‘(𝐾‘𝑘))) |
140 | 21, 22, 23, 24, 25 | algrp1 16277 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐾‘(𝑘 + 1)) = (𝐻‘(𝐾‘𝑘))) |
141 | 140 | ad2ant2r 744 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾‘(𝑘 + 1)) = (𝐻‘(𝐾‘𝑘))) |
142 | 139, 141 | eleqtrrd 2844 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ (𝐾‘(𝑘 + 1))) |
143 | 136, 29, 30 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐾:ℕ⟶𝑈) |
144 | 99 | peano2nnd 11990 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑘 + 1) ∈ ℕ) |
145 | 143, 144 | ffvelrnd 6959 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾‘(𝑘 + 1)) ∈ 𝑈) |
146 | 116, 117,
118, 119, 14, 120, 121, 19, 122 | ovolicc2lem1 24679 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐾‘(𝑘 + 1)) ∈ 𝑈) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ (𝐾‘(𝑘 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
147 | 106, 145,
146 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ (𝐾‘(𝑘 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
148 | 142, 147 | mpbid 231 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))) |
149 | 148 | simp3d 1143 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))) |
150 | 37 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) ∈ ℝ) |
151 | 17 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
152 | 19 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → 𝐺:𝑈⟶ℕ) |
153 | 143, 99 | ffvelrnd 6959 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐾‘𝑘) ∈ 𝑈) |
154 | 152, 153 | ffvelrnd 6959 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐺‘(𝐾‘𝑘)) ∈ ℕ) |
155 | 151, 154 | ffvelrnd 6959 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐹‘(𝐺‘(𝐾‘𝑘))) ∈ (ℝ ×
ℝ)) |
156 | | xp2nd 7857 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑘))) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ ℝ) |
157 | 155, 156 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ ℝ) |
158 | 152, 145 | ffvelrnd 6959 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐺‘(𝐾‘(𝑘 + 1))) ∈ ℕ) |
159 | 151, 158 | ffvelrnd 6959 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))) ∈ (ℝ ×
ℝ)) |
160 | | xp2nd 7857 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))) ∈ (ℝ × ℝ)
→ (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ∈ ℝ) |
161 | 159, 160 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ∈ ℝ) |
162 | | lttr 11052 |
. . . . . . . . . . . 12
⊢
(((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) ∈ ℝ ∧ (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∈ ℝ ∧ (2nd
‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ∈ ℝ) →
(((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))) |
163 | 150, 157,
161, 162 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))) |
164 | 149, 163 | mpan2d 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))) |
165 | 164 | imim2d 57 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
166 | 165 | com23 86 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 < 𝑘 → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
167 | 3 | breq1d 5089 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑘 → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))) ↔ (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑘)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))) |
168 | 149, 167 | syl5ibrcom 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 = 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1))))))) |
169 | 168 | a1dd 50 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 = 𝑘 → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
170 | 166, 169 | jaod 856 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ((𝑦 < 𝑘 ∨ 𝑦 = 𝑘) → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
171 | 105, 170 | sylbid 239 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → (𝑦 < (𝑘 + 1) → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
172 | 171 | com23 86 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚)) → ((𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))) → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))) |
173 | 97, 172 | animpimp2impd 843 |
. . . 4
⊢ (𝑘 ∈ ℕ → (((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘))))))) → ((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 (𝑘 + 1) ≤ 𝑚 → (𝑦 < (𝑘 + 1) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑘 + 1)))))))))) |
174 | 57, 67, 77, 67, 81, 173 | nnind 11991 |
. . 3
⊢ (𝑘 ∈ ℕ → ((𝜑 ∧ 𝑦 ∈ ℕ) → (∀𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))))) |
175 | 40, 42, 47, 174 | syl3c 66 |
. 2
⊢ ((𝜑 ∧ (𝑦 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑦 < 𝑘 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑦)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑘)))))) |
176 | 3, 6, 9, 12, 38, 175 | eqord1 11503 |
1
⊢ ((𝜑 ∧ (𝑁 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑃 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑁 = 𝑃 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑃)))))) |