Proof of Theorem qsqeqor
Step | Hyp | Ref
| Expression |
1 | | qre 9571 |
. . . . . . 7
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℝ) |
2 | 1 | ad3antrrr 489 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 0 ≤ 𝐵) → 𝐴 ∈ ℝ) |
3 | | simplr 525 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 0 ≤ 𝐵) → 0 ≤ 𝐴) |
4 | | qre 9571 |
. . . . . . 7
⊢ (𝐵 ∈ ℚ → 𝐵 ∈
ℝ) |
5 | 4 | ad3antlr 490 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 0 ≤ 𝐵) → 𝐵 ∈ ℝ) |
6 | | simpr 109 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 0 ≤ 𝐵) → 0 ≤ 𝐵) |
7 | | sq11 10535 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) = (𝐵↑2) ↔ 𝐴 = 𝐵)) |
8 | 2, 3, 5, 6, 7 | syl22anc 1234 |
. . . . 5
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 0 ≤ 𝐵) → ((𝐴↑2) = (𝐵↑2) ↔ 𝐴 = 𝐵)) |
9 | | orc 707 |
. . . . 5
⊢ (𝐴 = 𝐵 → (𝐴 = 𝐵 ∨ 𝐴 = -𝐵)) |
10 | 8, 9 | syl6bi 162 |
. . . 4
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 0 ≤ 𝐵) → ((𝐴↑2) = (𝐵↑2) → (𝐴 = 𝐵 ∨ 𝐴 = -𝐵))) |
11 | | oveq1 5857 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → (𝐴↑2) = (𝐵↑2)) |
12 | 11 | a1i 9 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 = 𝐵 → (𝐴↑2) = (𝐵↑2))) |
13 | | oveq1 5857 |
. . . . . . . . 9
⊢ (𝐴 = -𝐵 → (𝐴↑2) = (-𝐵↑2)) |
14 | 13 | adantl 275 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 = -𝐵) → (𝐴↑2) = (-𝐵↑2)) |
15 | | qcn 9580 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℚ → 𝐵 ∈
ℂ) |
16 | | sqneg 10522 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℂ → (-𝐵↑2) = (𝐵↑2)) |
17 | 15, 16 | syl 14 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℚ → (-𝐵↑2) = (𝐵↑2)) |
18 | 17 | ad2antlr 486 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 = -𝐵) → (-𝐵↑2) = (𝐵↑2)) |
19 | 14, 18 | eqtrd 2203 |
. . . . . . 7
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 = -𝐵) → (𝐴↑2) = (𝐵↑2)) |
20 | 19 | ex 114 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 = -𝐵 → (𝐴↑2) = (𝐵↑2))) |
21 | 12, 20 | jaod 712 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → ((𝐴 = 𝐵 ∨ 𝐴 = -𝐵) → (𝐴↑2) = (𝐵↑2))) |
22 | 21 | ad2antrr 485 |
. . . 4
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 0 ≤ 𝐵) → ((𝐴 = 𝐵 ∨ 𝐴 = -𝐵) → (𝐴↑2) = (𝐵↑2))) |
23 | 10, 22 | impbid 128 |
. . 3
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 0 ≤ 𝐵) → ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵))) |
24 | 17 | eqeq2d 2182 |
. . . . . 6
⊢ (𝐵 ∈ ℚ → ((𝐴↑2) = (-𝐵↑2) ↔ (𝐴↑2) = (𝐵↑2))) |
25 | 24 | ad3antlr 490 |
. . . . 5
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 𝐵 ≤ 0) → ((𝐴↑2) = (-𝐵↑2) ↔ (𝐴↑2) = (𝐵↑2))) |
26 | 1 | ad3antrrr 489 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 𝐵 ≤ 0) → 𝐴 ∈ ℝ) |
27 | | simplr 525 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 𝐵 ≤ 0) → 0 ≤ 𝐴) |
28 | | qnegcl 9582 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℚ → -𝐵 ∈
ℚ) |
29 | | qre 9571 |
. . . . . . . . 9
⊢ (-𝐵 ∈ ℚ → -𝐵 ∈
ℝ) |
30 | 28, 29 | syl 14 |
. . . . . . . 8
⊢ (𝐵 ∈ ℚ → -𝐵 ∈
ℝ) |
31 | 30 | ad3antlr 490 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 𝐵 ≤ 0) → -𝐵 ∈ ℝ) |
32 | | simpr 109 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 𝐵 ≤ 0) → 𝐵 ≤ 0) |
33 | 4 | le0neg1d 8423 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℚ → (𝐵 ≤ 0 ↔ 0 ≤ -𝐵)) |
34 | 33 | ad3antlr 490 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 𝐵 ≤ 0) → (𝐵 ≤ 0 ↔ 0 ≤ -𝐵)) |
35 | 32, 34 | mpbid 146 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 𝐵 ≤ 0) → 0 ≤ -𝐵) |
36 | | sq11 10535 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (-𝐵 ∈ ℝ ∧ 0 ≤
-𝐵)) → ((𝐴↑2) = (-𝐵↑2) ↔ 𝐴 = -𝐵)) |
37 | 26, 27, 31, 35, 36 | syl22anc 1234 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 𝐵 ≤ 0) → ((𝐴↑2) = (-𝐵↑2) ↔ 𝐴 = -𝐵)) |
38 | | olc 706 |
. . . . . 6
⊢ (𝐴 = -𝐵 → (𝐴 = 𝐵 ∨ 𝐴 = -𝐵)) |
39 | 37, 38 | syl6bi 162 |
. . . . 5
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 𝐵 ≤ 0) → ((𝐴↑2) = (-𝐵↑2) → (𝐴 = 𝐵 ∨ 𝐴 = -𝐵))) |
40 | 25, 39 | sylbird 169 |
. . . 4
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 𝐵 ≤ 0) → ((𝐴↑2) = (𝐵↑2) → (𝐴 = 𝐵 ∨ 𝐴 = -𝐵))) |
41 | 21 | ad2antrr 485 |
. . . 4
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 𝐵 ≤ 0) → ((𝐴 = 𝐵 ∨ 𝐴 = -𝐵) → (𝐴↑2) = (𝐵↑2))) |
42 | 40, 41 | impbid 128 |
. . 3
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) ∧ 𝐵 ≤ 0) → ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵))) |
43 | | 0z 9210 |
. . . . . 6
⊢ 0 ∈
ℤ |
44 | | zq 9572 |
. . . . . 6
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
45 | 43, 44 | ax-mp 5 |
. . . . 5
⊢ 0 ∈
ℚ |
46 | | qletric 10187 |
. . . . 5
⊢ ((0
∈ ℚ ∧ 𝐵
∈ ℚ) → (0 ≤ 𝐵 ∨ 𝐵 ≤ 0)) |
47 | 45, 46 | mpan 422 |
. . . 4
⊢ (𝐵 ∈ ℚ → (0 ≤
𝐵 ∨ 𝐵 ≤ 0)) |
48 | 47 | ad2antlr 486 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) → (0 ≤ 𝐵 ∨ 𝐵 ≤ 0)) |
49 | 23, 42, 48 | mpjaodan 793 |
. 2
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 0 ≤
𝐴) → ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵))) |
50 | | qnegcl 9582 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℚ → -𝐴 ∈
ℚ) |
51 | | qre 9571 |
. . . . . . . . . 10
⊢ (-𝐴 ∈ ℚ → -𝐴 ∈
ℝ) |
52 | 50, 51 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℚ → -𝐴 ∈
ℝ) |
53 | 52 | ad3antrrr 489 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 0 ≤ 𝐵) → -𝐴 ∈ ℝ) |
54 | | simplr 525 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 0 ≤ 𝐵) → 𝐴 ≤ 0) |
55 | 1 | le0neg1d 8423 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℚ → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) |
56 | 55 | ad3antrrr 489 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 0 ≤ 𝐵) → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) |
57 | 54, 56 | mpbid 146 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 0 ≤ 𝐵) → 0 ≤ -𝐴) |
58 | 4 | ad3antlr 490 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 0 ≤ 𝐵) → 𝐵 ∈ ℝ) |
59 | | simpr 109 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 0 ≤ 𝐵) → 0 ≤ 𝐵) |
60 | | sq11 10535 |
. . . . . . . 8
⊢ (((-𝐴 ∈ ℝ ∧ 0 ≤
-𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤
𝐵)) → ((-𝐴↑2) = (𝐵↑2) ↔ -𝐴 = 𝐵)) |
61 | 53, 57, 58, 59, 60 | syl22anc 1234 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 0 ≤ 𝐵) → ((-𝐴↑2) = (𝐵↑2) ↔ -𝐴 = 𝐵)) |
62 | 61 | biimpd 143 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 0 ≤ 𝐵) → ((-𝐴↑2) = (𝐵↑2) → -𝐴 = 𝐵)) |
63 | | qcn 9580 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℂ) |
64 | | sqneg 10522 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (-𝐴↑2) = (𝐴↑2)) |
65 | 63, 64 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℚ → (-𝐴↑2) = (𝐴↑2)) |
66 | 65 | adantr 274 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (-𝐴↑2) = (𝐴↑2)) |
67 | 66 | eqeq1d 2179 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → ((-𝐴↑2) = (𝐵↑2) ↔ (𝐴↑2) = (𝐵↑2))) |
68 | 67 | ad2antrr 485 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 0 ≤ 𝐵) → ((-𝐴↑2) = (𝐵↑2) ↔ (𝐴↑2) = (𝐵↑2))) |
69 | | negcon1 8158 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴)) |
70 | 63, 15, 69 | syl2an 287 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴)) |
71 | | eqcom 2172 |
. . . . . . . 8
⊢ (-𝐵 = 𝐴 ↔ 𝐴 = -𝐵) |
72 | 70, 71 | bitrdi 195 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (-𝐴 = 𝐵 ↔ 𝐴 = -𝐵)) |
73 | 72 | ad2antrr 485 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 0 ≤ 𝐵) → (-𝐴 = 𝐵 ↔ 𝐴 = -𝐵)) |
74 | 62, 68, 73 | 3imtr3d 201 |
. . . . 5
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 0 ≤ 𝐵) → ((𝐴↑2) = (𝐵↑2) → 𝐴 = -𝐵)) |
75 | 74, 38 | syl6 33 |
. . . 4
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 0 ≤ 𝐵) → ((𝐴↑2) = (𝐵↑2) → (𝐴 = 𝐵 ∨ 𝐴 = -𝐵))) |
76 | 21 | ad2antrr 485 |
. . . 4
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 0 ≤ 𝐵) → ((𝐴 = 𝐵 ∨ 𝐴 = -𝐵) → (𝐴↑2) = (𝐵↑2))) |
77 | 75, 76 | impbid 128 |
. . 3
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 0 ≤ 𝐵) → ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵))) |
78 | 52 | ad3antrrr 489 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → -𝐴 ∈ ℝ) |
79 | | simplr 525 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → 𝐴 ≤ 0) |
80 | 55 | ad3antrrr 489 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) |
81 | 79, 80 | mpbid 146 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → 0 ≤ -𝐴) |
82 | 30 | ad3antlr 490 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → -𝐵 ∈ ℝ) |
83 | | simpr 109 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → 𝐵 ≤ 0) |
84 | 33 | ad3antlr 490 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → (𝐵 ≤ 0 ↔ 0 ≤ -𝐵)) |
85 | 83, 84 | mpbid 146 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → 0 ≤ -𝐵) |
86 | | sq11 10535 |
. . . . . . 7
⊢ (((-𝐴 ∈ ℝ ∧ 0 ≤
-𝐴) ∧ (-𝐵 ∈ ℝ ∧ 0 ≤
-𝐵)) → ((-𝐴↑2) = (-𝐵↑2) ↔ -𝐴 = -𝐵)) |
87 | 78, 81, 82, 85, 86 | syl22anc 1234 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → ((-𝐴↑2) = (-𝐵↑2) ↔ -𝐴 = -𝐵)) |
88 | 65, 17 | eqeqan12d 2186 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → ((-𝐴↑2) = (-𝐵↑2) ↔ (𝐴↑2) = (𝐵↑2))) |
89 | 88 | ad2antrr 485 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → ((-𝐴↑2) = (-𝐵↑2) ↔ (𝐴↑2) = (𝐵↑2))) |
90 | 63 | ad3antrrr 489 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → 𝐴 ∈ ℂ) |
91 | 15 | ad3antlr 490 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → 𝐵 ∈ ℂ) |
92 | 90, 91 | neg11ad 8213 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵)) |
93 | 87, 89, 92 | 3bitr3d 217 |
. . . . 5
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → ((𝐴↑2) = (𝐵↑2) ↔ 𝐴 = 𝐵)) |
94 | 93, 9 | syl6bi 162 |
. . . 4
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → ((𝐴↑2) = (𝐵↑2) → (𝐴 = 𝐵 ∨ 𝐴 = -𝐵))) |
95 | 21 | ad2antrr 485 |
. . . 4
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → ((𝐴 = 𝐵 ∨ 𝐴 = -𝐵) → (𝐴↑2) = (𝐵↑2))) |
96 | 94, 95 | impbid 128 |
. . 3
⊢ ((((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) ∧ 𝐵 ≤ 0) → ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵))) |
97 | 47 | ad2antlr 486 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) → (0 ≤ 𝐵 ∨ 𝐵 ≤ 0)) |
98 | 77, 96, 97 | mpjaodan 793 |
. 2
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ 𝐴 ≤ 0) → ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵))) |
99 | | qletric 10187 |
. . . 4
⊢ ((0
∈ ℚ ∧ 𝐴
∈ ℚ) → (0 ≤ 𝐴 ∨ 𝐴 ≤ 0)) |
100 | 45, 99 | mpan 422 |
. . 3
⊢ (𝐴 ∈ ℚ → (0 ≤
𝐴 ∨ 𝐴 ≤ 0)) |
101 | 100 | adantr 274 |
. 2
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (0 ≤
𝐴 ∨ 𝐴 ≤ 0)) |
102 | 49, 98, 101 | mpjaodan 793 |
1
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵))) |