Proof of Theorem rpnnen2lem11
Step | Hyp | Ref
| Expression |
1 | | rpnnen2.3 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ ℕ) |
2 | | rpnnen2.2 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
3 | | rpnnen2.4 |
. . . . 5
⊢ (𝜑 → 𝑚 ∈ (𝐴 ∖ 𝐵)) |
4 | | eldifi 3732 |
. . . . . 6
⊢ (𝑚 ∈ (𝐴 ∖ 𝐵) → 𝑚 ∈ 𝐴) |
5 | | ssel2 3598 |
. . . . . 6
⊢ ((𝐴 ⊆ ℕ ∧ 𝑚 ∈ 𝐴) → 𝑚 ∈ ℕ) |
6 | 4, 5 | sylan2 491 |
. . . . 5
⊢ ((𝐴 ⊆ ℕ ∧ 𝑚 ∈ (𝐴 ∖ 𝐵)) → 𝑚 ∈ ℕ) |
7 | 2, 3, 6 | syl2anc 693 |
. . . 4
⊢ (𝜑 → 𝑚 ∈ ℕ) |
8 | | rpnnen2.1 |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) |
9 | 8 | rpnnen2lem6 14948 |
. . . 4
⊢ ((𝐵 ⊆ ℕ ∧ 𝑚 ∈ ℕ) →
Σ𝑘 ∈
(ℤ≥‘𝑚)((𝐹‘𝐵)‘𝑘) ∈ ℝ) |
10 | 1, 7, 9 | syl2anc 693 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐵)‘𝑘) ∈ ℝ) |
11 | | 3nn 11186 |
. . . . . 6
⊢ 3 ∈
ℕ |
12 | | nnrecre 11057 |
. . . . . 6
⊢ (3 ∈
ℕ → (1 / 3) ∈ ℝ) |
13 | 11, 12 | ax-mp 5 |
. . . . 5
⊢ (1 / 3)
∈ ℝ |
14 | 7 | nnnn0d 11351 |
. . . . 5
⊢ (𝜑 → 𝑚 ∈ ℕ0) |
15 | | reexpcl 12877 |
. . . . 5
⊢ (((1 / 3)
∈ ℝ ∧ 𝑚
∈ ℕ0) → ((1 / 3)↑𝑚) ∈ ℝ) |
16 | 13, 14, 15 | sylancr 695 |
. . . 4
⊢ (𝜑 → ((1 / 3)↑𝑚) ∈
ℝ) |
17 | 8 | rpnnen2lem6 14948 |
. . . . 5
⊢ ((𝐴 ⊆ ℕ ∧ 𝑚 ∈ ℕ) →
Σ𝑘 ∈
(ℤ≥‘𝑚)((𝐹‘𝐴)‘𝑘) ∈ ℝ) |
18 | 2, 7, 17 | syl2anc 693 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐴)‘𝑘) ∈ ℝ) |
19 | | nnrp 11842 |
. . . . . . . . 9
⊢ (3 ∈
ℕ → 3 ∈ ℝ+) |
20 | | rpreccl 11857 |
. . . . . . . . 9
⊢ (3 ∈
ℝ+ → (1 / 3) ∈ ℝ+) |
21 | 11, 19, 20 | mp2b 10 |
. . . . . . . 8
⊢ (1 / 3)
∈ ℝ+ |
22 | 7 | nnzd 11481 |
. . . . . . . 8
⊢ (𝜑 → 𝑚 ∈ ℤ) |
23 | | rpexpcl 12879 |
. . . . . . . 8
⊢ (((1 / 3)
∈ ℝ+ ∧ 𝑚 ∈ ℤ) → ((1 / 3)↑𝑚) ∈
ℝ+) |
24 | 21, 22, 23 | sylancr 695 |
. . . . . . 7
⊢ (𝜑 → ((1 / 3)↑𝑚) ∈
ℝ+) |
25 | 24 | rpred 11872 |
. . . . . 6
⊢ (𝜑 → ((1 / 3)↑𝑚) ∈
ℝ) |
26 | 25 | rehalfcld 11279 |
. . . . 5
⊢ (𝜑 → (((1 / 3)↑𝑚) / 2) ∈
ℝ) |
27 | 3 | snssd 4340 |
. . . . . . . . 9
⊢ (𝜑 → {𝑚} ⊆ (𝐴 ∖ 𝐵)) |
28 | 2 | ssdifd 3746 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ (ℕ ∖ 𝐵)) |
29 | 27, 28 | sstrd 3613 |
. . . . . . . 8
⊢ (𝜑 → {𝑚} ⊆ (ℕ ∖ 𝐵)) |
30 | 7 | snssd 4340 |
. . . . . . . . 9
⊢ (𝜑 → {𝑚} ⊆ ℕ) |
31 | | ssconb 3743 |
. . . . . . . . 9
⊢ ((𝐵 ⊆ ℕ ∧ {𝑚} ⊆ ℕ) → (𝐵 ⊆ (ℕ ∖ {𝑚}) ↔ {𝑚} ⊆ (ℕ ∖ 𝐵))) |
32 | 1, 30, 31 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ⊆ (ℕ ∖ {𝑚}) ↔ {𝑚} ⊆ (ℕ ∖ 𝐵))) |
33 | 29, 32 | mpbird 247 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ (ℕ ∖ {𝑚})) |
34 | | difssd 3738 |
. . . . . . 7
⊢ (𝜑 → (ℕ ∖ {𝑚}) ⊆
ℕ) |
35 | 8 | rpnnen2lem7 14949 |
. . . . . . 7
⊢ ((𝐵 ⊆ (ℕ ∖ {𝑚}) ∧ (ℕ ∖ {𝑚}) ⊆ ℕ ∧ 𝑚 ∈ ℕ) →
Σ𝑘 ∈
(ℤ≥‘𝑚)((𝐹‘𝐵)‘𝑘) ≤ Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘(ℕ ∖ {𝑚}))‘𝑘)) |
36 | 33, 34, 7, 35 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐵)‘𝑘) ≤ Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘(ℕ ∖ {𝑚}))‘𝑘)) |
37 | 8 | rpnnen2lem9 14951 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ →
Σ𝑘 ∈
(ℤ≥‘𝑚)((𝐹‘(ℕ ∖ {𝑚}))‘𝑘) = (0 + (((1 / 3)↑(𝑚 + 1)) / (1 − (1 /
3))))) |
38 | 7, 37 | syl 17 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘(ℕ ∖ {𝑚}))‘𝑘) = (0 + (((1 / 3)↑(𝑚 + 1)) / (1 − (1 /
3))))) |
39 | 13 | recni 10052 |
. . . . . . . . . . . 12
⊢ (1 / 3)
∈ ℂ |
40 | | expp1 12867 |
. . . . . . . . . . . 12
⊢ (((1 / 3)
∈ ℂ ∧ 𝑚
∈ ℕ0) → ((1 / 3)↑(𝑚 + 1)) = (((1 / 3)↑𝑚) · (1 / 3))) |
41 | 39, 14, 40 | sylancr 695 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1 / 3)↑(𝑚 + 1)) = (((1 / 3)↑𝑚) · (1 /
3))) |
42 | 25 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1 / 3)↑𝑚) ∈
ℂ) |
43 | | 3cn 11095 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℂ |
44 | | 3ne0 11115 |
. . . . . . . . . . . . 13
⊢ 3 ≠
0 |
45 | | divrec 10701 |
. . . . . . . . . . . . 13
⊢ ((((1 /
3)↑𝑚) ∈ ℂ
∧ 3 ∈ ℂ ∧ 3 ≠ 0) → (((1 / 3)↑𝑚) / 3) = (((1 / 3)↑𝑚) · (1 / 3))) |
46 | 43, 44, 45 | mp3an23 1416 |
. . . . . . . . . . . 12
⊢ (((1 /
3)↑𝑚) ∈ ℂ
→ (((1 / 3)↑𝑚) /
3) = (((1 / 3)↑𝑚)
· (1 / 3))) |
47 | 42, 46 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (((1 / 3)↑𝑚) / 3) = (((1 / 3)↑𝑚) · (1 /
3))) |
48 | 41, 47 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 / 3)↑(𝑚 + 1)) = (((1 / 3)↑𝑚) / 3)) |
49 | 48 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝜑 → (((1 / 3)↑(𝑚 + 1)) / (1 − (1 / 3))) =
((((1 / 3)↑𝑚) / 3) /
(1 − (1 / 3)))) |
50 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
51 | 43, 44 | pm3.2i 471 |
. . . . . . . . . . . . 13
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
52 | | divsubdir 10721 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℂ ∧ 1 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0))
→ ((3 − 1) / 3) = ((3 / 3) − (1 / 3))) |
53 | 43, 50, 51, 52 | mp3an 1424 |
. . . . . . . . . . . 12
⊢ ((3
− 1) / 3) = ((3 / 3) − (1 / 3)) |
54 | | 3m1e2 11137 |
. . . . . . . . . . . . 13
⊢ (3
− 1) = 2 |
55 | 54 | oveq1i 6660 |
. . . . . . . . . . . 12
⊢ ((3
− 1) / 3) = (2 / 3) |
56 | 43, 44 | dividi 10758 |
. . . . . . . . . . . . 13
⊢ (3 / 3) =
1 |
57 | 56 | oveq1i 6660 |
. . . . . . . . . . . 12
⊢ ((3 / 3)
− (1 / 3)) = (1 − (1 / 3)) |
58 | 53, 55, 57 | 3eqtr3ri 2653 |
. . . . . . . . . . 11
⊢ (1
− (1 / 3)) = (2 / 3) |
59 | 58 | oveq2i 6661 |
. . . . . . . . . 10
⊢ ((((1 /
3)↑𝑚) / 3) / (1
− (1 / 3))) = ((((1 / 3)↑𝑚) / 3) / (2 / 3)) |
60 | | 2cnne0 11242 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
61 | | divcan7 10734 |
. . . . . . . . . . . 12
⊢ ((((1 /
3)↑𝑚) ∈ ℂ
∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠
0)) → ((((1 / 3)↑𝑚) / 3) / (2 / 3)) = (((1 / 3)↑𝑚) / 2)) |
62 | 60, 51, 61 | mp3an23 1416 |
. . . . . . . . . . 11
⊢ (((1 /
3)↑𝑚) ∈ ℂ
→ ((((1 / 3)↑𝑚) /
3) / (2 / 3)) = (((1 / 3)↑𝑚) / 2)) |
63 | 42, 62 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((((1 / 3)↑𝑚) / 3) / (2 / 3)) = (((1 /
3)↑𝑚) /
2)) |
64 | 59, 63 | syl5eq 2668 |
. . . . . . . . 9
⊢ (𝜑 → ((((1 / 3)↑𝑚) / 3) / (1 − (1 / 3))) =
(((1 / 3)↑𝑚) /
2)) |
65 | 49, 64 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝜑 → (((1 / 3)↑(𝑚 + 1)) / (1 − (1 / 3))) =
(((1 / 3)↑𝑚) /
2)) |
66 | 65 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → (0 + (((1 / 3)↑(𝑚 + 1)) / (1 − (1 / 3)))) =
(0 + (((1 / 3)↑𝑚) /
2))) |
67 | 26 | recnd 10068 |
. . . . . . . 8
⊢ (𝜑 → (((1 / 3)↑𝑚) / 2) ∈
ℂ) |
68 | 67 | addid2d 10237 |
. . . . . . 7
⊢ (𝜑 → (0 + (((1 / 3)↑𝑚) / 2)) = (((1 / 3)↑𝑚) / 2)) |
69 | 38, 66, 68 | 3eqtrd 2660 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘(ℕ ∖ {𝑚}))‘𝑘) = (((1 / 3)↑𝑚) / 2)) |
70 | 36, 69 | breqtrd 4679 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐵)‘𝑘) ≤ (((1 / 3)↑𝑚) / 2)) |
71 | | rphalflt 11860 |
. . . . . 6
⊢ (((1 /
3)↑𝑚) ∈
ℝ+ → (((1 / 3)↑𝑚) / 2) < ((1 / 3)↑𝑚)) |
72 | 24, 71 | syl 17 |
. . . . 5
⊢ (𝜑 → (((1 / 3)↑𝑚) / 2) < ((1 / 3)↑𝑚)) |
73 | 10, 26, 25, 70, 72 | lelttrd 10195 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐵)‘𝑘) < ((1 / 3)↑𝑚)) |
74 | | eluznn 11758 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑚)) → 𝑘 ∈ ℕ) |
75 | 7, 74 | sylan 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → 𝑘 ∈ ℕ) |
76 | 8 | rpnnen2lem1 14943 |
. . . . . . . . 9
⊢ (({𝑚} ⊆ ℕ ∧ 𝑘 ∈ ℕ) → ((𝐹‘{𝑚})‘𝑘) = if(𝑘 ∈ {𝑚}, ((1 / 3)↑𝑘), 0)) |
77 | 30, 76 | sylan 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘{𝑚})‘𝑘) = if(𝑘 ∈ {𝑚}, ((1 / 3)↑𝑘), 0)) |
78 | 75, 77 | syldan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → ((𝐹‘{𝑚})‘𝑘) = if(𝑘 ∈ {𝑚}, ((1 / 3)↑𝑘), 0)) |
79 | 78 | sumeq2dv 14433 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘{𝑚})‘𝑘) = Σ𝑘 ∈ (ℤ≥‘𝑚)if(𝑘 ∈ {𝑚}, ((1 / 3)↑𝑘), 0)) |
80 | | uzid 11702 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
(ℤ≥‘𝑚)) |
81 | 22, 80 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑚 ∈ (ℤ≥‘𝑚)) |
82 | 81 | snssd 4340 |
. . . . . . 7
⊢ (𝜑 → {𝑚} ⊆ (ℤ≥‘𝑚)) |
83 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑚 ∈ V |
84 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → ((1 / 3)↑𝑘) = ((1 / 3)↑𝑚)) |
85 | 84 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → (((1 / 3)↑𝑘) ∈ ℂ ↔ ((1 / 3)↑𝑚) ∈
ℂ)) |
86 | 83, 85 | ralsn 4222 |
. . . . . . . 8
⊢
(∀𝑘 ∈
{𝑚} ((1 / 3)↑𝑘) ∈ ℂ ↔ ((1 /
3)↑𝑚) ∈
ℂ) |
87 | 42, 86 | sylibr 224 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ {𝑚} ((1 / 3)↑𝑘) ∈ ℂ) |
88 | | ssid 3624 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑚) ⊆ (ℤ≥‘𝑚) |
89 | 88 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 →
(ℤ≥‘𝑚) ⊆ (ℤ≥‘𝑚)) |
90 | 89 | orcd 407 |
. . . . . . 7
⊢ (𝜑 →
((ℤ≥‘𝑚) ⊆ (ℤ≥‘𝑚) ∨
(ℤ≥‘𝑚) ∈ Fin)) |
91 | | sumss2 14457 |
. . . . . . 7
⊢ ((({𝑚} ⊆
(ℤ≥‘𝑚) ∧ ∀𝑘 ∈ {𝑚} ((1 / 3)↑𝑘) ∈ ℂ) ∧
((ℤ≥‘𝑚) ⊆ (ℤ≥‘𝑚) ∨
(ℤ≥‘𝑚) ∈ Fin)) → Σ𝑘 ∈ {𝑚} ((1 / 3)↑𝑘) = Σ𝑘 ∈ (ℤ≥‘𝑚)if(𝑘 ∈ {𝑚}, ((1 / 3)↑𝑘), 0)) |
92 | 82, 87, 90, 91 | syl21anc 1325 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ {𝑚} ((1 / 3)↑𝑘) = Σ𝑘 ∈ (ℤ≥‘𝑚)if(𝑘 ∈ {𝑚}, ((1 / 3)↑𝑘), 0)) |
93 | 84 | sumsn 14475 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ ∧ ((1 /
3)↑𝑚) ∈ ℂ)
→ Σ𝑘 ∈
{𝑚} ((1 / 3)↑𝑘) = ((1 / 3)↑𝑚)) |
94 | 7, 42, 93 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ {𝑚} ((1 / 3)↑𝑘) = ((1 / 3)↑𝑚)) |
95 | 79, 92, 94 | 3eqtr2d 2662 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘{𝑚})‘𝑘) = ((1 / 3)↑𝑚)) |
96 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑚 ∈ 𝐴) |
97 | 96 | snssd 4340 |
. . . . . 6
⊢ (𝜑 → {𝑚} ⊆ 𝐴) |
98 | 8 | rpnnen2lem7 14949 |
. . . . . 6
⊢ (({𝑚} ⊆ 𝐴 ∧ 𝐴 ⊆ ℕ ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈
(ℤ≥‘𝑚)((𝐹‘{𝑚})‘𝑘) ≤ Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐴)‘𝑘)) |
99 | 97, 2, 7, 98 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘{𝑚})‘𝑘) ≤ Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐴)‘𝑘)) |
100 | 95, 99 | eqbrtrrd 4677 |
. . . 4
⊢ (𝜑 → ((1 / 3)↑𝑚) ≤ Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐴)‘𝑘)) |
101 | 10, 16, 18, 73, 100 | ltletrd 10197 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐵)‘𝑘) < Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐴)‘𝑘)) |
102 | 10, 101 | gtned 10172 |
. 2
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐴)‘𝑘) ≠ Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐵)‘𝑘)) |
103 | | rpnnen2.5 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵))) |
104 | | rpnnen2.6 |
. . . . 5
⊢ (𝜓 ↔ Σ𝑘 ∈ ℕ ((𝐹‘𝐴)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝐵)‘𝑘)) |
105 | 8, 2, 1, 3, 103, 104 | rpnnen2lem10 14952 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐴)‘𝑘) = Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐵)‘𝑘)) |
106 | 105 | ex 450 |
. . 3
⊢ (𝜑 → (𝜓 → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐴)‘𝑘) = Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐵)‘𝑘))) |
107 | 106 | necon3ad 2807 |
. 2
⊢ (𝜑 → (Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐴)‘𝑘) ≠ Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐵)‘𝑘) → ¬ 𝜓)) |
108 | 102, 107 | mpd 15 |
1
⊢ (𝜑 → ¬ 𝜓) |