Users' Mathboxes Mathbox for Jim Kingdon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  apdifflemf GIF version

Theorem apdifflemf 13346
Description: Lemma for apdiff 13348. Being apart from the point halfway between 𝑄 and 𝑅 suffices for 𝐴 to be a different distance from 𝑄 and from 𝑅. (Contributed by Jim Kingdon, 18-May-2024.)
Hypotheses
Ref Expression
apdifflemf.a (𝜑𝐴 ∈ ℝ)
apdifflemf.q (𝜑𝑄 ∈ ℚ)
apdifflemf.r (𝜑𝑅 ∈ ℚ)
apdifflemf.qr (𝜑𝑄 < 𝑅)
apdifflemf.ap (𝜑 → ((𝑄 + 𝑅) / 2) # 𝐴)
Assertion
Ref Expression
apdifflemf (𝜑 → (abs‘(𝐴𝑄)) # (abs‘(𝐴𝑅)))

Proof of Theorem apdifflemf
StepHypRef Expression
1 apdifflemf.a . . . . . . 7 (𝜑𝐴 ∈ ℝ)
21recnd 7806 . . . . . 6 (𝜑𝐴 ∈ ℂ)
3 apdifflemf.r . . . . . . 7 (𝜑𝑅 ∈ ℚ)
4 qcn 9438 . . . . . . 7 (𝑅 ∈ ℚ → 𝑅 ∈ ℂ)
53, 4syl 14 . . . . . 6 (𝜑𝑅 ∈ ℂ)
62, 5subcld 8085 . . . . 5 (𝜑 → (𝐴𝑅) ∈ ℂ)
76adantr 274 . . . 4 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝐴𝑅) ∈ ℂ)
87abscld 10965 . . 3 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (abs‘(𝐴𝑅)) ∈ ℝ)
9 apdifflemf.q . . . . . . 7 (𝜑𝑄 ∈ ℚ)
10 qcn 9438 . . . . . . 7 (𝑄 ∈ ℚ → 𝑄 ∈ ℂ)
119, 10syl 14 . . . . . 6 (𝜑𝑄 ∈ ℂ)
122, 11subcld 8085 . . . . 5 (𝜑 → (𝐴𝑄) ∈ ℂ)
1312abscld 10965 . . . 4 (𝜑 → (abs‘(𝐴𝑄)) ∈ ℝ)
1413adantr 274 . . 3 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (abs‘(𝐴𝑄)) ∈ ℝ)
15 qre 9429 . . . . . . . . . 10 (𝑄 ∈ ℚ → 𝑄 ∈ ℝ)
169, 15syl 14 . . . . . . . . 9 (𝜑𝑄 ∈ ℝ)
1716adantr 274 . . . . . . . 8 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑄 ∈ ℝ)
181adantr 274 . . . . . . . 8 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝐴 ∈ ℝ)
19 qaddcl 9439 . . . . . . . . . . . . . 14 ((𝑄 ∈ ℚ ∧ 𝑅 ∈ ℚ) → (𝑄 + 𝑅) ∈ ℚ)
209, 3, 19syl2anc 408 . . . . . . . . . . . . 13 (𝜑 → (𝑄 + 𝑅) ∈ ℚ)
21 qre 9429 . . . . . . . . . . . . 13 ((𝑄 + 𝑅) ∈ ℚ → (𝑄 + 𝑅) ∈ ℝ)
2220, 21syl 14 . . . . . . . . . . . 12 (𝜑 → (𝑄 + 𝑅) ∈ ℝ)
2322rehalfcld 8978 . . . . . . . . . . 11 (𝜑 → ((𝑄 + 𝑅) / 2) ∈ ℝ)
2423adantr 274 . . . . . . . . . 10 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → ((𝑄 + 𝑅) / 2) ∈ ℝ)
25 apdifflemf.qr . . . . . . . . . . . 12 (𝜑𝑄 < 𝑅)
26 qre 9429 . . . . . . . . . . . . . 14 (𝑅 ∈ ℚ → 𝑅 ∈ ℝ)
273, 26syl 14 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ ℝ)
28 avglt1 8970 . . . . . . . . . . . . 13 ((𝑄 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑄 < 𝑅𝑄 < ((𝑄 + 𝑅) / 2)))
2916, 27, 28syl2anc 408 . . . . . . . . . . . 12 (𝜑 → (𝑄 < 𝑅𝑄 < ((𝑄 + 𝑅) / 2)))
3025, 29mpbid 146 . . . . . . . . . . 11 (𝜑𝑄 < ((𝑄 + 𝑅) / 2))
3130adantr 274 . . . . . . . . . 10 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑄 < ((𝑄 + 𝑅) / 2))
32 simpr 109 . . . . . . . . . 10 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → ((𝑄 + 𝑅) / 2) < 𝐴)
3317, 24, 18, 31, 32lttrd 7900 . . . . . . . . 9 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑄 < 𝐴)
3417, 18, 33ltled 7893 . . . . . . . 8 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑄𝐴)
3517, 18, 34abssubge0d 10960 . . . . . . 7 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (abs‘(𝐴𝑄)) = (𝐴𝑄))
3635oveq2d 5790 . . . . . 6 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 − (abs‘(𝐴𝑄))) = (𝑅 − (𝐴𝑄)))
375adantr 274 . . . . . . 7 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑅 ∈ ℂ)
382adantr 274 . . . . . . 7 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝐴 ∈ ℂ)
3911adantr 274 . . . . . . 7 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑄 ∈ ℂ)
4037, 38, 39subsub3d 8115 . . . . . 6 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 − (𝐴𝑄)) = ((𝑅 + 𝑄) − 𝐴))
4137, 39addcomd 7925 . . . . . . 7 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 + 𝑄) = (𝑄 + 𝑅))
4241oveq1d 5789 . . . . . 6 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → ((𝑅 + 𝑄) − 𝐴) = ((𝑄 + 𝑅) − 𝐴))
4336, 40, 423eqtrd 2176 . . . . 5 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 − (abs‘(𝐴𝑄))) = ((𝑄 + 𝑅) − 𝐴))
4422adantr 274 . . . . . . . . 9 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑄 + 𝑅) ∈ ℝ)
45 2rp 9458 . . . . . . . . . 10 2 ∈ ℝ+
4645a1i 9 . . . . . . . . 9 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 2 ∈ ℝ+)
4744, 18, 46ltdivmuld 9547 . . . . . . . 8 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (((𝑄 + 𝑅) / 2) < 𝐴 ↔ (𝑄 + 𝑅) < (2 · 𝐴)))
4832, 47mpbid 146 . . . . . . 7 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑄 + 𝑅) < (2 · 𝐴))
49382timesd 8974 . . . . . . 7 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (2 · 𝐴) = (𝐴 + 𝐴))
5048, 49breqtrd 3954 . . . . . 6 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑄 + 𝑅) < (𝐴 + 𝐴))
5144, 18, 18ltsubaddd 8315 . . . . . 6 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (((𝑄 + 𝑅) − 𝐴) < 𝐴 ↔ (𝑄 + 𝑅) < (𝐴 + 𝐴)))
5250, 51mpbird 166 . . . . 5 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → ((𝑄 + 𝑅) − 𝐴) < 𝐴)
5343, 52eqbrtrd 3950 . . . 4 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 − (abs‘(𝐴𝑄))) < 𝐴)
5425adantr 274 . . . . . . 7 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑄 < 𝑅)
5527adantr 274 . . . . . . . 8 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑅 ∈ ℝ)
56 difrp 9492 . . . . . . . 8 ((𝑄 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑄 < 𝑅 ↔ (𝑅𝑄) ∈ ℝ+))
5717, 55, 56syl2anc 408 . . . . . . 7 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑄 < 𝑅 ↔ (𝑅𝑄) ∈ ℝ+))
5854, 57mpbid 146 . . . . . 6 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅𝑄) ∈ ℝ+)
5918, 58ltaddrpd 9529 . . . . 5 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝐴 < (𝐴 + (𝑅𝑄)))
6035oveq2d 5790 . . . . . 6 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 + (abs‘(𝐴𝑄))) = (𝑅 + (𝐴𝑄)))
6137, 38, 39addsub12d 8108 . . . . . 6 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 + (𝐴𝑄)) = (𝐴 + (𝑅𝑄)))
6260, 61eqtrd 2172 . . . . 5 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 + (abs‘(𝐴𝑄))) = (𝐴 + (𝑅𝑄)))
6359, 62breqtrrd 3956 . . . 4 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝐴 < (𝑅 + (abs‘(𝐴𝑄))))
6418, 55, 14absdifltd 10962 . . . 4 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → ((abs‘(𝐴𝑅)) < (abs‘(𝐴𝑄)) ↔ ((𝑅 − (abs‘(𝐴𝑄))) < 𝐴𝐴 < (𝑅 + (abs‘(𝐴𝑄))))))
6553, 63, 64mpbir2and 928 . . 3 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (abs‘(𝐴𝑅)) < (abs‘(𝐴𝑄)))
668, 14, 65gtapd 8411 . 2 ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (abs‘(𝐴𝑄)) # (abs‘(𝐴𝑅)))
6713adantr 274 . . 3 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → (abs‘(𝐴𝑄)) ∈ ℝ)
686adantr 274 . . . 4 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → (𝐴𝑅) ∈ ℂ)
6968abscld 10965 . . 3 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → (abs‘(𝐴𝑅)) ∈ ℝ)
7011, 5, 2subsubd 8113 . . . . . . 7 (𝜑 → (𝑄 − (𝑅𝐴)) = ((𝑄𝑅) + 𝐴))
7116, 27sublt0d 8344 . . . . . . . . 9 (𝜑 → ((𝑄𝑅) < 0 ↔ 𝑄 < 𝑅))
7225, 71mpbird 166 . . . . . . . 8 (𝜑 → (𝑄𝑅) < 0)
7316, 27resubcld 8155 . . . . . . . . 9 (𝜑 → (𝑄𝑅) ∈ ℝ)
74 ltaddnegr 8199 . . . . . . . . 9 (((𝑄𝑅) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑄𝑅) < 0 ↔ ((𝑄𝑅) + 𝐴) < 𝐴))
7573, 1, 74syl2anc 408 . . . . . . . 8 (𝜑 → ((𝑄𝑅) < 0 ↔ ((𝑄𝑅) + 𝐴) < 𝐴))
7672, 75mpbid 146 . . . . . . 7 (𝜑 → ((𝑄𝑅) + 𝐴) < 𝐴)
7770, 76eqbrtrd 3950 . . . . . 6 (𝜑 → (𝑄 − (𝑅𝐴)) < 𝐴)
7877adantr 274 . . . . 5 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → (𝑄 − (𝑅𝐴)) < 𝐴)
791adantr 274 . . . . . . . 8 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → 𝐴 ∈ ℝ)
8022adantr 274 . . . . . . . 8 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → (𝑄 + 𝑅) ∈ ℝ)
81 simpr 109 . . . . . . . 8 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → 𝐴 < ((𝑄 + 𝑅) / 2))
8279, 79, 80, 81, 81lt2halvesd 8979 . . . . . . 7 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → (𝐴 + 𝐴) < (𝑄 + 𝑅))
8379, 79, 80ltaddsub2d 8320 . . . . . . 7 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → ((𝐴 + 𝐴) < (𝑄 + 𝑅) ↔ 𝐴 < ((𝑄 + 𝑅) − 𝐴)))
8482, 83mpbid 146 . . . . . 6 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → 𝐴 < ((𝑄 + 𝑅) − 𝐴))
8511adantr 274 . . . . . . 7 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → 𝑄 ∈ ℂ)
865adantr 274 . . . . . . 7 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → 𝑅 ∈ ℂ)
872adantr 274 . . . . . . 7 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → 𝐴 ∈ ℂ)
8885, 86, 87addsubassd 8105 . . . . . 6 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → ((𝑄 + 𝑅) − 𝐴) = (𝑄 + (𝑅𝐴)))
8984, 88breqtrd 3954 . . . . 5 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → 𝐴 < (𝑄 + (𝑅𝐴)))
9016adantr 274 . . . . . 6 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → 𝑄 ∈ ℝ)
9127adantr 274 . . . . . . 7 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → 𝑅 ∈ ℝ)
9291, 79resubcld 8155 . . . . . 6 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → (𝑅𝐴) ∈ ℝ)
9379, 90, 92absdifltd 10962 . . . . 5 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → ((abs‘(𝐴𝑄)) < (𝑅𝐴) ↔ ((𝑄 − (𝑅𝐴)) < 𝐴𝐴 < (𝑄 + (𝑅𝐴)))))
9478, 89, 93mpbir2and 928 . . . 4 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → (abs‘(𝐴𝑄)) < (𝑅𝐴))
9523adantr 274 . . . . . . 7 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → ((𝑄 + 𝑅) / 2) ∈ ℝ)
96 avglt2 8971 . . . . . . . . . 10 ((𝑄 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑄 < 𝑅 ↔ ((𝑄 + 𝑅) / 2) < 𝑅))
9716, 27, 96syl2anc 408 . . . . . . . . 9 (𝜑 → (𝑄 < 𝑅 ↔ ((𝑄 + 𝑅) / 2) < 𝑅))
9825, 97mpbid 146 . . . . . . . 8 (𝜑 → ((𝑄 + 𝑅) / 2) < 𝑅)
9998adantr 274 . . . . . . 7 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → ((𝑄 + 𝑅) / 2) < 𝑅)
10079, 95, 91, 81, 99lttrd 7900 . . . . . 6 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → 𝐴 < 𝑅)
10179, 91, 100ltled 7893 . . . . 5 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → 𝐴𝑅)
10279, 91, 101abssuble0d 10961 . . . 4 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → (abs‘(𝐴𝑅)) = (𝑅𝐴))
10394, 102breqtrrd 3956 . . 3 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → (abs‘(𝐴𝑄)) < (abs‘(𝐴𝑅)))
10467, 69, 103ltapd 8412 . 2 ((𝜑𝐴 < ((𝑄 + 𝑅) / 2)) → (abs‘(𝐴𝑄)) # (abs‘(𝐴𝑅)))
105 apdifflemf.ap . . 3 (𝜑 → ((𝑄 + 𝑅) / 2) # 𝐴)
106 reaplt 8362 . . . 4 ((((𝑄 + 𝑅) / 2) ∈ ℝ ∧ 𝐴 ∈ ℝ) → (((𝑄 + 𝑅) / 2) # 𝐴 ↔ (((𝑄 + 𝑅) / 2) < 𝐴𝐴 < ((𝑄 + 𝑅) / 2))))
10723, 1, 106syl2anc 408 . . 3 (𝜑 → (((𝑄 + 𝑅) / 2) # 𝐴 ↔ (((𝑄 + 𝑅) / 2) < 𝐴𝐴 < ((𝑄 + 𝑅) / 2))))
108105, 107mpbid 146 . 2 (𝜑 → (((𝑄 + 𝑅) / 2) < 𝐴𝐴 < ((𝑄 + 𝑅) / 2)))
10966, 104, 108mpjaodan 787 1 (𝜑 → (abs‘(𝐴𝑄)) # (abs‘(𝐴𝑅)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wo 697  wcel 1480   class class class wbr 3929  cfv 5123  (class class class)co 5774  cc 7630  cr 7631  0cc0 7632   + caddc 7635   · cmul 7637   < clt 7812  cmin 7945   # cap 8355   / cdiv 8444  2c2 8783  cq 9423  +crp 9453  abscabs 10781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7723  ax-resscn 7724  ax-1cn 7725  ax-1re 7726  ax-icn 7727  ax-addcl 7728  ax-addrcl 7729  ax-mulcl 7730  ax-mulrcl 7731  ax-addcom 7732  ax-mulcom 7733  ax-addass 7734  ax-mulass 7735  ax-distr 7736  ax-i2m1 7737  ax-0lt1 7738  ax-1rid 7739  ax-0id 7740  ax-rnegex 7741  ax-precex 7742  ax-cnre 7743  ax-pre-ltirr 7744  ax-pre-ltwlin 7745  ax-pre-lttrn 7746  ax-pre-apti 7747  ax-pre-ltadd 7748  ax-pre-mulgt0 7749  ax-pre-mulext 7750  ax-arch 7751  ax-caucvg 7752
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-frec 6288  df-pnf 7814  df-mnf 7815  df-xr 7816  df-ltxr 7817  df-le 7818  df-sub 7947  df-neg 7948  df-reap 8349  df-ap 8356  df-div 8445  df-inn 8733  df-2 8791  df-3 8792  df-4 8793  df-n0 8990  df-z 9067  df-uz 9339  df-q 9424  df-rp 9454  df-seqfrec 10231  df-exp 10305  df-cj 10626  df-re 10627  df-im 10628  df-rsqrt 10782  df-abs 10783
This theorem is referenced by:  apdiff  13348
  Copyright terms: Public domain W3C validator