Step | Hyp | Ref
| Expression |
1 | | evennn2n 16109 |
. . . 4
โข (๐ โ โ โ (2
โฅ ๐ โ
โ๐ โ โ (2
ยท ๐) = ๐)) |
2 | 1 | 3ad2ant3 1135 |
. . 3
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (2 โฅ ๐ โ
โ๐ โ โ (2
ยท ๐) = ๐)) |
3 | | oveq2 7315 |
. . . . . . . . 9
โข (๐ = (2 ยท ๐) โ (2โ๐) = (2โ(2 ยท ๐))) |
4 | 3 | eqcoms 2744 |
. . . . . . . 8
โข ((2
ยท ๐) = ๐ โ (2โ๐) = (2โ(2 ยท ๐))) |
5 | | 2cnd 12101 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 2 โ
โ) |
6 | | nncn 12031 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
7 | 5, 6 | mulcomd 11046 |
. . . . . . . . . . 11
โข (๐ โ โ โ (2
ยท ๐) = (๐ ยท 2)) |
8 | 7 | oveq2d 7323 |
. . . . . . . . . 10
โข (๐ โ โ โ
(2โ(2 ยท ๐)) =
(2โ(๐ ยท
2))) |
9 | | 2nn0 12300 |
. . . . . . . . . . . 12
โข 2 โ
โ0 |
10 | 9 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ โ 2 โ
โ0) |
11 | | nnnn0 12290 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ0) |
12 | 5, 10, 11 | expmuld 13917 |
. . . . . . . . . 10
โข (๐ โ โ โ
(2โ(๐ ยท 2)) =
((2โ๐)โ2)) |
13 | 8, 12 | eqtrd 2776 |
. . . . . . . . 9
โข (๐ โ โ โ
(2โ(2 ยท ๐)) =
((2โ๐)โ2)) |
14 | 13 | adantl 483 |
. . . . . . . 8
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โ (2โ(2 ยท ๐)) = ((2โ๐)โ2)) |
15 | 4, 14 | sylan9eqr 2798 |
. . . . . . 7
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง (2 ยท ๐) =
๐) โ (2โ๐) = ((2โ๐)โ2)) |
16 | 15 | oveq1d 7322 |
. . . . . 6
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง (2 ยท ๐) =
๐) โ ((2โ๐) โ 1) = (((2โ๐)โ2) โ
1)) |
17 | 16 | eqeq1d 2738 |
. . . . 5
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง (2 ยท ๐) =
๐) โ (((2โ๐) โ 1) = (๐โ๐) โ (((2โ๐)โ2) โ 1) = (๐โ๐))) |
18 | | elnn1uz2 12715 |
. . . . . . . 8
โข (๐ โ โ โ (๐ = 1 โจ ๐ โ
(โคโฅโ2))) |
19 | | oveq2 7315 |
. . . . . . . . . . . . . . . . 17
โข (๐ = 1 โ (2โ๐) = (2โ1)) |
20 | | 2cn 12098 |
. . . . . . . . . . . . . . . . . 18
โข 2 โ
โ |
21 | | exp1 13838 |
. . . . . . . . . . . . . . . . . 18
โข (2 โ
โ โ (2โ1) = 2) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
โข
(2โ1) = 2 |
23 | 19, 22 | eqtrdi 2792 |
. . . . . . . . . . . . . . . 16
โข (๐ = 1 โ (2โ๐) = 2) |
24 | 23 | oveq1d 7322 |
. . . . . . . . . . . . . . 15
โข (๐ = 1 โ ((2โ๐)โ2) =
(2โ2)) |
25 | 24 | oveq1d 7322 |
. . . . . . . . . . . . . 14
โข (๐ = 1 โ (((2โ๐)โ2) โ 1) =
((2โ2) โ 1)) |
26 | | sq2 13964 |
. . . . . . . . . . . . . . . 16
โข
(2โ2) = 4 |
27 | 26 | oveq1i 7317 |
. . . . . . . . . . . . . . 15
โข
((2โ2) โ 1) = (4 โ 1) |
28 | | 4m1e3 12152 |
. . . . . . . . . . . . . . 15
โข (4
โ 1) = 3 |
29 | 27, 28 | eqtri 2764 |
. . . . . . . . . . . . . 14
โข
((2โ2) โ 1) = 3 |
30 | 25, 29 | eqtrdi 2792 |
. . . . . . . . . . . . 13
โข (๐ = 1 โ (((2โ๐)โ2) โ 1) =
3) |
31 | 30 | eqeq1d 2738 |
. . . . . . . . . . . 12
โข (๐ = 1 โ ((((2โ๐)โ2) โ 1) = (๐โ๐) โ 3 = (๐โ๐))) |
32 | 31 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ = 1 โง (๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ)) โ
((((2โ๐)โ2)
โ 1) = (๐โ๐) โ 3 = (๐โ๐))) |
33 | | eqcom 2743 |
. . . . . . . . . . . . . 14
โข (3 =
(๐โ๐) โ (๐โ๐) = 3) |
34 | | eldifi 4067 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
35 | | prmnn 16428 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
โ) |
36 | | nnre 12030 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
โ) |
37 | 34, 35, 36 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
38 | 37 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ โ
โ) |
39 | | nnnn0 12290 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ ๐ โ
โ0) |
40 | 39 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ โ
โ0) |
41 | 38, 40 | reexpcld 13931 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐โ๐) โ
โ) |
42 | 41 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (๐โ๐) = 3) โ (๐โ๐) โ โ) |
43 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (๐โ๐) = 3) โ (๐โ๐) = 3) |
44 | 42, 43 | eqled 11128 |
. . . . . . . . . . . . . . 15
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (๐โ๐) = 3) โ (๐โ๐) โค 3) |
45 | 44 | ex 414 |
. . . . . . . . . . . . . 14
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((๐โ๐) = 3 โ (๐โ๐) โค 3)) |
46 | 33, 45 | syl5bi 242 |
. . . . . . . . . . . . 13
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (3 = (๐โ๐) โ (๐โ๐) โค 3)) |
47 | 35 | nnred 12038 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ๐ โ
โ) |
48 | | prmgt1 16451 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ 1 <
๐) |
49 | 47, 48 | jca 513 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (๐ โ โ โง 1 <
๐)) |
50 | 34, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (โ โ {2})
โ (๐ โ โ
โง 1 < ๐)) |
51 | 50 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐ โ โ
โง 1 < ๐)) |
52 | | nnz 12392 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ๐ โ
โค) |
53 | 52 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ โ
โค) |
54 | | 3rp 12786 |
. . . . . . . . . . . . . . . 16
โข 3 โ
โ+ |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ 3 โ โ+) |
56 | | efexple 26478 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง 1 <
๐) โง ๐ โ โค โง 3 โ
โ+) โ ((๐โ๐) โค 3 โ ๐ โค (โโ((logโ3) /
(logโ๐))))) |
57 | 51, 53, 55, 56 | syl3anc 1371 |
. . . . . . . . . . . . . 14
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((๐โ๐) โค 3 โ ๐ โค
(โโ((logโ3) / (logโ๐))))) |
58 | | oddprmge3 16454 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โ โ {2})
โ ๐ โ
(โคโฅโ3)) |
59 | | eluzle 12645 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ
(โคโฅโ3) โ 3 โค ๐) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โ โ {2})
โ 3 โค ๐) |
61 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โ โ {2})
โ 3 โ โ+) |
62 | | nnrp 12791 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
โ+) |
63 | 34, 35, 62 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โ โ {2})
โ ๐ โ
โ+) |
64 | 61, 63 | logled 25831 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โ โ {2})
โ (3 โค ๐ โ
(logโ3) โค (logโ๐))) |
65 | 60, 64 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โ โ {2})
โ (logโ3) โค (logโ๐)) |
66 | 65 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (logโ3) โค (logโ๐)) |
67 | | relogcl 25780 |
. . . . . . . . . . . . . . . . . 18
โข (3 โ
โ+ โ (logโ3) โ โ) |
68 | 54, 67 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
โข
(logโ3) โ โ |
69 | | rplogcl 25808 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง 1 <
๐) โ (logโ๐) โ
โ+) |
70 | 34, 49, 69 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โ โ {2})
โ (logโ๐) โ
โ+) |
71 | 70 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (logโ๐) โ
โ+) |
72 | | divle1le 12850 |
. . . . . . . . . . . . . . . . 17
โข
(((logโ3) โ โ โง (logโ๐) โ โ+) โ
(((logโ3) / (logโ๐)) โค 1 โ (logโ3) โค
(logโ๐))) |
73 | 68, 71, 72 | sylancr 588 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (((logโ3) / (logโ๐)) โค 1 โ (logโ3) โค
(logโ๐))) |
74 | 66, 73 | mpbird 257 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((logโ3) / (logโ๐)) โค 1) |
75 | | fldivle 13601 |
. . . . . . . . . . . . . . . . 17
โข
(((logโ3) โ โ โง (logโ๐) โ โ+) โ
(โโ((logโ3) / (logโ๐))) โค ((logโ3) / (logโ๐))) |
76 | 68, 71, 75 | sylancr 588 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (โโ((logโ3) / (logโ๐))) โค ((logโ3) / (logโ๐))) |
77 | | nnre 12030 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ ๐ โ
โ) |
78 | 77 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ โ
โ) |
79 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (โ โ {2})
โ (logโ3) โ โ) |
80 | 62 | relogcld 25827 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ
(logโ๐) โ
โ) |
81 | 34, 35, 80 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (โ โ {2})
โ (logโ๐) โ
โ) |
82 | 35 | nnrpd 12820 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ ๐ โ
โ+) |
83 | | 1red 11026 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ 1 โ
โ) |
84 | 83, 48 | gtned 11160 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ ๐ โ 1) |
85 | 82, 84 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ (๐ โ โ+
โง ๐ โ
1)) |
86 | | logne0 25784 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โ+
โง ๐ โ 1) โ
(logโ๐) โ
0) |
87 | 34, 85, 86 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (โ โ {2})
โ (logโ๐) โ
0) |
88 | 79, 81, 87 | redivcld 11853 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (โ โ {2})
โ ((logโ3) / (logโ๐)) โ โ) |
89 | 88 | flcld 13568 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โ โ {2})
โ (โโ((logโ3) / (logโ๐))) โ โค) |
90 | 89 | zred 12476 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โ โ {2})
โ (โโ((logโ3) / (logโ๐))) โ โ) |
91 | 90 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (โโ((logโ3) / (logโ๐))) โ โ) |
92 | 88 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((logโ3) / (logโ๐)) โ โ) |
93 | | letr 11119 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง
(โโ((logโ3) / (logโ๐))) โ โ โง ((logโ3) /
(logโ๐)) โ
โ) โ ((๐ โค
(โโ((logโ3) / (logโ๐))) โง (โโ((logโ3) /
(logโ๐))) โค
((logโ3) / (logโ๐))) โ ๐ โค ((logโ3) / (logโ๐)))) |
94 | 78, 91, 92, 93 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((๐ โค
(โโ((logโ3) / (logโ๐))) โง (โโ((logโ3) /
(logโ๐))) โค
((logโ3) / (logโ๐))) โ ๐ โค ((logโ3) / (logโ๐)))) |
95 | | 1red 11026 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ 1 โ โ) |
96 | | letr 11119 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ โง
((logโ3) / (logโ๐)) โ โ โง 1 โ โ)
โ ((๐ โค
((logโ3) / (logโ๐)) โง ((logโ3) / (logโ๐)) โค 1) โ ๐ โค 1)) |
97 | 78, 92, 95, 96 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((๐ โค
((logโ3) / (logโ๐)) โง ((logโ3) / (logโ๐)) โค 1) โ ๐ โค 1)) |
98 | | nnge1 12051 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ 1 โค
๐) |
99 | | eqcom 2743 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = 1 โ 1 = ๐) |
100 | | 1red 11026 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ 1 โ
โ) |
101 | 100, 77 | letri3d 11167 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ (1 =
๐ โ (1 โค ๐ โง ๐ โค 1))) |
102 | 99, 101 | bitr2id 284 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ ((1 โค
๐ โง ๐ โค 1) โ ๐ = 1)) |
103 | 102 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ ((1 โค
๐ โง ๐ โค 1) โ ๐ = 1)) |
104 | 98, 103 | mpand 693 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ (๐ โค 1 โ ๐ = 1)) |
105 | 104 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐ โค 1 โ
๐ = 1)) |
106 | 97, 105 | syld 47 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((๐ โค
((logโ3) / (logโ๐)) โง ((logโ3) / (logโ๐)) โค 1) โ ๐ = 1)) |
107 | 106 | expd 417 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐ โค
((logโ3) / (logโ๐)) โ (((logโ3) / (logโ๐)) โค 1 โ ๐ = 1))) |
108 | 94, 107 | syld 47 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((๐ โค
(โโ((logโ3) / (logโ๐))) โง (โโ((logโ3) /
(logโ๐))) โค
((logโ3) / (logโ๐))) โ (((logโ3) /
(logโ๐)) โค 1
โ ๐ =
1))) |
109 | 76, 108 | mpan2d 692 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐ โค
(โโ((logโ3) / (logโ๐))) โ (((logโ3) /
(logโ๐)) โค 1
โ ๐ =
1))) |
110 | 74, 109 | mpid 44 |
. . . . . . . . . . . . . 14
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐ โค
(โโ((logโ3) / (logโ๐))) โ ๐ = 1)) |
111 | 57, 110 | sylbid 239 |
. . . . . . . . . . . . 13
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((๐โ๐) โค 3 โ ๐ = 1)) |
112 | 46, 111 | syld 47 |
. . . . . . . . . . . 12
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (3 = (๐โ๐) โ ๐ = 1)) |
113 | 112 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ = 1 โง (๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ)) โ (3 =
(๐โ๐) โ ๐ = 1)) |
114 | 32, 113 | sylbid 239 |
. . . . . . . . . 10
โข ((๐ = 1 โง (๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ)) โ
((((2โ๐)โ2)
โ 1) = (๐โ๐) โ ๐ = 1)) |
115 | 114 | ex 414 |
. . . . . . . . 9
โข (๐ = 1 โ ((๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โ
((((2โ๐)โ2)
โ 1) = (๐โ๐) โ ๐ = 1))) |
116 | | sq1 13962 |
. . . . . . . . . . . . . 14
โข
(1โ2) = 1 |
117 | 116 | eqcomi 2745 |
. . . . . . . . . . . . 13
โข 1 =
(1โ2) |
118 | 117 | oveq2i 7318 |
. . . . . . . . . . . 12
โข
(((2โ๐)โ2)
โ 1) = (((2โ๐)โ2) โ
(1โ2)) |
119 | 118 | eqeq1i 2741 |
. . . . . . . . . . 11
โข
((((2โ๐)โ2) โ 1) = (๐โ๐) โ (((2โ๐)โ2) โ (1โ2)) = (๐โ๐)) |
120 | | eqcom 2743 |
. . . . . . . . . . . 12
โข
((((2โ๐)โ2) โ (1โ2)) = (๐โ๐) โ (๐โ๐) = (((2โ๐)โ2) โ
(1โ2))) |
121 | 9 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ
(โคโฅโ2) โ 2 โ
โ0) |
122 | | eluzge2nn0 12677 |
. . . . . . . . . . . . . . . 16
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ0) |
123 | 121, 122 | nn0expcld 14011 |
. . . . . . . . . . . . . . 15
โข (๐ โ
(โคโฅโ2) โ (2โ๐) โ
โ0) |
124 | 123 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ
(โคโฅโ2) โง (๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ)) โ
(2โ๐) โ
โ0) |
125 | | 1nn0 12299 |
. . . . . . . . . . . . . . 15
โข 1 โ
โ0 |
126 | 125 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ โ
(โคโฅโ2) โง (๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ)) โ 1
โ โ0) |
127 | | 1p1e2 12148 |
. . . . . . . . . . . . . . . . 17
โข (1 + 1) =
2 |
128 | 22 | eqcomi 2745 |
. . . . . . . . . . . . . . . . 17
โข 2 =
(2โ1) |
129 | 127, 128 | eqtri 2764 |
. . . . . . . . . . . . . . . 16
โข (1 + 1) =
(2โ1) |
130 | | eluz2gt1 12710 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ
(โคโฅโ2) โ 1 < ๐) |
131 | | 2re 12097 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โ
โ |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ
(โคโฅโ2) โ 2 โ โ) |
133 | | 1zzd 12401 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ
(โคโฅโ2) โ 1 โ โค) |
134 | | eluzelz 12642 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ
(โคโฅโ2) โ ๐ โ โค) |
135 | | 1lt2 12194 |
. . . . . . . . . . . . . . . . . . 19
โข 1 <
2 |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ
(โคโฅโ2) โ 1 < 2) |
137 | 132, 133,
134, 136 | ltexp2d 14018 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ
(โคโฅโ2) โ (1 < ๐ โ (2โ1) < (2โ๐))) |
138 | 130, 137 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข (๐ โ
(โคโฅโ2) โ (2โ1) < (2โ๐)) |
139 | 129, 138 | eqbrtrid 5116 |
. . . . . . . . . . . . . . 15
โข (๐ โ
(โคโฅโ2) โ (1 + 1) < (2โ๐)) |
140 | 139 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ
(โคโฅโ2) โง (๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ)) โ (1 + 1)
< (2โ๐)) |
141 | 34, 39 | anim12i 614 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (๐ โ โ
โง ๐ โ
โ0)) |
142 | 141 | 3adant3 1132 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐ โ โ
โง ๐ โ
โ0)) |
143 | 142 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โ
(โคโฅโ2) โง (๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ)) โ (๐ โ โ โง ๐ โ
โ0)) |
144 | | difsqpwdvds 16637 |
. . . . . . . . . . . . . 14
โข
((((2โ๐) โ
โ0 โง 1 โ โ0 โง (1 + 1) <
(2โ๐)) โง (๐ โ โ โง ๐ โ โ0))
โ ((๐โ๐) = (((2โ๐)โ2) โ (1โ2)) โ ๐ โฅ (2 ยท
1))) |
145 | 124, 126,
140, 143, 144 | syl31anc 1373 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ2) โง (๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ)) โ ((๐โ๐) = (((2โ๐)โ2) โ (1โ2)) โ ๐ โฅ (2 ยท
1))) |
146 | | 2t1e2 12186 |
. . . . . . . . . . . . . . . . . 18
โข (2
ยท 1) = 2 |
147 | 146 | breq2i 5089 |
. . . . . . . . . . . . . . . . 17
โข (๐ โฅ (2 ยท 1) โ
๐ โฅ
2) |
148 | | prmuz2 16450 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
149 | 34, 148 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โ โ {2})
โ ๐ โ
(โคโฅโ2)) |
150 | | 2prm 16446 |
. . . . . . . . . . . . . . . . . 18
โข 2 โ
โ |
151 | | dvdsprm 16457 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ
(โคโฅโ2) โง 2 โ โ) โ (๐ โฅ 2 โ ๐ = 2)) |
152 | 149, 150,
151 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โ โ {2})
โ (๐ โฅ 2 โ
๐ = 2)) |
153 | 147, 152 | bitrid 283 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (โ โ {2})
โ (๐ โฅ (2
ยท 1) โ ๐ =
2)) |
154 | | eldifsn 4726 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โ โ {2})
โ (๐ โ โ
โง ๐ โ
2)) |
155 | | eqneqall 2952 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = 2 โ (๐ โ 2 โ ๐ = 1)) |
156 | 155 | com12 32 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 2 โ (๐ = 2 โ ๐ = 1)) |
157 | 154, 156 | simplbiim 506 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (โ โ {2})
โ (๐ = 2 โ ๐ = 1)) |
158 | 153, 157 | sylbid 239 |
. . . . . . . . . . . . . . 15
โข (๐ โ (โ โ {2})
โ (๐ โฅ (2
ยท 1) โ ๐ =
1)) |
159 | 158 | 3ad2ant1 1133 |
. . . . . . . . . . . . . 14
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐ โฅ (2
ยท 1) โ ๐ =
1)) |
160 | 159 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ2) โง (๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ)) โ (๐ โฅ (2 ยท 1) โ
๐ = 1)) |
161 | 145, 160 | syld 47 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ)) โ ((๐โ๐) = (((2โ๐)โ2) โ (1โ2)) โ ๐ = 1)) |
162 | 120, 161 | syl5bi 242 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ)) โ
((((2โ๐)โ2)
โ (1โ2)) = (๐โ๐) โ ๐ = 1)) |
163 | 119, 162 | syl5bi 242 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ2) โง (๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ)) โ
((((2โ๐)โ2)
โ 1) = (๐โ๐) โ ๐ = 1)) |
164 | 163 | ex 414 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ2) โ ((๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โ
((((2โ๐)โ2)
โ 1) = (๐โ๐) โ ๐ = 1))) |
165 | 115, 164 | jaoi 855 |
. . . . . . . 8
โข ((๐ = 1 โจ ๐ โ (โคโฅโ2))
โ ((๐ โ (โ
โ {2}) โง ๐ โ
โ โง ๐ โ
โ) โ ((((2โ๐)โ2) โ 1) = (๐โ๐) โ ๐ = 1))) |
166 | 18, 165 | sylbi 216 |
. . . . . . 7
โข (๐ โ โ โ ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((((2โ๐)โ2) โ 1) = (๐โ๐) โ ๐ = 1))) |
167 | 166 | impcom 409 |
. . . . . 6
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โ ((((2โ๐)โ2) โ 1) = (๐โ๐) โ ๐ = 1)) |
168 | 167 | adantr 482 |
. . . . 5
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง (2 ยท ๐) =
๐) โ ((((2โ๐)โ2) โ 1) = (๐โ๐) โ ๐ = 1)) |
169 | 17, 168 | sylbid 239 |
. . . 4
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ โ)
โง (2 ยท ๐) =
๐) โ (((2โ๐) โ 1) = (๐โ๐) โ ๐ = 1)) |
170 | 169 | rexlimdva2 3151 |
. . 3
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (โ๐ โ
โ (2 ยท ๐) =
๐ โ (((2โ๐) โ 1) = (๐โ๐) โ ๐ = 1))) |
171 | 2, 170 | sylbid 239 |
. 2
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (2 โฅ ๐ โ
(((2โ๐) โ 1) =
(๐โ๐) โ ๐ = 1))) |
172 | 171 | 3imp 1111 |
1
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง 2 โฅ ๐ โง
((2โ๐) โ 1) =
(๐โ๐)) โ ๐ = 1) |