Step | Hyp | Ref
| Expression |
1 | | 1lt2nq 7407 |
. . . . . . 7
โข
1Q <Q
(1Q +Q
1Q) |
2 | | 1nq 7367 |
. . . . . . . 8
โข
1Q โ Q |
3 | | addclnq 7376 |
. . . . . . . . 9
โข
((1Q โ Q โง
1Q โ Q) โ
(1Q +Q
1Q) โ Q) |
4 | 2, 2, 3 | mp2an 426 |
. . . . . . . 8
โข
(1Q +Q
1Q) โ Q |
5 | | ltmnqg 7402 |
. . . . . . . 8
โข
((1Q โ Q โง
(1Q +Q
1Q) โ Q โง ๐ต โ Q) โ
(1Q <Q
(1Q +Q
1Q) โ (๐ต ยทQ
1Q) <Q (๐ต ยทQ
(1Q +Q
1Q)))) |
6 | 2, 4, 5 | mp3an12 1327 |
. . . . . . 7
โข (๐ต โ Q โ
(1Q <Q
(1Q +Q
1Q) โ (๐ต ยทQ
1Q) <Q (๐ต ยทQ
(1Q +Q
1Q)))) |
7 | 1, 6 | mpbii 148 |
. . . . . 6
โข (๐ต โ Q โ
(๐ต
ยทQ 1Q)
<Q (๐ต ยทQ
(1Q +Q
1Q))) |
8 | | mulidnq 7390 |
. . . . . 6
โข (๐ต โ Q โ
(๐ต
ยทQ 1Q) = ๐ต) |
9 | | distrnqg 7388 |
. . . . . . . 8
โข ((๐ต โ Q โง
1Q โ Q โง
1Q โ Q) โ (๐ต ยทQ
(1Q +Q
1Q)) = ((๐ต ยทQ
1Q) +Q (๐ต ยทQ
1Q))) |
10 | 2, 2, 9 | mp3an23 1329 |
. . . . . . 7
โข (๐ต โ Q โ
(๐ต
ยทQ (1Q
+Q 1Q)) = ((๐ต ยทQ
1Q) +Q (๐ต ยทQ
1Q))) |
11 | 8, 8 | oveq12d 5895 |
. . . . . . 7
โข (๐ต โ Q โ
((๐ต
ยทQ 1Q)
+Q (๐ต ยทQ
1Q)) = (๐ต +Q ๐ต)) |
12 | 10, 11 | eqtrd 2210 |
. . . . . 6
โข (๐ต โ Q โ
(๐ต
ยทQ (1Q
+Q 1Q)) = (๐ต +Q ๐ต)) |
13 | 7, 8, 12 | 3brtr3d 4036 |
. . . . 5
โข (๐ต โ Q โ
๐ต
<Q (๐ต +Q ๐ต)) |
14 | 13 | adantl 277 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q)
โ ๐ต
<Q (๐ต +Q ๐ต)) |
15 | | simpr 110 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q)
โ ๐ต โ
Q) |
16 | | addclnq 7376 |
. . . . . . 7
โข ((๐ต โ Q โง
๐ต โ Q)
โ (๐ต
+Q ๐ต) โ Q) |
17 | 16 | anidms 397 |
. . . . . 6
โข (๐ต โ Q โ
(๐ต
+Q ๐ต) โ Q) |
18 | 17 | adantl 277 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ต
+Q ๐ต) โ Q) |
19 | | simpl 109 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q)
โ ๐ด โ
Q) |
20 | | ltanqg 7401 |
. . . . 5
โข ((๐ต โ Q โง
(๐ต
+Q ๐ต) โ Q โง ๐ด โ Q) โ
(๐ต
<Q (๐ต +Q ๐ต) โ (๐ด +Q ๐ต) <Q
(๐ด
+Q (๐ต +Q ๐ต)))) |
21 | 15, 18, 19, 20 | syl3anc 1238 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ต
<Q (๐ต +Q ๐ต) โ (๐ด +Q ๐ต) <Q
(๐ด
+Q (๐ต +Q ๐ต)))) |
22 | 14, 21 | mpbid 147 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
+Q ๐ต) <Q (๐ด +Q
(๐ต
+Q ๐ต))) |
23 | | addcomnqg 7382 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
+Q ๐ต) = (๐ต +Q ๐ด)) |
24 | | addcomnqg 7382 |
. . . . 5
โข ((๐ โ Q โง
๐ โ Q)
โ (๐
+Q ๐ ) = (๐ +Q ๐)) |
25 | 24 | adantl 277 |
. . . 4
โข (((๐ด โ Q โง
๐ต โ Q)
โง (๐ โ
Q โง ๐
โ Q)) โ (๐ +Q ๐ ) = (๐ +Q ๐)) |
26 | | addassnqg 7383 |
. . . . 5
โข ((๐ โ Q โง
๐ โ Q
โง ๐ก โ
Q) โ ((๐
+Q ๐ ) +Q ๐ก) = (๐ +Q (๐ +Q
๐ก))) |
27 | 26 | adantl 277 |
. . . 4
โข (((๐ด โ Q โง
๐ต โ Q)
โง (๐ โ
Q โง ๐
โ Q โง ๐ก โ Q)) โ ((๐ +Q
๐ )
+Q ๐ก) = (๐ +Q (๐ +Q
๐ก))) |
28 | 19, 15, 15, 25, 27 | caov12d 6058 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
+Q (๐ต +Q ๐ต)) = (๐ต +Q (๐ด +Q
๐ต))) |
29 | 22, 23, 28 | 3brtr3d 4036 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ต
+Q ๐ด) <Q (๐ต +Q
(๐ด
+Q ๐ต))) |
30 | | addclnq 7376 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
+Q ๐ต) โ Q) |
31 | | ltanqg 7401 |
. . 3
โข ((๐ด โ Q โง
(๐ด
+Q ๐ต) โ Q โง ๐ต โ Q) โ
(๐ด
<Q (๐ด +Q ๐ต) โ (๐ต +Q ๐ด) <Q
(๐ต
+Q (๐ด +Q ๐ต)))) |
32 | 19, 30, 15, 31 | syl3anc 1238 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
<Q (๐ด +Q ๐ต) โ (๐ต +Q ๐ด) <Q
(๐ต
+Q (๐ด +Q ๐ต)))) |
33 | 29, 32 | mpbird 167 |
1
โข ((๐ด โ Q โง
๐ต โ Q)
โ ๐ด
<Q (๐ด +Q ๐ต)) |