Step | Hyp | Ref
| Expression |
1 | | eleq1 2838 |
. . . . . 6
⊢ (𝑎 = 𝐷 → (𝑎 ∈ ℤ ↔ 𝐷 ∈ ℤ)) |
2 | 1 | anbi2d 632 |
. . . . 5
⊢ (𝑎 = 𝐷 → ((𝜑 ∧ 𝑎 ∈ ℤ) ↔ (𝜑 ∧ 𝐷 ∈ ℤ))) |
3 | | csbeq1 3804 |
. . . . . . 7
⊢ (𝑎 = 𝐷 → ⦋𝑎 / 𝑥⦌𝐴 = ⦋𝐷 / 𝑥⦌𝐴) |
4 | 3 | fveq2d 6655 |
. . . . . 6
⊢ (𝑎 = 𝐷 → (abs‘⦋𝑎 / 𝑥⦌𝐴) = (abs‘⦋𝐷 / 𝑥⦌𝐴)) |
5 | | fveq2 6651 |
. . . . . . 7
⊢ (𝑎 = 𝐷 → (abs‘𝑎) = (abs‘𝐷)) |
6 | 5 | csbeq1d 3805 |
. . . . . 6
⊢ (𝑎 = 𝐷 → ⦋(abs‘𝑎) / 𝑥⦌𝐴 = ⦋(abs‘𝐷) / 𝑥⦌𝐴) |
7 | 4, 6 | eqeq12d 2775 |
. . . . 5
⊢ (𝑎 = 𝐷 → ((abs‘⦋𝑎 / 𝑥⦌𝐴) = ⦋(abs‘𝑎) / 𝑥⦌𝐴 ↔ (abs‘⦋𝐷 / 𝑥⦌𝐴) = ⦋(abs‘𝐷) / 𝑥⦌𝐴)) |
8 | 2, 7 | imbi12d 349 |
. . . 4
⊢ (𝑎 = 𝐷 → (((𝜑 ∧ 𝑎 ∈ ℤ) →
(abs‘⦋𝑎
/ 𝑥⦌𝐴) =
⦋(abs‘𝑎) / 𝑥⦌𝐴) ↔ ((𝜑 ∧ 𝐷 ∈ ℤ) →
(abs‘⦋𝐷
/ 𝑥⦌𝐴) =
⦋(abs‘𝐷) / 𝑥⦌𝐴))) |
9 | | nfv 1916 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ℤ) |
10 | | nfcsb1v 3825 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑎 / 𝑥⦌𝐴 |
11 | 10 | nfel1 2933 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑎 / 𝑥⦌𝐴 ∈ ℝ |
12 | 9, 11 | nfim 1898 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ℤ) → ⦋𝑎 / 𝑥⦌𝐴 ∈ ℝ) |
13 | | eleq1 2838 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (𝑥 ∈ ℤ ↔ 𝑎 ∈ ℤ)) |
14 | 13 | anbi2d 632 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → ((𝜑 ∧ 𝑥 ∈ ℤ) ↔ (𝜑 ∧ 𝑎 ∈ ℤ))) |
15 | | csbeq1a 3815 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → 𝐴 = ⦋𝑎 / 𝑥⦌𝐴) |
16 | 15 | eleq1d 2835 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (𝐴 ∈ ℝ ↔ ⦋𝑎 / 𝑥⦌𝐴 ∈ ℝ)) |
17 | 14, 16 | imbi12d 349 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐴 ∈ ℝ) ↔ ((𝜑 ∧ 𝑎 ∈ ℤ) → ⦋𝑎 / 𝑥⦌𝐴 ∈ ℝ))) |
18 | | oddcomabszz.1 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐴 ∈ ℝ) |
19 | 12, 17, 18 | chvarfv 2241 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → ⦋𝑎 / 𝑥⦌𝐴 ∈ ℝ) |
20 | 19 | adantr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 0 ≤ 𝑎) → ⦋𝑎 / 𝑥⦌𝐴 ∈ ℝ) |
21 | | nfv 1916 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎) |
22 | | nfcv 2917 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥0 |
23 | | nfcv 2917 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥
≤ |
24 | 22, 23, 10 | nfbr 5072 |
. . . . . . . . . 10
⊢
Ⅎ𝑥0 ≤
⦋𝑎 / 𝑥⦌𝐴 |
25 | 21, 24 | nfim 1898 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎) → 0 ≤
⦋𝑎 / 𝑥⦌𝐴) |
26 | | breq2 5029 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (0 ≤ 𝑥 ↔ 0 ≤ 𝑎)) |
27 | 13, 26 | 3anbi23d 1437 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → ((𝜑 ∧ 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥) ↔ (𝜑 ∧ 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎))) |
28 | 15 | breq2d 5037 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (0 ≤ 𝐴 ↔ 0 ≤ ⦋𝑎 / 𝑥⦌𝐴)) |
29 | 27, 28 | imbi12d 349 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥) → 0 ≤ 𝐴) ↔ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎) → 0 ≤
⦋𝑎 / 𝑥⦌𝐴))) |
30 | | oddcomabszz.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥) → 0 ≤ 𝐴) |
31 | 25, 29, 30 | chvarfv 2241 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎) → 0 ≤
⦋𝑎 / 𝑥⦌𝐴) |
32 | 31 | 3expa 1116 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 0 ≤ 𝑎) → 0 ≤
⦋𝑎 / 𝑥⦌𝐴) |
33 | 20, 32 | absidd 14815 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 0 ≤ 𝑎) →
(abs‘⦋𝑎
/ 𝑥⦌𝐴) = ⦋𝑎 / 𝑥⦌𝐴) |
34 | | zre 12009 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℝ) |
35 | 34 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 0 ≤ 𝑎) → 𝑎 ∈ ℝ) |
36 | | absid 14689 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℝ ∧ 0 ≤
𝑎) → (abs‘𝑎) = 𝑎) |
37 | 35, 36 | sylancom 592 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 0 ≤ 𝑎) → (abs‘𝑎) = 𝑎) |
38 | 37 | csbeq1d 3805 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 0 ≤ 𝑎) →
⦋(abs‘𝑎) / 𝑥⦌𝐴 = ⦋𝑎 / 𝑥⦌𝐴) |
39 | 33, 38 | eqtr4d 2797 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 0 ≤ 𝑎) →
(abs‘⦋𝑎
/ 𝑥⦌𝐴) =
⦋(abs‘𝑎) / 𝑥⦌𝐴) |
40 | | nfv 1916 |
. . . . . . . 8
⊢
Ⅎ𝑦((𝜑 ∧ 𝑎 ∈ ℤ) → ⦋-𝑎 / 𝑥⦌𝐴 = -⦋𝑎 / 𝑥⦌𝐴) |
41 | | eleq1 2838 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑎 → (𝑦 ∈ ℤ ↔ 𝑎 ∈ ℤ)) |
42 | 41 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑦 = 𝑎 → ((𝜑 ∧ 𝑦 ∈ ℤ) ↔ (𝜑 ∧ 𝑎 ∈ ℤ))) |
43 | | negex 10907 |
. . . . . . . . . . . 12
⊢ -𝑦 ∈ V |
44 | | oddcomabszz.5 |
. . . . . . . . . . . 12
⊢ (𝑥 = -𝑦 → 𝐴 = 𝐶) |
45 | 43, 44 | csbie 3836 |
. . . . . . . . . . 11
⊢
⦋-𝑦 /
𝑥⦌𝐴 = 𝐶 |
46 | | negeq 10901 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑎 → -𝑦 = -𝑎) |
47 | 46 | csbeq1d 3805 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑎 → ⦋-𝑦 / 𝑥⦌𝐴 = ⦋-𝑎 / 𝑥⦌𝐴) |
48 | 45, 47 | syl5eqr 2808 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑎 → 𝐶 = ⦋-𝑎 / 𝑥⦌𝐴) |
49 | | vex 3411 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
50 | | oddcomabszz.4 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) |
51 | 49, 50 | csbie 3836 |
. . . . . . . . . . . 12
⊢
⦋𝑦 /
𝑥⦌𝐴 = 𝐵 |
52 | | csbeq1 3804 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑎 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑎 / 𝑥⦌𝐴) |
53 | 51, 52 | syl5eqr 2808 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑎 → 𝐵 = ⦋𝑎 / 𝑥⦌𝐴) |
54 | 53 | negeqd 10903 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑎 → -𝐵 = -⦋𝑎 / 𝑥⦌𝐴) |
55 | 48, 54 | eqeq12d 2775 |
. . . . . . . . 9
⊢ (𝑦 = 𝑎 → (𝐶 = -𝐵 ↔ ⦋-𝑎 / 𝑥⦌𝐴 = -⦋𝑎 / 𝑥⦌𝐴)) |
56 | 42, 55 | imbi12d 349 |
. . . . . . . 8
⊢ (𝑦 = 𝑎 → (((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐶 = -𝐵) ↔ ((𝜑 ∧ 𝑎 ∈ ℤ) → ⦋-𝑎 / 𝑥⦌𝐴 = -⦋𝑎 / 𝑥⦌𝐴))) |
57 | | oddcomabszz.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐶 = -𝐵) |
58 | 40, 56, 57 | chvarfv 2241 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → ⦋-𝑎 / 𝑥⦌𝐴 = -⦋𝑎 / 𝑥⦌𝐴) |
59 | 58 | adantr 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≤ 0) → ⦋-𝑎 / 𝑥⦌𝐴 = -⦋𝑎 / 𝑥⦌𝐴) |
60 | 34 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≤ 0) → 𝑎 ∈ ℝ) |
61 | | absnid 14691 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ≤ 0) → (abs‘𝑎) = -𝑎) |
62 | 60, 61 | sylancom 592 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≤ 0) → (abs‘𝑎) = -𝑎) |
63 | 62 | csbeq1d 3805 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≤ 0) →
⦋(abs‘𝑎) / 𝑥⦌𝐴 = ⦋-𝑎 / 𝑥⦌𝐴) |
64 | 19 | adantr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≤ 0) → ⦋𝑎 / 𝑥⦌𝐴 ∈ ℝ) |
65 | | znegcl 12041 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℤ → -𝑎 ∈
ℤ) |
66 | | nfv 1916 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝜑 ∧ -𝑎 ∈ ℤ ∧ 0 ≤ -𝑎) |
67 | | nfcsb1v 3825 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥⦋-𝑎 / 𝑥⦌𝐴 |
68 | 22, 23, 67 | nfbr 5072 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥0 ≤
⦋-𝑎 / 𝑥⦌𝐴 |
69 | 66, 68 | nfim 1898 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥((𝜑 ∧ -𝑎 ∈ ℤ ∧ 0 ≤ -𝑎) → 0 ≤
⦋-𝑎 / 𝑥⦌𝐴) |
70 | | negex 10907 |
. . . . . . . . . . . . 13
⊢ -𝑎 ∈ V |
71 | | eleq1 2838 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = -𝑎 → (𝑥 ∈ ℤ ↔ -𝑎 ∈ ℤ)) |
72 | | breq2 5029 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = -𝑎 → (0 ≤ 𝑥 ↔ 0 ≤ -𝑎)) |
73 | 71, 72 | 3anbi23d 1437 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = -𝑎 → ((𝜑 ∧ 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥) ↔ (𝜑 ∧ -𝑎 ∈ ℤ ∧ 0 ≤ -𝑎))) |
74 | | csbeq1a 3815 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = -𝑎 → 𝐴 = ⦋-𝑎 / 𝑥⦌𝐴) |
75 | 74 | breq2d 5037 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = -𝑎 → (0 ≤ 𝐴 ↔ 0 ≤ ⦋-𝑎 / 𝑥⦌𝐴)) |
76 | 73, 75 | imbi12d 349 |
. . . . . . . . . . . . 13
⊢ (𝑥 = -𝑎 → (((𝜑 ∧ 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥) → 0 ≤ 𝐴) ↔ ((𝜑 ∧ -𝑎 ∈ ℤ ∧ 0 ≤ -𝑎) → 0 ≤
⦋-𝑎 / 𝑥⦌𝐴))) |
77 | 69, 70, 76, 30 | vtoclf 3474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ -𝑎 ∈ ℤ ∧ 0 ≤ -𝑎) → 0 ≤
⦋-𝑎 / 𝑥⦌𝐴) |
78 | 77 | 3expia 1119 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ -𝑎 ∈ ℤ) → (0 ≤ -𝑎 → 0 ≤
⦋-𝑎 / 𝑥⦌𝐴)) |
79 | 65, 78 | sylan2 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (0 ≤ -𝑎 → 0 ≤
⦋-𝑎 / 𝑥⦌𝐴)) |
80 | 58 | breq2d 5037 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (0 ≤
⦋-𝑎 / 𝑥⦌𝐴 ↔ 0 ≤ -⦋𝑎 / 𝑥⦌𝐴)) |
81 | 79, 80 | sylibd 242 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (0 ≤ -𝑎 → 0 ≤
-⦋𝑎 / 𝑥⦌𝐴)) |
82 | 34 | adantl 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → 𝑎 ∈ ℝ) |
83 | 82 | le0neg1d 11234 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (𝑎 ≤ 0 ↔ 0 ≤ -𝑎)) |
84 | 19 | le0neg1d 11234 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (⦋𝑎 / 𝑥⦌𝐴 ≤ 0 ↔ 0 ≤ -⦋𝑎 / 𝑥⦌𝐴)) |
85 | 81, 83, 84 | 3imtr4d 298 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (𝑎 ≤ 0 → ⦋𝑎 / 𝑥⦌𝐴 ≤ 0)) |
86 | 85 | imp 411 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≤ 0) → ⦋𝑎 / 𝑥⦌𝐴 ≤ 0) |
87 | 64, 86 | absnidd 14806 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≤ 0) →
(abs‘⦋𝑎
/ 𝑥⦌𝐴) = -⦋𝑎 / 𝑥⦌𝐴) |
88 | 59, 63, 87 | 3eqtr4rd 2805 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≤ 0) →
(abs‘⦋𝑎
/ 𝑥⦌𝐴) =
⦋(abs‘𝑎) / 𝑥⦌𝐴) |
89 | | 0re 10666 |
. . . . . . 7
⊢ 0 ∈
ℝ |
90 | | letric 10763 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ 𝑎
∈ ℝ) → (0 ≤ 𝑎 ∨ 𝑎 ≤ 0)) |
91 | 89, 34, 90 | sylancr 591 |
. . . . . 6
⊢ (𝑎 ∈ ℤ → (0 ≤
𝑎 ∨ 𝑎 ≤ 0)) |
92 | 91 | adantl 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (0 ≤ 𝑎 ∨ 𝑎 ≤ 0)) |
93 | 39, 88, 92 | mpjaodan 957 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) →
(abs‘⦋𝑎
/ 𝑥⦌𝐴) =
⦋(abs‘𝑎) / 𝑥⦌𝐴) |
94 | 8, 93 | vtoclg 3483 |
. . 3
⊢ (𝐷 ∈ ℤ → ((𝜑 ∧ 𝐷 ∈ ℤ) →
(abs‘⦋𝐷
/ 𝑥⦌𝐴) =
⦋(abs‘𝐷) / 𝑥⦌𝐴)) |
95 | 94 | anabsi7 671 |
. 2
⊢ ((𝜑 ∧ 𝐷 ∈ ℤ) →
(abs‘⦋𝐷
/ 𝑥⦌𝐴) =
⦋(abs‘𝐷) / 𝑥⦌𝐴) |
96 | | nfcvd 2918 |
. . . . 5
⊢ (𝐷 ∈ ℤ →
Ⅎ𝑥𝐸) |
97 | | oddcomabszz.6 |
. . . . 5
⊢ (𝑥 = 𝐷 → 𝐴 = 𝐸) |
98 | 96, 97 | csbiegf 3834 |
. . . 4
⊢ (𝐷 ∈ ℤ →
⦋𝐷 / 𝑥⦌𝐴 = 𝐸) |
99 | 98 | fveq2d 6655 |
. . 3
⊢ (𝐷 ∈ ℤ →
(abs‘⦋𝐷
/ 𝑥⦌𝐴) = (abs‘𝐸)) |
100 | 99 | adantl 486 |
. 2
⊢ ((𝜑 ∧ 𝐷 ∈ ℤ) →
(abs‘⦋𝐷
/ 𝑥⦌𝐴) = (abs‘𝐸)) |
101 | | fvex 6664 |
. . . 4
⊢
(abs‘𝐷) ∈
V |
102 | | oddcomabszz.7 |
. . . 4
⊢ (𝑥 = (abs‘𝐷) → 𝐴 = 𝐹) |
103 | 101, 102 | csbie 3836 |
. . 3
⊢
⦋(abs‘𝐷) / 𝑥⦌𝐴 = 𝐹 |
104 | 103 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝐷 ∈ ℤ) →
⦋(abs‘𝐷) / 𝑥⦌𝐴 = 𝐹) |
105 | 95, 100, 104 | 3eqtr3d 2802 |
1
⊢ ((𝜑 ∧ 𝐷 ∈ ℤ) → (abs‘𝐸) = 𝐹) |