Step | Hyp | Ref
| Expression |
1 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ℤ) |
2 | | nffvmpt1 6728 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) |
3 | 2 | nfel1 2920 |
. . . . 5
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ |
4 | 1, 3 | nfim 1904 |
. . . 4
⊢
Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ) |
5 | | eleq1 2825 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥 ∈ ℤ ↔ 𝑎 ∈ ℤ)) |
6 | 5 | anbi2d 632 |
. . . . 5
⊢ (𝑥 = 𝑎 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ 𝑎 ∈ ℤ))) |
7 | | fveq2 6717 |
. . . . . 6
⊢ (𝑥 = 𝑎 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)) |
8 | 7 | eleq1d 2822 |
. . . . 5
⊢ (𝑥 = 𝑎 → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) ∈ ℝ ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ)) |
9 | 6, 8 | imbi12d 348 |
. . . 4
⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) ∈ ℝ) ↔ ((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ))) |
10 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℤ) |
11 | | monotoddzz.2 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) |
12 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ ↦ 𝐸) = (𝑥 ∈ ℤ ↦ 𝐸) |
13 | 12 | fvmpt2 6829 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝐸 ∈ ℝ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸) |
14 | 10, 11, 13 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸) |
15 | 14, 11 | eqeltrd 2838 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) ∈ ℝ) |
16 | 4, 9, 15 | chvarfv 2238 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ) |
17 | | eleq1 2825 |
. . . . . 6
⊢ (𝑦 = 𝑎 → (𝑦 ∈ ℤ ↔ 𝑎 ∈ ℤ)) |
18 | 17 | anbi2d 632 |
. . . . 5
⊢ (𝑦 = 𝑎 → ((𝜑 ∧ 𝑦 ∈ ℤ) ↔ (𝜑 ∧ 𝑎 ∈ ℤ))) |
19 | | negeq 11070 |
. . . . . . 7
⊢ (𝑦 = 𝑎 → -𝑦 = -𝑎) |
20 | 19 | fveq2d 6721 |
. . . . . 6
⊢ (𝑦 = 𝑎 → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑎)) |
21 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑦 = 𝑎 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)) |
22 | 21 | negeqd 11072 |
. . . . . 6
⊢ (𝑦 = 𝑎 → -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)) |
23 | 20, 22 | eqeq12d 2753 |
. . . . 5
⊢ (𝑦 = 𝑎 → (((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑎) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎))) |
24 | 18, 23 | imbi12d 348 |
. . . 4
⊢ (𝑦 = 𝑎 → (((𝜑 ∧ 𝑦 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦)) ↔ ((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑎) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)))) |
25 | | monotoddzz.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐺 = -𝐹) |
26 | | monotoddzz.7 |
. . . . . 6
⊢ (𝑥 = -𝑦 → 𝐸 = 𝐺) |
27 | | znegcl 12212 |
. . . . . . 7
⊢ (𝑦 ∈ ℤ → -𝑦 ∈
ℤ) |
28 | 27 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → -𝑦 ∈ ℤ) |
29 | | negex 11076 |
. . . . . . . 8
⊢ -𝑦 ∈ V |
30 | | eleq1 2825 |
. . . . . . . . . 10
⊢ (𝑥 = -𝑦 → (𝑥 ∈ ℤ ↔ -𝑦 ∈ ℤ)) |
31 | 30 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑥 = -𝑦 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ -𝑦 ∈ ℤ))) |
32 | 26 | eleq1d 2822 |
. . . . . . . . 9
⊢ (𝑥 = -𝑦 → (𝐸 ∈ ℝ ↔ 𝐺 ∈ ℝ)) |
33 | 31, 32 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑥 = -𝑦 → (((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) ↔ ((𝜑 ∧ -𝑦 ∈ ℤ) → 𝐺 ∈ ℝ))) |
34 | 29, 33, 11 | vtocl 3474 |
. . . . . . 7
⊢ ((𝜑 ∧ -𝑦 ∈ ℤ) → 𝐺 ∈ ℝ) |
35 | 27, 34 | sylan2 596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐺 ∈ ℝ) |
36 | 12, 26, 28, 35 | fvmptd3 6841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = 𝐺) |
37 | | monotoddzz.6 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → 𝐸 = 𝐹) |
38 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ ℤ) |
39 | | eleq1 2825 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ∈ ℤ ↔ 𝑦 ∈ ℤ)) |
40 | 39 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ 𝑦 ∈ ℤ))) |
41 | 37 | eleq1d 2822 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐸 ∈ ℝ ↔ 𝐹 ∈ ℝ)) |
42 | 40, 41 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) ↔ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐹 ∈ ℝ))) |
43 | 42, 11 | chvarvv 2007 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐹 ∈ ℝ) |
44 | 12, 37, 38, 43 | fvmptd3 6841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹) |
45 | 44 | negeqd 11072 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = -𝐹) |
46 | 25, 36, 45 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦)) |
47 | 24, 46 | chvarvv 2007 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑎) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)) |
48 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈
ℕ0) |
49 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑥 𝑎 < 𝑏 |
50 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑥
< |
51 | | nffvmpt1 6728 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏) |
52 | 2, 50, 51 | nfbr 5100 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏) |
53 | 49, 52 | nfim 1904 |
. . . . 5
⊢
Ⅎ𝑥(𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)) |
54 | 48, 53 | nfim 1904 |
. . . 4
⊢
Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
55 | | eleq1 2825 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥 ∈ ℕ0 ↔ 𝑎 ∈
ℕ0)) |
56 | 55 | 3anbi2d 1443 |
. . . . 5
⊢ (𝑥 = 𝑎 → ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
↔ (𝜑 ∧ 𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0))) |
57 | | breq1 5056 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥 < 𝑏 ↔ 𝑎 < 𝑏)) |
58 | 7 | breq1d 5063 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏) ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
59 | 57, 58 | imbi12d 348 |
. . . . 5
⊢ (𝑥 = 𝑎 → ((𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)) ↔ (𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)))) |
60 | 56, 59 | imbi12d 348 |
. . . 4
⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) ↔ ((𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))))) |
61 | | eleq1 2825 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (𝑦 ∈ ℕ0 ↔ 𝑏 ∈
ℕ0)) |
62 | 61 | 3anbi3d 1444 |
. . . . . 6
⊢ (𝑦 = 𝑏 → ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
↔ (𝜑 ∧ 𝑥 ∈ ℕ0
∧ 𝑏 ∈
ℕ0))) |
63 | | breq2 5057 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (𝑥 < 𝑦 ↔ 𝑥 < 𝑏)) |
64 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑦 = 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)) |
65 | 64 | breq2d 5065 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
66 | 63, 65 | imbi12d 348 |
. . . . . 6
⊢ (𝑦 = 𝑏 → ((𝑥 < 𝑦 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦)) ↔ (𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)))) |
67 | 62, 66 | imbi12d 348 |
. . . . 5
⊢ (𝑦 = 𝑏 → (((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (𝑥 < 𝑦 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦))) ↔ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))))) |
68 | | monotoddzz.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (𝑥 < 𝑦 → 𝐸 < 𝐹)) |
69 | | nn0z 12200 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℤ) |
70 | 69, 14 | sylan2 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸) |
71 | 70 | 3adant3 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ ((𝑥 ∈ ℤ
↦ 𝐸)‘𝑥) = 𝐸) |
72 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ ℕ0) |
73 | | nffvmpt1 6728 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) |
74 | 73 | nfeq1 2919 |
. . . . . . . . . 10
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹 |
75 | 72, 74 | nfim 1904 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹) |
76 | | eleq1 2825 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ∈ ℕ0 ↔ 𝑦 ∈
ℕ0)) |
77 | 76 | anbi2d 632 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ ℕ0) ↔ (𝜑 ∧ 𝑦 ∈
ℕ0))) |
78 | | fveq2 6717 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦)) |
79 | 78, 37 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸 ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹)) |
80 | 77, 79 | imbi12d 348 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸) ↔ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹))) |
81 | 75, 80, 70 | chvarfv 2238 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹) |
82 | 81 | 3adant2 1133 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ ((𝑥 ∈ ℤ
↦ 𝐸)‘𝑦) = 𝐹) |
83 | 71, 82 | breq12d 5066 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (((𝑥 ∈ ℤ
↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) ↔ 𝐸 < 𝐹)) |
84 | 68, 83 | sylibrd 262 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (𝑥 < 𝑦 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦))) |
85 | 67, 84 | chvarvv 2007 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
86 | 54, 60, 85 | chvarfv 2238 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
87 | 16, 47, 86 | monotoddzzfi 40467 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐴) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐵))) |
88 | | monotoddzz.4 |
. . . 4
⊢ (𝑥 = 𝐴 → 𝐸 = 𝐶) |
89 | | simp2 1139 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∈ ℤ) |
90 | | eleq1 2825 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝑥 ∈ ℤ ↔ 𝐴 ∈ ℤ)) |
91 | 90 | anbi2d 632 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ 𝐴 ∈ ℤ))) |
92 | 88 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐸 ∈ ℝ ↔ 𝐶 ∈ ℝ)) |
93 | 91, 92 | imbi12d 348 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) ↔ ((𝜑 ∧ 𝐴 ∈ ℤ) → 𝐶 ∈ ℝ))) |
94 | 93, 11 | vtoclg 3481 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → ((𝜑 ∧ 𝐴 ∈ ℤ) → 𝐶 ∈ ℝ)) |
95 | 94 | anabsi7 671 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ) → 𝐶 ∈ ℝ) |
96 | 95 | 3adant3 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐶 ∈ ℝ) |
97 | 12, 88, 89, 96 | fvmptd3 6841 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐴) = 𝐶) |
98 | | monotoddzz.5 |
. . . 4
⊢ (𝑥 = 𝐵 → 𝐸 = 𝐷) |
99 | | simp3 1140 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∈ ℤ) |
100 | | eleq1 2825 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → (𝑥 ∈ ℤ ↔ 𝐵 ∈ ℤ)) |
101 | 100 | anbi2d 632 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ 𝐵 ∈ ℤ))) |
102 | 98 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝐸 ∈ ℝ ↔ 𝐷 ∈ ℝ)) |
103 | 101, 102 | imbi12d 348 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) ↔ ((𝜑 ∧ 𝐵 ∈ ℤ) → 𝐷 ∈ ℝ))) |
104 | 103, 11 | vtoclg 3481 |
. . . . . 6
⊢ (𝐵 ∈ ℤ → ((𝜑 ∧ 𝐵 ∈ ℤ) → 𝐷 ∈ ℝ)) |
105 | 104 | anabsi7 671 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ ℤ) → 𝐷 ∈ ℝ) |
106 | 105 | 3adant2 1133 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐷 ∈ ℝ) |
107 | 12, 98, 99, 106 | fvmptd3 6841 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐵) = 𝐷) |
108 | 97, 107 | breq12d 5066 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝐴) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐵) ↔ 𝐶 < 𝐷)) |
109 | 87, 108 | bitrd 282 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ 𝐶 < 𝐷)) |