Step | Hyp | Ref
| Expression |
1 | | fourierdlem26.5 |
. . . 4
โข ๐ธ = (๐ฅ โ โ โฆ (๐ฅ + ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐))) |
2 | 1 | a1i 11 |
. . 3
โข (๐ โ ๐ธ = (๐ฅ โ โ โฆ (๐ฅ + ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐)))) |
3 | | simpr 486 |
. . . 4
โข ((๐ โง ๐ฅ = ๐) โ ๐ฅ = ๐) |
4 | 3 | oveq2d 7374 |
. . . . . . 7
โข ((๐ โง ๐ฅ = ๐) โ (๐ต โ ๐ฅ) = (๐ต โ ๐)) |
5 | 4 | oveq1d 7373 |
. . . . . 6
โข ((๐ โง ๐ฅ = ๐) โ ((๐ต โ ๐ฅ) / ๐) = ((๐ต โ ๐) / ๐)) |
6 | 5 | fveq2d 6847 |
. . . . 5
โข ((๐ โง ๐ฅ = ๐) โ (โโ((๐ต โ ๐ฅ) / ๐)) = (โโ((๐ต โ ๐) / ๐))) |
7 | 6 | oveq1d 7373 |
. . . 4
โข ((๐ โง ๐ฅ = ๐) โ ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐) = ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) |
8 | 3, 7 | oveq12d 7376 |
. . 3
โข ((๐ โง ๐ฅ = ๐) โ (๐ฅ + ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐)) = (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
9 | | fourierdlem26.8 |
. . . . 5
โข (๐ โ ๐ โ (๐(,](๐ + ๐))) |
10 | | fourierdlem26.6 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
11 | 10 | rexrd 11210 |
. . . . . 6
โข (๐ โ ๐ โ
โ*) |
12 | | fourierdlem26.4 |
. . . . . . . 8
โข ๐ = (๐ต โ ๐ด) |
13 | | fourierdlem26.2 |
. . . . . . . . 9
โข (๐ โ ๐ต โ โ) |
14 | | fourierdlem26.1 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
15 | 13, 14 | resubcld 11588 |
. . . . . . . 8
โข (๐ โ (๐ต โ ๐ด) โ โ) |
16 | 12, 15 | eqeltrid 2838 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
17 | 10, 16 | readdcld 11189 |
. . . . . 6
โข (๐ โ (๐ + ๐) โ โ) |
18 | | elioc2 13333 |
. . . . . 6
โข ((๐ โ โ*
โง (๐ + ๐) โ โ) โ (๐ โ (๐(,](๐ + ๐)) โ (๐ โ โ โง ๐ < ๐ โง ๐ โค (๐ + ๐)))) |
19 | 11, 17, 18 | syl2anc 585 |
. . . . 5
โข (๐ โ (๐ โ (๐(,](๐ + ๐)) โ (๐ โ โ โง ๐ < ๐ โง ๐ โค (๐ + ๐)))) |
20 | 9, 19 | mpbid 231 |
. . . 4
โข (๐ โ (๐ โ โ โง ๐ < ๐ โง ๐ โค (๐ + ๐))) |
21 | 20 | simp1d 1143 |
. . 3
โข (๐ โ ๐ โ โ) |
22 | 13, 21 | resubcld 11588 |
. . . . . . . 8
โข (๐ โ (๐ต โ ๐) โ โ) |
23 | | fourierdlem26.3 |
. . . . . . . . . . 11
โข (๐ โ ๐ด < ๐ต) |
24 | 14, 13 | posdifd 11747 |
. . . . . . . . . . 11
โข (๐ โ (๐ด < ๐ต โ 0 < (๐ต โ ๐ด))) |
25 | 23, 24 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ 0 < (๐ต โ ๐ด)) |
26 | 25, 12 | breqtrrdi 5148 |
. . . . . . . . 9
โข (๐ โ 0 < ๐) |
27 | 26 | gt0ne0d 11724 |
. . . . . . . 8
โข (๐ โ ๐ โ 0) |
28 | 22, 16, 27 | redivcld 11988 |
. . . . . . 7
โข (๐ โ ((๐ต โ ๐) / ๐) โ โ) |
29 | 28 | flcld 13709 |
. . . . . 6
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) โ โค) |
30 | 29 | zred 12612 |
. . . . 5
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) โ โ) |
31 | 30, 16 | remulcld 11190 |
. . . 4
โข (๐ โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ โ) |
32 | 21, 31 | readdcld 11189 |
. . 3
โข (๐ โ (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ โ) |
33 | 2, 8, 21, 32 | fvmptd 6956 |
. 2
โข (๐ โ (๐ธโ๐) = (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
34 | 10 | recnd 11188 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
35 | 21 | recnd 11188 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
36 | 34, 35 | pncan3d 11520 |
. . . . . . . . . . 11
โข (๐ โ (๐ + (๐ โ ๐)) = ๐) |
37 | 36 | eqcomd 2739 |
. . . . . . . . . 10
โข (๐ โ ๐ = (๐ + (๐ โ ๐))) |
38 | 37 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ โ (๐ต โ ๐) = (๐ต โ (๐ + (๐ โ ๐)))) |
39 | 13 | recnd 11188 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ โ) |
40 | 35, 34 | subcld 11517 |
. . . . . . . . . 10
โข (๐ โ (๐ โ ๐) โ โ) |
41 | 39, 34, 40 | subsub4d 11548 |
. . . . . . . . 9
โข (๐ โ ((๐ต โ ๐) โ (๐ โ ๐)) = (๐ต โ (๐ + (๐ โ ๐)))) |
42 | 38, 41 | eqtr4d 2776 |
. . . . . . . 8
โข (๐ โ (๐ต โ ๐) = ((๐ต โ ๐) โ (๐ โ ๐))) |
43 | 42 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ ((๐ต โ ๐) / ๐) = (((๐ต โ ๐) โ (๐ โ ๐)) / ๐)) |
44 | 13, 10 | resubcld 11588 |
. . . . . . . . 9
โข (๐ โ (๐ต โ ๐) โ โ) |
45 | 44 | recnd 11188 |
. . . . . . . 8
โข (๐ โ (๐ต โ ๐) โ โ) |
46 | 16 | recnd 11188 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
47 | 45, 40, 46, 27 | divsubdird 11975 |
. . . . . . 7
โข (๐ โ (((๐ต โ ๐) โ (๐ โ ๐)) / ๐) = (((๐ต โ ๐) / ๐) โ ((๐ โ ๐) / ๐))) |
48 | 40, 46, 27 | divnegd 11949 |
. . . . . . . . . 10
โข (๐ โ -((๐ โ ๐) / ๐) = (-(๐ โ ๐) / ๐)) |
49 | 35, 34 | negsubdi2d 11533 |
. . . . . . . . . . 11
โข (๐ โ -(๐ โ ๐) = (๐ โ ๐)) |
50 | 49 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ โ (-(๐ โ ๐) / ๐) = ((๐ โ ๐) / ๐)) |
51 | 48, 50 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ -((๐ โ ๐) / ๐) = ((๐ โ ๐) / ๐)) |
52 | 51 | oveq2d 7374 |
. . . . . . . 8
โข (๐ โ (((๐ต โ ๐) / ๐) + -((๐ โ ๐) / ๐)) = (((๐ต โ ๐) / ๐) + ((๐ โ ๐) / ๐))) |
53 | 44, 16, 27 | redivcld 11988 |
. . . . . . . . . 10
โข (๐ โ ((๐ต โ ๐) / ๐) โ โ) |
54 | 53 | recnd 11188 |
. . . . . . . . 9
โข (๐ โ ((๐ต โ ๐) / ๐) โ โ) |
55 | 40, 46, 27 | divcld 11936 |
. . . . . . . . 9
โข (๐ โ ((๐ โ ๐) / ๐) โ โ) |
56 | 54, 55 | negsubd 11523 |
. . . . . . . 8
โข (๐ โ (((๐ต โ ๐) / ๐) + -((๐ โ ๐) / ๐)) = (((๐ต โ ๐) / ๐) โ ((๐ โ ๐) / ๐))) |
57 | | 1cnd 11155 |
. . . . . . . . . . . 12
โข (๐ โ 1 โ
โ) |
58 | 54, 57 | npcand 11521 |
. . . . . . . . . . 11
โข (๐ โ ((((๐ต โ ๐) / ๐) โ 1) + 1) = ((๐ต โ ๐) / ๐)) |
59 | 58 | eqcomd 2739 |
. . . . . . . . . 10
โข (๐ โ ((๐ต โ ๐) / ๐) = ((((๐ต โ ๐) / ๐) โ 1) + 1)) |
60 | 59 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ (((๐ต โ ๐) / ๐) + ((๐ โ ๐) / ๐)) = (((((๐ต โ ๐) / ๐) โ 1) + 1) + ((๐ โ ๐) / ๐))) |
61 | 54, 57 | subcld 11517 |
. . . . . . . . . 10
โข (๐ โ (((๐ต โ ๐) / ๐) โ 1) โ
โ) |
62 | 34, 35 | subcld 11517 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ ๐) โ โ) |
63 | 62, 46, 27 | divcld 11936 |
. . . . . . . . . 10
โข (๐ โ ((๐ โ ๐) / ๐) โ โ) |
64 | 61, 57, 63 | addassd 11182 |
. . . . . . . . 9
โข (๐ โ (((((๐ต โ ๐) / ๐) โ 1) + 1) + ((๐ โ ๐) / ๐)) = ((((๐ต โ ๐) / ๐) โ 1) + (1 + ((๐ โ ๐) / ๐)))) |
65 | 60, 64 | eqtrd 2773 |
. . . . . . . 8
โข (๐ โ (((๐ต โ ๐) / ๐) + ((๐ โ ๐) / ๐)) = ((((๐ต โ ๐) / ๐) โ 1) + (1 + ((๐ โ ๐) / ๐)))) |
66 | 52, 56, 65 | 3eqtr3d 2781 |
. . . . . . 7
โข (๐ โ (((๐ต โ ๐) / ๐) โ ((๐ โ ๐) / ๐)) = ((((๐ต โ ๐) / ๐) โ 1) + (1 + ((๐ โ ๐) / ๐)))) |
67 | 43, 47, 66 | 3eqtrd 2777 |
. . . . . 6
โข (๐ โ ((๐ต โ ๐) / ๐) = ((((๐ต โ ๐) / ๐) โ 1) + (1 + ((๐ โ ๐) / ๐)))) |
68 | 67 | fveq2d 6847 |
. . . . 5
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) = (โโ((((๐ต โ ๐) / ๐) โ 1) + (1 + ((๐ โ ๐) / ๐))))) |
69 | 10, 21 | resubcld 11588 |
. . . . . . . . 9
โข (๐ โ (๐ โ ๐) โ โ) |
70 | 16, 69 | readdcld 11189 |
. . . . . . . 8
โข (๐ โ (๐ + (๐ โ ๐)) โ โ) |
71 | 16, 26 | elrpd 12959 |
. . . . . . . 8
โข (๐ โ ๐ โ
โ+) |
72 | 34, 46 | addcomd 11362 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ + ๐) = (๐ + ๐)) |
73 | 72 | oveq2d 7374 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐(,](๐ + ๐)) = (๐(,](๐ + ๐))) |
74 | 9, 73 | eleqtrd 2836 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ (๐(,](๐ + ๐))) |
75 | 16, 10 | readdcld 11189 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ + ๐) โ โ) |
76 | | elioc2 13333 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ*
โง (๐ + ๐) โ โ) โ (๐ โ (๐(,](๐ + ๐)) โ (๐ โ โ โง ๐ < ๐ โง ๐ โค (๐ + ๐)))) |
77 | 11, 75, 76 | syl2anc 585 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ (๐(,](๐ + ๐)) โ (๐ โ โ โง ๐ < ๐ โง ๐ โค (๐ + ๐)))) |
78 | 74, 77 | mpbid 231 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ โ โง ๐ < ๐ โง ๐ โค (๐ + ๐))) |
79 | 78 | simp3d 1145 |
. . . . . . . . . . 11
โข (๐ โ ๐ โค (๐ + ๐)) |
80 | 21, 10, 16 | lesubaddd 11757 |
. . . . . . . . . . 11
โข (๐ โ ((๐ โ ๐) โค ๐ โ ๐ โค (๐ + ๐))) |
81 | 79, 80 | mpbird 257 |
. . . . . . . . . 10
โข (๐ โ (๐ โ ๐) โค ๐) |
82 | 21, 10 | resubcld 11588 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ ๐) โ โ) |
83 | 16, 82 | subge0d 11750 |
. . . . . . . . . 10
โข (๐ โ (0 โค (๐ โ (๐ โ ๐)) โ (๐ โ ๐) โค ๐)) |
84 | 81, 83 | mpbird 257 |
. . . . . . . . 9
โข (๐ โ 0 โค (๐ โ (๐ โ ๐))) |
85 | 46, 35, 34 | subsub2d 11546 |
. . . . . . . . 9
โข (๐ โ (๐ โ (๐ โ ๐)) = (๐ + (๐ โ ๐))) |
86 | 84, 85 | breqtrd 5132 |
. . . . . . . 8
โข (๐ โ 0 โค (๐ + (๐ โ ๐))) |
87 | 70, 71, 86 | divge0d 13002 |
. . . . . . 7
โข (๐ โ 0 โค ((๐ + (๐ โ ๐)) / ๐)) |
88 | 46, 62, 46, 27 | divdird 11974 |
. . . . . . . 8
โข (๐ โ ((๐ + (๐ โ ๐)) / ๐) = ((๐ / ๐) + ((๐ โ ๐) / ๐))) |
89 | 46, 27 | dividd 11934 |
. . . . . . . . . 10
โข (๐ โ (๐ / ๐) = 1) |
90 | 89 | eqcomd 2739 |
. . . . . . . . 9
โข (๐ โ 1 = (๐ / ๐)) |
91 | 90 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ (1 + ((๐ โ ๐) / ๐)) = ((๐ / ๐) + ((๐ โ ๐) / ๐))) |
92 | 88, 91 | eqtr4d 2776 |
. . . . . . 7
โข (๐ โ ((๐ + (๐ โ ๐)) / ๐) = (1 + ((๐ โ ๐) / ๐))) |
93 | 87, 92 | breqtrd 5132 |
. . . . . 6
โข (๐ โ 0 โค (1 + ((๐ โ ๐) / ๐))) |
94 | 20 | simp2d 1144 |
. . . . . . . . 9
โข (๐ โ ๐ < ๐) |
95 | 10, 21 | sublt0d 11786 |
. . . . . . . . 9
โข (๐ โ ((๐ โ ๐) < 0 โ ๐ < ๐)) |
96 | 94, 95 | mpbird 257 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐) < 0) |
97 | 69, 71, 96 | divlt0gt0d 43607 |
. . . . . . 7
โข (๐ โ ((๐ โ ๐) / ๐) < 0) |
98 | 69, 16, 27 | redivcld 11988 |
. . . . . . . 8
โข (๐ โ ((๐ โ ๐) / ๐) โ โ) |
99 | | 1red 11161 |
. . . . . . . 8
โข (๐ โ 1 โ
โ) |
100 | | ltaddneg 11375 |
. . . . . . . 8
โข ((((๐ โ ๐) / ๐) โ โ โง 1 โ โ)
โ (((๐ โ ๐) / ๐) < 0 โ (1 + ((๐ โ ๐) / ๐)) < 1)) |
101 | 98, 99, 100 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (((๐ โ ๐) / ๐) < 0 โ (1 + ((๐ โ ๐) / ๐)) < 1)) |
102 | 97, 101 | mpbid 231 |
. . . . . 6
โข (๐ โ (1 + ((๐ โ ๐) / ๐)) < 1) |
103 | 53 | flcld 13709 |
. . . . . . . . . . . . . . 15
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) โ โค) |
104 | 103 | zcnd 12613 |
. . . . . . . . . . . . . 14
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) โ โ) |
105 | 104, 46 | mulcld 11180 |
. . . . . . . . . . . . 13
โข (๐ โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ โ) |
106 | 34, 105 | pncan2d 11519 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ ๐) = ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) |
107 | 106 | eqcomd 2739 |
. . . . . . . . . . 11
โข (๐ โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) = ((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ ๐)) |
108 | 107 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ โ (((โโ((๐ต โ ๐) / ๐)) ยท ๐) / ๐) = (((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ ๐) / ๐)) |
109 | 104, 46, 27 | divcan4d 11942 |
. . . . . . . . . 10
โข (๐ โ (((โโ((๐ต โ ๐) / ๐)) ยท ๐) / ๐) = (โโ((๐ต โ ๐) / ๐))) |
110 | | id 22 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = ๐ โ ๐ฅ = ๐) |
111 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ = ๐ โ (๐ต โ ๐ฅ) = (๐ต โ ๐)) |
112 | 111 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ = ๐ โ ((๐ต โ ๐ฅ) / ๐) = ((๐ต โ ๐) / ๐)) |
113 | 112 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ = ๐ โ (โโ((๐ต โ ๐ฅ) / ๐)) = (โโ((๐ต โ ๐) / ๐))) |
114 | 113 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = ๐ โ ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐) = ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) |
115 | 110, 114 | oveq12d 7376 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = ๐ โ (๐ฅ + ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐)) = (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
116 | 115 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ = ๐) โ (๐ฅ + ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐)) = (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
117 | | reflcl 13707 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ต โ ๐) / ๐) โ โ โ
(โโ((๐ต โ
๐) / ๐)) โ โ) |
118 | 53, 117 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) โ โ) |
119 | 118, 16 | remulcld 11190 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ โ) |
120 | 10, 119 | readdcld 11189 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ โ) |
121 | 2, 116, 10, 120 | fvmptd 6956 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ธโ๐) = (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
122 | 121 | eqcomd 2739 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) = (๐ธโ๐)) |
123 | 122 | oveq1d 7373 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ ๐) = ((๐ธโ๐) โ ๐)) |
124 | 123 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ โ (((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ ๐) / ๐) = (((๐ธโ๐) โ ๐) / ๐)) |
125 | | fourierdlem26.7 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ธโ๐) = ๐ต) |
126 | 125 | oveq1d 7373 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ธโ๐) โ ๐) = (๐ต โ ๐)) |
127 | 126 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ โ (((๐ธโ๐) โ ๐) / ๐) = ((๐ต โ ๐) / ๐)) |
128 | 124, 127 | eqtrd 2773 |
. . . . . . . . . 10
โข (๐ โ (((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ ๐) / ๐) = ((๐ต โ ๐) / ๐)) |
129 | 108, 109,
128 | 3eqtr3d 2781 |
. . . . . . . . 9
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) = ((๐ต โ ๐) / ๐)) |
130 | 129, 103 | eqeltrrd 2835 |
. . . . . . . 8
โข (๐ โ ((๐ต โ ๐) / ๐) โ โค) |
131 | | 1zzd 12539 |
. . . . . . . 8
โข (๐ โ 1 โ
โค) |
132 | 130, 131 | zsubcld 12617 |
. . . . . . 7
โข (๐ โ (((๐ต โ ๐) / ๐) โ 1) โ
โค) |
133 | 99, 98 | readdcld 11189 |
. . . . . . 7
โข (๐ โ (1 + ((๐ โ ๐) / ๐)) โ โ) |
134 | | flbi2 13728 |
. . . . . . 7
โข
(((((๐ต โ ๐) / ๐) โ 1) โ โค โง (1 +
((๐ โ ๐) / ๐)) โ โ) โ
((โโ((((๐ต
โ ๐) / ๐) โ 1) + (1 + ((๐ โ ๐) / ๐)))) = (((๐ต โ ๐) / ๐) โ 1) โ (0 โค (1 + ((๐ โ ๐) / ๐)) โง (1 + ((๐ โ ๐) / ๐)) < 1))) |
135 | 132, 133,
134 | syl2anc 585 |
. . . . . 6
โข (๐ โ ((โโ((((๐ต โ ๐) / ๐) โ 1) + (1 + ((๐ โ ๐) / ๐)))) = (((๐ต โ ๐) / ๐) โ 1) โ (0 โค (1 + ((๐ โ ๐) / ๐)) โง (1 + ((๐ โ ๐) / ๐)) < 1))) |
136 | 93, 102, 135 | mpbir2and 712 |
. . . . 5
โข (๐ โ (โโ((((๐ต โ ๐) / ๐) โ 1) + (1 + ((๐ โ ๐) / ๐)))) = (((๐ต โ ๐) / ๐) โ 1)) |
137 | 129 | eqcomd 2739 |
. . . . . 6
โข (๐ โ ((๐ต โ ๐) / ๐) = (โโ((๐ต โ ๐) / ๐))) |
138 | 137 | oveq1d 7373 |
. . . . 5
โข (๐ โ (((๐ต โ ๐) / ๐) โ 1) = ((โโ((๐ต โ ๐) / ๐)) โ 1)) |
139 | 68, 136, 138 | 3eqtrd 2777 |
. . . 4
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) = ((โโ((๐ต โ ๐) / ๐)) โ 1)) |
140 | 139 | oveq1d 7373 |
. . 3
โข (๐ โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) = (((โโ((๐ต โ ๐) / ๐)) โ 1) ยท ๐)) |
141 | 140 | oveq2d 7374 |
. 2
โข (๐ โ (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) = (๐ + (((โโ((๐ต โ ๐) / ๐)) โ 1) ยท ๐))) |
142 | 37 | oveq1d 7373 |
. . 3
โข (๐ โ (๐ + (((โโ((๐ต โ ๐) / ๐)) โ 1) ยท ๐)) = ((๐ + (๐ โ ๐)) + (((โโ((๐ต โ ๐) / ๐)) โ 1) ยท ๐))) |
143 | 104, 57, 46 | subdird 11617 |
. . . . 5
โข (๐ โ (((โโ((๐ต โ ๐) / ๐)) โ 1) ยท ๐) = (((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ (1 ยท ๐))) |
144 | 143 | oveq2d 7374 |
. . . 4
โข (๐ โ ((๐ + (๐ โ ๐)) + (((โโ((๐ต โ ๐) / ๐)) โ 1) ยท ๐)) = ((๐ + (๐ โ ๐)) + (((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ (1 ยท ๐)))) |
145 | 34, 40 | addcld 11179 |
. . . . . 6
โข (๐ โ (๐ + (๐ โ ๐)) โ โ) |
146 | 57, 46 | mulcld 11180 |
. . . . . 6
โข (๐ โ (1 ยท ๐) โ
โ) |
147 | 145, 105,
146 | addsubassd 11537 |
. . . . 5
โข (๐ โ (((๐ + (๐ โ ๐)) + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ (1 ยท ๐)) = ((๐ + (๐ โ ๐)) + (((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ (1 ยท ๐)))) |
148 | 147 | eqcomd 2739 |
. . . 4
โข (๐ โ ((๐ + (๐ โ ๐)) + (((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ (1 ยท ๐))) = (((๐ + (๐ โ ๐)) + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ (1 ยท ๐))) |
149 | 34, 40, 105 | add32d 11387 |
. . . . . 6
โข (๐ โ ((๐ + (๐ โ ๐)) + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) = ((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) + (๐ โ ๐))) |
150 | 149 | oveq1d 7373 |
. . . . 5
โข (๐ โ (((๐ + (๐ โ ๐)) + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ (1 ยท ๐)) = (((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) + (๐ โ ๐)) โ (1 ยท ๐))) |
151 | 122 | oveq1d 7373 |
. . . . . 6
โข (๐ โ ((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) + (๐ โ ๐)) = ((๐ธโ๐) + (๐ โ ๐))) |
152 | 46 | mulid2d 11178 |
. . . . . 6
โข (๐ โ (1 ยท ๐) = ๐) |
153 | 151, 152 | oveq12d 7376 |
. . . . 5
โข (๐ โ (((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) + (๐ โ ๐)) โ (1 ยท ๐)) = (((๐ธโ๐) + (๐ โ ๐)) โ ๐)) |
154 | 125, 13 | eqeltrd 2834 |
. . . . . . . 8
โข (๐ โ (๐ธโ๐) โ โ) |
155 | 154 | recnd 11188 |
. . . . . . 7
โข (๐ โ (๐ธโ๐) โ โ) |
156 | 155, 40, 46 | addsubd 11538 |
. . . . . 6
โข (๐ โ (((๐ธโ๐) + (๐ โ ๐)) โ ๐) = (((๐ธโ๐) โ ๐) + (๐ โ ๐))) |
157 | 125 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ ((๐ธโ๐) โ ๐) = (๐ต โ ๐)) |
158 | 12 | a1i 11 |
. . . . . . . . 9
โข (๐ โ ๐ = (๐ต โ ๐ด)) |
159 | 158 | oveq2d 7374 |
. . . . . . . 8
โข (๐ โ (๐ต โ ๐) = (๐ต โ (๐ต โ ๐ด))) |
160 | 14 | recnd 11188 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
161 | 39, 160 | nncand 11522 |
. . . . . . . 8
โข (๐ โ (๐ต โ (๐ต โ ๐ด)) = ๐ด) |
162 | 157, 159,
161 | 3eqtrd 2777 |
. . . . . . 7
โข (๐ โ ((๐ธโ๐) โ ๐) = ๐ด) |
163 | 162 | oveq1d 7373 |
. . . . . 6
โข (๐ โ (((๐ธโ๐) โ ๐) + (๐ โ ๐)) = (๐ด + (๐ โ ๐))) |
164 | 156, 163 | eqtrd 2773 |
. . . . 5
โข (๐ โ (((๐ธโ๐) + (๐ โ ๐)) โ ๐) = (๐ด + (๐ โ ๐))) |
165 | 150, 153,
164 | 3eqtrd 2777 |
. . . 4
โข (๐ โ (((๐ + (๐ โ ๐)) + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ (1 ยท ๐)) = (๐ด + (๐ โ ๐))) |
166 | 144, 148,
165 | 3eqtrd 2777 |
. . 3
โข (๐ โ ((๐ + (๐ โ ๐)) + (((โโ((๐ต โ ๐) / ๐)) โ 1) ยท ๐)) = (๐ด + (๐ โ ๐))) |
167 | 142, 166 | eqtrd 2773 |
. 2
โข (๐ โ (๐ + (((โโ((๐ต โ ๐) / ๐)) โ 1) ยท ๐)) = (๐ด + (๐ โ ๐))) |
168 | 33, 141, 167 | 3eqtrd 2777 |
1
โข (๐ โ (๐ธโ๐) = (๐ด + (๐ โ ๐))) |