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	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝐴 ∈ ℝ )
	oddcomabszz.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥 ) → 0 ≤ 𝐴 )
	oddcomabszz.3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℤ ) → 𝐶 = - 𝐵 )
	oddcomabszz.4	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
	oddcomabszz.5	⊢ ( 𝑥 = - 𝑦 → 𝐴 = 𝐶 )
	oddcomabszz.6	⊢ ( 𝑥 = 𝐷 → 𝐴 = 𝐸 )
	oddcomabszz.7	⊢ ( 𝑥 = ( abs ‘ 𝐷 ) → 𝐴 = 𝐹 )
Assertion	oddcomabszz	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ℤ ) → ( abs ‘ 𝐸 ) = 𝐹 )

Proof

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