Step | Hyp | Ref
| Expression |
1 | | oveq2 7401 |
. . . . . . 7
β’ (π = 0 β (πβπ) = (πβ0)) |
2 | 1 | fveq2d 6882 |
. . . . . 6
β’ (π = 0 β (πΉβ(πβπ)) = (πΉβ(πβ0))) |
3 | | oveq2 7401 |
. . . . . 6
β’ (π = 0 β ((πΉβπ)βπ) = ((πΉβπ)β0)) |
4 | 2, 3 | eqeq12d 2747 |
. . . . 5
β’ (π = 0 β ((πΉβ(πβπ)) = ((πΉβπ)βπ) β (πΉβ(πβ0)) = ((πΉβπ)β0))) |
5 | 4 | imbi2d 340 |
. . . 4
β’ (π = 0 β (((πΉ β π΄ β§ π β β) β (πΉβ(πβπ)) = ((πΉβπ)βπ)) β ((πΉ β π΄ β§ π β β) β (πΉβ(πβ0)) = ((πΉβπ)β0)))) |
6 | | oveq2 7401 |
. . . . . . 7
β’ (π = π β (πβπ) = (πβπ)) |
7 | 6 | fveq2d 6882 |
. . . . . 6
β’ (π = π β (πΉβ(πβπ)) = (πΉβ(πβπ))) |
8 | | oveq2 7401 |
. . . . . 6
β’ (π = π β ((πΉβπ)βπ) = ((πΉβπ)βπ)) |
9 | 7, 8 | eqeq12d 2747 |
. . . . 5
β’ (π = π β ((πΉβ(πβπ)) = ((πΉβπ)βπ) β (πΉβ(πβπ)) = ((πΉβπ)βπ))) |
10 | 9 | imbi2d 340 |
. . . 4
β’ (π = π β (((πΉ β π΄ β§ π β β) β (πΉβ(πβπ)) = ((πΉβπ)βπ)) β ((πΉ β π΄ β§ π β β) β (πΉβ(πβπ)) = ((πΉβπ)βπ)))) |
11 | | oveq2 7401 |
. . . . . . 7
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
12 | 11 | fveq2d 6882 |
. . . . . 6
β’ (π = (π + 1) β (πΉβ(πβπ)) = (πΉβ(πβ(π + 1)))) |
13 | | oveq2 7401 |
. . . . . 6
β’ (π = (π + 1) β ((πΉβπ)βπ) = ((πΉβπ)β(π + 1))) |
14 | 12, 13 | eqeq12d 2747 |
. . . . 5
β’ (π = (π + 1) β ((πΉβ(πβπ)) = ((πΉβπ)βπ) β (πΉβ(πβ(π + 1))) = ((πΉβπ)β(π + 1)))) |
15 | 14 | imbi2d 340 |
. . . 4
β’ (π = (π + 1) β (((πΉ β π΄ β§ π β β) β (πΉβ(πβπ)) = ((πΉβπ)βπ)) β ((πΉ β π΄ β§ π β β) β (πΉβ(πβ(π + 1))) = ((πΉβπ)β(π + 1))))) |
16 | | oveq2 7401 |
. . . . . . 7
β’ (π = π β (πβπ) = (πβπ)) |
17 | 16 | fveq2d 6882 |
. . . . . 6
β’ (π = π β (πΉβ(πβπ)) = (πΉβ(πβπ))) |
18 | | oveq2 7401 |
. . . . . 6
β’ (π = π β ((πΉβπ)βπ) = ((πΉβπ)βπ)) |
19 | 17, 18 | eqeq12d 2747 |
. . . . 5
β’ (π = π β ((πΉβ(πβπ)) = ((πΉβπ)βπ) β (πΉβ(πβπ)) = ((πΉβπ)βπ))) |
20 | 19 | imbi2d 340 |
. . . 4
β’ (π = π β (((πΉ β π΄ β§ π β β) β (πΉβ(πβπ)) = ((πΉβπ)βπ)) β ((πΉ β π΄ β§ π β β) β (πΉβ(πβπ)) = ((πΉβπ)βπ)))) |
21 | | ax-1ne0 11161 |
. . . . . . 7
β’ 1 β
0 |
22 | | qabsabv.a |
. . . . . . . 8
β’ π΄ = (AbsValβπ) |
23 | | qrng.q |
. . . . . . . . 9
β’ π = (βfld
βΎs β) |
24 | 23 | qrng1 27052 |
. . . . . . . 8
β’ 1 =
(1rβπ) |
25 | 23 | qrng0 27051 |
. . . . . . . 8
β’ 0 =
(0gβπ) |
26 | 22, 24, 25 | abv1z 20389 |
. . . . . . 7
β’ ((πΉ β π΄ β§ 1 β 0) β (πΉβ1) = 1) |
27 | 21, 26 | mpan2 689 |
. . . . . 6
β’ (πΉ β π΄ β (πΉβ1) = 1) |
28 | 27 | adantr 481 |
. . . . 5
β’ ((πΉ β π΄ β§ π β β) β (πΉβ1) = 1) |
29 | | qcn 12929 |
. . . . . . . 8
β’ (π β β β π β
β) |
30 | 29 | adantl 482 |
. . . . . . 7
β’ ((πΉ β π΄ β§ π β β) β π β β) |
31 | 30 | exp0d 14087 |
. . . . . 6
β’ ((πΉ β π΄ β§ π β β) β (πβ0) = 1) |
32 | 31 | fveq2d 6882 |
. . . . 5
β’ ((πΉ β π΄ β§ π β β) β (πΉβ(πβ0)) = (πΉβ1)) |
33 | 23 | qrngbas 27049 |
. . . . . . . 8
β’ β =
(Baseβπ) |
34 | 22, 33 | abvcl 20381 |
. . . . . . 7
β’ ((πΉ β π΄ β§ π β β) β (πΉβπ) β β) |
35 | 34 | recnd 11224 |
. . . . . 6
β’ ((πΉ β π΄ β§ π β β) β (πΉβπ) β β) |
36 | 35 | exp0d 14087 |
. . . . 5
β’ ((πΉ β π΄ β§ π β β) β ((πΉβπ)β0) = 1) |
37 | 28, 32, 36 | 3eqtr4d 2781 |
. . . 4
β’ ((πΉ β π΄ β§ π β β) β (πΉβ(πβ0)) = ((πΉβπ)β0)) |
38 | | oveq1 7400 |
. . . . . . 7
β’ ((πΉβ(πβπ)) = ((πΉβπ)βπ) β ((πΉβ(πβπ)) Β· (πΉβπ)) = (((πΉβπ)βπ) Β· (πΉβπ))) |
39 | | expp1 14016 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β0)
β (πβ(π + 1)) = ((πβπ) Β· π)) |
40 | 30, 39 | sylan 580 |
. . . . . . . . . 10
β’ (((πΉ β π΄ β§ π β β) β§ π β β0) β (πβ(π + 1)) = ((πβπ) Β· π)) |
41 | 40 | fveq2d 6882 |
. . . . . . . . 9
β’ (((πΉ β π΄ β§ π β β) β§ π β β0) β (πΉβ(πβ(π + 1))) = (πΉβ((πβπ) Β· π))) |
42 | | simpll 765 |
. . . . . . . . . 10
β’ (((πΉ β π΄ β§ π β β) β§ π β β0) β πΉ β π΄) |
43 | | qexpcl 14025 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β0)
β (πβπ) β
β) |
44 | 43 | adantll 712 |
. . . . . . . . . 10
β’ (((πΉ β π΄ β§ π β β) β§ π β β0) β (πβπ) β β) |
45 | | simplr 767 |
. . . . . . . . . 10
β’ (((πΉ β π΄ β§ π β β) β§ π β β0) β π β
β) |
46 | | qex 12927 |
. . . . . . . . . . . 12
β’ β
β V |
47 | | cnfldmul 20884 |
. . . . . . . . . . . . 13
β’ Β·
= (.rββfld) |
48 | 23, 47 | ressmulr 17234 |
. . . . . . . . . . . 12
β’ (β
β V β Β· = (.rβπ)) |
49 | 46, 48 | ax-mp 5 |
. . . . . . . . . . 11
β’ Β·
= (.rβπ) |
50 | 22, 33, 49 | abvmul 20386 |
. . . . . . . . . 10
β’ ((πΉ β π΄ β§ (πβπ) β β β§ π β β) β (πΉβ((πβπ) Β· π)) = ((πΉβ(πβπ)) Β· (πΉβπ))) |
51 | 42, 44, 45, 50 | syl3anc 1371 |
. . . . . . . . 9
β’ (((πΉ β π΄ β§ π β β) β§ π β β0) β (πΉβ((πβπ) Β· π)) = ((πΉβ(πβπ)) Β· (πΉβπ))) |
52 | 41, 51 | eqtrd 2771 |
. . . . . . . 8
β’ (((πΉ β π΄ β§ π β β) β§ π β β0) β (πΉβ(πβ(π + 1))) = ((πΉβ(πβπ)) Β· (πΉβπ))) |
53 | | expp1 14016 |
. . . . . . . . 9
β’ (((πΉβπ) β β β§ π β β0) β ((πΉβπ)β(π + 1)) = (((πΉβπ)βπ) Β· (πΉβπ))) |
54 | 35, 53 | sylan 580 |
. . . . . . . 8
β’ (((πΉ β π΄ β§ π β β) β§ π β β0) β ((πΉβπ)β(π + 1)) = (((πΉβπ)βπ) Β· (πΉβπ))) |
55 | 52, 54 | eqeq12d 2747 |
. . . . . . 7
β’ (((πΉ β π΄ β§ π β β) β§ π β β0) β ((πΉβ(πβ(π + 1))) = ((πΉβπ)β(π + 1)) β ((πΉβ(πβπ)) Β· (πΉβπ)) = (((πΉβπ)βπ) Β· (πΉβπ)))) |
56 | 38, 55 | imbitrrid 245 |
. . . . . 6
β’ (((πΉ β π΄ β§ π β β) β§ π β β0) β ((πΉβ(πβπ)) = ((πΉβπ)βπ) β (πΉβ(πβ(π + 1))) = ((πΉβπ)β(π + 1)))) |
57 | 56 | expcom 414 |
. . . . 5
β’ (π β β0
β ((πΉ β π΄ β§ π β β) β ((πΉβ(πβπ)) = ((πΉβπ)βπ) β (πΉβ(πβ(π + 1))) = ((πΉβπ)β(π + 1))))) |
58 | 57 | a2d 29 |
. . . 4
β’ (π β β0
β (((πΉ β π΄ β§ π β β) β (πΉβ(πβπ)) = ((πΉβπ)βπ)) β ((πΉ β π΄ β§ π β β) β (πΉβ(πβ(π + 1))) = ((πΉβπ)β(π + 1))))) |
59 | 5, 10, 15, 20, 37, 58 | nn0ind 12639 |
. . 3
β’ (π β β0
β ((πΉ β π΄ β§ π β β) β (πΉβ(πβπ)) = ((πΉβπ)βπ))) |
60 | 59 | com12 32 |
. 2
β’ ((πΉ β π΄ β§ π β β) β (π β β0 β (πΉβ(πβπ)) = ((πΉβπ)βπ))) |
61 | 60 | 3impia 1117 |
1
β’ ((πΉ β π΄ β§ π β β β§ π β β0) β (πΉβ(πβπ)) = ((πΉβπ)βπ)) |