Step | Hyp | Ref
| Expression |
1 | | ruc.6 |
. . 3
⊢ 𝑆 = sup(ran (1st
∘ 𝐺), ℝ, <
) |
2 | | ruc.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
3 | | ruc.2 |
. . . . . 6
⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
4 | | ruc.4 |
. . . . . 6
⊢ 𝐶 = ({〈0, 〈0,
1〉〉} ∪ 𝐹) |
5 | | ruc.5 |
. . . . . 6
⊢ 𝐺 = seq0(𝐷, 𝐶) |
6 | 2, 3, 4, 5 | ruclem11 14808 |
. . . . 5
⊢ (𝜑 → (ran (1st
∘ 𝐺) ⊆ ℝ
∧ ran (1st ∘ 𝐺) ≠ ∅ ∧ ∀𝑧 ∈ ran (1st
∘ 𝐺)𝑧 ≤ 1)) |
7 | 6 | simp1d 1066 |
. . . 4
⊢ (𝜑 → ran (1st
∘ 𝐺) ⊆
ℝ) |
8 | 6 | simp2d 1067 |
. . . 4
⊢ (𝜑 → ran (1st
∘ 𝐺) ≠
∅) |
9 | | 1re 9918 |
. . . . 5
⊢ 1 ∈
ℝ |
10 | 6 | simp3d 1068 |
. . . . 5
⊢ (𝜑 → ∀𝑧 ∈ ran (1st ∘ 𝐺)𝑧 ≤ 1) |
11 | | breq2 4587 |
. . . . . . 7
⊢ (𝑛 = 1 → (𝑧 ≤ 𝑛 ↔ 𝑧 ≤ 1)) |
12 | 11 | ralbidv 2969 |
. . . . . 6
⊢ (𝑛 = 1 → (∀𝑧 ∈ ran (1st
∘ 𝐺)𝑧 ≤ 𝑛 ↔ ∀𝑧 ∈ ran (1st ∘ 𝐺)𝑧 ≤ 1)) |
13 | 12 | rspcev 3282 |
. . . . 5
⊢ ((1
∈ ℝ ∧ ∀𝑧 ∈ ran (1st ∘ 𝐺)𝑧 ≤ 1) → ∃𝑛 ∈ ℝ ∀𝑧 ∈ ran (1st ∘ 𝐺)𝑧 ≤ 𝑛) |
14 | 9, 10, 13 | sylancr 694 |
. . . 4
⊢ (𝜑 → ∃𝑛 ∈ ℝ ∀𝑧 ∈ ran (1st ∘ 𝐺)𝑧 ≤ 𝑛) |
15 | | suprcl 10862 |
. . . 4
⊢ ((ran
(1st ∘ 𝐺)
⊆ ℝ ∧ ran (1st ∘ 𝐺) ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ran (1st
∘ 𝐺)𝑧 ≤ 𝑛) → sup(ran (1st ∘
𝐺), ℝ, < ) ∈
ℝ) |
16 | 7, 8, 14, 15 | syl3anc 1318 |
. . 3
⊢ (𝜑 → sup(ran (1st
∘ 𝐺), ℝ, < )
∈ ℝ) |
17 | 1, 16 | syl5eqel 2692 |
. 2
⊢ (𝜑 → 𝑆 ∈ ℝ) |
18 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶ℝ) |
19 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
20 | 2, 3, 4, 5 | ruclem6 14803 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:ℕ0⟶(ℝ ×
ℝ)) |
21 | | nnm1nn0 11211 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
22 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝐺:ℕ0⟶(ℝ ×
ℝ) ∧ (𝑛 −
1) ∈ ℕ0) → (𝐺‘(𝑛 − 1)) ∈ (ℝ ×
ℝ)) |
23 | 20, 21, 22 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘(𝑛 − 1)) ∈ (ℝ ×
ℝ)) |
24 | | xp1st 7089 |
. . . . . . . . . 10
⊢ ((𝐺‘(𝑛 − 1)) ∈ (ℝ × ℝ)
→ (1st ‘(𝐺‘(𝑛 − 1))) ∈
ℝ) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐺‘(𝑛 − 1))) ∈
ℝ) |
26 | | xp2nd 7090 |
. . . . . . . . . 10
⊢ ((𝐺‘(𝑛 − 1)) ∈ (ℝ × ℝ)
→ (2nd ‘(𝐺‘(𝑛 − 1))) ∈
ℝ) |
27 | 23, 26 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐺‘(𝑛 − 1))) ∈
ℝ) |
28 | 2 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ℝ) |
29 | | eqid 2610 |
. . . . . . . . 9
⊢
(1st ‘(〈(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))〉𝐷(𝐹‘𝑛))) = (1st
‘(〈(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))〉𝐷(𝐹‘𝑛))) |
30 | | eqid 2610 |
. . . . . . . . 9
⊢
(2nd ‘(〈(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))〉𝐷(𝐹‘𝑛))) = (2nd
‘(〈(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))〉𝐷(𝐹‘𝑛))) |
31 | 2, 3, 4, 5 | ruclem8 14805 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 − 1) ∈ ℕ0)
→ (1st ‘(𝐺‘(𝑛 − 1))) < (2nd
‘(𝐺‘(𝑛 − 1)))) |
32 | 21, 31 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐺‘(𝑛 − 1))) <
(2nd ‘(𝐺‘(𝑛 − 1)))) |
33 | 18, 19, 25, 27, 28, 29, 30, 32 | ruclem3 14801 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) < (1st
‘(〈(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))〉𝐷(𝐹‘𝑛))) ∨ (2nd
‘(〈(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))〉𝐷(𝐹‘𝑛))) < (𝐹‘𝑛))) |
34 | 2, 3, 4, 5 | ruclem7 14804 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 − 1) ∈ ℕ0)
→ (𝐺‘((𝑛 − 1) + 1)) = ((𝐺‘(𝑛 − 1))𝐷(𝐹‘((𝑛 − 1) + 1)))) |
35 | 21, 34 | sylan2 490 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘((𝑛 − 1) + 1)) = ((𝐺‘(𝑛 − 1))𝐷(𝐹‘((𝑛 − 1) + 1)))) |
36 | | nncn 10905 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
38 | | ax-1cn 9873 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
39 | | npcan 10169 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) + 1) = 𝑛) |
40 | 37, 38, 39 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 − 1) + 1) = 𝑛) |
41 | 40 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘((𝑛 − 1) + 1)) = (𝐺‘𝑛)) |
42 | | 1st2nd2 7096 |
. . . . . . . . . . . . . 14
⊢ ((𝐺‘(𝑛 − 1)) ∈ (ℝ × ℝ)
→ (𝐺‘(𝑛 − 1)) =
〈(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))〉) |
43 | 23, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘(𝑛 − 1)) = 〈(1st
‘(𝐺‘(𝑛 − 1))), (2nd
‘(𝐺‘(𝑛 −
1)))〉) |
44 | 40 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘((𝑛 − 1) + 1)) = (𝐹‘𝑛)) |
45 | 43, 44 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐺‘(𝑛 − 1))𝐷(𝐹‘((𝑛 − 1) + 1))) = (〈(1st
‘(𝐺‘(𝑛 − 1))), (2nd
‘(𝐺‘(𝑛 − 1)))〉𝐷(𝐹‘𝑛))) |
46 | 35, 41, 45 | 3eqtr3d 2652 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = (〈(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))〉𝐷(𝐹‘𝑛))) |
47 | 46 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐺‘𝑛)) = (1st
‘(〈(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))〉𝐷(𝐹‘𝑛)))) |
48 | 47 | breq2d 4595 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) < (1st ‘(𝐺‘𝑛)) ↔ (𝐹‘𝑛) < (1st
‘(〈(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))〉𝐷(𝐹‘𝑛))))) |
49 | 46 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐺‘𝑛)) = (2nd
‘(〈(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))〉𝐷(𝐹‘𝑛)))) |
50 | 49 | breq1d 4593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐺‘𝑛)) < (𝐹‘𝑛) ↔ (2nd
‘(〈(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))〉𝐷(𝐹‘𝑛))) < (𝐹‘𝑛))) |
51 | 48, 50 | orbi12d 742 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝐹‘𝑛) < (1st ‘(𝐺‘𝑛)) ∨ (2nd ‘(𝐺‘𝑛)) < (𝐹‘𝑛)) ↔ ((𝐹‘𝑛) < (1st
‘(〈(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))〉𝐷(𝐹‘𝑛))) ∨ (2nd
‘(〈(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))〉𝐷(𝐹‘𝑛))) < (𝐹‘𝑛)))) |
52 | 33, 51 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) < (1st ‘(𝐺‘𝑛)) ∨ (2nd ‘(𝐺‘𝑛)) < (𝐹‘𝑛))) |
53 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (1st
∘ 𝐺) ⊆
ℝ) |
54 | 8 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (1st
∘ 𝐺) ≠
∅) |
55 | 14 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∃𝑛 ∈ ℝ ∀𝑧 ∈ ran (1st
∘ 𝐺)𝑧 ≤ 𝑛) |
56 | | nnnn0 11176 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
57 | | fvco3 6185 |
. . . . . . . . . . . . 13
⊢ ((𝐺:ℕ0⟶(ℝ ×
ℝ) ∧ 𝑛 ∈
ℕ0) → ((1st ∘ 𝐺)‘𝑛) = (1st ‘(𝐺‘𝑛))) |
58 | 20, 56, 57 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
∘ 𝐺)‘𝑛) = (1st
‘(𝐺‘𝑛))) |
59 | 20 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ0⟶(ℝ ×
ℝ)) |
60 | | 1stcof 7087 |
. . . . . . . . . . . . . 14
⊢ (𝐺:ℕ0⟶(ℝ ×
ℝ) → (1st ∘ 𝐺):ℕ0⟶ℝ) |
61 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢
((1st ∘ 𝐺):ℕ0⟶ℝ →
(1st ∘ 𝐺)
Fn ℕ0) |
62 | 59, 60, 61 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
∘ 𝐺) Fn
ℕ0) |
63 | 56 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) |
64 | | fnfvelrn 6264 |
. . . . . . . . . . . . 13
⊢
(((1st ∘ 𝐺) Fn ℕ0 ∧ 𝑛 ∈ ℕ0)
→ ((1st ∘ 𝐺)‘𝑛) ∈ ran (1st ∘ 𝐺)) |
65 | 62, 63, 64 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
∘ 𝐺)‘𝑛) ∈ ran (1st
∘ 𝐺)) |
66 | 58, 65 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐺‘𝑛)) ∈ ran (1st
∘ 𝐺)) |
67 | | suprub 10863 |
. . . . . . . . . . 11
⊢ (((ran
(1st ∘ 𝐺)
⊆ ℝ ∧ ran (1st ∘ 𝐺) ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ran (1st
∘ 𝐺)𝑧 ≤ 𝑛) ∧ (1st ‘(𝐺‘𝑛)) ∈ ran (1st ∘ 𝐺)) → (1st
‘(𝐺‘𝑛)) ≤ sup(ran (1st
∘ 𝐺), ℝ, <
)) |
68 | 53, 54, 55, 66, 67 | syl31anc 1321 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐺‘𝑛)) ≤ sup(ran (1st
∘ 𝐺), ℝ, <
)) |
69 | 68, 1 | syl6breqr 4625 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐺‘𝑛)) ≤ 𝑆) |
70 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝐺:ℕ0⟶(ℝ ×
ℝ) ∧ 𝑛 ∈
ℕ0) → (𝐺‘𝑛) ∈ (ℝ ×
ℝ)) |
71 | 20, 56, 70 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ (ℝ ×
ℝ)) |
72 | | xp1st 7089 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑛) ∈ (ℝ × ℝ) →
(1st ‘(𝐺‘𝑛)) ∈ ℝ) |
73 | 71, 72 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐺‘𝑛)) ∈
ℝ) |
74 | 17 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ∈ ℝ) |
75 | | ltletr 10008 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑛) ∈ ℝ ∧ (1st
‘(𝐺‘𝑛)) ∈ ℝ ∧ 𝑆 ∈ ℝ) → (((𝐹‘𝑛) < (1st ‘(𝐺‘𝑛)) ∧ (1st ‘(𝐺‘𝑛)) ≤ 𝑆) → (𝐹‘𝑛) < 𝑆)) |
76 | 28, 73, 74, 75 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝐹‘𝑛) < (1st ‘(𝐺‘𝑛)) ∧ (1st ‘(𝐺‘𝑛)) ≤ 𝑆) → (𝐹‘𝑛) < 𝑆)) |
77 | 69, 76 | mpan2d 706 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) < (1st ‘(𝐺‘𝑛)) → (𝐹‘𝑛) < 𝑆)) |
78 | | fvco3 6185 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺:ℕ0⟶(ℝ ×
ℝ) ∧ 𝑘 ∈
ℕ0) → ((1st ∘ 𝐺)‘𝑘) = (1st ‘(𝐺‘𝑘))) |
79 | 59, 78 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) →
((1st ∘ 𝐺)‘𝑘) = (1st ‘(𝐺‘𝑘))) |
80 | 59 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ (ℝ ×
ℝ)) |
81 | | xp1st 7089 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑘) ∈ (ℝ × ℝ) →
(1st ‘(𝐺‘𝑘)) ∈ ℝ) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) →
(1st ‘(𝐺‘𝑘)) ∈ ℝ) |
83 | | xp2nd 7090 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺‘𝑛) ∈ (ℝ × ℝ) →
(2nd ‘(𝐺‘𝑛)) ∈ ℝ) |
84 | 71, 83 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐺‘𝑛)) ∈
ℝ) |
85 | 84 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) →
(2nd ‘(𝐺‘𝑛)) ∈ ℝ) |
86 | 18 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → 𝐹:ℕ⟶ℝ) |
87 | 19 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
88 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
89 | 63 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
90 | 86, 87, 4, 5, 88, 89 | ruclem10 14807 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) →
(1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑛))) |
91 | 82, 85, 90 | ltled 10064 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) →
(1st ‘(𝐺‘𝑘)) ≤ (2nd ‘(𝐺‘𝑛))) |
92 | 79, 91 | eqbrtrd 4605 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) →
((1st ∘ 𝐺)‘𝑘) ≤ (2nd ‘(𝐺‘𝑛))) |
93 | 92 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ ℕ0
((1st ∘ 𝐺)‘𝑘) ≤ (2nd ‘(𝐺‘𝑛))) |
94 | | breq1 4586 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((1st ∘
𝐺)‘𝑘) → (𝑧 ≤ (2nd ‘(𝐺‘𝑛)) ↔ ((1st ∘ 𝐺)‘𝑘) ≤ (2nd ‘(𝐺‘𝑛)))) |
95 | 94 | ralrn 6270 |
. . . . . . . . . . . . 13
⊢
((1st ∘ 𝐺) Fn ℕ0 →
(∀𝑧 ∈ ran
(1st ∘ 𝐺)𝑧 ≤ (2nd ‘(𝐺‘𝑛)) ↔ ∀𝑘 ∈ ℕ0 ((1st
∘ 𝐺)‘𝑘) ≤ (2nd
‘(𝐺‘𝑛)))) |
96 | 62, 95 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑧 ∈ ran (1st
∘ 𝐺)𝑧 ≤ (2nd
‘(𝐺‘𝑛)) ↔ ∀𝑘 ∈ ℕ0
((1st ∘ 𝐺)‘𝑘) ≤ (2nd ‘(𝐺‘𝑛)))) |
97 | 93, 96 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑧 ∈ ran (1st
∘ 𝐺)𝑧 ≤ (2nd
‘(𝐺‘𝑛))) |
98 | | suprleub 10866 |
. . . . . . . . . . . 12
⊢ (((ran
(1st ∘ 𝐺)
⊆ ℝ ∧ ran (1st ∘ 𝐺) ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ran (1st
∘ 𝐺)𝑧 ≤ 𝑛) ∧ (2nd ‘(𝐺‘𝑛)) ∈ ℝ) → (sup(ran
(1st ∘ 𝐺),
ℝ, < ) ≤ (2nd ‘(𝐺‘𝑛)) ↔ ∀𝑧 ∈ ran (1st ∘ 𝐺)𝑧 ≤ (2nd ‘(𝐺‘𝑛)))) |
99 | 53, 54, 55, 84, 98 | syl31anc 1321 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (sup(ran
(1st ∘ 𝐺),
ℝ, < ) ≤ (2nd ‘(𝐺‘𝑛)) ↔ ∀𝑧 ∈ ran (1st ∘ 𝐺)𝑧 ≤ (2nd ‘(𝐺‘𝑛)))) |
100 | 97, 99 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran
(1st ∘ 𝐺),
ℝ, < ) ≤ (2nd ‘(𝐺‘𝑛))) |
101 | 1, 100 | syl5eqbr 4618 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ≤ (2nd ‘(𝐺‘𝑛))) |
102 | | lelttr 10007 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℝ ∧
(2nd ‘(𝐺‘𝑛)) ∈ ℝ ∧ (𝐹‘𝑛) ∈ ℝ) → ((𝑆 ≤ (2nd ‘(𝐺‘𝑛)) ∧ (2nd ‘(𝐺‘𝑛)) < (𝐹‘𝑛)) → 𝑆 < (𝐹‘𝑛))) |
103 | 74, 84, 28, 102 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑆 ≤ (2nd ‘(𝐺‘𝑛)) ∧ (2nd ‘(𝐺‘𝑛)) < (𝐹‘𝑛)) → 𝑆 < (𝐹‘𝑛))) |
104 | 101, 103 | mpand 707 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐺‘𝑛)) < (𝐹‘𝑛) → 𝑆 < (𝐹‘𝑛))) |
105 | 77, 104 | orim12d 879 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝐹‘𝑛) < (1st ‘(𝐺‘𝑛)) ∨ (2nd ‘(𝐺‘𝑛)) < (𝐹‘𝑛)) → ((𝐹‘𝑛) < 𝑆 ∨ 𝑆 < (𝐹‘𝑛)))) |
106 | 52, 105 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) < 𝑆 ∨ 𝑆 < (𝐹‘𝑛))) |
107 | 28, 74 | lttri2d 10055 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ≠ 𝑆 ↔ ((𝐹‘𝑛) < 𝑆 ∨ 𝑆 < (𝐹‘𝑛)))) |
108 | 106, 107 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ≠ 𝑆) |
109 | 108 | neneqd 2787 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ¬ (𝐹‘𝑛) = 𝑆) |
110 | 109 | nrexdv 2984 |
. . 3
⊢ (𝜑 → ¬ ∃𝑛 ∈ ℕ (𝐹‘𝑛) = 𝑆) |
111 | | risset 3044 |
. . . 4
⊢ (𝑆 ∈ ran 𝐹 ↔ ∃𝑧 ∈ ran 𝐹 𝑧 = 𝑆) |
112 | | ffn 5958 |
. . . . 5
⊢ (𝐹:ℕ⟶ℝ →
𝐹 Fn
ℕ) |
113 | | eqeq1 2614 |
. . . . . 6
⊢ (𝑧 = (𝐹‘𝑛) → (𝑧 = 𝑆 ↔ (𝐹‘𝑛) = 𝑆)) |
114 | 113 | rexrn 6269 |
. . . . 5
⊢ (𝐹 Fn ℕ → (∃𝑧 ∈ ran 𝐹 𝑧 = 𝑆 ↔ ∃𝑛 ∈ ℕ (𝐹‘𝑛) = 𝑆)) |
115 | 2, 112, 114 | 3syl 18 |
. . . 4
⊢ (𝜑 → (∃𝑧 ∈ ran 𝐹 𝑧 = 𝑆 ↔ ∃𝑛 ∈ ℕ (𝐹‘𝑛) = 𝑆)) |
116 | 111, 115 | syl5bb 271 |
. . 3
⊢ (𝜑 → (𝑆 ∈ ran 𝐹 ↔ ∃𝑛 ∈ ℕ (𝐹‘𝑛) = 𝑆)) |
117 | 110, 116 | mtbird 314 |
. 2
⊢ (𝜑 → ¬ 𝑆 ∈ ran 𝐹) |
118 | 17, 117 | eldifd 3551 |
1
⊢ (𝜑 → 𝑆 ∈ (ℝ ∖ ran 𝐹)) |