Step | Hyp | Ref
| Expression |
1 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ℤ) |
2 | | nffvmpt1 6111 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) |
3 | 2 | nfel1 2765 |
. . . . 5
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ |
4 | 1, 3 | nfim 1813 |
. . . 4
⊢
Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ) |
5 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥 ∈ ℤ ↔ 𝑎 ∈ ℤ)) |
6 | 5 | anbi2d 736 |
. . . . 5
⊢ (𝑥 = 𝑎 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ 𝑎 ∈ ℤ))) |
7 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑎 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)) |
8 | 7 | eleq1d 2672 |
. . . . 5
⊢ (𝑥 = 𝑎 → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) ∈ ℝ ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ)) |
9 | 6, 8 | imbi12d 333 |
. . . 4
⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) ∈ ℝ) ↔ ((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ))) |
10 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℤ) |
11 | | monotoddzz.2 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) |
12 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ ↦ 𝐸) = (𝑥 ∈ ℤ ↦ 𝐸) |
13 | 12 | fvmpt2 6200 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝐸 ∈ ℝ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸) |
14 | 10, 11, 13 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸) |
15 | 14, 11 | eqeltrd 2688 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) ∈ ℝ) |
16 | 4, 9, 15 | chvar 2250 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ) |
17 | | eleq1 2676 |
. . . . . 6
⊢ (𝑦 = 𝑎 → (𝑦 ∈ ℤ ↔ 𝑎 ∈ ℤ)) |
18 | 17 | anbi2d 736 |
. . . . 5
⊢ (𝑦 = 𝑎 → ((𝜑 ∧ 𝑦 ∈ ℤ) ↔ (𝜑 ∧ 𝑎 ∈ ℤ))) |
19 | | negeq 10152 |
. . . . . . 7
⊢ (𝑦 = 𝑎 → -𝑦 = -𝑎) |
20 | 19 | fveq2d 6107 |
. . . . . 6
⊢ (𝑦 = 𝑎 → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑎)) |
21 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑦 = 𝑎 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)) |
22 | 21 | negeqd 10154 |
. . . . . 6
⊢ (𝑦 = 𝑎 → -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)) |
23 | 20, 22 | eqeq12d 2625 |
. . . . 5
⊢ (𝑦 = 𝑎 → (((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑎) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎))) |
24 | 18, 23 | imbi12d 333 |
. . . 4
⊢ (𝑦 = 𝑎 → (((𝜑 ∧ 𝑦 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦)) ↔ ((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑎) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)))) |
25 | | monotoddzz.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐺 = -𝐹) |
26 | | znegcl 11289 |
. . . . . . 7
⊢ (𝑦 ∈ ℤ → -𝑦 ∈
ℤ) |
27 | 26 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → -𝑦 ∈ ℤ) |
28 | | negex 10158 |
. . . . . . . 8
⊢ -𝑦 ∈ V |
29 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑥 = -𝑦 → (𝑥 ∈ ℤ ↔ -𝑦 ∈ ℤ)) |
30 | 29 | anbi2d 736 |
. . . . . . . . 9
⊢ (𝑥 = -𝑦 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ -𝑦 ∈ ℤ))) |
31 | | monotoddzz.7 |
. . . . . . . . . 10
⊢ (𝑥 = -𝑦 → 𝐸 = 𝐺) |
32 | 31 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑥 = -𝑦 → (𝐸 ∈ ℝ ↔ 𝐺 ∈ ℝ)) |
33 | 30, 32 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑥 = -𝑦 → (((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) ↔ ((𝜑 ∧ -𝑦 ∈ ℤ) → 𝐺 ∈ ℝ))) |
34 | 28, 33, 11 | vtocl 3232 |
. . . . . . 7
⊢ ((𝜑 ∧ -𝑦 ∈ ℤ) → 𝐺 ∈ ℝ) |
35 | 26, 34 | sylan2 490 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐺 ∈ ℝ) |
36 | 31, 12 | fvmptg 6189 |
. . . . . 6
⊢ ((-𝑦 ∈ ℤ ∧ 𝐺 ∈ ℝ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = 𝐺) |
37 | 27, 35, 36 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = 𝐺) |
38 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ ℤ) |
39 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ∈ ℤ ↔ 𝑦 ∈ ℤ)) |
40 | 39 | anbi2d 736 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ 𝑦 ∈ ℤ))) |
41 | | monotoddzz.6 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝐸 = 𝐹) |
42 | 41 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐸 ∈ ℝ ↔ 𝐹 ∈ ℝ)) |
43 | 40, 42 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) ↔ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐹 ∈ ℝ))) |
44 | 43, 11 | chvarv 2251 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐹 ∈ ℝ) |
45 | 41, 12 | fvmptg 6189 |
. . . . . . 7
⊢ ((𝑦 ∈ ℤ ∧ 𝐹 ∈ ℝ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹) |
46 | 38, 44, 45 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹) |
47 | 46 | negeqd 10154 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = -𝐹) |
48 | 25, 37, 47 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦)) |
49 | 24, 48 | chvarv 2251 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑎) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)) |
50 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈
ℕ0) |
51 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑥 𝑎 < 𝑏 |
52 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥
< |
53 | | nffvmpt1 6111 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏) |
54 | 2, 52, 53 | nfbr 4629 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏) |
55 | 51, 54 | nfim 1813 |
. . . . 5
⊢
Ⅎ𝑥(𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)) |
56 | 50, 55 | nfim 1813 |
. . . 4
⊢
Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
57 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥 ∈ ℕ0 ↔ 𝑎 ∈
ℕ0)) |
58 | 57 | 3anbi2d 1396 |
. . . . 5
⊢ (𝑥 = 𝑎 → ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
↔ (𝜑 ∧ 𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0))) |
59 | | breq1 4586 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥 < 𝑏 ↔ 𝑎 < 𝑏)) |
60 | 7 | breq1d 4593 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏) ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
61 | 59, 60 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝑎 → ((𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)) ↔ (𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)))) |
62 | 58, 61 | imbi12d 333 |
. . . 4
⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) ↔ ((𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))))) |
63 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (𝑦 ∈ ℕ0 ↔ 𝑏 ∈
ℕ0)) |
64 | 63 | 3anbi3d 1397 |
. . . . . 6
⊢ (𝑦 = 𝑏 → ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
↔ (𝜑 ∧ 𝑥 ∈ ℕ0
∧ 𝑏 ∈
ℕ0))) |
65 | | breq2 4587 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (𝑥 < 𝑦 ↔ 𝑥 < 𝑏)) |
66 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)) |
67 | 66 | breq2d 4595 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
68 | 65, 67 | imbi12d 333 |
. . . . . 6
⊢ (𝑦 = 𝑏 → ((𝑥 < 𝑦 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦)) ↔ (𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)))) |
69 | 64, 68 | imbi12d 333 |
. . . . 5
⊢ (𝑦 = 𝑏 → (((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (𝑥 < 𝑦 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦))) ↔ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))))) |
70 | | monotoddzz.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (𝑥 < 𝑦 → 𝐸 < 𝐹)) |
71 | | nn0z 11277 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℤ) |
72 | 71, 14 | sylan2 490 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸) |
73 | 72 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ ((𝑥 ∈ ℤ
↦ 𝐸)‘𝑥) = 𝐸) |
74 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ ℕ0) |
75 | | nffvmpt1 6111 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) |
76 | 75 | nfeq1 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹 |
77 | 74, 76 | nfim 1813 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹) |
78 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ∈ ℕ0 ↔ 𝑦 ∈
ℕ0)) |
79 | 78 | anbi2d 736 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ ℕ0) ↔ (𝜑 ∧ 𝑦 ∈
ℕ0))) |
80 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦)) |
81 | 80, 41 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸 ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹)) |
82 | 79, 81 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸) ↔ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹))) |
83 | 77, 82, 72 | chvar 2250 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹) |
84 | 83 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ ((𝑥 ∈ ℤ
↦ 𝐸)‘𝑦) = 𝐹) |
85 | 73, 84 | breq12d 4596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (((𝑥 ∈ ℤ
↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) ↔ 𝐸 < 𝐹)) |
86 | 70, 85 | sylibrd 248 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (𝑥 < 𝑦 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦))) |
87 | 69, 86 | chvarv 2251 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
88 | 56, 62, 87 | chvar 2250 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
89 | 16, 49, 88 | monotoddzzfi 36525 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐴) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐵))) |
90 | | simp2 1055 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∈ ℤ) |
91 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝑥 ∈ ℤ ↔ 𝐴 ∈ ℤ)) |
92 | 91 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ 𝐴 ∈ ℤ))) |
93 | | monotoddzz.4 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → 𝐸 = 𝐶) |
94 | 93 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐸 ∈ ℝ ↔ 𝐶 ∈ ℝ)) |
95 | 92, 94 | imbi12d 333 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) ↔ ((𝜑 ∧ 𝐴 ∈ ℤ) → 𝐶 ∈ ℝ))) |
96 | 95, 11 | vtoclg 3239 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → ((𝜑 ∧ 𝐴 ∈ ℤ) → 𝐶 ∈ ℝ)) |
97 | 96 | anabsi7 856 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ) → 𝐶 ∈ ℝ) |
98 | 97 | 3adant3 1074 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐶 ∈ ℝ) |
99 | 93, 12 | fvmptg 6189 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℝ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐴) = 𝐶) |
100 | 90, 98, 99 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐴) = 𝐶) |
101 | | simp3 1056 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∈ ℤ) |
102 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → (𝑥 ∈ ℤ ↔ 𝐵 ∈ ℤ)) |
103 | 102 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ 𝐵 ∈ ℤ))) |
104 | | monotoddzz.5 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → 𝐸 = 𝐷) |
105 | 104 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝐸 ∈ ℝ ↔ 𝐷 ∈ ℝ)) |
106 | 103, 105 | imbi12d 333 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) ↔ ((𝜑 ∧ 𝐵 ∈ ℤ) → 𝐷 ∈ ℝ))) |
107 | 106, 11 | vtoclg 3239 |
. . . . . 6
⊢ (𝐵 ∈ ℤ → ((𝜑 ∧ 𝐵 ∈ ℤ) → 𝐷 ∈ ℝ)) |
108 | 107 | anabsi7 856 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ ℤ) → 𝐷 ∈ ℝ) |
109 | 108 | 3adant2 1073 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐷 ∈ ℝ) |
110 | 104, 12 | fvmptg 6189 |
. . . 4
⊢ ((𝐵 ∈ ℤ ∧ 𝐷 ∈ ℝ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐵) = 𝐷) |
111 | 101, 109,
110 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐵) = 𝐷) |
112 | 100, 111 | breq12d 4596 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝐴) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐵) ↔ 𝐶 < 𝐷)) |
113 | 89, 112 | bitrd 267 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ 𝐶 < 𝐷)) |