Step | Hyp | Ref
| Expression |
1 | | nn0cn 12428 |
. . . . . . 7
โข (๐ด โ โ0
โ ๐ด โ
โ) |
2 | | nn0cn 12428 |
. . . . . . 7
โข (๐ต โ โ0
โ ๐ต โ
โ) |
3 | 1, 2 | anim12i 614 |
. . . . . 6
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ (๐ด โ โ โง ๐ต โ โ)) |
4 | 3 | 3adant3 1133 |
. . . . 5
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ (๐ด โ โ โง ๐ต โ โ)) |
5 | | subsq 14120 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) โ (๐ตโ2)) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) |
6 | 4, 5 | syl 17 |
. . . 4
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ ((๐ดโ2) โ (๐ตโ2)) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) |
7 | 6 | adantr 482 |
. . 3
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ ((๐ดโ2) โ (๐ตโ2)) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) |
8 | 7 | eqeq2d 2744 |
. 2
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ ((๐ถโ๐ท) = ((๐ดโ2) โ (๐ตโ2)) โ (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต)))) |
9 | | simprl 770 |
. . . . . . 7
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ ๐ถ โ
โ) |
10 | | nn0z 12529 |
. . . . . . . . . . . 12
โข (๐ด โ โ0
โ ๐ด โ
โค) |
11 | | nn0z 12529 |
. . . . . . . . . . . 12
โข (๐ต โ โ0
โ ๐ต โ
โค) |
12 | 10, 11 | anim12i 614 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ (๐ด โ โค โง ๐ต โ โค)) |
13 | | zaddcl 12548 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด + ๐ต) โ โค) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ (๐ด + ๐ต) โ โค) |
15 | 14 | 3adant3 1133 |
. . . . . . . . 9
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ (๐ด + ๐ต) โ โค) |
16 | | nn0re 12427 |
. . . . . . . . . . . . 13
โข (๐ต โ โ0
โ ๐ต โ
โ) |
17 | 16 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ ๐ต โ โ) |
18 | | 1red 11161 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ 1 โ โ) |
19 | | nn0re 12427 |
. . . . . . . . . . . . 13
โข (๐ด โ โ0
โ ๐ด โ
โ) |
20 | 19 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ ๐ด โ โ) |
21 | 17, 18, 20 | ltaddsub2d 11761 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ ((๐ต + 1) < ๐ด โ 1 < (๐ด โ ๐ต))) |
22 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ ๐ต โ
โ0) |
23 | 20, 22, 18 | 3jca 1129 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ (๐ด โ โ โง ๐ต โ โ0 โง 1 โ
โ)) |
24 | | difgtsumgt 12471 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ0
โง 1 โ โ) โ (1 < (๐ด โ ๐ต) โ 1 < (๐ด + ๐ต))) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ (1 < (๐ด โ ๐ต) โ 1 < (๐ด + ๐ต))) |
26 | 21, 25 | sylbid 239 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ ((๐ต + 1) < ๐ด โ 1 < (๐ด + ๐ต))) |
27 | 26 | 3impia 1118 |
. . . . . . . . 9
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ 1 < (๐ด + ๐ต)) |
28 | | eluz2b1 12849 |
. . . . . . . . 9
โข ((๐ด + ๐ต) โ (โคโฅโ2)
โ ((๐ด + ๐ต) โ โค โง 1 <
(๐ด + ๐ต))) |
29 | 15, 27, 28 | sylanbrc 584 |
. . . . . . . 8
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ (๐ด + ๐ต) โ
(โคโฅโ2)) |
30 | 29 | adantr 482 |
. . . . . . 7
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ (๐ด + ๐ต) โ
(โคโฅโ2)) |
31 | | simprr 772 |
. . . . . . 7
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ ๐ท โ
โ0) |
32 | 9, 30, 31 | 3jca 1129 |
. . . . . 6
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ (๐ถ โ โ โง (๐ด + ๐ต) โ (โคโฅโ2)
โง ๐ท โ
โ0)) |
33 | 32 | adantr 482 |
. . . . 5
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ (๐ถ โ โ โง (๐ด + ๐ต) โ (โคโฅโ2)
โง ๐ท โ
โ0)) |
34 | | zsubcl 12550 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด โ ๐ต) โ โค) |
35 | 13, 34 | jca 513 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ต โ โค) โ ((๐ด + ๐ต) โ โค โง (๐ด โ ๐ต) โ โค)) |
36 | 12, 35 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ ((๐ด + ๐ต) โ โค โง (๐ด โ ๐ต) โ โค)) |
37 | 36 | 3adant3 1133 |
. . . . . . . 8
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ ((๐ด + ๐ต) โ โค โง (๐ด โ ๐ต) โ โค)) |
38 | | dvdsmul1 16165 |
. . . . . . . 8
โข (((๐ด + ๐ต) โ โค โง (๐ด โ ๐ต) โ โค) โ (๐ด + ๐ต) โฅ ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) |
39 | 37, 38 | syl 17 |
. . . . . . 7
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ (๐ด + ๐ต) โฅ ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) |
40 | 39 | ad2antrr 725 |
. . . . . 6
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ (๐ด + ๐ต) โฅ ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) |
41 | | breq2 5110 |
. . . . . . 7
โข ((๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต)) โ ((๐ด + ๐ต) โฅ (๐ถโ๐ท) โ (๐ด + ๐ต) โฅ ((๐ด + ๐ต) ยท (๐ด โ ๐ต)))) |
42 | 41 | adantl 483 |
. . . . . 6
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ ((๐ด + ๐ต) โฅ (๐ถโ๐ท) โ (๐ด + ๐ต) โฅ ((๐ด + ๐ต) ยท (๐ด โ ๐ต)))) |
43 | 40, 42 | mpbird 257 |
. . . . 5
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ (๐ด + ๐ต) โฅ (๐ถโ๐ท)) |
44 | | dvdsprmpweqnn 16762 |
. . . . 5
โข ((๐ถ โ โ โง (๐ด + ๐ต) โ (โคโฅโ2)
โง ๐ท โ
โ0) โ ((๐ด + ๐ต) โฅ (๐ถโ๐ท) โ โ๐ โ โ (๐ด + ๐ต) = (๐ถโ๐))) |
45 | 33, 43, 44 | sylc 65 |
. . . 4
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ โ๐ โ โ (๐ด + ๐ต) = (๐ถโ๐)) |
46 | | prmz 16556 |
. . . . . . . . . . 11
โข (๐ถ โ โ โ ๐ถ โ
โค) |
47 | | iddvdsexp 16167 |
. . . . . . . . . . 11
โข ((๐ถ โ โค โง ๐ โ โ) โ ๐ถ โฅ (๐ถโ๐)) |
48 | 46, 47 | sylan 581 |
. . . . . . . . . 10
โข ((๐ถ โ โ โง ๐ โ โ) โ ๐ถ โฅ (๐ถโ๐)) |
49 | | breq2 5110 |
. . . . . . . . . 10
โข ((๐ด + ๐ต) = (๐ถโ๐) โ (๐ถ โฅ (๐ด + ๐ต) โ ๐ถ โฅ (๐ถโ๐))) |
50 | 48, 49 | syl5ibrcom 247 |
. . . . . . . . 9
โข ((๐ถ โ โ โง ๐ โ โ) โ ((๐ด + ๐ต) = (๐ถโ๐) โ ๐ถ โฅ (๐ด + ๐ต))) |
51 | 50 | rexlimdva 3149 |
. . . . . . . 8
โข (๐ถ โ โ โ
(โ๐ โ โ
(๐ด + ๐ต) = (๐ถโ๐) โ ๐ถ โฅ (๐ด + ๐ต))) |
52 | 51 | adantr 482 |
. . . . . . 7
โข ((๐ถ โ โ โง ๐ท โ โ0)
โ (โ๐ โ
โ (๐ด + ๐ต) = (๐ถโ๐) โ ๐ถ โฅ (๐ด + ๐ต))) |
53 | 52 | adantl 483 |
. . . . . 6
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ
(โ๐ โ โ
(๐ด + ๐ต) = (๐ถโ๐) โ ๐ถ โฅ (๐ด + ๐ต))) |
54 | 53 | adantr 482 |
. . . . 5
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ (โ๐ โ โ (๐ด + ๐ต) = (๐ถโ๐) โ ๐ถ โฅ (๐ด + ๐ต))) |
55 | 12, 34 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ (๐ด โ ๐ต) โ โค) |
56 | 55 | 3adant3 1133 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ (๐ด โ ๐ต) โ โค) |
57 | 21 | biimp3a 1470 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ 1 < (๐ด โ ๐ต)) |
58 | | eluz2b1 12849 |
. . . . . . . . . . 11
โข ((๐ด โ ๐ต) โ (โคโฅโ2)
โ ((๐ด โ ๐ต) โ โค โง 1 <
(๐ด โ ๐ต))) |
59 | 56, 57, 58 | sylanbrc 584 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ (๐ด โ ๐ต) โ
(โคโฅโ2)) |
60 | 59 | adantr 482 |
. . . . . . . . 9
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ (๐ด โ ๐ต) โ
(โคโฅโ2)) |
61 | 9, 60, 31 | 3jca 1129 |
. . . . . . . 8
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ (๐ถ โ โ โง (๐ด โ ๐ต) โ (โคโฅโ2)
โง ๐ท โ
โ0)) |
62 | 61 | adantr 482 |
. . . . . . 7
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ (๐ถ โ โ โง (๐ด โ ๐ต) โ (โคโฅโ2)
โง ๐ท โ
โ0)) |
63 | | dvdsmul2 16166 |
. . . . . . . . . 10
โข (((๐ด + ๐ต) โ โค โง (๐ด โ ๐ต) โ โค) โ (๐ด โ ๐ต) โฅ ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) |
64 | 37, 63 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ (๐ด โ ๐ต) โฅ ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) |
65 | 64 | ad2antrr 725 |
. . . . . . . 8
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ (๐ด โ ๐ต) โฅ ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) |
66 | | breq2 5110 |
. . . . . . . . 9
โข ((๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต)) โ ((๐ด โ ๐ต) โฅ (๐ถโ๐ท) โ (๐ด โ ๐ต) โฅ ((๐ด + ๐ต) ยท (๐ด โ ๐ต)))) |
67 | 66 | adantl 483 |
. . . . . . . 8
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ ((๐ด โ ๐ต) โฅ (๐ถโ๐ท) โ (๐ด โ ๐ต) โฅ ((๐ด + ๐ต) ยท (๐ด โ ๐ต)))) |
68 | 65, 67 | mpbird 257 |
. . . . . . 7
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ (๐ด โ ๐ต) โฅ (๐ถโ๐ท)) |
69 | | dvdsprmpweqnn 16762 |
. . . . . . 7
โข ((๐ถ โ โ โง (๐ด โ ๐ต) โ (โคโฅโ2)
โง ๐ท โ
โ0) โ ((๐ด โ ๐ต) โฅ (๐ถโ๐ท) โ โ๐ โ โ (๐ด โ ๐ต) = (๐ถโ๐))) |
70 | 62, 68, 69 | sylc 65 |
. . . . . 6
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ โ๐ โ โ (๐ด โ ๐ต) = (๐ถโ๐)) |
71 | | iddvdsexp 16167 |
. . . . . . . . . . . . 13
โข ((๐ถ โ โค โง ๐ โ โ) โ ๐ถ โฅ (๐ถโ๐)) |
72 | 46, 71 | sylan 581 |
. . . . . . . . . . . 12
โข ((๐ถ โ โ โง ๐ โ โ) โ ๐ถ โฅ (๐ถโ๐)) |
73 | | breq2 5110 |
. . . . . . . . . . . 12
โข ((๐ด โ ๐ต) = (๐ถโ๐) โ (๐ถ โฅ (๐ด โ ๐ต) โ ๐ถ โฅ (๐ถโ๐))) |
74 | 72, 73 | syl5ibrcom 247 |
. . . . . . . . . . 11
โข ((๐ถ โ โ โง ๐ โ โ) โ ((๐ด โ ๐ต) = (๐ถโ๐) โ ๐ถ โฅ (๐ด โ ๐ต))) |
75 | 74 | rexlimdva 3149 |
. . . . . . . . . 10
โข (๐ถ โ โ โ
(โ๐ โ โ
(๐ด โ ๐ต) = (๐ถโ๐) โ ๐ถ โฅ (๐ด โ ๐ต))) |
76 | 75 | adantr 482 |
. . . . . . . . 9
โข ((๐ถ โ โ โง ๐ท โ โ0)
โ (โ๐ โ
โ (๐ด โ ๐ต) = (๐ถโ๐) โ ๐ถ โฅ (๐ด โ ๐ต))) |
77 | 76 | adantl 483 |
. . . . . . . 8
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ
(โ๐ โ โ
(๐ด โ ๐ต) = (๐ถโ๐) โ ๐ถ โฅ (๐ด โ ๐ต))) |
78 | 77 | adantr 482 |
. . . . . . 7
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ (โ๐ โ โ (๐ด โ ๐ต) = (๐ถโ๐) โ ๐ถ โฅ (๐ด โ ๐ต))) |
79 | 46 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ถ โ โ โง ๐ท โ โ0)
โ ๐ถ โ
โค) |
80 | 37, 79 | anim12ci 615 |
. . . . . . . . . . . 12
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ (๐ถ โ โค โง ((๐ด + ๐ต) โ โค โง (๐ด โ ๐ต) โ โค))) |
81 | | 3anass 1096 |
. . . . . . . . . . . 12
โข ((๐ถ โ โค โง (๐ด + ๐ต) โ โค โง (๐ด โ ๐ต) โ โค) โ (๐ถ โ โค โง ((๐ด + ๐ต) โ โค โง (๐ด โ ๐ต) โ โค))) |
82 | 80, 81 | sylibr 233 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ (๐ถ โ โค โง (๐ด + ๐ต) โ โค โง (๐ด โ ๐ต) โ โค)) |
83 | | dvds2sub 16178 |
. . . . . . . . . . 11
โข ((๐ถ โ โค โง (๐ด + ๐ต) โ โค โง (๐ด โ ๐ต) โ โค) โ ((๐ถ โฅ (๐ด + ๐ต) โง ๐ถ โฅ (๐ด โ ๐ต)) โ ๐ถ โฅ ((๐ด + ๐ต) โ (๐ด โ ๐ต)))) |
84 | 82, 83 | syl 17 |
. . . . . . . . . 10
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ ((๐ถ โฅ (๐ด + ๐ต) โง ๐ถ โฅ (๐ด โ ๐ต)) โ ๐ถ โฅ ((๐ด + ๐ต) โ (๐ด โ ๐ต)))) |
85 | 1 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ ๐ด โ โ) |
86 | 2 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ ๐ต โ โ) |
87 | 85, 86, 86 | pnncand 11556 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ ((๐ด + ๐ต) โ (๐ด โ ๐ต)) = (๐ต + ๐ต)) |
88 | 2 | 2timesd 12401 |
. . . . . . . . . . . . . . . 16
โข (๐ต โ โ0
โ (2 ยท ๐ต) =
(๐ต + ๐ต)) |
89 | 88 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
โข (๐ต โ โ0
โ (๐ต + ๐ต) = (2 ยท ๐ต)) |
90 | 89 | 3ad2ant2 1135 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ (๐ต + ๐ต) = (2 ยท ๐ต)) |
91 | 87, 90 | eqtrd 2773 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ ((๐ด + ๐ต) โ (๐ด โ ๐ต)) = (2 ยท ๐ต)) |
92 | 91 | breq2d 5118 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ (๐ถ โฅ ((๐ด + ๐ต) โ (๐ด โ ๐ต)) โ ๐ถ โฅ (2 ยท ๐ต))) |
93 | 92 | biimpd 228 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โ (๐ถ โฅ ((๐ด + ๐ต) โ (๐ด โ ๐ต)) โ ๐ถ โฅ (2 ยท ๐ต))) |
94 | 93 | adantr 482 |
. . . . . . . . . 10
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ (๐ถ โฅ ((๐ด + ๐ต) โ (๐ด โ ๐ต)) โ ๐ถ โฅ (2 ยท ๐ต))) |
95 | 84, 94 | syld 47 |
. . . . . . . . 9
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ ((๐ถ โฅ (๐ด + ๐ต) โง ๐ถ โฅ (๐ด โ ๐ต)) โ ๐ถ โฅ (2 ยท ๐ต))) |
96 | 95 | expcomd 418 |
. . . . . . . 8
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ (๐ถ โฅ (๐ด โ ๐ต) โ (๐ถ โฅ (๐ด + ๐ต) โ ๐ถ โฅ (2 ยท ๐ต)))) |
97 | 96 | adantr 482 |
. . . . . . 7
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ (๐ถ โฅ (๐ด โ ๐ต) โ (๐ถ โฅ (๐ด + ๐ต) โ ๐ถ โฅ (2 ยท ๐ต)))) |
98 | 78, 97 | syld 47 |
. . . . . 6
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ (โ๐ โ โ (๐ด โ ๐ต) = (๐ถโ๐) โ (๐ถ โฅ (๐ด + ๐ต) โ ๐ถ โฅ (2 ยท ๐ต)))) |
99 | 70, 98 | mpd 15 |
. . . . 5
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ (๐ถ โฅ (๐ด + ๐ต) โ ๐ถ โฅ (2 ยท ๐ต))) |
100 | 54, 99 | syld 47 |
. . . 4
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ (โ๐ โ โ (๐ด + ๐ต) = (๐ถโ๐) โ ๐ถ โฅ (2 ยท ๐ต))) |
101 | 45, 100 | mpd 15 |
. . 3
โข ((((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โง (๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) โ ๐ถ โฅ (2 ยท ๐ต)) |
102 | 101 | ex 414 |
. 2
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ ((๐ถโ๐ท) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต)) โ ๐ถ โฅ (2 ยท ๐ต))) |
103 | 8, 102 | sylbid 239 |
1
โข (((๐ด โ โ0
โง ๐ต โ
โ0 โง (๐ต + 1) < ๐ด) โง (๐ถ โ โ โง ๐ท โ โ0)) โ ((๐ถโ๐ท) = ((๐ดโ2) โ (๐ตโ2)) โ ๐ถ โฅ (2 ยท ๐ต))) |