Step | Hyp | Ref
| Expression |
1 | | simpl 109 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
โ) |
2 | 1 | nnsqcld 10674 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ2) โ
โ) |
3 | 2 | nnred 8931 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ2) โ
โ) |
4 | | 0red 7957 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โ
โ) |
5 | 2 | nngt0d 8962 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 <
(๐ดโ2)) |
6 | 4, 3, 5 | ltled 8075 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
(๐ดโ2)) |
7 | | simpr 110 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ
โ) |
8 | 7 | nnsqcld 10674 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ตโ2) โ
โ) |
9 | 8 | nnrpd 9693 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ตโ2) โ
โ+) |
10 | 3, 6, 9 | sqrtdivd 11176 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ((๐ดโ2)
/ (๐ตโ2))) =
((โโ(๐ดโ2))
/ (โโ(๐ตโ2)))) |
11 | 1 | nnred 8931 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
โ) |
12 | 1 | nngt0d 8962 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 <
๐ด) |
13 | 4, 11, 12 | ltled 8075 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
๐ด) |
14 | 11, 13 | sqrtsqd 11173 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ดโ2))
= ๐ด) |
15 | 7 | nnred 8931 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ
โ) |
16 | 7 | nngt0d 8962 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 <
๐ต) |
17 | 4, 15, 16 | ltled 8075 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
๐ต) |
18 | 15, 17 | sqrtsqd 11173 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ตโ2))
= ๐ต) |
19 | 14, 18 | oveq12d 5892 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ(๐ดโ2))
/ (โโ(๐ตโ2))) = (๐ด / ๐ต)) |
20 | 10, 19 | eqtrd 2210 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ((๐ดโ2)
/ (๐ตโ2))) = (๐ด / ๐ต)) |
21 | | sqne2sq 12176 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ2) โ (2 ยท (๐ตโ2))) |
22 | 2 | nncnd 8932 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ2) โ
โ) |
23 | | 2cnd 8991 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ 2 โ
โ) |
24 | 8 | nncnd 8932 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ตโ2) โ
โ) |
25 | 8 | nnap0d 8964 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ตโ2) # 0) |
26 | 22, 23, 24, 25 | divmulap3d 8781 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ2) / (๐ตโ2)) = 2 โ (๐ดโ2) = (2 ยท (๐ตโ2)))) |
27 | 26 | necon3bid 2388 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ2) / (๐ตโ2)) โ 2 โ (๐ดโ2) โ (2 ยท (๐ตโ2)))) |
28 | 21, 27 | mpbird 167 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) / (๐ตโ2)) โ 2) |
29 | 2 | nnzd 9373 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ2) โ
โค) |
30 | | znq 9623 |
. . . . . . 7
โข (((๐ดโ2) โ โค โง
(๐ตโ2) โ โ)
โ ((๐ดโ2) / (๐ตโ2)) โ
โ) |
31 | 29, 8, 30 | syl2anc 411 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) / (๐ตโ2)) โ โ) |
32 | | 2z 9280 |
. . . . . . 7
โข 2 โ
โค |
33 | | zq 9625 |
. . . . . . 7
โข (2 โ
โค โ 2 โ โ) |
34 | 32, 33 | mp1i 10 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ 2 โ
โ) |
35 | | qapne 9638 |
. . . . . 6
โข ((((๐ดโ2) / (๐ตโ2)) โ โ โง 2 โ
โ) โ (((๐ดโ2) / (๐ตโ2)) # 2 โ ((๐ดโ2) / (๐ตโ2)) โ 2)) |
36 | 31, 34, 35 | syl2anc 411 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ2) / (๐ตโ2)) # 2 โ ((๐ดโ2) / (๐ตโ2)) โ 2)) |
37 | 28, 36 | mpbird 167 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) / (๐ตโ2)) # 2) |
38 | | qre 9624 |
. . . . . 6
โข (((๐ดโ2) / (๐ตโ2)) โ โ โ ((๐ดโ2) / (๐ตโ2)) โ โ) |
39 | 31, 38 | syl 14 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) / (๐ตโ2)) โ โ) |
40 | 8 | nnred 8931 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ตโ2) โ
โ) |
41 | 8 | nngt0d 8962 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 <
(๐ตโ2)) |
42 | 3, 40, 5, 41 | divgt0d 8891 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 <
((๐ดโ2) / (๐ตโ2))) |
43 | 4, 39, 42 | ltled 8075 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
((๐ดโ2) / (๐ตโ2))) |
44 | | 2re 8988 |
. . . . . 6
โข 2 โ
โ |
45 | 44 | a1i 9 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ 2 โ
โ) |
46 | | 0le2 9008 |
. . . . . 6
โข 0 โค
2 |
47 | 46 | a1i 9 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
2) |
48 | | sqrt11ap 11046 |
. . . . 5
โข
(((((๐ดโ2) /
(๐ตโ2)) โ โ
โง 0 โค ((๐ดโ2) /
(๐ตโ2))) โง (2
โ โ โง 0 โค 2)) โ ((โโ((๐ดโ2) / (๐ตโ2))) # (โโ2) โ
((๐ดโ2) / (๐ตโ2)) # 2)) |
49 | 39, 43, 45, 47, 48 | syl22anc 1239 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ((๐ดโ2)
/ (๐ตโ2))) #
(โโ2) โ ((๐ดโ2) / (๐ตโ2)) # 2)) |
50 | 37, 49 | mpbird 167 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ((๐ดโ2)
/ (๐ตโ2))) #
(โโ2)) |
51 | 20, 50 | eqbrtrrd 4027 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด / ๐ต) # (โโ2)) |
52 | | nnz 9271 |
. . . . 5
โข (๐ด โ โ โ ๐ด โ
โค) |
53 | | znq 9623 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โ) โ (๐ด / ๐ต) โ โ) |
54 | 52, 53 | sylan 283 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด / ๐ต) โ โ) |
55 | | qcn 9633 |
. . . 4
โข ((๐ด / ๐ต) โ โ โ (๐ด / ๐ต) โ โ) |
56 | 54, 55 | syl 14 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด / ๐ต) โ โ) |
57 | | sqrt2re 12162 |
. . . . 5
โข
(โโ2) โ โ |
58 | 57 | recni 7968 |
. . . 4
โข
(โโ2) โ โ |
59 | 58 | a1i 9 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ2) โ โ) |
60 | | apsym 8562 |
. . 3
โข (((๐ด / ๐ต) โ โ โง (โโ2)
โ โ) โ ((๐ด
/ ๐ต) # (โโ2)
โ (โโ2) # (๐ด / ๐ต))) |
61 | 56, 59, 60 | syl2anc 411 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด / ๐ต) # (โโ2) โ
(โโ2) # (๐ด /
๐ต))) |
62 | 51, 61 | mpbid 147 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ2) # (๐ด /
๐ต)) |