Step | Hyp | Ref
| Expression |
1 | | ovolicc.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
2 | 1 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝐵 ∈ ℝ) |
3 | | ovolicc2.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
4 | | inss2 4118 |
. . . . . . . . 9
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
5 | | fss 6515 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
6 | 3, 4, 5 | sylancl 589 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
7 | 6 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
8 | | ovolicc2.8 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝑈⟶ℕ) |
9 | 8 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝐺:𝑈⟶ℕ) |
10 | | nnuz 12356 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
11 | | ovolicc2.15 |
. . . . . . . . . . . 12
⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ ×
{𝐶})) |
12 | | 1zzd 12087 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℤ) |
13 | | ovolicc2.14 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ 𝑇) |
14 | | ovolicc2.11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻:𝑇⟶𝑇) |
15 | 10, 11, 12, 13, 14 | algrf 16007 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾:ℕ⟶𝑇) |
16 | 15 | ffvelrnda 6855 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝐾‘𝑁) ∈ 𝑇) |
17 | | ineq1 4094 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝐾‘𝑁) → (𝑢 ∩ (𝐴[,]𝐵)) = ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) |
18 | 17 | neeq1d 2993 |
. . . . . . . . . . 11
⊢ (𝑢 = (𝐾‘𝑁) → ((𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅ ↔ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵)) ≠ ∅)) |
19 | | ovolicc2.10 |
. . . . . . . . . . 11
⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} |
20 | 18, 19 | elrab2 3588 |
. . . . . . . . . 10
⊢ ((𝐾‘𝑁) ∈ 𝑇 ↔ ((𝐾‘𝑁) ∈ 𝑈 ∧ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵)) ≠ ∅)) |
21 | 16, 20 | sylib 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → ((𝐾‘𝑁) ∈ 𝑈 ∧ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵)) ≠ ∅)) |
22 | 21 | simpld 498 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝐾‘𝑁) ∈ 𝑈) |
23 | 9, 22 | ffvelrnd 6856 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝐺‘(𝐾‘𝑁)) ∈ ℕ) |
24 | 7, 23 | ffvelrnd 6856 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘𝑁))) ∈ (ℝ ×
ℝ)) |
25 | | xp2nd 7740 |
. . . . . 6
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑁))) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ∈ ℝ) |
26 | 24, 25 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ∈ ℝ) |
27 | 2, 26 | ltnled 10858 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ↔ ¬ (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ≤ 𝐵)) |
28 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) → 𝑁 ∈ ℕ) |
29 | 1 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) → 𝐵 ∈ ℝ) |
30 | 21 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) → ((𝐾‘𝑁) ∈ 𝑈 ∧ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵)) ≠ ∅)) |
31 | 30 | simprd 499 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) → ((𝐾‘𝑁) ∩ (𝐴[,]𝐵)) ≠ ∅) |
32 | | n0 4233 |
. . . . . . . . 9
⊢ (((𝐾‘𝑁) ∩ (𝐴[,]𝐵)) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) |
33 | 31, 32 | sylib 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) → ∃𝑥 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) |
34 | | xp1st 7739 |
. . . . . . . . . . . 12
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑁))) ∈ (ℝ × ℝ) →
(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ∈ ℝ) |
35 | 24, 34 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ∈ ℝ) |
36 | 35 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ∈ ℝ) |
37 | 36 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) ∧ 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ∈ ℝ) |
38 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) ∧ 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) → 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) |
39 | | elin 3857 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵)) ↔ (𝑥 ∈ (𝐾‘𝑁) ∧ 𝑥 ∈ (𝐴[,]𝐵))) |
40 | 38, 39 | sylib 221 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) ∧ 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) → (𝑥 ∈ (𝐾‘𝑁) ∧ 𝑥 ∈ (𝐴[,]𝐵))) |
41 | 40 | simprd 499 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) ∧ 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) → 𝑥 ∈ (𝐴[,]𝐵)) |
42 | | ovolicc.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℝ) |
43 | | elicc2 12879 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
44 | 42, 1, 43 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
45 | 44 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) ∧ 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
46 | 41, 45 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) ∧ 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
47 | 46 | simp1d 1143 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) ∧ 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) → 𝑥 ∈ ℝ) |
48 | 1 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) ∧ 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) → 𝐵 ∈ ℝ) |
49 | 40 | simpld 498 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) ∧ 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) → 𝑥 ∈ (𝐾‘𝑁)) |
50 | 30 | simpld 498 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) → (𝐾‘𝑁) ∈ 𝑈) |
51 | | ovolicc.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
52 | | ovolicc2.4 |
. . . . . . . . . . . . . 14
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
53 | | ovolicc2.6 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) |
54 | | ovolicc2.7 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) |
55 | | ovolicc2.9 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) |
56 | 42, 1, 51, 52, 3, 53, 54, 8, 55 | ovolicc2lem1 24262 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐾‘𝑁) ∈ 𝑈) → (𝑥 ∈ (𝐾‘𝑁) ↔ (𝑥 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁))))))) |
57 | 50, 56 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) → (𝑥 ∈ (𝐾‘𝑁) ↔ (𝑥 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁))))))) |
58 | 57 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) ∧ 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) → (𝑥 ∈ (𝐾‘𝑁) ↔ (𝑥 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁))))))) |
59 | 49, 58 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) ∧ 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) → (𝑥 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) |
60 | 59 | simp2d 1144 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) ∧ 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) < 𝑥) |
61 | 46 | simp3d 1145 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) ∧ 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) → 𝑥 ≤ 𝐵) |
62 | 37, 47, 48, 60, 61 | ltletrd 10871 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) ∧ 𝑥 ∈ ((𝐾‘𝑁) ∩ (𝐴[,]𝐵))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) < 𝐵) |
63 | 33, 62 | exlimddv 1941 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) < 𝐵) |
64 | | simprr 773 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) → 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁))))) |
65 | 42, 1, 51, 52, 3, 53, 54, 8, 55 | ovolicc2lem1 24262 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐾‘𝑁) ∈ 𝑈) → (𝐵 ∈ (𝐾‘𝑁) ↔ (𝐵 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) < 𝐵 ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁))))))) |
66 | 50, 65 | syldan 594 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) → (𝐵 ∈ (𝐾‘𝑁) ↔ (𝐵 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) < 𝐵 ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁))))))) |
67 | 29, 63, 64, 66 | mpbir3and 1343 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) → 𝐵 ∈ (𝐾‘𝑁)) |
68 | | fveq2 6668 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝐾‘𝑛) = (𝐾‘𝑁)) |
69 | 68 | eleq2d 2818 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝐵 ∈ (𝐾‘𝑛) ↔ 𝐵 ∈ (𝐾‘𝑁))) |
70 | | ovolicc2.16 |
. . . . . . 7
⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} |
71 | 69, 70 | elrab2 3588 |
. . . . . 6
⊢ (𝑁 ∈ 𝑊 ↔ (𝑁 ∈ ℕ ∧ 𝐵 ∈ (𝐾‘𝑁))) |
72 | 28, 67, 71 | sylanbrc 586 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))))) → 𝑁 ∈ 𝑊) |
73 | 72 | expr 460 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) → 𝑁 ∈ 𝑊)) |
74 | 27, 73 | sylbird 263 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (¬
(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ≤ 𝐵 → 𝑁 ∈ 𝑊)) |
75 | 74 | con1d 147 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (¬ 𝑁 ∈ 𝑊 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ≤ 𝐵)) |
76 | 75 | impr 458 |
1
⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ ¬ 𝑁 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ≤ 𝐵) |