Proof of Theorem dyadss
Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) |
2 | | simpllr 773 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → 𝐵 ∈ ℤ) |
3 | | simplrr 775 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → 𝐷 ∈
ℕ0) |
4 | | dyadmbl.1 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) |
5 | 4 | dyadval 24754 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℤ ∧ 𝐷 ∈ ℕ0)
→ (𝐵𝐹𝐷) = 〈(𝐵 / (2↑𝐷)), ((𝐵 + 1) / (2↑𝐷))〉) |
6 | 2, 3, 5 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → (𝐵𝐹𝐷) = 〈(𝐵 / (2↑𝐷)), ((𝐵 + 1) / (2↑𝐷))〉) |
7 | 6 | fveq2d 6775 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → ([,]‘(𝐵𝐹𝐷)) = ([,]‘〈(𝐵 / (2↑𝐷)), ((𝐵 + 1) / (2↑𝐷))〉)) |
8 | | df-ov 7274 |
. . . . . . . 8
⊢ ((𝐵 / (2↑𝐷))[,]((𝐵 + 1) / (2↑𝐷))) = ([,]‘〈(𝐵 / (2↑𝐷)), ((𝐵 + 1) / (2↑𝐷))〉) |
9 | 7, 8 | eqtr4di 2798 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → ([,]‘(𝐵𝐹𝐷)) = ((𝐵 / (2↑𝐷))[,]((𝐵 + 1) / (2↑𝐷)))) |
10 | 2 | zred 12425 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → 𝐵 ∈ ℝ) |
11 | | 2nn 12046 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
12 | | nnexpcl 13793 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ 𝐷
∈ ℕ0) → (2↑𝐷) ∈ ℕ) |
13 | 11, 3, 12 | sylancr 587 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → (2↑𝐷) ∈ ℕ) |
14 | 10, 13 | nndivred 12027 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → (𝐵 / (2↑𝐷)) ∈ ℝ) |
15 | | peano2re 11148 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → (𝐵 + 1) ∈
ℝ) |
16 | 10, 15 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → (𝐵 + 1) ∈ ℝ) |
17 | 16, 13 | nndivred 12027 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → ((𝐵 + 1) / (2↑𝐷)) ∈ ℝ) |
18 | | iccssre 13160 |
. . . . . . . 8
⊢ (((𝐵 / (2↑𝐷)) ∈ ℝ ∧ ((𝐵 + 1) / (2↑𝐷)) ∈ ℝ) → ((𝐵 / (2↑𝐷))[,]((𝐵 + 1) / (2↑𝐷))) ⊆ ℝ) |
19 | 14, 17, 18 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → ((𝐵 / (2↑𝐷))[,]((𝐵 + 1) / (2↑𝐷))) ⊆ ℝ) |
20 | 9, 19 | eqsstrd 3964 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → ([,]‘(𝐵𝐹𝐷)) ⊆ ℝ) |
21 | | ovolss 24647 |
. . . . . 6
⊢
((([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) ∧ ([,]‘(𝐵𝐹𝐷)) ⊆ ℝ) →
(vol*‘([,]‘(𝐴𝐹𝐶))) ≤ (vol*‘([,]‘(𝐵𝐹𝐷)))) |
22 | 1, 20, 21 | syl2anc 584 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → (vol*‘([,]‘(𝐴𝐹𝐶))) ≤ (vol*‘([,]‘(𝐵𝐹𝐷)))) |
23 | | simplll 772 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → 𝐴 ∈ ℤ) |
24 | | simplrl 774 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → 𝐶 ∈
ℕ0) |
25 | 4 | dyadovol 24755 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℕ0)
→ (vol*‘([,]‘(𝐴𝐹𝐶))) = (1 / (2↑𝐶))) |
26 | 23, 24, 25 | syl2anc 584 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → (vol*‘([,]‘(𝐴𝐹𝐶))) = (1 / (2↑𝐶))) |
27 | 4 | dyadovol 24755 |
. . . . . 6
⊢ ((𝐵 ∈ ℤ ∧ 𝐷 ∈ ℕ0)
→ (vol*‘([,]‘(𝐵𝐹𝐷))) = (1 / (2↑𝐷))) |
28 | 2, 3, 27 | syl2anc 584 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → (vol*‘([,]‘(𝐵𝐹𝐷))) = (1 / (2↑𝐷))) |
29 | 22, 26, 28 | 3brtr3d 5110 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → (1 / (2↑𝐶)) ≤ (1 / (2↑𝐷))) |
30 | | nnexpcl 13793 |
. . . . . 6
⊢ ((2
∈ ℕ ∧ 𝐶
∈ ℕ0) → (2↑𝐶) ∈ ℕ) |
31 | 11, 24, 30 | sylancr 587 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → (2↑𝐶) ∈ ℕ) |
32 | | nnre 11980 |
. . . . . . 7
⊢
((2↑𝐷) ∈
ℕ → (2↑𝐷)
∈ ℝ) |
33 | | nngt0 12004 |
. . . . . . 7
⊢
((2↑𝐷) ∈
ℕ → 0 < (2↑𝐷)) |
34 | 32, 33 | jca 512 |
. . . . . 6
⊢
((2↑𝐷) ∈
ℕ → ((2↑𝐷)
∈ ℝ ∧ 0 < (2↑𝐷))) |
35 | | nnre 11980 |
. . . . . . 7
⊢
((2↑𝐶) ∈
ℕ → (2↑𝐶)
∈ ℝ) |
36 | | nngt0 12004 |
. . . . . . 7
⊢
((2↑𝐶) ∈
ℕ → 0 < (2↑𝐶)) |
37 | 35, 36 | jca 512 |
. . . . . 6
⊢
((2↑𝐶) ∈
ℕ → ((2↑𝐶)
∈ ℝ ∧ 0 < (2↑𝐶))) |
38 | | lerec 11858 |
. . . . . 6
⊢
((((2↑𝐷) ∈
ℝ ∧ 0 < (2↑𝐷)) ∧ ((2↑𝐶) ∈ ℝ ∧ 0 < (2↑𝐶))) → ((2↑𝐷) ≤ (2↑𝐶) ↔ (1 / (2↑𝐶)) ≤ (1 / (2↑𝐷)))) |
39 | 34, 37, 38 | syl2an 596 |
. . . . 5
⊢
(((2↑𝐷) ∈
ℕ ∧ (2↑𝐶)
∈ ℕ) → ((2↑𝐷) ≤ (2↑𝐶) ↔ (1 / (2↑𝐶)) ≤ (1 / (2↑𝐷)))) |
40 | 13, 31, 39 | syl2anc 584 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → ((2↑𝐷) ≤ (2↑𝐶) ↔ (1 / (2↑𝐶)) ≤ (1 / (2↑𝐷)))) |
41 | 29, 40 | mpbird 256 |
. . 3
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → (2↑𝐷) ≤ (2↑𝐶)) |
42 | | 2re 12047 |
. . . . 5
⊢ 2 ∈
ℝ |
43 | 42 | a1i 11 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → 2 ∈
ℝ) |
44 | 3 | nn0zd 12423 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → 𝐷 ∈ ℤ) |
45 | 24 | nn0zd 12423 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → 𝐶 ∈ ℤ) |
46 | | 1lt2 12144 |
. . . . 5
⊢ 1 <
2 |
47 | 46 | a1i 11 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → 1 < 2) |
48 | 43, 44, 45, 47 | leexp2d 13967 |
. . 3
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → (𝐷 ≤ 𝐶 ↔ (2↑𝐷) ≤ (2↑𝐶))) |
49 | 41, 48 | mpbird 256 |
. 2
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) → 𝐷 ≤ 𝐶) |
50 | 49 | ex 413 |
1
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) → 𝐷 ≤ 𝐶)) |