Step | Hyp | Ref
| Expression |
1 | | axcontlem5.1 |
. . . . . 6
โข ๐ท = {๐ โ (๐ผโ๐) โฃ (๐ Btwn โจ๐, ๐โฉ โจ ๐ Btwn โจ๐, ๐โฉ)} |
2 | | axcontlem5.2 |
. . . . . 6
โข ๐น = {โจ๐ฅ, ๐กโฉ โฃ (๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))} |
3 | 1, 2 | axcontlem2 28011 |
. . . . 5
โข (((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โ ๐น:๐ทโ1-1-ontoโ(0[,)+โ)) |
4 | | f1of 6804 |
. . . . 5
โข (๐น:๐ทโ1-1-ontoโ(0[,)+โ) โ ๐น:๐ทโถ(0[,)+โ)) |
5 | 3, 4 | syl 17 |
. . . 4
โข (((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โ ๐น:๐ทโถ(0[,)+โ)) |
6 | 5 | ffvelcdmda 7055 |
. . 3
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ๐ โ ๐ท) โ (๐นโ๐) โ (0[,)+โ)) |
7 | | eleq1 2820 |
. . 3
โข ((๐นโ๐) = ๐ โ ((๐นโ๐) โ (0[,)+โ) โ ๐ โ
(0[,)+โ))) |
8 | 6, 7 | syl5ibcom 244 |
. 2
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ๐ โ ๐ท) โ ((๐นโ๐) = ๐ โ ๐ โ (0[,)+โ))) |
9 | | simpl 483 |
. . 3
โข ((๐ โ (0[,)+โ) โง
โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))) โ ๐ โ (0[,)+โ)) |
10 | 9 | a1i 11 |
. 2
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ๐ โ ๐ท) โ ((๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))) โ ๐ โ (0[,)+โ))) |
11 | | f1ofn 6805 |
. . . . . . 7
โข (๐น:๐ทโ1-1-ontoโ(0[,)+โ) โ ๐น Fn ๐ท) |
12 | 3, 11 | syl 17 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โ ๐น Fn ๐ท) |
13 | | fnbrfvb 6915 |
. . . . . 6
โข ((๐น Fn ๐ท โง ๐ โ ๐ท) โ ((๐นโ๐) = ๐ โ ๐๐น๐)) |
14 | 12, 13 | sylan 580 |
. . . . 5
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ๐ โ ๐ท) โ ((๐นโ๐) = ๐ โ ๐๐น๐)) |
15 | 14 | 3adant3 1132 |
. . . 4
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ๐ โ ๐ท โง ๐ โ (0[,)+โ)) โ ((๐นโ๐) = ๐ โ ๐๐น๐)) |
16 | | eleq1 2820 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ฅ โ ๐ท โ ๐ โ ๐ท)) |
17 | | fveq1 6861 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ (๐ฅโ๐) = (๐โ๐)) |
18 | 17 | eqeq1d 2733 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ ((๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ (๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))))) |
19 | 18 | ralbidv 3176 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))))) |
20 | 19 | anbi2d 629 |
. . . . . . . 8
โข (๐ฅ = ๐ โ ((๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))) โ (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))) |
21 | 16, 20 | anbi12d 631 |
. . . . . . 7
โข (๐ฅ = ๐ โ ((๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))))) โ (๐ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))))))) |
22 | | eleq1 2820 |
. . . . . . . . . 10
โข (๐ก = ๐ โ (๐ก โ (0[,)+โ) โ ๐ โ
(0[,)+โ))) |
23 | | oveq2 7385 |
. . . . . . . . . . . . . 14
โข (๐ก = ๐ โ (1 โ ๐ก) = (1 โ ๐)) |
24 | 23 | oveq1d 7392 |
. . . . . . . . . . . . 13
โข (๐ก = ๐ โ ((1 โ ๐ก) ยท (๐โ๐)) = ((1 โ ๐) ยท (๐โ๐))) |
25 | | oveq1 7384 |
. . . . . . . . . . . . 13
โข (๐ก = ๐ โ (๐ก ยท (๐โ๐)) = (๐ ยท (๐โ๐))) |
26 | 24, 25 | oveq12d 7395 |
. . . . . . . . . . . 12
โข (๐ก = ๐ โ (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))) |
27 | 26 | eqeq2d 2742 |
. . . . . . . . . . 11
โข (๐ก = ๐ โ ((๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ (๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐))))) |
28 | 27 | ralbidv 3176 |
. . . . . . . . . 10
โข (๐ก = ๐ โ (โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐))))) |
29 | 22, 28 | anbi12d 631 |
. . . . . . . . 9
โข (๐ก = ๐ โ ((๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))) โ (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))))) |
30 | 29 | anbi2d 629 |
. . . . . . . 8
โข (๐ก = ๐ โ ((๐ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))))) โ (๐ โ ๐ท โง (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐))))))) |
31 | | anass 469 |
. . . . . . . . . . 11
โข (((๐ โ ๐ท โง ๐ โ (0[,)+โ)) โง ๐ โ (0[,)+โ)) โ
(๐ โ ๐ท โง (๐ โ (0[,)+โ) โง ๐ โ
(0[,)+โ)))) |
32 | | anidm 565 |
. . . . . . . . . . . 12
โข ((๐ โ (0[,)+โ) โง
๐ โ (0[,)+โ))
โ ๐ โ
(0[,)+โ)) |
33 | 32 | anbi2i 623 |
. . . . . . . . . . 11
โข ((๐ โ ๐ท โง (๐ โ (0[,)+โ) โง ๐ โ (0[,)+โ))) โ
(๐ โ ๐ท โง ๐ โ (0[,)+โ))) |
34 | 31, 33 | bitr2i 275 |
. . . . . . . . . 10
โข ((๐ โ ๐ท โง ๐ โ (0[,)+โ)) โ ((๐ โ ๐ท โง ๐ โ (0[,)+โ)) โง ๐ โ
(0[,)+โ))) |
35 | 34 | anbi1i 624 |
. . . . . . . . 9
โข (((๐ โ ๐ท โง ๐ โ (0[,)+โ)) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))) โ (((๐ โ ๐ท โง ๐ โ (0[,)+โ)) โง ๐ โ (0[,)+โ)) โง
โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐))))) |
36 | | anass 469 |
. . . . . . . . 9
โข (((๐ โ ๐ท โง ๐ โ (0[,)+โ)) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))) โ (๐ โ ๐ท โง (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))))) |
37 | | anass 469 |
. . . . . . . . 9
โข ((((๐ โ ๐ท โง ๐ โ (0[,)+โ)) โง ๐ โ (0[,)+โ)) โง
โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))) โ ((๐ โ ๐ท โง ๐ โ (0[,)+โ)) โง (๐ โ (0[,)+โ) โง
โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))))) |
38 | 35, 36, 37 | 3bitr3i 300 |
. . . . . . . 8
โข ((๐ โ ๐ท โง (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐))))) โ ((๐ โ ๐ท โง ๐ โ (0[,)+โ)) โง (๐ โ (0[,)+โ) โง
โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))))) |
39 | 30, 38 | bitrdi 286 |
. . . . . . 7
โข (๐ก = ๐ โ ((๐ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))))) โ ((๐ โ ๐ท โง ๐ โ (0[,)+โ)) โง (๐ โ (0[,)+โ) โง
โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐))))))) |
40 | 21, 39, 2 | brabg 5516 |
. . . . . 6
โข ((๐ โ ๐ท โง ๐ โ (0[,)+โ)) โ (๐๐น๐ โ ((๐ โ ๐ท โง ๐ โ (0[,)+โ)) โง (๐ โ (0[,)+โ) โง
โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐))))))) |
41 | 40 | bianabs 542 |
. . . . 5
โข ((๐ โ ๐ท โง ๐ โ (0[,)+โ)) โ (๐๐น๐ โ (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))))) |
42 | 41 | 3adant1 1130 |
. . . 4
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ๐ โ ๐ท โง ๐ โ (0[,)+โ)) โ (๐๐น๐ โ (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))))) |
43 | 15, 42 | bitrd 278 |
. . 3
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ๐ โ ๐ท โง ๐ โ (0[,)+โ)) โ ((๐นโ๐) = ๐ โ (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))))) |
44 | 43 | 3expia 1121 |
. 2
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ๐ โ ๐ท) โ (๐ โ (0[,)+โ) โ ((๐นโ๐) = ๐ โ (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐))))))) |
45 | 8, 10, 44 | pm5.21ndd 380 |
1
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ๐ โ ๐ท) โ ((๐นโ๐) = ๐ โ (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))))) |