Metamath Proof Explorer

Theorem oddcomabszz

Description: An odd function which takes nonnegative values on nonnegative arguments commutes with abs . (Contributed by Stefan O'Rear, 26-Sep-2014)

Ref Expression
Hypotheses oddcomabszz.1 ⊢ φ ∧ x ∈ ℤ → A ∈ ℝ
oddcomabszz.2 ⊢ φ ∧ x ∈ ℤ ∧ 0 ≤ x → 0 ≤ A
oddcomabszz.3 ⊢ φ ∧ y ∈ ℤ → C = − B
oddcomabszz.4 ⊢ x = y → A = B
oddcomabszz.5 ⊢ x = − y → A = C
oddcomabszz.6 ⊢ x = D → A = E
oddcomabszz.7 ⊢ x = D → A = F
Assertion oddcomabszz ⊢ φ ∧ D ∈ ℤ → E = F

Proof

Step Hyp Ref Expression
1 oddcomabszz.1 ⊢ φ ∧ x ∈ ℤ → A ∈ ℝ
2 oddcomabszz.2 ⊢ φ ∧ x ∈ ℤ ∧ 0 ≤ x → 0 ≤ A
3 oddcomabszz.3 ⊢ φ ∧ y ∈ ℤ → C = − B
4 oddcomabszz.4 ⊢ x = y → A = B
5 oddcomabszz.5 ⊢ x = − y → A = C
6 oddcomabszz.6 ⊢ x = D → A = E
7 oddcomabszz.7 ⊢ x = D → A = F
8 eleq1 ⊢ a = D → a ∈ ℤ ↔ D ∈ ℤ
9 8 anbi2d ⊢ a = D → φ ∧ a ∈ ℤ ↔ φ ∧ D ∈ ℤ
10 csbeq1 ⊢ a = D → ⦋ a / x⦌ A = ⦋ D / x⦌ A
11 10 fveq2d ⊢ a = D → ⦋ a / x⦌ A = ⦋ D / x⦌ A
12 fveq2 ⊢ a = D → a = D
13 12 csbeq1d ⊢ a = D → ⦋ a / x⦌ A = ⦋ D / x⦌ A
14 11 13 eqeq12d ⊢ a = D → ⦋ a / x⦌ A = ⦋ a / x⦌ A ↔ ⦋ D / x⦌ A = ⦋ D / x⦌ A
15 9 14 imbi12d ⊢ a = D → φ ∧ a ∈ ℤ → ⦋ a / x⦌ A = ⦋ a / x⦌ A ↔ φ ∧ D ∈ ℤ → ⦋ D / x⦌ A = ⦋ D / x⦌ A
16 nfv ⊢ Ⅎ x φ ∧ a ∈ ℤ
17 nfcsb1v ⊢ Ⅎ _ x ⦋ a / x⦌ A
18 17 nfel1 ⊢ Ⅎ x ⦋ a / x⦌ A ∈ ℝ
19 16 18 nfim ⊢ Ⅎ x φ ∧ a ∈ ℤ → ⦋ a / x⦌ A ∈ ℝ
20 eleq1 ⊢ x = a → x ∈ ℤ ↔ a ∈ ℤ
21 20 anbi2d ⊢ x = a → φ ∧ x ∈ ℤ ↔ φ ∧ a ∈ ℤ
22 csbeq1a ⊢ x = a → A = ⦋ a / x⦌ A
23 22 eleq1d ⊢ x = a → A ∈ ℝ ↔ ⦋ a / x⦌ A ∈ ℝ
24 21 23 imbi12d ⊢ x = a → φ ∧ x ∈ ℤ → A ∈ ℝ ↔ φ ∧ a ∈ ℤ → ⦋ a / x⦌ A ∈ ℝ
25 19 24 1 chvarfv ⊢ φ ∧ a ∈ ℤ → ⦋ a / x⦌ A ∈ ℝ
26 25 adantr ⊢ φ ∧ a ∈ ℤ ∧ 0 ≤ a → ⦋ a / x⦌ A ∈ ℝ
27 nfv ⊢ Ⅎ x φ ∧ a ∈ ℤ ∧ 0 ≤ a
28 nfcv ⊢ Ⅎ _ x 0
29 nfcv ⊢ Ⅎ _ x ≤
30 28 29 17 nfbr ⊢ Ⅎ x 0 ≤ ⦋ a / x⦌ A
31 27 30 nfim ⊢ Ⅎ x φ ∧ a ∈ ℤ ∧ 0 ≤ a → 0 ≤ ⦋ a / x⦌ A
32 breq2 ⊢ x = a → 0 ≤ x ↔ 0 ≤ a
33 20 32 3anbi23d ⊢ x = a → φ ∧ x ∈ ℤ ∧ 0 ≤ x ↔ φ ∧ a ∈ ℤ ∧ 0 ≤ a
34 22 breq2d ⊢ x = a → 0 ≤ A ↔ 0 ≤ ⦋ a / x⦌ A
35 33 34 imbi12d ⊢ x = a → φ ∧ x ∈ ℤ ∧ 0 ≤ x → 0 ≤ A ↔ φ ∧ a ∈ ℤ ∧ 0 ≤ a → 0 ≤ ⦋ a / x⦌ A
36 31 35 2 chvarfv ⊢ φ ∧ a ∈ ℤ ∧ 0 ≤ a → 0 ≤ ⦋ a / x⦌ A
37 36 3expa ⊢ φ ∧ a ∈ ℤ ∧ 0 ≤ a → 0 ≤ ⦋ a / x⦌ A
38 26 37 absidd ⊢ φ ∧ a ∈ ℤ ∧ 0 ≤ a → ⦋ a / x⦌ A = ⦋ a / x⦌ A
39 zre ⊢ a ∈ ℤ → a ∈ ℝ
40 39 ad2antlr ⊢ φ ∧ a ∈ ℤ ∧ 0 ≤ a → a ∈ ℝ
41 absid ⊢ a ∈ ℝ ∧ 0 ≤ a → a = a
42 40 41 sylancom ⊢ φ ∧ a ∈ ℤ ∧ 0 ≤ a → a = a
43 42 csbeq1d ⊢ φ ∧ a ∈ ℤ ∧ 0 ≤ a → ⦋ a / x⦌ A = ⦋ a / x⦌ A
44 38 43 eqtr4d ⊢ φ ∧ a ∈ ℤ ∧ 0 ≤ a → ⦋ a / x⦌ A = ⦋ a / x⦌ A
45 nfv ⊢ Ⅎ y φ ∧ a ∈ ℤ → ⦋ − a / x⦌ A = − ⦋ a / x⦌ A
46 eleq1 ⊢ y = a → y ∈ ℤ ↔ a ∈ ℤ
47 46 anbi2d ⊢ y = a → φ ∧ y ∈ ℤ ↔ φ ∧ a ∈ ℤ
48 negex ⊢ − y ∈ V
49 48 5 csbie ⊢ ⦋ − y / x⦌ A = C
50 negeq ⊢ y = a → − y = − a
51 50 csbeq1d ⊢ y = a → ⦋ − y / x⦌ A = ⦋ − a / x⦌ A
52 49 51 eqtr3id ⊢ y = a → C = ⦋ − a / x⦌ A
53 vex ⊢ y ∈ V
54 53 4 csbie ⊢ ⦋ y / x⦌ A = B
55 csbeq1 ⊢ y = a → ⦋ y / x⦌ A = ⦋ a / x⦌ A
56 54 55 eqtr3id ⊢ y = a → B = ⦋ a / x⦌ A
57 56 negeqd ⊢ y = a → − B = − ⦋ a / x⦌ A
58 52 57 eqeq12d ⊢ y = a → C = − B ↔ ⦋ − a / x⦌ A = − ⦋ a / x⦌ A
59 47 58 imbi12d ⊢ y = a → φ ∧ y ∈ ℤ → C = − B ↔ φ ∧ a ∈ ℤ → ⦋ − a / x⦌ A = − ⦋ a / x⦌ A
60 45 59 3 chvarfv ⊢ φ ∧ a ∈ ℤ → ⦋ − a / x⦌ A = − ⦋ a / x⦌ A
61 60 adantr ⊢ φ ∧ a ∈ ℤ ∧ a ≤ 0 → ⦋ − a / x⦌ A = − ⦋ a / x⦌ A
62 39 ad2antlr ⊢ φ ∧ a ∈ ℤ ∧ a ≤ 0 → a ∈ ℝ
63 absnid ⊢ a ∈ ℝ ∧ a ≤ 0 → a = − a
64 62 63 sylancom ⊢ φ ∧ a ∈ ℤ ∧ a ≤ 0 → a = − a
65 64 csbeq1d ⊢ φ ∧ a ∈ ℤ ∧ a ≤ 0 → ⦋ a / x⦌ A = ⦋ − a / x⦌ A
66 25 adantr ⊢ φ ∧ a ∈ ℤ ∧ a ≤ 0 → ⦋ a / x⦌ A ∈ ℝ
67 znegcl ⊢ a ∈ ℤ → − a ∈ ℤ
68 nfv ⊢ Ⅎ x φ ∧ − a ∈ ℤ ∧ 0 ≤ − a
69 nfcsb1v ⊢ Ⅎ _ x ⦋ − a / x⦌ A
70 28 29 69 nfbr ⊢ Ⅎ x 0 ≤ ⦋ − a / x⦌ A
71 68 70 nfim ⊢ Ⅎ x φ ∧ − a ∈ ℤ ∧ 0 ≤ − a → 0 ≤ ⦋ − a / x⦌ A
72 negex ⊢ − a ∈ V
73 eleq1 ⊢ x = − a → x ∈ ℤ ↔ − a ∈ ℤ
74 breq2 ⊢ x = − a → 0 ≤ x ↔ 0 ≤ − a
75 73 74 3anbi23d ⊢ x = − a → φ ∧ x ∈ ℤ ∧ 0 ≤ x ↔ φ ∧ − a ∈ ℤ ∧ 0 ≤ − a
76 csbeq1a ⊢ x = − a → A = ⦋ − a / x⦌ A
77 76 breq2d ⊢ x = − a → 0 ≤ A ↔ 0 ≤ ⦋ − a / x⦌ A
78 75 77 imbi12d ⊢ x = − a → φ ∧ x ∈ ℤ ∧ 0 ≤ x → 0 ≤ A ↔ φ ∧ − a ∈ ℤ ∧ 0 ≤ − a → 0 ≤ ⦋ − a / x⦌ A
79 71 72 78 2 vtoclf ⊢ φ ∧ − a ∈ ℤ ∧ 0 ≤ − a → 0 ≤ ⦋ − a / x⦌ A
80 79 3expia ⊢ φ ∧ − a ∈ ℤ → 0 ≤ − a → 0 ≤ ⦋ − a / x⦌ A
81 67 80 sylan2 ⊢ φ ∧ a ∈ ℤ → 0 ≤ − a → 0 ≤ ⦋ − a / x⦌ A
82 60 breq2d ⊢ φ ∧ a ∈ ℤ → 0 ≤ ⦋ − a / x⦌ A ↔ 0 ≤ − ⦋ a / x⦌ A
83 81 82 sylibd ⊢ φ ∧ a ∈ ℤ → 0 ≤ − a → 0 ≤ − ⦋ a / x⦌ A
84 39 adantl ⊢ φ ∧ a ∈ ℤ → a ∈ ℝ
85 84 le0neg1d ⊢ φ ∧ a ∈ ℤ → a ≤ 0 ↔ 0 ≤ − a
86 25 le0neg1d ⊢ φ ∧ a ∈ ℤ → ⦋ a / x⦌ A ≤ 0 ↔ 0 ≤ − ⦋ a / x⦌ A
87 83 85 86 3imtr4d ⊢ φ ∧ a ∈ ℤ → a ≤ 0 → ⦋ a / x⦌ A ≤ 0
88 87 imp ⊢ φ ∧ a ∈ ℤ ∧ a ≤ 0 → ⦋ a / x⦌ A ≤ 0
89 66 88 absnidd ⊢ φ ∧ a ∈ ℤ ∧ a ≤ 0 → ⦋ a / x⦌ A = − ⦋ a / x⦌ A
90 61 65 89 3eqtr4rd ⊢ φ ∧ a ∈ ℤ ∧ a ≤ 0 → ⦋ a / x⦌ A = ⦋ a / x⦌ A
91 0re ⊢ 0 ∈ ℝ
92 letric ⊢ 0 ∈ ℝ ∧ a ∈ ℝ → 0 ≤ a ∨ a ≤ 0
93 91 39 92 sylancr ⊢ a ∈ ℤ → 0 ≤ a ∨ a ≤ 0
94 93 adantl ⊢ φ ∧ a ∈ ℤ → 0 ≤ a ∨ a ≤ 0
95 44 90 94 mpjaodan ⊢ φ ∧ a ∈ ℤ → ⦋ a / x⦌ A = ⦋ a / x⦌ A
96 15 95 vtoclg ⊢ D ∈ ℤ → φ ∧ D ∈ ℤ → ⦋ D / x⦌ A = ⦋ D / x⦌ A
97 96 anabsi7 ⊢ φ ∧ D ∈ ℤ → ⦋ D / x⦌ A = ⦋ D / x⦌ A
98 nfcvd ⊢ D ∈ ℤ → Ⅎ _ x E
99 98 6 csbiegf ⊢ D ∈ ℤ → ⦋ D / x⦌ A = E
100 99 fveq2d ⊢ D ∈ ℤ → ⦋ D / x⦌ A = E
101 100 adantl ⊢ φ ∧ D ∈ ℤ → ⦋ D / x⦌ A = E
102 fvex ⊢ D ∈ V
103 102 7 csbie ⊢ ⦋ D / x⦌ A = F
104 103 a1i ⊢ φ ∧ D ∈ ℤ → ⦋ D / x⦌ A = F
105 97 101 104 3eqtr3d ⊢ φ ∧ D ∈ ℤ → E = F