Step | Hyp | Ref
| Expression |
1 | | nfv 1843 |
. . . . 5
⊢
Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ℤ) |
2 | | nffvmpt1 6199 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) |
3 | 2 | nfel1 2779 |
. . . . 5
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ |
4 | 1, 3 | nfim 1825 |
. . . 4
⊢
Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ) |
5 | | eleq1 2689 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥 ∈ ℤ ↔ 𝑎 ∈ ℤ)) |
6 | 5 | anbi2d 740 |
. . . . 5
⊢ (𝑥 = 𝑎 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ 𝑎 ∈ ℤ))) |
7 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = 𝑎 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)) |
8 | 7 | eleq1d 2686 |
. . . . 5
⊢ (𝑥 = 𝑎 → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) ∈ ℝ ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ)) |
9 | 6, 8 | imbi12d 334 |
. . . 4
⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) ∈ ℝ) ↔ ((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ))) |
10 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℤ) |
11 | | monotoddzz.2 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) |
12 | | eqid 2622 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ ↦ 𝐸) = (𝑥 ∈ ℤ ↦ 𝐸) |
13 | 12 | fvmpt2 6291 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝐸 ∈ ℝ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸) |
14 | 10, 11, 13 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸) |
15 | 14, 11 | eqeltrd 2701 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) ∈ ℝ) |
16 | 4, 9, 15 | chvar 2262 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) ∈ ℝ) |
17 | | eleq1 2689 |
. . . . . 6
⊢ (𝑦 = 𝑎 → (𝑦 ∈ ℤ ↔ 𝑎 ∈ ℤ)) |
18 | 17 | anbi2d 740 |
. . . . 5
⊢ (𝑦 = 𝑎 → ((𝜑 ∧ 𝑦 ∈ ℤ) ↔ (𝜑 ∧ 𝑎 ∈ ℤ))) |
19 | | negeq 10273 |
. . . . . . 7
⊢ (𝑦 = 𝑎 → -𝑦 = -𝑎) |
20 | 19 | fveq2d 6195 |
. . . . . 6
⊢ (𝑦 = 𝑎 → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑎)) |
21 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑦 = 𝑎 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)) |
22 | 21 | negeqd 10275 |
. . . . . 6
⊢ (𝑦 = 𝑎 → -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)) |
23 | 20, 22 | eqeq12d 2637 |
. . . . 5
⊢ (𝑦 = 𝑎 → (((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑎) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎))) |
24 | 18, 23 | imbi12d 334 |
. . . 4
⊢ (𝑦 = 𝑎 → (((𝜑 ∧ 𝑦 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦)) ↔ ((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑎) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)))) |
25 | | monotoddzz.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐺 = -𝐹) |
26 | | znegcl 11412 |
. . . . . . 7
⊢ (𝑦 ∈ ℤ → -𝑦 ∈
ℤ) |
27 | 26 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → -𝑦 ∈ ℤ) |
28 | | negex 10279 |
. . . . . . . 8
⊢ -𝑦 ∈ V |
29 | | eleq1 2689 |
. . . . . . . . . 10
⊢ (𝑥 = -𝑦 → (𝑥 ∈ ℤ ↔ -𝑦 ∈ ℤ)) |
30 | 29 | anbi2d 740 |
. . . . . . . . 9
⊢ (𝑥 = -𝑦 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ -𝑦 ∈ ℤ))) |
31 | | monotoddzz.7 |
. . . . . . . . . 10
⊢ (𝑥 = -𝑦 → 𝐸 = 𝐺) |
32 | 31 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑥 = -𝑦 → (𝐸 ∈ ℝ ↔ 𝐺 ∈ ℝ)) |
33 | 30, 32 | imbi12d 334 |
. . . . . . . 8
⊢ (𝑥 = -𝑦 → (((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) ↔ ((𝜑 ∧ -𝑦 ∈ ℤ) → 𝐺 ∈ ℝ))) |
34 | 28, 33, 11 | vtocl 3259 |
. . . . . . 7
⊢ ((𝜑 ∧ -𝑦 ∈ ℤ) → 𝐺 ∈ ℝ) |
35 | 26, 34 | sylan2 491 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐺 ∈ ℝ) |
36 | 31, 12 | fvmptg 6280 |
. . . . . 6
⊢ ((-𝑦 ∈ ℤ ∧ 𝐺 ∈ ℝ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = 𝐺) |
37 | 27, 35, 36 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = 𝐺) |
38 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ ℤ) |
39 | | eleq1 2689 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ∈ ℤ ↔ 𝑦 ∈ ℤ)) |
40 | 39 | anbi2d 740 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ 𝑦 ∈ ℤ))) |
41 | | monotoddzz.6 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝐸 = 𝐹) |
42 | 41 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐸 ∈ ℝ ↔ 𝐹 ∈ ℝ)) |
43 | 40, 42 | imbi12d 334 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) ↔ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐹 ∈ ℝ))) |
44 | 43, 11 | chvarv 2263 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐹 ∈ ℝ) |
45 | 41, 12 | fvmptg 6280 |
. . . . . . 7
⊢ ((𝑦 ∈ ℤ ∧ 𝐹 ∈ ℝ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹) |
46 | 38, 44, 45 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹) |
47 | 46 | negeqd 10275 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = -𝐹) |
48 | 25, 37, 47 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑦) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦)) |
49 | 24, 48 | chvarv 2263 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘-𝑎) = -((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎)) |
50 | | nfv 1843 |
. . . . 5
⊢
Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈
ℕ0) |
51 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑥 𝑎 < 𝑏 |
52 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑥
< |
53 | | nffvmpt1 6199 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏) |
54 | 2, 52, 53 | nfbr 4699 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏) |
55 | 51, 54 | nfim 1825 |
. . . . 5
⊢
Ⅎ𝑥(𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)) |
56 | 50, 55 | nfim 1825 |
. . . 4
⊢
Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
57 | | eleq1 2689 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥 ∈ ℕ0 ↔ 𝑎 ∈
ℕ0)) |
58 | 57 | 3anbi2d 1404 |
. . . . 5
⊢ (𝑥 = 𝑎 → ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
↔ (𝜑 ∧ 𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0))) |
59 | | breq1 4656 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥 < 𝑏 ↔ 𝑎 < 𝑏)) |
60 | 7 | breq1d 4663 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏) ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
61 | 59, 60 | imbi12d 334 |
. . . . 5
⊢ (𝑥 = 𝑎 → ((𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)) ↔ (𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)))) |
62 | 58, 61 | imbi12d 334 |
. . . 4
⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) ↔ ((𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))))) |
63 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (𝑦 ∈ ℕ0 ↔ 𝑏 ∈
ℕ0)) |
64 | 63 | 3anbi3d 1405 |
. . . . . 6
⊢ (𝑦 = 𝑏 → ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
↔ (𝜑 ∧ 𝑥 ∈ ℕ0
∧ 𝑏 ∈
ℕ0))) |
65 | | breq2 4657 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (𝑥 < 𝑦 ↔ 𝑥 < 𝑏)) |
66 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑦 = 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)) |
67 | 66 | breq2d 4665 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
68 | 65, 67 | imbi12d 334 |
. . . . . 6
⊢ (𝑦 = 𝑏 → ((𝑥 < 𝑦 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦)) ↔ (𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏)))) |
69 | 64, 68 | imbi12d 334 |
. . . . 5
⊢ (𝑦 = 𝑏 → (((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (𝑥 < 𝑦 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦))) ↔ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))))) |
70 | | monotoddzz.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (𝑥 < 𝑦 → 𝐸 < 𝐹)) |
71 | | nn0z 11400 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℤ) |
72 | 71, 14 | sylan2 491 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸) |
73 | 72 | 3adant3 1081 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ ((𝑥 ∈ ℤ
↦ 𝐸)‘𝑥) = 𝐸) |
74 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ ℕ0) |
75 | | nffvmpt1 6199 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) |
76 | 75 | nfeq1 2778 |
. . . . . . . . . 10
⊢
Ⅎ𝑥((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹 |
77 | 74, 76 | nfim 1825 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹) |
78 | | eleq1 2689 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ∈ ℕ0 ↔ 𝑦 ∈
ℕ0)) |
79 | 78 | anbi2d 740 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ ℕ0) ↔ (𝜑 ∧ 𝑦 ∈
ℕ0))) |
80 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦)) |
81 | 80, 41 | eqeq12d 2637 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸 ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹)) |
82 | 79, 81 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) = 𝐸) ↔ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹))) |
83 | 77, 82, 72 | chvar 2262 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) = 𝐹) |
84 | 83 | 3adant2 1080 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ ((𝑥 ∈ ℤ
↦ 𝐸)‘𝑦) = 𝐹) |
85 | 73, 84 | breq12d 4666 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (((𝑥 ∈ ℤ
↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦) ↔ 𝐸 < 𝐹)) |
86 | 70, 85 | sylibrd 249 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (𝑥 < 𝑦 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑦))) |
87 | 69, 86 | chvarv 2263 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑥 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑥) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
88 | 56, 62, 87 | chvar 2262 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0)
→ (𝑎 < 𝑏 → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑎) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝑏))) |
89 | 16, 49, 88 | monotoddzzfi 37507 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐴) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐵))) |
90 | | simp2 1062 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∈ ℤ) |
91 | | eleq1 2689 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝑥 ∈ ℤ ↔ 𝐴 ∈ ℤ)) |
92 | 91 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ 𝐴 ∈ ℤ))) |
93 | | monotoddzz.4 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → 𝐸 = 𝐶) |
94 | 93 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐸 ∈ ℝ ↔ 𝐶 ∈ ℝ)) |
95 | 92, 94 | imbi12d 334 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) ↔ ((𝜑 ∧ 𝐴 ∈ ℤ) → 𝐶 ∈ ℝ))) |
96 | 95, 11 | vtoclg 3266 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → ((𝜑 ∧ 𝐴 ∈ ℤ) → 𝐶 ∈ ℝ)) |
97 | 96 | anabsi7 860 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ) → 𝐶 ∈ ℝ) |
98 | 97 | 3adant3 1081 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐶 ∈ ℝ) |
99 | 93, 12 | fvmptg 6280 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℝ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐴) = 𝐶) |
100 | 90, 98, 99 | syl2anc 693 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐴) = 𝐶) |
101 | | simp3 1063 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∈ ℤ) |
102 | | eleq1 2689 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → (𝑥 ∈ ℤ ↔ 𝐵 ∈ ℤ)) |
103 | 102 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ 𝐵 ∈ ℤ))) |
104 | | monotoddzz.5 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → 𝐸 = 𝐷) |
105 | 104 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝐸 ∈ ℝ ↔ 𝐷 ∈ ℝ)) |
106 | 103, 105 | imbi12d 334 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) ↔ ((𝜑 ∧ 𝐵 ∈ ℤ) → 𝐷 ∈ ℝ))) |
107 | 106, 11 | vtoclg 3266 |
. . . . . 6
⊢ (𝐵 ∈ ℤ → ((𝜑 ∧ 𝐵 ∈ ℤ) → 𝐷 ∈ ℝ)) |
108 | 107 | anabsi7 860 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ ℤ) → 𝐷 ∈ ℝ) |
109 | 108 | 3adant2 1080 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐷 ∈ ℝ) |
110 | 104, 12 | fvmptg 6280 |
. . . 4
⊢ ((𝐵 ∈ ℤ ∧ 𝐷 ∈ ℝ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐵) = 𝐷) |
111 | 101, 109,
110 | syl2anc 693 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐵) = 𝐷) |
112 | 100, 111 | breq12d 4666 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((𝑥 ∈ ℤ ↦ 𝐸)‘𝐴) < ((𝑥 ∈ ℤ ↦ 𝐸)‘𝐵) ↔ 𝐶 < 𝐷)) |
113 | 89, 112 | bitrd 268 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ 𝐶 < 𝐷)) |