Proof of Theorem apdifflemf
Step | Hyp | Ref
| Expression |
1 | | apdifflemf.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | 1 | recnd 7885 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
3 | | apdifflemf.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℚ) |
4 | | qcn 9521 |
. . . . . . 7
⊢ (𝑅 ∈ ℚ → 𝑅 ∈
ℂ) |
5 | 3, 4 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ ℂ) |
6 | 2, 5 | subcld 8165 |
. . . . 5
⊢ (𝜑 → (𝐴 − 𝑅) ∈ ℂ) |
7 | 6 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝐴 − 𝑅) ∈ ℂ) |
8 | 7 | abscld 11058 |
. . 3
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (abs‘(𝐴 − 𝑅)) ∈ ℝ) |
9 | | apdifflemf.q |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ ℚ) |
10 | | qcn 9521 |
. . . . . . 7
⊢ (𝑄 ∈ ℚ → 𝑄 ∈
ℂ) |
11 | 9, 10 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ ℂ) |
12 | 2, 11 | subcld 8165 |
. . . . 5
⊢ (𝜑 → (𝐴 − 𝑄) ∈ ℂ) |
13 | 12 | abscld 11058 |
. . . 4
⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) ∈ ℝ) |
14 | 13 | adantr 274 |
. . 3
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (abs‘(𝐴 − 𝑄)) ∈ ℝ) |
15 | | qre 9512 |
. . . . . . . . . 10
⊢ (𝑄 ∈ ℚ → 𝑄 ∈
ℝ) |
16 | 9, 15 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ ℝ) |
17 | 16 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑄 ∈ ℝ) |
18 | 1 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝐴 ∈ ℝ) |
19 | | qaddcl 9522 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ ℚ ∧ 𝑅 ∈ ℚ) → (𝑄 + 𝑅) ∈ ℚ) |
20 | 9, 3, 19 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄 + 𝑅) ∈ ℚ) |
21 | | qre 9512 |
. . . . . . . . . . . . 13
⊢ ((𝑄 + 𝑅) ∈ ℚ → (𝑄 + 𝑅) ∈ ℝ) |
22 | 20, 21 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 + 𝑅) ∈ ℝ) |
23 | 22 | rehalfcld 9058 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑄 + 𝑅) / 2) ∈ ℝ) |
24 | 23 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → ((𝑄 + 𝑅) / 2) ∈ ℝ) |
25 | | apdifflemf.qr |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 < 𝑅) |
26 | | qre 9512 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℚ → 𝑅 ∈
ℝ) |
27 | 3, 26 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ ℝ) |
28 | | avglt1 9050 |
. . . . . . . . . . . . 13
⊢ ((𝑄 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑄 < 𝑅 ↔ 𝑄 < ((𝑄 + 𝑅) / 2))) |
29 | 16, 27, 28 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 < 𝑅 ↔ 𝑄 < ((𝑄 + 𝑅) / 2))) |
30 | 25, 29 | mpbid 146 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 < ((𝑄 + 𝑅) / 2)) |
31 | 30 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑄 < ((𝑄 + 𝑅) / 2)) |
32 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → ((𝑄 + 𝑅) / 2) < 𝐴) |
33 | 17, 24, 18, 31, 32 | lttrd 7980 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑄 < 𝐴) |
34 | 17, 18, 33 | ltled 7973 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑄 ≤ 𝐴) |
35 | 17, 18, 34 | abssubge0d 11053 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (abs‘(𝐴 − 𝑄)) = (𝐴 − 𝑄)) |
36 | 35 | oveq2d 5830 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 − (abs‘(𝐴 − 𝑄))) = (𝑅 − (𝐴 − 𝑄))) |
37 | 5 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑅 ∈ ℂ) |
38 | 2 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝐴 ∈ ℂ) |
39 | 11 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑄 ∈ ℂ) |
40 | 37, 38, 39 | subsub3d 8195 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 − (𝐴 − 𝑄)) = ((𝑅 + 𝑄) − 𝐴)) |
41 | 37, 39 | addcomd 8005 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 + 𝑄) = (𝑄 + 𝑅)) |
42 | 41 | oveq1d 5829 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → ((𝑅 + 𝑄) − 𝐴) = ((𝑄 + 𝑅) − 𝐴)) |
43 | 36, 40, 42 | 3eqtrd 2191 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 − (abs‘(𝐴 − 𝑄))) = ((𝑄 + 𝑅) − 𝐴)) |
44 | 22 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑄 + 𝑅) ∈ ℝ) |
45 | | 2rp 9543 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ+ |
46 | 45 | a1i 9 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 2 ∈
ℝ+) |
47 | 44, 18, 46 | ltdivmuld 9633 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (((𝑄 + 𝑅) / 2) < 𝐴 ↔ (𝑄 + 𝑅) < (2 · 𝐴))) |
48 | 32, 47 | mpbid 146 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑄 + 𝑅) < (2 · 𝐴)) |
49 | 38 | 2timesd 9054 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (2 · 𝐴) = (𝐴 + 𝐴)) |
50 | 48, 49 | breqtrd 3986 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑄 + 𝑅) < (𝐴 + 𝐴)) |
51 | 44, 18, 18 | ltsubaddd 8395 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (((𝑄 + 𝑅) − 𝐴) < 𝐴 ↔ (𝑄 + 𝑅) < (𝐴 + 𝐴))) |
52 | 50, 51 | mpbird 166 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → ((𝑄 + 𝑅) − 𝐴) < 𝐴) |
53 | 43, 52 | eqbrtrd 3982 |
. . . 4
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 − (abs‘(𝐴 − 𝑄))) < 𝐴) |
54 | 25 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑄 < 𝑅) |
55 | 27 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝑅 ∈ ℝ) |
56 | | difrp 9577 |
. . . . . . . 8
⊢ ((𝑄 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑄 < 𝑅 ↔ (𝑅 − 𝑄) ∈
ℝ+)) |
57 | 17, 55, 56 | syl2anc 409 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑄 < 𝑅 ↔ (𝑅 − 𝑄) ∈
ℝ+)) |
58 | 54, 57 | mpbid 146 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 − 𝑄) ∈
ℝ+) |
59 | 18, 58 | ltaddrpd 9615 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝐴 < (𝐴 + (𝑅 − 𝑄))) |
60 | 35 | oveq2d 5830 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 + (abs‘(𝐴 − 𝑄))) = (𝑅 + (𝐴 − 𝑄))) |
61 | 37, 38, 39 | addsub12d 8188 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 + (𝐴 − 𝑄)) = (𝐴 + (𝑅 − 𝑄))) |
62 | 60, 61 | eqtrd 2187 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (𝑅 + (abs‘(𝐴 − 𝑄))) = (𝐴 + (𝑅 − 𝑄))) |
63 | 59, 62 | breqtrrd 3988 |
. . . 4
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → 𝐴 < (𝑅 + (abs‘(𝐴 − 𝑄)))) |
64 | 18, 55, 14 | absdifltd 11055 |
. . . 4
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → ((abs‘(𝐴 − 𝑅)) < (abs‘(𝐴 − 𝑄)) ↔ ((𝑅 − (abs‘(𝐴 − 𝑄))) < 𝐴 ∧ 𝐴 < (𝑅 + (abs‘(𝐴 − 𝑄)))))) |
65 | 53, 63, 64 | mpbir2and 929 |
. . 3
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (abs‘(𝐴 − 𝑅)) < (abs‘(𝐴 − 𝑄))) |
66 | 8, 14, 65 | gtapd 8491 |
. 2
⊢ ((𝜑 ∧ ((𝑄 + 𝑅) / 2) < 𝐴) → (abs‘(𝐴 − 𝑄)) # (abs‘(𝐴 − 𝑅))) |
67 | 13 | adantr 274 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → (abs‘(𝐴 − 𝑄)) ∈ ℝ) |
68 | 6 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → (𝐴 − 𝑅) ∈ ℂ) |
69 | 68 | abscld 11058 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → (abs‘(𝐴 − 𝑅)) ∈ ℝ) |
70 | 11, 5, 2 | subsubd 8193 |
. . . . . . 7
⊢ (𝜑 → (𝑄 − (𝑅 − 𝐴)) = ((𝑄 − 𝑅) + 𝐴)) |
71 | 16, 27 | sublt0d 8424 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑄 − 𝑅) < 0 ↔ 𝑄 < 𝑅)) |
72 | 25, 71 | mpbird 166 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 − 𝑅) < 0) |
73 | 16, 27 | resubcld 8235 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄 − 𝑅) ∈ ℝ) |
74 | | ltaddnegr 8279 |
. . . . . . . . 9
⊢ (((𝑄 − 𝑅) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑄 − 𝑅) < 0 ↔ ((𝑄 − 𝑅) + 𝐴) < 𝐴)) |
75 | 73, 1, 74 | syl2anc 409 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄 − 𝑅) < 0 ↔ ((𝑄 − 𝑅) + 𝐴) < 𝐴)) |
76 | 72, 75 | mpbid 146 |
. . . . . . 7
⊢ (𝜑 → ((𝑄 − 𝑅) + 𝐴) < 𝐴) |
77 | 70, 76 | eqbrtrd 3982 |
. . . . . 6
⊢ (𝜑 → (𝑄 − (𝑅 − 𝐴)) < 𝐴) |
78 | 77 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → (𝑄 − (𝑅 − 𝐴)) < 𝐴) |
79 | 1 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → 𝐴 ∈ ℝ) |
80 | 22 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → (𝑄 + 𝑅) ∈ ℝ) |
81 | | simpr 109 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → 𝐴 < ((𝑄 + 𝑅) / 2)) |
82 | 79, 79, 80, 81, 81 | lt2halvesd 9059 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → (𝐴 + 𝐴) < (𝑄 + 𝑅)) |
83 | 79, 79, 80 | ltaddsub2d 8400 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → ((𝐴 + 𝐴) < (𝑄 + 𝑅) ↔ 𝐴 < ((𝑄 + 𝑅) − 𝐴))) |
84 | 82, 83 | mpbid 146 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → 𝐴 < ((𝑄 + 𝑅) − 𝐴)) |
85 | 11 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → 𝑄 ∈ ℂ) |
86 | 5 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → 𝑅 ∈ ℂ) |
87 | 2 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → 𝐴 ∈ ℂ) |
88 | 85, 86, 87 | addsubassd 8185 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → ((𝑄 + 𝑅) − 𝐴) = (𝑄 + (𝑅 − 𝐴))) |
89 | 84, 88 | breqtrd 3986 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → 𝐴 < (𝑄 + (𝑅 − 𝐴))) |
90 | 16 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → 𝑄 ∈ ℝ) |
91 | 27 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → 𝑅 ∈ ℝ) |
92 | 91, 79 | resubcld 8235 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → (𝑅 − 𝐴) ∈ ℝ) |
93 | 79, 90, 92 | absdifltd 11055 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → ((abs‘(𝐴 − 𝑄)) < (𝑅 − 𝐴) ↔ ((𝑄 − (𝑅 − 𝐴)) < 𝐴 ∧ 𝐴 < (𝑄 + (𝑅 − 𝐴))))) |
94 | 78, 89, 93 | mpbir2and 929 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → (abs‘(𝐴 − 𝑄)) < (𝑅 − 𝐴)) |
95 | 23 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → ((𝑄 + 𝑅) / 2) ∈ ℝ) |
96 | | avglt2 9051 |
. . . . . . . . . 10
⊢ ((𝑄 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑄 < 𝑅 ↔ ((𝑄 + 𝑅) / 2) < 𝑅)) |
97 | 16, 27, 96 | syl2anc 409 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄 < 𝑅 ↔ ((𝑄 + 𝑅) / 2) < 𝑅)) |
98 | 25, 97 | mpbid 146 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄 + 𝑅) / 2) < 𝑅) |
99 | 98 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → ((𝑄 + 𝑅) / 2) < 𝑅) |
100 | 79, 95, 91, 81, 99 | lttrd 7980 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → 𝐴 < 𝑅) |
101 | 79, 91, 100 | ltled 7973 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → 𝐴 ≤ 𝑅) |
102 | 79, 91, 101 | abssuble0d 11054 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → (abs‘(𝐴 − 𝑅)) = (𝑅 − 𝐴)) |
103 | 94, 102 | breqtrrd 3988 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → (abs‘(𝐴 − 𝑄)) < (abs‘(𝐴 − 𝑅))) |
104 | 67, 69, 103 | ltapd 8492 |
. 2
⊢ ((𝜑 ∧ 𝐴 < ((𝑄 + 𝑅) / 2)) → (abs‘(𝐴 − 𝑄)) # (abs‘(𝐴 − 𝑅))) |
105 | | apdifflemf.ap |
. . 3
⊢ (𝜑 → ((𝑄 + 𝑅) / 2) # 𝐴) |
106 | | reaplt 8442 |
. . . 4
⊢ ((((𝑄 + 𝑅) / 2) ∈ ℝ ∧ 𝐴 ∈ ℝ) → (((𝑄 + 𝑅) / 2) # 𝐴 ↔ (((𝑄 + 𝑅) / 2) < 𝐴 ∨ 𝐴 < ((𝑄 + 𝑅) / 2)))) |
107 | 23, 1, 106 | syl2anc 409 |
. . 3
⊢ (𝜑 → (((𝑄 + 𝑅) / 2) # 𝐴 ↔ (((𝑄 + 𝑅) / 2) < 𝐴 ∨ 𝐴 < ((𝑄 + 𝑅) / 2)))) |
108 | 105, 107 | mpbid 146 |
. 2
⊢ (𝜑 → (((𝑄 + 𝑅) / 2) < 𝐴 ∨ 𝐴 < ((𝑄 + 𝑅) / 2))) |
109 | 66, 104, 108 | mpjaodan 788 |
1
⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) # (abs‘(𝐴 − 𝑅))) |