Proof of Theorem apdifflemr
Step | Hyp | Ref
| Expression |
1 | | 2cnd 8885 |
. . . . 5
⊢ (𝜑 → 2 ∈
ℂ) |
2 | | apdifflemr.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 2 | recnd 7885 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℂ) |
4 | 3 | 2timesd 9054 |
. . . . . 6
⊢ (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴)) |
5 | | apdifflemr.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(𝐴 − -1)) #
(abs‘(𝐴 −
1))) |
6 | | 1cnd 7873 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℂ) |
7 | 3, 6 | subnegd 8172 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 − -1) = (𝐴 + 1)) |
8 | 3, 6, 7 | comraddd 8011 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 − -1) = (1 + 𝐴)) |
9 | 8 | fveq2d 5465 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(𝐴 − -1)) = (abs‘(1 +
𝐴))) |
10 | 3, 6 | abssubd 11070 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(𝐴 − 1)) = (abs‘(1
− 𝐴))) |
11 | 5, 9, 10 | 3brtr3d 3991 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘(1 + 𝐴)) # (abs‘(1 − 𝐴))) |
12 | 6, 3 | addcld 7876 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 + 𝐴) ∈ ℂ) |
13 | 6, 3 | subcld 8165 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 − 𝐴) ∈
ℂ) |
14 | | absext 10940 |
. . . . . . . . . . . 12
⊢ (((1 +
𝐴) ∈ ℂ ∧ (1
− 𝐴) ∈ ℂ)
→ ((abs‘(1 + 𝐴))
# (abs‘(1 − 𝐴))
→ (1 + 𝐴) # (1 −
𝐴))) |
15 | 12, 13, 14 | syl2anc 409 |
. . . . . . . . . . 11
⊢ (𝜑 → ((abs‘(1 + 𝐴)) # (abs‘(1 − 𝐴)) → (1 + 𝐴) # (1 − 𝐴))) |
16 | 11, 15 | mpd 13 |
. . . . . . . . . 10
⊢ (𝜑 → (1 + 𝐴) # (1 − 𝐴)) |
17 | 6, 3 | negsubd 8171 |
. . . . . . . . . 10
⊢ (𝜑 → (1 + -𝐴) = (1 − 𝐴)) |
18 | 16, 17 | breqtrrd 3988 |
. . . . . . . . 9
⊢ (𝜑 → (1 + 𝐴) # (1 + -𝐴)) |
19 | 3 | negcld 8152 |
. . . . . . . . . 10
⊢ (𝜑 → -𝐴 ∈ ℂ) |
20 | | apadd2 8463 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ -𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 # -𝐴 ↔ (1 + 𝐴) # (1 + -𝐴))) |
21 | 3, 19, 6, 20 | syl3anc 1217 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 # -𝐴 ↔ (1 + 𝐴) # (1 + -𝐴))) |
22 | 18, 21 | mpbird 166 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 # -𝐴) |
23 | | apadd2 8463 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ -𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐴 # -𝐴 ↔ (𝐴 + 𝐴) # (𝐴 + -𝐴))) |
24 | 3, 19, 3, 23 | syl3anc 1217 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 # -𝐴 ↔ (𝐴 + 𝐴) # (𝐴 + -𝐴))) |
25 | 22, 24 | mpbid 146 |
. . . . . . 7
⊢ (𝜑 → (𝐴 + 𝐴) # (𝐴 + -𝐴)) |
26 | 3 | negidd 8155 |
. . . . . . 7
⊢ (𝜑 → (𝐴 + -𝐴) = 0) |
27 | 25, 26 | breqtrd 3986 |
. . . . . 6
⊢ (𝜑 → (𝐴 + 𝐴) # 0) |
28 | 4, 27 | eqbrtrd 3982 |
. . . . 5
⊢ (𝜑 → (2 · 𝐴) # 0) |
29 | 1, 3, 28 | mulap0bbd 8513 |
. . . 4
⊢ (𝜑 → 𝐴 # 0) |
30 | 29 | adantr 274 |
. . 3
⊢ ((𝜑 ∧ 𝑆 = 0) → 𝐴 # 0) |
31 | | simpr 109 |
. . 3
⊢ ((𝜑 ∧ 𝑆 = 0) → 𝑆 = 0) |
32 | 30, 31 | breqtrrd 3988 |
. 2
⊢ ((𝜑 ∧ 𝑆 = 0) → 𝐴 # 𝑆) |
33 | 4 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (2 · 𝐴) = (𝐴 + 𝐴)) |
34 | | apdifflemr.as |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (abs‘(𝐴 − 0)) # (abs‘(𝐴 − (2 · 𝑆)))) |
35 | 3 | subid1d 8154 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 − 0) = 𝐴) |
36 | 35 | fveq2d 5465 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘(𝐴 − 0)) = (abs‘𝐴)) |
37 | | 2z 9174 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
38 | | zq 9513 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℤ → 2 ∈ ℚ) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℚ |
40 | 39 | a1i 9 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ∈
ℚ) |
41 | | apdifflemr.s |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ ℚ) |
42 | | qmulcl 9524 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℚ ∧ 𝑆
∈ ℚ) → (2 · 𝑆) ∈ ℚ) |
43 | 40, 41, 42 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 · 𝑆) ∈
ℚ) |
44 | | qcn 9521 |
. . . . . . . . . . . 12
⊢ ((2
· 𝑆) ∈ ℚ
→ (2 · 𝑆)
∈ ℂ) |
45 | 43, 44 | syl 14 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝑆) ∈
ℂ) |
46 | 3, 45 | abssubd 11070 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘(𝐴 − (2 · 𝑆))) = (abs‘((2 ·
𝑆) − 𝐴))) |
47 | 36, 46 | breq12d 3974 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘(𝐴 − 0)) # (abs‘(𝐴 − (2 · 𝑆))) ↔ (abs‘𝐴) # (abs‘((2 ·
𝑆) − 𝐴)))) |
48 | 47 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → ((abs‘(𝐴 − 0)) # (abs‘(𝐴 − (2 · 𝑆))) ↔ (abs‘𝐴) # (abs‘((2 ·
𝑆) − 𝐴)))) |
49 | 34, 48 | mpbid 146 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (abs‘𝐴) # (abs‘((2 · 𝑆) − 𝐴))) |
50 | 3 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐴 ∈ ℂ) |
51 | 45, 3 | subcld 8165 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · 𝑆) − 𝐴) ∈ ℂ) |
52 | 51 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → ((2 · 𝑆) − 𝐴) ∈ ℂ) |
53 | | absext 10940 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ ((2
· 𝑆) − 𝐴) ∈ ℂ) →
((abs‘𝐴) #
(abs‘((2 · 𝑆)
− 𝐴)) → 𝐴 # ((2 · 𝑆) − 𝐴))) |
54 | 50, 52, 53 | syl2anc 409 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → ((abs‘𝐴) # (abs‘((2 ·
𝑆) − 𝐴)) → 𝐴 # ((2 · 𝑆) − 𝐴))) |
55 | 49, 54 | mpd 13 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐴 # ((2 · 𝑆) − 𝐴)) |
56 | | apadd2 8463 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ ((2
· 𝑆) − 𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐴 # ((2 · 𝑆) − 𝐴) ↔ (𝐴 + 𝐴) # (𝐴 + ((2 · 𝑆) − 𝐴)))) |
57 | 50, 52, 50, 56 | syl3anc 1217 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐴 # ((2 · 𝑆) − 𝐴) ↔ (𝐴 + 𝐴) # (𝐴 + ((2 · 𝑆) − 𝐴)))) |
58 | 55, 57 | mpbid 146 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐴 + 𝐴) # (𝐴 + ((2 · 𝑆) − 𝐴))) |
59 | 45 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (2 · 𝑆) ∈
ℂ) |
60 | 50, 59 | pncan3d 8168 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐴 + ((2 · 𝑆) − 𝐴)) = (2 · 𝑆)) |
61 | 58, 60 | breqtrd 3986 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐴 + 𝐴) # (2 · 𝑆)) |
62 | 33, 61 | eqbrtrd 3982 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (2 · 𝐴) # (2 · 𝑆)) |
63 | | qcn 9521 |
. . . . . 6
⊢ (𝑆 ∈ ℚ → 𝑆 ∈
ℂ) |
64 | 41, 63 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ ℂ) |
65 | 64 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑆 ∈ ℂ) |
66 | | 2cnd 8885 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 2 ∈
ℂ) |
67 | | 2ap0 8905 |
. . . . 5
⊢ 2 #
0 |
68 | 67 | a1i 9 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 2 # 0) |
69 | | apmul2 8641 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑆 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 # 0)) → (𝐴 # 𝑆 ↔ (2 · 𝐴) # (2 · 𝑆))) |
70 | 50, 65, 66, 68, 69 | syl112anc 1221 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐴 # 𝑆 ↔ (2 · 𝐴) # (2 · 𝑆))) |
71 | 62, 70 | mpbird 166 |
. 2
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐴 # 𝑆) |
72 | | 0z 9157 |
. . . . . 6
⊢ 0 ∈
ℤ |
73 | | zq 9513 |
. . . . . 6
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
74 | 72, 73 | ax-mp 5 |
. . . . 5
⊢ 0 ∈
ℚ |
75 | | qdceq 10124 |
. . . . 5
⊢ ((𝑆 ∈ ℚ ∧ 0 ∈
ℚ) → DECID 𝑆 = 0) |
76 | 41, 74, 75 | sylancl 410 |
. . . 4
⊢ (𝜑 → DECID 𝑆 = 0) |
77 | | exmiddc 822 |
. . . 4
⊢
(DECID 𝑆 = 0 → (𝑆 = 0 ∨ ¬ 𝑆 = 0)) |
78 | 76, 77 | syl 14 |
. . 3
⊢ (𝜑 → (𝑆 = 0 ∨ ¬ 𝑆 = 0)) |
79 | | df-ne 2325 |
. . . 4
⊢ (𝑆 ≠ 0 ↔ ¬ 𝑆 = 0) |
80 | 79 | orbi2i 752 |
. . 3
⊢ ((𝑆 = 0 ∨ 𝑆 ≠ 0) ↔ (𝑆 = 0 ∨ ¬ 𝑆 = 0)) |
81 | 78, 80 | sylibr 133 |
. 2
⊢ (𝜑 → (𝑆 = 0 ∨ 𝑆 ≠ 0)) |
82 | 32, 71, 81 | mpjaodan 788 |
1
⊢ (𝜑 → 𝐴 # 𝑆) |