Step | Hyp | Ref
| Expression |
1 | | odd2np1 16158 |
. . . . 5
โข (๐ด โ โค โ (ยฌ 2
โฅ ๐ด โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐ด)) |
2 | | odd2np1 16158 |
. . . . 5
โข (๐ต โ โค โ (ยฌ 2
โฅ ๐ต โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐ต)) |
3 | 1, 2 | bi2anan9 638 |
. . . 4
โข ((๐ด โ โค โง ๐ต โ โค) โ ((ยฌ
2 โฅ ๐ด โง ยฌ 2
โฅ ๐ต) โ
(โ๐ โ โค
((2 ยท ๐) + 1) =
๐ด โง โ๐ โ โค ((2 ยท
๐) + 1) = ๐ต))) |
4 | | reeanv 3216 |
. . . . 5
โข
(โ๐ โ
โค โ๐ โ
โค (((2 ยท ๐) +
1) = ๐ด โง ((2 ยท
๐) + 1) = ๐ต) โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ด โง โ๐ โ โค ((2 ยท ๐) + 1) = ๐ต)) |
5 | | 2z 12466 |
. . . . . . . . 9
โข 2 โ
โค |
6 | | zaddcl 12474 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + ๐) โ โค) |
7 | 6 | peano2zd 12543 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ + ๐) + 1) โ โค) |
8 | | dvdsmul1 16095 |
. . . . . . . . 9
โข ((2
โ โค โง ((๐ +
๐) + 1) โ โค)
โ 2 โฅ (2 ยท ((๐ + ๐) + 1))) |
9 | 5, 7, 8 | sylancr 588 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ 2
โฅ (2 ยท ((๐ +
๐) + 1))) |
10 | | zcn 12438 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
โ) |
11 | | zcn 12438 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
โ) |
12 | | addcl 11067 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + ๐) โ โ) |
13 | | 2cn 12162 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
14 | | ax-1cn 11043 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
15 | | adddi 11074 |
. . . . . . . . . . . . . 14
โข ((2
โ โ โง (๐ +
๐) โ โ โง 1
โ โ) โ (2 ยท ((๐ + ๐) + 1)) = ((2 ยท (๐ + ๐)) + (2 ยท 1))) |
16 | 13, 14, 15 | mp3an13 1453 |
. . . . . . . . . . . . 13
โข ((๐ + ๐) โ โ โ (2 ยท ((๐ + ๐) + 1)) = ((2 ยท (๐ + ๐)) + (2 ยท 1))) |
17 | 12, 16 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ((๐ + ๐) + 1)) = ((2 ยท (๐ + ๐)) + (2 ยท 1))) |
18 | | adddi 11074 |
. . . . . . . . . . . . . 14
โข ((2
โ โ โง ๐
โ โ โง ๐
โ โ) โ (2 ยท (๐ + ๐)) = ((2 ยท ๐) + (2 ยท ๐))) |
19 | 13, 18 | mp3an1 1449 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท (๐ + ๐)) = ((2 ยท ๐) + (2 ยท ๐))) |
20 | 19 | oveq1d 7365 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ ((2
ยท (๐ + ๐)) + (2 ยท 1)) = (((2
ยท ๐) + (2 ยท
๐)) + (2 ยท
1))) |
21 | 17, 20 | eqtrd 2778 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ((๐ + ๐) + 1)) = (((2 ยท ๐) + (2 ยท ๐)) + (2 ยท
1))) |
22 | | 2t1e2 12250 |
. . . . . . . . . . . . 13
โข (2
ยท 1) = 2 |
23 | | df-2 12150 |
. . . . . . . . . . . . 13
โข 2 = (1 +
1) |
24 | 22, 23 | eqtri 2766 |
. . . . . . . . . . . 12
โข (2
ยท 1) = (1 + 1) |
25 | 24 | oveq2i 7361 |
. . . . . . . . . . 11
โข (((2
ยท ๐) + (2 ยท
๐)) + (2 ยท 1)) =
(((2 ยท ๐) + (2
ยท ๐)) + (1 +
1)) |
26 | 21, 25 | eqtrdi 2794 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ((๐ + ๐) + 1)) = (((2 ยท ๐) + (2 ยท ๐)) + (1 + 1))) |
27 | | mulcl 11069 |
. . . . . . . . . . . 12
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
28 | 13, 27 | mpan 689 |
. . . . . . . . . . 11
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
29 | | mulcl 11069 |
. . . . . . . . . . . 12
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
30 | 13, 29 | mpan 689 |
. . . . . . . . . . 11
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
31 | | add4 11309 |
. . . . . . . . . . . 12
โข ((((2
ยท ๐) โ โ
โง (2 ยท ๐) โ
โ) โง (1 โ โ โง 1 โ โ)) โ (((2 ยท
๐) + (2 ยท ๐)) + (1 + 1)) = (((2 ยท
๐) + 1) + ((2 ยท
๐) + 1))) |
32 | 14, 14, 31 | mpanr12 704 |
. . . . . . . . . . 11
โข (((2
ยท ๐) โ โ
โง (2 ยท ๐) โ
โ) โ (((2 ยท ๐) + (2 ยท ๐)) + (1 + 1)) = (((2 ยท ๐) + 1) + ((2 ยท ๐) + 1))) |
33 | 28, 30, 32 | syl2an 597 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (((2
ยท ๐) + (2 ยท
๐)) + (1 + 1)) = (((2
ยท ๐) + 1) + ((2
ยท ๐) +
1))) |
34 | 26, 33 | eqtrd 2778 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ((๐ + ๐) + 1)) = (((2 ยท ๐) + 1) + ((2 ยท ๐) + 1))) |
35 | 10, 11, 34 | syl2an 597 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ (2
ยท ((๐ + ๐) + 1)) = (((2 ยท ๐) + 1) + ((2 ยท ๐) + 1))) |
36 | 9, 35 | breqtrd 5130 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ 2
โฅ (((2 ยท ๐) +
1) + ((2 ยท ๐) +
1))) |
37 | | oveq12 7359 |
. . . . . . . 8
โข ((((2
ยท ๐) + 1) = ๐ด โง ((2 ยท ๐) + 1) = ๐ต) โ (((2 ยท ๐) + 1) + ((2 ยท ๐) + 1)) = (๐ด + ๐ต)) |
38 | 37 | breq2d 5116 |
. . . . . . 7
โข ((((2
ยท ๐) + 1) = ๐ด โง ((2 ยท ๐) + 1) = ๐ต) โ (2 โฅ (((2 ยท ๐) + 1) + ((2 ยท ๐) + 1)) โ 2 โฅ (๐ด + ๐ต))) |
39 | 36, 38 | syl5ibcom 245 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โค) โ ((((2
ยท ๐) + 1) = ๐ด โง ((2 ยท ๐) + 1) = ๐ต) โ 2 โฅ (๐ด + ๐ต))) |
40 | 39 | rexlimivv 3195 |
. . . . 5
โข
(โ๐ โ
โค โ๐ โ
โค (((2 ยท ๐) +
1) = ๐ด โง ((2 ยท
๐) + 1) = ๐ต) โ 2 โฅ (๐ด + ๐ต)) |
41 | 4, 40 | sylbir 234 |
. . . 4
โข
((โ๐ โ
โค ((2 ยท ๐) +
1) = ๐ด โง โ๐ โ โค ((2 ยท
๐) + 1) = ๐ต) โ 2 โฅ (๐ด + ๐ต)) |
42 | 3, 41 | syl6bi 253 |
. . 3
โข ((๐ด โ โค โง ๐ต โ โค) โ ((ยฌ
2 โฅ ๐ด โง ยฌ 2
โฅ ๐ต) โ 2 โฅ
(๐ด + ๐ต))) |
43 | 42 | imp 408 |
. 2
โข (((๐ด โ โค โง ๐ต โ โค) โง (ยฌ 2
โฅ ๐ด โง ยฌ 2
โฅ ๐ต)) โ 2
โฅ (๐ด + ๐ต)) |
44 | 43 | an4s 659 |
1
โข (((๐ด โ โค โง ยฌ 2
โฅ ๐ด) โง (๐ต โ โค โง ยฌ 2
โฅ ๐ต)) โ 2
โฅ (๐ด + ๐ต)) |