Step | Hyp | Ref
| Expression |
1 | | axcontlem7.1 |
. . . . . 6
โข ๐ท = {๐ โ (๐ผโ๐) โฃ (๐ Btwn โจ๐, ๐โฉ โจ ๐ Btwn โจ๐, ๐โฉ)} |
2 | 1 | ssrab3 4081 |
. . . . 5
โข ๐ท โ (๐ผโ๐) |
3 | 2 | sseli 3979 |
. . . 4
โข (๐ โ ๐ท โ ๐ โ (๐ผโ๐)) |
4 | 3 | ad2antrl 725 |
. . 3
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ ๐ โ (๐ผโ๐)) |
5 | | simpll2 1212 |
. . 3
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ ๐ โ (๐ผโ๐)) |
6 | 2 | sseli 3979 |
. . . 4
โข (๐ โ ๐ท โ ๐ โ (๐ผโ๐)) |
7 | 6 | ad2antll 726 |
. . 3
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ ๐ โ (๐ผโ๐)) |
8 | | brbtwn 28421 |
. . 3
โข ((๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โ (๐ Btwn โจ๐, ๐โฉ โ โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))))) |
9 | 4, 5, 7, 8 | syl3anc 1370 |
. 2
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ (๐ Btwn โจ๐, ๐โฉ โ โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))))) |
10 | | axcontlem7.2 |
. . . . 5
โข ๐น = {โจ๐ฅ, ๐กโฉ โฃ (๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))} |
11 | 1, 10 | axcontlem6 28491 |
. . . 4
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ๐ โ ๐ท) โ ((๐นโ๐) โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) |
12 | 1, 10 | axcontlem6 28491 |
. . . 4
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ๐ โ ๐ท) โ ((๐นโ๐) โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) |
13 | 11, 12 | anim12dan 618 |
. . 3
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ (((๐นโ๐) โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))) โง ((๐นโ๐) โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))))) |
14 | | an4 653 |
. . . . 5
โข ((((๐นโ๐) โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))) โง ((๐นโ๐) โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) โ (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง
(โ๐ โ
(1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))))) |
15 | | r19.26 3110 |
. . . . . 6
โข
(โ๐ โ
(1...๐)((๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โง (๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))) โ (โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) |
16 | 15 | anbi2i 622 |
. . . . 5
โข ((((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง โ๐ โ (1...๐)((๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โง (๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) โ (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง
(โ๐ โ
(1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))))) |
17 | 14, 16 | bitr4i 277 |
. . . 4
โข ((((๐นโ๐) โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))) โง ((๐นโ๐) โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) โ (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง โ๐ โ (1...๐)((๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โง (๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))))) |
18 | | id 22 |
. . . . . . . . . 10
โข ((๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โ (๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))) |
19 | | oveq2 7420 |
. . . . . . . . . . 11
โข ((๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โ (๐ก ยท (๐โ๐)) = (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) |
20 | 19 | oveq2d 7428 |
. . . . . . . . . 10
โข ((๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โ (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))))) |
21 | 18, 20 | eqeqan12d 2745 |
. . . . . . . . 9
โข (((๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โง (๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))) โ ((๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))))) |
22 | 21 | ralimi 3082 |
. . . . . . . 8
โข
(โ๐ โ
(1...๐)((๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โง (๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))) โ โ๐ โ (1...๐)((๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))))) |
23 | | ralbi 3102 |
. . . . . . . 8
โข
(โ๐ โ
(1...๐)((๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))))) โ (โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ โ๐ โ (1...๐)(((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))))) |
24 | 22, 23 | syl 17 |
. . . . . . 7
โข
(โ๐ โ
(1...๐)((๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โง (๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))) โ (โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ โ๐ โ (1...๐)(((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))))) |
25 | 24 | rexbidv 3177 |
. . . . . 6
โข
(โ๐ โ
(1...๐)((๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โง (๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))) โ (โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ โ๐ก โ (0[,]1)โ๐ โ (1...๐)(((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))))) |
26 | | simpll2 1212 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ ๐ โ (๐ผโ๐)) |
27 | | fveecn 28424 |
. . . . . . . . . . . . 13
โข ((๐ โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐โ๐) โ โ) |
28 | 26, 27 | sylan 579 |
. . . . . . . . . . . 12
โข
(((((๐ โ
โ โง ๐ โ
(๐ผโ๐) โง
๐ โ
(๐ผโ๐)) โง
๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โง ๐ โ (1...๐)) โ (๐โ๐) โ โ) |
29 | | simpll3 1213 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ ๐ โ (๐ผโ๐)) |
30 | | fveecn 28424 |
. . . . . . . . . . . . 13
โข ((๐ โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐โ๐) โ โ) |
31 | 29, 30 | sylan 579 |
. . . . . . . . . . . 12
โข
(((((๐ โ
โ โง ๐ โ
(๐ผโ๐) โง
๐ โ
(๐ผโ๐)) โง
๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โง ๐ โ (1...๐)) โ (๐โ๐) โ โ) |
32 | | elicc01 13448 |
. . . . . . . . . . . . . . . 16
โข (๐ก โ (0[,]1) โ (๐ก โ โ โง 0 โค
๐ก โง ๐ก โค 1)) |
33 | 32 | simp1bi 1144 |
. . . . . . . . . . . . . . 15
โข (๐ก โ (0[,]1) โ ๐ก โ
โ) |
34 | 33 | recnd 11247 |
. . . . . . . . . . . . . 14
โข (๐ก โ (0[,]1) โ ๐ก โ
โ) |
35 | 34 | ad2antll 726 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ ๐ก โ
โ) |
36 | 35 | adantr 480 |
. . . . . . . . . . . 12
โข
(((((๐ โ
โ โง ๐ โ
(๐ผโ๐) โง
๐ โ
(๐ผโ๐)) โง
๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โง ๐ โ (1...๐)) โ ๐ก โ โ) |
37 | | elrege0 13436 |
. . . . . . . . . . . . . . . . 17
โข ((๐นโ๐) โ (0[,)+โ) โ ((๐นโ๐) โ โ โง 0 โค (๐นโ๐))) |
38 | 37 | simplbi 497 |
. . . . . . . . . . . . . . . 16
โข ((๐นโ๐) โ (0[,)+โ) โ (๐นโ๐) โ โ) |
39 | 38 | recnd 11247 |
. . . . . . . . . . . . . . 15
โข ((๐นโ๐) โ (0[,)+โ) โ (๐นโ๐) โ โ) |
40 | 39 | adantr 480 |
. . . . . . . . . . . . . 14
โข (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โ (๐นโ๐) โ โ) |
41 | 40 | ad2antrl 725 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ (๐นโ๐) โ โ) |
42 | 41 | adantr 480 |
. . . . . . . . . . . 12
โข
(((((๐ โ
โ โง ๐ โ
(๐ผโ๐) โง
๐ โ
(๐ผโ๐)) โง
๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โง ๐ โ (1...๐)) โ (๐นโ๐) โ โ) |
43 | | elrege0 13436 |
. . . . . . . . . . . . . . . . 17
โข ((๐นโ๐) โ (0[,)+โ) โ ((๐นโ๐) โ โ โง 0 โค (๐นโ๐))) |
44 | 43 | simplbi 497 |
. . . . . . . . . . . . . . . 16
โข ((๐นโ๐) โ (0[,)+โ) โ (๐นโ๐) โ โ) |
45 | 44 | recnd 11247 |
. . . . . . . . . . . . . . 15
โข ((๐นโ๐) โ (0[,)+โ) โ (๐นโ๐) โ โ) |
46 | 45 | adantl 481 |
. . . . . . . . . . . . . 14
โข (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โ (๐นโ๐) โ โ) |
47 | 46 | ad2antrl 725 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ (๐นโ๐) โ โ) |
48 | 47 | adantr 480 |
. . . . . . . . . . . 12
โข
(((((๐ โ
โ โง ๐ โ
(๐ผโ๐) โง
๐ โ
(๐ผโ๐)) โง
๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โง ๐ โ (1...๐)) โ (๐นโ๐) โ โ) |
49 | | ax-1cn 11171 |
. . . . . . . . . . . . . . . . 17
โข 1 โ
โ |
50 | | simpr1 1193 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ๐ก โ โ) |
51 | | simpr3 1195 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (๐นโ๐) โ โ) |
52 | 50, 51 | mulcld 11239 |
. . . . . . . . . . . . . . . . 17
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (๐ก ยท (๐นโ๐)) โ โ) |
53 | | subcl 11464 |
. . . . . . . . . . . . . . . . 17
โข ((1
โ โ โง (๐ก
ยท (๐นโ๐)) โ โ) โ (1
โ (๐ก ยท (๐นโ๐))) โ โ) |
54 | 49, 52, 53 | sylancr 586 |
. . . . . . . . . . . . . . . 16
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (1 โ (๐ก ยท (๐นโ๐))) โ โ) |
55 | | subcl 11464 |
. . . . . . . . . . . . . . . . . . 19
โข ((1
โ โ โง (๐นโ๐) โ โ) โ (1 โ (๐นโ๐)) โ โ) |
56 | 49, 55 | mpan 687 |
. . . . . . . . . . . . . . . . . 18
โข ((๐นโ๐) โ โ โ (1 โ (๐นโ๐)) โ โ) |
57 | 56 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . 17
โข ((๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ) โ (1 โ (๐นโ๐)) โ โ) |
58 | 57 | adantl 481 |
. . . . . . . . . . . . . . . 16
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (1 โ (๐นโ๐)) โ โ) |
59 | | simpll 764 |
. . . . . . . . . . . . . . . 16
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (๐โ๐) โ โ) |
60 | 54, 58, 59 | subdird 11676 |
. . . . . . . . . . . . . . 15
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (((1 โ
(๐ก ยท (๐นโ๐))) โ (1 โ (๐นโ๐))) ยท (๐โ๐)) = (((1 โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) โ ((1 โ (๐นโ๐)) ยท (๐โ๐)))) |
61 | | simpr2 1194 |
. . . . . . . . . . . . . . . . 17
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (๐นโ๐) โ โ) |
62 | | nnncan1 11501 |
. . . . . . . . . . . . . . . . 17
โข ((1
โ โ โง (๐ก
ยท (๐นโ๐)) โ โ โง (๐นโ๐) โ โ) โ ((1 โ (๐ก ยท (๐นโ๐))) โ (1 โ (๐นโ๐))) = ((๐นโ๐) โ (๐ก ยท (๐นโ๐)))) |
63 | 49, 52, 61, 62 | mp3an2i 1465 |
. . . . . . . . . . . . . . . 16
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((1 โ (๐ก ยท (๐นโ๐))) โ (1 โ (๐นโ๐))) = ((๐นโ๐) โ (๐ก ยท (๐นโ๐)))) |
64 | 63 | oveq1d 7427 |
. . . . . . . . . . . . . . 15
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (((1 โ
(๐ก ยท (๐นโ๐))) โ (1 โ (๐นโ๐))) ยท (๐โ๐)) = (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐))) |
65 | | subdi 11652 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ก โ โ โง 1 โ
โ โง (๐นโ๐) โ โ) โ (๐ก ยท (1 โ (๐นโ๐))) = ((๐ก ยท 1) โ (๐ก ยท (๐นโ๐)))) |
66 | 49, 65 | mp3an2 1448 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ก โ โ โง (๐นโ๐) โ โ) โ (๐ก ยท (1 โ (๐นโ๐))) = ((๐ก ยท 1) โ (๐ก ยท (๐นโ๐)))) |
67 | | mulrid 11217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ก โ โ โ (๐ก ยท 1) = ๐ก) |
68 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ก โ โ โง (๐นโ๐) โ โ) โ (๐ก ยท 1) = ๐ก) |
69 | 68 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ก โ โ โง (๐นโ๐) โ โ) โ ((๐ก ยท 1) โ (๐ก ยท (๐นโ๐))) = (๐ก โ (๐ก ยท (๐นโ๐)))) |
70 | 66, 69 | eqtrd 2771 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ก โ โ โง (๐นโ๐) โ โ) โ (๐ก ยท (1 โ (๐นโ๐))) = (๐ก โ (๐ก ยท (๐นโ๐)))) |
71 | 50, 51, 70 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (๐ก ยท (1 โ (๐นโ๐))) = (๐ก โ (๐ก ยท (๐นโ๐)))) |
72 | 71 | oveq2d 7428 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((1 โ ๐ก) + (๐ก ยท (1 โ (๐นโ๐)))) = ((1 โ ๐ก) + (๐ก โ (๐ก ยท (๐นโ๐))))) |
73 | | npncan 11486 |
. . . . . . . . . . . . . . . . . . . 20
โข ((1
โ โ โง ๐ก
โ โ โง (๐ก
ยท (๐นโ๐)) โ โ) โ ((1
โ ๐ก) + (๐ก โ (๐ก ยท (๐นโ๐)))) = (1 โ (๐ก ยท (๐นโ๐)))) |
74 | 49, 50, 52, 73 | mp3an2i 1465 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((1 โ ๐ก) + (๐ก โ (๐ก ยท (๐นโ๐)))) = (1 โ (๐ก ยท (๐นโ๐)))) |
75 | 72, 74 | eqtr2d 2772 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (1 โ (๐ก ยท (๐นโ๐))) = ((1 โ ๐ก) + (๐ก ยท (1 โ (๐นโ๐))))) |
76 | 75 | oveq1d 7427 |
. . . . . . . . . . . . . . . . 17
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((1 โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) = (((1 โ ๐ก) + (๐ก ยท (1 โ (๐นโ๐)))) ยท (๐โ๐))) |
77 | | subcl 11464 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((1
โ โ โง ๐ก
โ โ) โ (1 โ ๐ก) โ โ) |
78 | 49, 77 | mpan 687 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ก โ โ โ (1
โ ๐ก) โ
โ) |
79 | 78 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ) โ (1 โ ๐ก) โ
โ) |
80 | 79 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (1 โ ๐ก) โ
โ) |
81 | | subcl 11464 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((1
โ โ โง (๐นโ๐) โ โ) โ (1 โ (๐นโ๐)) โ โ) |
82 | 49, 81 | mpan 687 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐นโ๐) โ โ โ (1 โ (๐นโ๐)) โ โ) |
83 | 82 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ) โ (1 โ (๐นโ๐)) โ โ) |
84 | 83 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (1 โ (๐นโ๐)) โ โ) |
85 | 50, 84 | mulcld 11239 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (๐ก ยท (1 โ (๐นโ๐))) โ โ) |
86 | 80, 85, 59 | adddird 11244 |
. . . . . . . . . . . . . . . . 17
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (((1 โ ๐ก) + (๐ก ยท (1 โ (๐นโ๐)))) ยท (๐โ๐)) = (((1 โ ๐ก) ยท (๐โ๐)) + ((๐ก ยท (1 โ (๐นโ๐))) ยท (๐โ๐)))) |
87 | 50, 84, 59 | mulassd 11242 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((๐ก ยท (1 โ (๐นโ๐))) ยท (๐โ๐)) = (๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐)))) |
88 | 87 | oveq2d 7428 |
. . . . . . . . . . . . . . . . 17
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (((1 โ ๐ก) ยท (๐โ๐)) + ((๐ก ยท (1 โ (๐นโ๐))) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐))))) |
89 | 76, 86, 88 | 3eqtrd 2775 |
. . . . . . . . . . . . . . . 16
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((1 โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐))))) |
90 | 89 | oveq1d 7427 |
. . . . . . . . . . . . . . 15
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (((1 โ
(๐ก ยท (๐นโ๐))) ยท (๐โ๐)) โ ((1 โ (๐นโ๐)) ยท (๐โ๐))) = ((((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐)))) โ ((1 โ (๐นโ๐)) ยท (๐โ๐)))) |
91 | 60, 64, 90 | 3eqtr3d 2779 |
. . . . . . . . . . . . . 14
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) = ((((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐)))) โ ((1 โ (๐นโ๐)) ยท (๐โ๐)))) |
92 | | simplr 766 |
. . . . . . . . . . . . . . . 16
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (๐โ๐) โ โ) |
93 | 61, 52, 92 | subdird 11676 |
. . . . . . . . . . . . . . 15
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) = (((๐นโ๐) ยท (๐โ๐)) โ ((๐ก ยท (๐นโ๐)) ยท (๐โ๐)))) |
94 | 50, 51, 92 | mulassd 11242 |
. . . . . . . . . . . . . . . 16
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((๐ก ยท (๐นโ๐)) ยท (๐โ๐)) = (๐ก ยท ((๐นโ๐) ยท (๐โ๐)))) |
95 | 94 | oveq2d 7428 |
. . . . . . . . . . . . . . 15
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (((๐นโ๐) ยท (๐โ๐)) โ ((๐ก ยท (๐นโ๐)) ยท (๐โ๐))) = (((๐นโ๐) ยท (๐โ๐)) โ (๐ก ยท ((๐นโ๐) ยท (๐โ๐))))) |
96 | 93, 95 | eqtrd 2771 |
. . . . . . . . . . . . . 14
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) = (((๐นโ๐) ยท (๐โ๐)) โ (๐ก ยท ((๐นโ๐) ยท (๐โ๐))))) |
97 | 91, 96 | eqeq12d 2747 |
. . . . . . . . . . . . 13
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) = (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) โ ((((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐)))) โ ((1 โ (๐นโ๐)) ยท (๐โ๐))) = (((๐นโ๐) ยท (๐โ๐)) โ (๐ก ยท ((๐นโ๐) ยท (๐โ๐)))))) |
98 | 58, 59 | mulcld 11239 |
. . . . . . . . . . . . . 14
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((1 โ (๐นโ๐)) ยท (๐โ๐)) โ โ) |
99 | 61, 92 | mulcld 11239 |
. . . . . . . . . . . . . 14
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((๐นโ๐) ยท (๐โ๐)) โ โ) |
100 | 80, 59 | mulcld 11239 |
. . . . . . . . . . . . . . 15
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((1 โ ๐ก) ยท (๐โ๐)) โ โ) |
101 | 84, 59 | mulcld 11239 |
. . . . . . . . . . . . . . . 16
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((1 โ (๐นโ๐)) ยท (๐โ๐)) โ โ) |
102 | 50, 101 | mulcld 11239 |
. . . . . . . . . . . . . . 15
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐))) โ โ) |
103 | 100, 102 | addcld 11238 |
. . . . . . . . . . . . . 14
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐)))) โ โ) |
104 | 51, 92 | mulcld 11239 |
. . . . . . . . . . . . . . 15
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((๐นโ๐) ยท (๐โ๐)) โ โ) |
105 | 50, 104 | mulcld 11239 |
. . . . . . . . . . . . . 14
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (๐ก ยท ((๐นโ๐) ยท (๐โ๐))) โ โ) |
106 | 98, 99, 103, 105 | addsubeq4d 11627 |
. . . . . . . . . . . . 13
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((((1 โ
(๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = ((((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐)))) + (๐ก ยท ((๐นโ๐) ยท (๐โ๐)))) โ ((((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐)))) โ ((1 โ (๐นโ๐)) ยท (๐โ๐))) = (((๐นโ๐) ยท (๐โ๐)) โ (๐ก ยท ((๐นโ๐) ยท (๐โ๐)))))) |
107 | 100, 102,
105 | addassd 11241 |
. . . . . . . . . . . . . . 15
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((((1 โ
๐ก) ยท (๐โ๐)) + (๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐)))) + (๐ก ยท ((๐นโ๐) ยท (๐โ๐)))) = (((1 โ ๐ก) ยท (๐โ๐)) + ((๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐))) + (๐ก ยท ((๐นโ๐) ยท (๐โ๐)))))) |
108 | 50, 101, 104 | adddid 11243 |
. . . . . . . . . . . . . . . 16
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))) = ((๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐))) + (๐ก ยท ((๐นโ๐) ยท (๐โ๐))))) |
109 | 108 | oveq2d 7428 |
. . . . . . . . . . . . . . 15
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) = (((1 โ ๐ก) ยท (๐โ๐)) + ((๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐))) + (๐ก ยท ((๐นโ๐) ยท (๐โ๐)))))) |
110 | 107, 109 | eqtr4d 2774 |
. . . . . . . . . . . . . 14
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((((1 โ
๐ก) ยท (๐โ๐)) + (๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐)))) + (๐ก ยท ((๐นโ๐) ยท (๐โ๐)))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))))) |
111 | 110 | eqeq2d 2742 |
. . . . . . . . . . . . 13
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((((1 โ
(๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = ((((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท ((1 โ (๐นโ๐)) ยท (๐โ๐)))) + (๐ก ยท ((๐นโ๐) ยท (๐โ๐)))) โ (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))))) |
112 | 97, 106, 111 | 3bitr2rd 307 |
. . . . . . . . . . . 12
โข ((((๐โ๐) โ โ โง (๐โ๐) โ โ) โง (๐ก โ โ โง (๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ ((((1 โ
(๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) โ (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) = (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)))) |
113 | 28, 31, 36, 42, 48, 112 | syl23anc 1376 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ โง ๐ โ
(๐ผโ๐) โง
๐ โ
(๐ผโ๐)) โง
๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โง ๐ โ (1...๐)) โ ((((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) โ (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) = (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)))) |
114 | 113 | ralbidva 3174 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ
(โ๐ โ
(1...๐)(((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) โ โ๐ โ (1...๐)(((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) = (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)))) |
115 | 36, 48 | mulcld 11239 |
. . . . . . . . . . . . 13
โข
(((((๐ โ
โ โง ๐ โ
(๐ผโ๐) โง
๐ โ
(๐ผโ๐)) โง
๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โง ๐ โ (1...๐)) โ (๐ก ยท (๐นโ๐)) โ โ) |
116 | 42, 115 | subcld 11576 |
. . . . . . . . . . . 12
โข
(((((๐ โ
โ โง ๐ โ
(๐ผโ๐) โง
๐ โ
(๐ผโ๐)) โง
๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โง ๐ โ (1...๐)) โ ((๐นโ๐) โ (๐ก ยท (๐นโ๐))) โ โ) |
117 | | mulcan1g 11872 |
. . . . . . . . . . . 12
โข ((((๐นโ๐) โ (๐ก ยท (๐นโ๐))) โ โ โง (๐โ๐) โ โ โง (๐โ๐) โ โ) โ ((((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) = (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) โ (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โจ (๐โ๐) = (๐โ๐)))) |
118 | 116, 28, 31, 117 | syl3anc 1370 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ โง ๐ โ
(๐ผโ๐) โง
๐ โ
(๐ผโ๐)) โง
๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โง ๐ โ (1...๐)) โ ((((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) = (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) โ (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โจ (๐โ๐) = (๐โ๐)))) |
119 | 118 | ralbidva 3174 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ
(โ๐ โ
(1...๐)(((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) = (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) ยท (๐โ๐)) โ โ๐ โ (1...๐)(((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โจ (๐โ๐) = (๐โ๐)))) |
120 | | r19.32v 3190 |
. . . . . . . . . . 11
โข
(โ๐ โ
(1...๐)(((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โจ (๐โ๐) = (๐โ๐)) โ (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โจ โ๐ โ (1...๐)(๐โ๐) = (๐โ๐))) |
121 | | simplr 766 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ ๐ โ ๐) |
122 | 121 | neneqd 2944 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ ยฌ
๐ = ๐) |
123 | | biorf 934 |
. . . . . . . . . . . . . 14
โข (ยฌ
๐ = ๐ โ (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โ (๐ = ๐ โจ ((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0))) |
124 | | orcom 867 |
. . . . . . . . . . . . . 14
โข ((๐ = ๐ โจ ((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0) โ (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โจ ๐ = ๐)) |
125 | 123, 124 | bitrdi 286 |
. . . . . . . . . . . . 13
โข (ยฌ
๐ = ๐ โ (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โ (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โจ ๐ = ๐))) |
126 | 122, 125 | syl 17 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ
(((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โ (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โจ ๐ = ๐))) |
127 | 35, 47 | mulcld 11239 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ (๐ก ยท (๐นโ๐)) โ โ) |
128 | 41, 127 | subeq0ad 11586 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ
(((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โ (๐นโ๐) = (๐ก ยท (๐นโ๐)))) |
129 | | eqeefv 28425 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โ (๐ = ๐ โ โ๐ โ (1...๐)(๐โ๐) = (๐โ๐))) |
130 | 129 | 3adant1 1129 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โ (๐ = ๐ โ โ๐ โ (1...๐)(๐โ๐) = (๐โ๐))) |
131 | 130 | adantr 480 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โ (๐ = ๐ โ โ๐ โ (1...๐)(๐โ๐) = (๐โ๐))) |
132 | 131 | adantr 480 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ (๐ = ๐ โ โ๐ โ (1...๐)(๐โ๐) = (๐โ๐))) |
133 | 132 | orbi2d 913 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ
((((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โจ ๐ = ๐) โ (((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โจ โ๐ โ (1...๐)(๐โ๐) = (๐โ๐)))) |
134 | 126, 128,
133 | 3bitr3rd 309 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ
((((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โจ โ๐ โ (1...๐)(๐โ๐) = (๐โ๐)) โ (๐นโ๐) = (๐ก ยท (๐นโ๐)))) |
135 | 120, 134 | bitrid 282 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ
(โ๐ โ
(1...๐)(((๐นโ๐) โ (๐ก ยท (๐นโ๐))) = 0 โจ (๐โ๐) = (๐โ๐)) โ (๐นโ๐) = (๐ก ยท (๐นโ๐)))) |
136 | 114, 119,
135 | 3bitrd 304 |
. . . . . . . . 9
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1))) โ
(โ๐ โ
(1...๐)(((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) โ (๐นโ๐) = (๐ก ยท (๐นโ๐)))) |
137 | 136 | anassrs 467 |
. . . . . . . 8
โข
(((((๐ โ
โ โง ๐ โ
(๐ผโ๐) โง
๐ โ
(๐ผโ๐)) โง
๐ โ ๐) โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ))) โง ๐ก โ (0[,]1)) โ
(โ๐ โ
(1...๐)(((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) โ (๐นโ๐) = (๐ก ยท (๐นโ๐)))) |
138 | 137 | rexbidva 3175 |
. . . . . . 7
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ))) โ
(โ๐ก โ
(0[,]1)โ๐ โ
(1...๐)(((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) โ โ๐ก โ (0[,]1)(๐นโ๐) = (๐ก ยท (๐นโ๐)))) |
139 | 33 | adantl 481 |
. . . . . . . . . . . . 13
โข ((((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1)) โ ๐ก โ
โ) |
140 | | 1red 11220 |
. . . . . . . . . . . . 13
โข ((((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1)) โ 1 โ
โ) |
141 | 43 | biimpi 215 |
. . . . . . . . . . . . . 14
โข ((๐นโ๐) โ (0[,)+โ) โ ((๐นโ๐) โ โ โง 0 โค (๐นโ๐))) |
142 | 141 | ad2antlr 724 |
. . . . . . . . . . . . 13
โข ((((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1)) โ ((๐นโ๐) โ โ โง 0 โค (๐นโ๐))) |
143 | 32 | simp3bi 1146 |
. . . . . . . . . . . . . 14
โข (๐ก โ (0[,]1) โ ๐ก โค 1) |
144 | 143 | adantl 481 |
. . . . . . . . . . . . 13
โข ((((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1)) โ ๐ก โค 1) |
145 | | lemul1a 12073 |
. . . . . . . . . . . . 13
โข (((๐ก โ โ โง 1 โ
โ โง ((๐นโ๐) โ โ โง 0 โค (๐นโ๐))) โง ๐ก โค 1) โ (๐ก ยท (๐นโ๐)) โค (1 ยท (๐นโ๐))) |
146 | 139, 140,
142, 144, 145 | syl31anc 1372 |
. . . . . . . . . . . 12
โข ((((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1)) โ (๐ก ยท (๐นโ๐)) โค (1 ยท (๐นโ๐))) |
147 | 45 | ad2antlr 724 |
. . . . . . . . . . . . 13
โข ((((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1)) โ (๐นโ๐) โ โ) |
148 | 147 | mullidd 11237 |
. . . . . . . . . . . 12
โข ((((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1)) โ (1
ยท (๐นโ๐)) = (๐นโ๐)) |
149 | 146, 148 | breqtrd 5175 |
. . . . . . . . . . 11
โข ((((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1)) โ (๐ก ยท (๐นโ๐)) โค (๐นโ๐)) |
150 | | breq1 5152 |
. . . . . . . . . . 11
โข ((๐นโ๐) = (๐ก ยท (๐นโ๐)) โ ((๐นโ๐) โค (๐นโ๐) โ (๐ก ยท (๐นโ๐)) โค (๐นโ๐))) |
151 | 149, 150 | syl5ibrcom 246 |
. . . . . . . . . 10
โข ((((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง ๐ก โ (0[,]1)) โ ((๐นโ๐) = (๐ก ยท (๐นโ๐)) โ (๐นโ๐) โค (๐นโ๐))) |
152 | 151 | rexlimdva 3154 |
. . . . . . . . 9
โข (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โ
(โ๐ก โ
(0[,]1)(๐นโ๐) = (๐ก ยท (๐นโ๐)) โ (๐นโ๐) โค (๐นโ๐))) |
153 | | 0elunit 13451 |
. . . . . . . . . . . . . 14
โข 0 โ
(0[,]1) |
154 | | simpl 482 |
. . . . . . . . . . . . . . 15
โข (((๐นโ๐) = 0 โง (๐นโ๐) โ (0[,)+โ)) โ (๐นโ๐) = 0) |
155 | 45 | mul02d 11417 |
. . . . . . . . . . . . . . . 16
โข ((๐นโ๐) โ (0[,)+โ) โ (0 ยท
(๐นโ๐)) = 0) |
156 | 155 | adantl 481 |
. . . . . . . . . . . . . . 15
โข (((๐นโ๐) = 0 โง (๐นโ๐) โ (0[,)+โ)) โ (0 ยท
(๐นโ๐)) = 0) |
157 | 154, 156 | eqtr4d 2774 |
. . . . . . . . . . . . . 14
โข (((๐นโ๐) = 0 โง (๐นโ๐) โ (0[,)+โ)) โ (๐นโ๐) = (0 ยท (๐นโ๐))) |
158 | | oveq1 7419 |
. . . . . . . . . . . . . . 15
โข (๐ก = 0 โ (๐ก ยท (๐นโ๐)) = (0 ยท (๐นโ๐))) |
159 | 158 | rspceeqv 3634 |
. . . . . . . . . . . . . 14
โข ((0
โ (0[,]1) โง (๐นโ๐) = (0 ยท (๐นโ๐))) โ โ๐ก โ (0[,]1)(๐นโ๐) = (๐ก ยท (๐นโ๐))) |
160 | 153, 157,
159 | sylancr 586 |
. . . . . . . . . . . . 13
โข (((๐นโ๐) = 0 โง (๐นโ๐) โ (0[,)+โ)) โ โ๐ก โ (0[,]1)(๐นโ๐) = (๐ก ยท (๐นโ๐))) |
161 | 160 | adantrl 713 |
. . . . . . . . . . . 12
โข (((๐นโ๐) = 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ))) โ
โ๐ก โ
(0[,]1)(๐นโ๐) = (๐ก ยท (๐นโ๐))) |
162 | 161 | a1d 25 |
. . . . . . . . . . 11
โข (((๐นโ๐) = 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ))) โ ((๐นโ๐) โค (๐นโ๐) โ โ๐ก โ (0[,]1)(๐นโ๐) = (๐ก ยท (๐นโ๐)))) |
163 | 162 | ex 412 |
. . . . . . . . . 10
โข ((๐นโ๐) = 0 โ (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โ ((๐นโ๐) โค (๐นโ๐) โ โ๐ก โ (0[,]1)(๐นโ๐) = (๐ก ยท (๐นโ๐))))) |
164 | | simp3 1137 |
. . . . . . . . . . . . 13
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ (๐นโ๐) โค (๐นโ๐)) |
165 | 38 | adantr 480 |
. . . . . . . . . . . . . . 15
โข (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โ (๐นโ๐) โ โ) |
166 | 165 | 3ad2ant2 1133 |
. . . . . . . . . . . . . 14
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ (๐นโ๐) โ โ) |
167 | 37 | simprbi 496 |
. . . . . . . . . . . . . . . 16
โข ((๐นโ๐) โ (0[,)+โ) โ 0 โค (๐นโ๐)) |
168 | 167 | adantr 480 |
. . . . . . . . . . . . . . 15
โข (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โ 0 โค
(๐นโ๐)) |
169 | 168 | 3ad2ant2 1133 |
. . . . . . . . . . . . . 14
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ 0 โค (๐นโ๐)) |
170 | 44 | adantl 481 |
. . . . . . . . . . . . . . 15
โข (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โ (๐นโ๐) โ โ) |
171 | 170 | 3ad2ant2 1133 |
. . . . . . . . . . . . . 14
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ (๐นโ๐) โ โ) |
172 | | 0red 11222 |
. . . . . . . . . . . . . . 15
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ 0 โ โ) |
173 | | simp1 1135 |
. . . . . . . . . . . . . . . 16
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ (๐นโ๐) โ 0) |
174 | 166, 169,
173 | ne0gt0d 11356 |
. . . . . . . . . . . . . . 15
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ 0 < (๐นโ๐)) |
175 | 172, 166,
171, 174, 164 | ltletrd 11379 |
. . . . . . . . . . . . . 14
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ 0 < (๐นโ๐)) |
176 | | divelunit 13476 |
. . . . . . . . . . . . . 14
โข ((((๐นโ๐) โ โ โง 0 โค (๐นโ๐)) โง ((๐นโ๐) โ โ โง 0 < (๐นโ๐))) โ (((๐นโ๐) / (๐นโ๐)) โ (0[,]1) โ (๐นโ๐) โค (๐นโ๐))) |
177 | 166, 169,
171, 175, 176 | syl22anc 836 |
. . . . . . . . . . . . 13
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ (((๐นโ๐) / (๐นโ๐)) โ (0[,]1) โ (๐นโ๐) โค (๐นโ๐))) |
178 | 164, 177 | mpbird 256 |
. . . . . . . . . . . 12
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ ((๐นโ๐) / (๐นโ๐)) โ (0[,]1)) |
179 | 40 | 3ad2ant2 1133 |
. . . . . . . . . . . . . 14
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ (๐นโ๐) โ โ) |
180 | 46 | 3ad2ant2 1133 |
. . . . . . . . . . . . . 14
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ (๐นโ๐) โ โ) |
181 | 175 | gt0ne0d 11783 |
. . . . . . . . . . . . . 14
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ (๐นโ๐) โ 0) |
182 | 179, 180,
181 | divcan1d 11996 |
. . . . . . . . . . . . 13
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ (((๐นโ๐) / (๐นโ๐)) ยท (๐นโ๐)) = (๐นโ๐)) |
183 | 182 | eqcomd 2737 |
. . . . . . . . . . . 12
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ (๐นโ๐) = (((๐นโ๐) / (๐นโ๐)) ยท (๐นโ๐))) |
184 | | oveq1 7419 |
. . . . . . . . . . . . 13
โข (๐ก = ((๐นโ๐) / (๐นโ๐)) โ (๐ก ยท (๐นโ๐)) = (((๐นโ๐) / (๐นโ๐)) ยท (๐นโ๐))) |
185 | 184 | rspceeqv 3634 |
. . . . . . . . . . . 12
โข ((((๐นโ๐) / (๐นโ๐)) โ (0[,]1) โง (๐นโ๐) = (((๐นโ๐) / (๐นโ๐)) ยท (๐นโ๐))) โ โ๐ก โ (0[,]1)(๐นโ๐) = (๐ก ยท (๐นโ๐))) |
186 | 178, 183,
185 | syl2anc 583 |
. . . . . . . . . . 11
โข (((๐นโ๐) โ 0 โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง (๐นโ๐) โค (๐นโ๐)) โ โ๐ก โ (0[,]1)(๐นโ๐) = (๐ก ยท (๐นโ๐))) |
187 | 186 | 3exp 1118 |
. . . . . . . . . 10
โข ((๐นโ๐) โ 0 โ (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โ ((๐นโ๐) โค (๐นโ๐) โ โ๐ก โ (0[,]1)(๐นโ๐) = (๐ก ยท (๐นโ๐))))) |
188 | 163, 187 | pm2.61ine 3024 |
. . . . . . . . 9
โข (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โ ((๐นโ๐) โค (๐นโ๐) โ โ๐ก โ (0[,]1)(๐นโ๐) = (๐ก ยท (๐นโ๐)))) |
189 | 152, 188 | impbid 211 |
. . . . . . . 8
โข (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โ
(โ๐ก โ
(0[,]1)(๐นโ๐) = (๐ก ยท (๐นโ๐)) โ (๐นโ๐) โค (๐นโ๐))) |
190 | 189 | adantl 481 |
. . . . . . 7
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ))) โ
(โ๐ก โ
(0[,]1)(๐นโ๐) = (๐ก ยท (๐นโ๐)) โ (๐นโ๐) โค (๐นโ๐))) |
191 | 138, 190 | bitrd 278 |
. . . . . 6
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ))) โ
(โ๐ก โ
(0[,]1)โ๐ โ
(1...๐)(((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) โ (๐นโ๐) โค (๐นโ๐))) |
192 | 25, 191 | sylan9bbr 510 |
. . . . 5
โข
(((((๐ โ
โ โง ๐ โ
(๐ผโ๐) โง
๐ โ
(๐ผโ๐)) โง
๐ โ ๐) โง ((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ))) โง
โ๐ โ (1...๐)((๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โง (๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) โ (โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ (๐นโ๐) โค (๐นโ๐))) |
193 | 192 | anasss 466 |
. . . 4
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง (๐นโ๐) โ (0[,)+โ)) โง โ๐ โ (1...๐)((๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))) โง (๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))))) โ (โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ (๐นโ๐) โค (๐นโ๐))) |
194 | 17, 193 | sylan2b 593 |
. . 3
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (((๐นโ๐) โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))) โง ((๐นโ๐) โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐)))))) โ (โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ (๐นโ๐) โค (๐นโ๐))) |
195 | 13, 194 | syldan 590 |
. 2
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ (โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ (๐นโ๐) โค (๐นโ๐))) |
196 | 9, 195 | bitrd 278 |
1
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ (๐ Btwn โจ๐, ๐โฉ โ (๐นโ๐) โค (๐นโ๐))) |