Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ruclem12 Structured version   Visualization version   GIF version

Theorem ruclem12 15014
 Description: Lemma for ruc 15016. The supremum of the increasing sequence 1st ∘ 𝐺 is a real number that is not in the range of 𝐹. (Contributed by Mario Carneiro, 28-May-2014.)
Hypotheses
Ref Expression
ruc.1 (𝜑𝐹:ℕ⟶ℝ)
ruc.2 (𝜑𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ (((1st𝑥) + (2nd𝑥)) / 2) / 𝑚if(𝑚 < 𝑦, ⟨(1st𝑥), 𝑚⟩, ⟨((𝑚 + (2nd𝑥)) / 2), (2nd𝑥)⟩)))
ruc.4 𝐶 = ({⟨0, ⟨0, 1⟩⟩} ∪ 𝐹)
ruc.5 𝐺 = seq0(𝐷, 𝐶)
ruc.6 𝑆 = sup(ran (1st𝐺), ℝ, < )
Assertion
Ref Expression
ruclem12 (𝜑𝑆 ∈ (ℝ ∖ ran 𝐹))
Distinct variable groups:   𝑥,𝑚,𝑦,𝐹   𝑚,𝐺,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑚)   𝐶(𝑥,𝑦,𝑚)   𝐷(𝑥,𝑦,𝑚)   𝑆(𝑥,𝑦,𝑚)

Proof of Theorem ruclem12
Dummy variables 𝑧 𝑛 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef 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(𝐷, 𝐶)
62, 3, 4, 5ruclem11 15013 . . . . 5 (𝜑 → (ran (1st𝐺) ⊆ ℝ ∧ ran (1st𝐺) ≠ ∅ ∧ ∀𝑧 ∈ ran (1st𝐺)𝑧 ≤ 1))
76simp1d 1093 . . . 4 (𝜑 → ran (1st𝐺) ⊆ ℝ)
86simp2d 1094 . . . 4 (𝜑 → ran (1st𝐺) ≠ ∅)
9 1re 10077 . . . . 5 1 ∈ ℝ
106simp3d 1095 . . . . 5 (𝜑 → ∀𝑧 ∈ ran (1st𝐺)𝑧 ≤ 1)
11 breq2 4689 . . . . . . 7 (𝑛 = 1 → (𝑧𝑛𝑧 ≤ 1))
1211ralbidv 3015 . . . . . 6 (𝑛 = 1 → (∀𝑧 ∈ ran (1st𝐺)𝑧𝑛 ↔ ∀𝑧 ∈ ran (1st𝐺)𝑧 ≤ 1))
1312rspcev 3340 . . . . 5 ((1 ∈ ℝ ∧ ∀𝑧 ∈ ran (1st𝐺)𝑧 ≤ 1) → ∃𝑛 ∈ ℝ ∀𝑧 ∈ ran (1st𝐺)𝑧𝑛)
149, 10, 13sylancr 696 . . . 4 (𝜑 → ∃𝑛 ∈ ℝ ∀𝑧 ∈ ran (1st𝐺)𝑧𝑛)
15 suprcl 11021 . . . 4 ((ran (1st𝐺) ⊆ ℝ ∧ ran (1st𝐺) ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ran (1st𝐺)𝑧𝑛) → sup(ran (1st𝐺), ℝ, < ) ∈ ℝ)
167, 8, 14, 15syl3anc 1366 . . 3 (𝜑 → sup(ran (1st𝐺), ℝ, < ) ∈ ℝ)
171, 16syl5eqel 2734 . 2 (𝜑𝑆 ∈ ℝ)
182adantr 480 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝐹:ℕ⟶ℝ)
193adantr 480 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ (((1st𝑥) + (2nd𝑥)) / 2) / 𝑚if(𝑚 < 𝑦, ⟨(1st𝑥), 𝑚⟩, ⟨((𝑚 + (2nd𝑥)) / 2), (2nd𝑥)⟩)))
202, 3, 4, 5ruclem6 15008 . . . . . . . . . . 11 (𝜑𝐺:ℕ0⟶(ℝ × ℝ))
21 nnm1nn0 11372 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
22 ffvelrn 6397 . . . . . . . . . . 11 ((𝐺:ℕ0⟶(ℝ × ℝ) ∧ (𝑛 − 1) ∈ ℕ0) → (𝐺‘(𝑛 − 1)) ∈ (ℝ × ℝ))
2320, 21, 22syl2an 493 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐺‘(𝑛 − 1)) ∈ (ℝ × ℝ))
24 xp1st 7242 . . . . . . . . . 10 ((𝐺‘(𝑛 − 1)) ∈ (ℝ × ℝ) → (1st ‘(𝐺‘(𝑛 − 1))) ∈ ℝ)
2523, 24syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺‘(𝑛 − 1))) ∈ ℝ)
26 xp2nd 7243 . . . . . . . . . 10 ((𝐺‘(𝑛 − 1)) ∈ (ℝ × ℝ) → (2nd ‘(𝐺‘(𝑛 − 1))) ∈ ℝ)
2723, 26syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺‘(𝑛 − 1))) ∈ ℝ)
282ffvelrnda 6399 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ℝ)
29 eqid 2651 . . . . . . . . 9 (1st ‘(⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩𝐷(𝐹𝑛))) = (1st ‘(⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩𝐷(𝐹𝑛)))
30 eqid 2651 . . . . . . . . 9 (2nd ‘(⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩𝐷(𝐹𝑛))) = (2nd ‘(⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩𝐷(𝐹𝑛)))
312, 3, 4, 5ruclem8 15010 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 − 1) ∈ ℕ0) → (1st ‘(𝐺‘(𝑛 − 1))) < (2nd ‘(𝐺‘(𝑛 − 1))))
3221, 31sylan2 490 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺‘(𝑛 − 1))) < (2nd ‘(𝐺‘(𝑛 − 1))))
3318, 19, 25, 27, 28, 29, 30, 32ruclem3 15006 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((𝐹𝑛) < (1st ‘(⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩𝐷(𝐹𝑛))) ∨ (2nd ‘(⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩𝐷(𝐹𝑛))) < (𝐹𝑛)))
342, 3, 4, 5ruclem7 15009 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 − 1) ∈ ℕ0) → (𝐺‘((𝑛 − 1) + 1)) = ((𝐺‘(𝑛 − 1))𝐷(𝐹‘((𝑛 − 1) + 1))))
3521, 34sylan2 490 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝐺‘((𝑛 − 1) + 1)) = ((𝐺‘(𝑛 − 1))𝐷(𝐹‘((𝑛 − 1) + 1))))
36 nncn 11066 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
3736adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
38 ax-1cn 10032 . . . . . . . . . . . . . 14 1 ∈ ℂ
39 npcan 10328 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 − 1) + 1) = 𝑛)
4037, 38, 39sylancl 695 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((𝑛 − 1) + 1) = 𝑛)
4140fveq2d 6233 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝐺‘((𝑛 − 1) + 1)) = (𝐺𝑛))
42 1st2nd2 7249 . . . . . . . . . . . . . 14 ((𝐺‘(𝑛 − 1)) ∈ (ℝ × ℝ) → (𝐺‘(𝑛 − 1)) = ⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩)
4323, 42syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝐺‘(𝑛 − 1)) = ⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩)
4440fveq2d 6233 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝐹‘((𝑛 − 1) + 1)) = (𝐹𝑛))
4543, 44oveq12d 6708 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((𝐺‘(𝑛 − 1))𝐷(𝐹‘((𝑛 − 1) + 1))) = (⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩𝐷(𝐹𝑛)))
4635, 41, 453eqtr3d 2693 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) = (⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩𝐷(𝐹𝑛)))
4746fveq2d 6233 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) = (1st ‘(⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩𝐷(𝐹𝑛))))
4847breq2d 4697 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((𝐹𝑛) < (1st ‘(𝐺𝑛)) ↔ (𝐹𝑛) < (1st ‘(⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩𝐷(𝐹𝑛)))))
4946fveq2d 6233 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = (2nd ‘(⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩𝐷(𝐹𝑛))))
5049breq1d 4695 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((2nd ‘(𝐺𝑛)) < (𝐹𝑛) ↔ (2nd ‘(⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩𝐷(𝐹𝑛))) < (𝐹𝑛)))
5148, 50orbi12d 746 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((𝐹𝑛) < (1st ‘(𝐺𝑛)) ∨ (2nd ‘(𝐺𝑛)) < (𝐹𝑛)) ↔ ((𝐹𝑛) < (1st ‘(⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩𝐷(𝐹𝑛))) ∨ (2nd ‘(⟨(1st ‘(𝐺‘(𝑛 − 1))), (2nd ‘(𝐺‘(𝑛 − 1)))⟩𝐷(𝐹𝑛))) < (𝐹𝑛))))
5233, 51mpbird 247 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐹𝑛) < (1st ‘(𝐺𝑛)) ∨ (2nd ‘(𝐺𝑛)) < (𝐹𝑛)))
537adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ran (1st𝐺) ⊆ ℝ)
548adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ran (1st𝐺) ≠ ∅)
5514adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ∃𝑛 ∈ ℝ ∀𝑧 ∈ ran (1st𝐺)𝑧𝑛)
56 nnnn0 11337 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
57 fvco3 6314 . . . . . . . . . . . . 13 ((𝐺:ℕ0⟶(ℝ × ℝ) ∧ 𝑛 ∈ ℕ0) → ((1st𝐺)‘𝑛) = (1st ‘(𝐺𝑛)))
5820, 56, 57syl2an 493 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((1st𝐺)‘𝑛) = (1st ‘(𝐺𝑛)))
5920adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 𝐺:ℕ0⟶(ℝ × ℝ))
60 1stcof 7240 . . . . . . . . . . . . . 14 (𝐺:ℕ0⟶(ℝ × ℝ) → (1st𝐺):ℕ0⟶ℝ)
61 ffn 6083 . . . . . . . . . . . . . 14 ((1st𝐺):ℕ0⟶ℝ → (1st𝐺) Fn ℕ0)
6259, 60, 613syl 18 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (1st𝐺) Fn ℕ0)
6356adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
64 fnfvelrn 6396 . . . . . . . . . . . . 13 (((1st𝐺) Fn ℕ0𝑛 ∈ ℕ0) → ((1st𝐺)‘𝑛) ∈ ran (1st𝐺))
6562, 63, 64syl2anc 694 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((1st𝐺)‘𝑛) ∈ ran (1st𝐺))
6658, 65eqeltrrd 2731 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) ∈ ran (1st𝐺))
67 suprub 11022 . . . . . . . . . . 11 (((ran (1st𝐺) ⊆ ℝ ∧ ran (1st𝐺) ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ran (1st𝐺)𝑧𝑛) ∧ (1st ‘(𝐺𝑛)) ∈ ran (1st𝐺)) → (1st ‘(𝐺𝑛)) ≤ sup(ran (1st𝐺), ℝ, < ))
6853, 54, 55, 66, 67syl31anc 1369 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) ≤ sup(ran (1st𝐺), ℝ, < ))
6968, 1syl6breqr 4727 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) ≤ 𝑆)
70 ffvelrn 6397 . . . . . . . . . . . 12 ((𝐺:ℕ0⟶(ℝ × ℝ) ∧ 𝑛 ∈ ℕ0) → (𝐺𝑛) ∈ (ℝ × ℝ))
7120, 56, 70syl2an 493 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ (ℝ × ℝ))
72 xp1st 7242 . . . . . . . . . . 11 ((𝐺𝑛) ∈ (ℝ × ℝ) → (1st ‘(𝐺𝑛)) ∈ ℝ)
7371, 72syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) ∈ ℝ)
7417adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 𝑆 ∈ ℝ)
75 ltletr 10167 . . . . . . . . . 10 (((𝐹𝑛) ∈ ℝ ∧ (1st ‘(𝐺𝑛)) ∈ ℝ ∧ 𝑆 ∈ ℝ) → (((𝐹𝑛) < (1st ‘(𝐺𝑛)) ∧ (1st ‘(𝐺𝑛)) ≤ 𝑆) → (𝐹𝑛) < 𝑆))
7628, 73, 74, 75syl3anc 1366 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((𝐹𝑛) < (1st ‘(𝐺𝑛)) ∧ (1st ‘(𝐺𝑛)) ≤ 𝑆) → (𝐹𝑛) < 𝑆))
7769, 76mpan2d 710 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((𝐹𝑛) < (1st ‘(𝐺𝑛)) → (𝐹𝑛) < 𝑆))
78 fvco3 6314 . . . . . . . . . . . . . . 15 ((𝐺:ℕ0⟶(ℝ × ℝ) ∧ 𝑘 ∈ ℕ0) → ((1st𝐺)‘𝑘) = (1st ‘(𝐺𝑘)))
7959, 78sylan 487 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → ((1st𝐺)‘𝑘) = (1st ‘(𝐺𝑘)))
8059ffvelrnda 6399 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ (ℝ × ℝ))
81 xp1st 7242 . . . . . . . . . . . . . . . 16 ((𝐺𝑘) ∈ (ℝ × ℝ) → (1st ‘(𝐺𝑘)) ∈ ℝ)
8280, 81syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (1st ‘(𝐺𝑘)) ∈ ℝ)
83 xp2nd 7243 . . . . . . . . . . . . . . . . 17 ((𝐺𝑛) ∈ (ℝ × ℝ) → (2nd ‘(𝐺𝑛)) ∈ ℝ)
8471, 83syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) ∈ ℝ)
8584adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (2nd ‘(𝐺𝑛)) ∈ ℝ)
8618adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → 𝐹:ℕ⟶ℝ)
8719adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ (((1st𝑥) + (2nd𝑥)) / 2) / 𝑚if(𝑚 < 𝑦, ⟨(1st𝑥), 𝑚⟩, ⟨((𝑚 + (2nd𝑥)) / 2), (2nd𝑥)⟩)))
88 simpr 476 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
8963adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → 𝑛 ∈ ℕ0)
9086, 87, 4, 5, 88, 89ruclem10 15012 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (1st ‘(𝐺𝑘)) < (2nd ‘(𝐺𝑛)))
9182, 85, 90ltled 10223 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (1st ‘(𝐺𝑘)) ≤ (2nd ‘(𝐺𝑛)))
9279, 91eqbrtrd 4707 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → ((1st𝐺)‘𝑘) ≤ (2nd ‘(𝐺𝑛)))
9392ralrimiva 2995 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ∀𝑘 ∈ ℕ0 ((1st𝐺)‘𝑘) ≤ (2nd ‘(𝐺𝑛)))
94 breq1 4688 . . . . . . . . . . . . . 14 (𝑧 = ((1st𝐺)‘𝑘) → (𝑧 ≤ (2nd ‘(𝐺𝑛)) ↔ ((1st𝐺)‘𝑘) ≤ (2nd ‘(𝐺𝑛))))
9594ralrn 6402 . . . . . . . . . . . . 13 ((1st𝐺) Fn ℕ0 → (∀𝑧 ∈ ran (1st𝐺)𝑧 ≤ (2nd ‘(𝐺𝑛)) ↔ ∀𝑘 ∈ ℕ0 ((1st𝐺)‘𝑘) ≤ (2nd ‘(𝐺𝑛))))
9662, 95syl 17 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (∀𝑧 ∈ ran (1st𝐺)𝑧 ≤ (2nd ‘(𝐺𝑛)) ↔ ∀𝑘 ∈ ℕ0 ((1st𝐺)‘𝑘) ≤ (2nd ‘(𝐺𝑛))))
9793, 96mpbird 247 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ∀𝑧 ∈ ran (1st𝐺)𝑧 ≤ (2nd ‘(𝐺𝑛)))
98 suprleub 11027 . . . . . . . . . . . 12 (((ran (1st𝐺) ⊆ ℝ ∧ ran (1st𝐺) ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ran (1st𝐺)𝑧𝑛) ∧ (2nd ‘(𝐺𝑛)) ∈ ℝ) → (sup(ran (1st𝐺), ℝ, < ) ≤ (2nd ‘(𝐺𝑛)) ↔ ∀𝑧 ∈ ran (1st𝐺)𝑧 ≤ (2nd ‘(𝐺𝑛))))
9953, 54, 55, 84, 98syl31anc 1369 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (sup(ran (1st𝐺), ℝ, < ) ≤ (2nd ‘(𝐺𝑛)) ↔ ∀𝑧 ∈ ran (1st𝐺)𝑧 ≤ (2nd ‘(𝐺𝑛))))
10097, 99mpbird 247 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → sup(ran (1st𝐺), ℝ, < ) ≤ (2nd ‘(𝐺𝑛)))
1011, 100syl5eqbr 4720 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑆 ≤ (2nd ‘(𝐺𝑛)))
102 lelttr 10166 . . . . . . . . . 10 ((𝑆 ∈ ℝ ∧ (2nd ‘(𝐺𝑛)) ∈ ℝ ∧ (𝐹𝑛) ∈ ℝ) → ((𝑆 ≤ (2nd ‘(𝐺𝑛)) ∧ (2nd ‘(𝐺𝑛)) < (𝐹𝑛)) → 𝑆 < (𝐹𝑛)))
10374, 84, 28, 102syl3anc 1366 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((𝑆 ≤ (2nd ‘(𝐺𝑛)) ∧ (2nd ‘(𝐺𝑛)) < (𝐹𝑛)) → 𝑆 < (𝐹𝑛)))
104101, 103mpand 711 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((2nd ‘(𝐺𝑛)) < (𝐹𝑛) → 𝑆 < (𝐹𝑛)))
10577, 104orim12d 901 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (((𝐹𝑛) < (1st ‘(𝐺𝑛)) ∨ (2nd ‘(𝐺𝑛)) < (𝐹𝑛)) → ((𝐹𝑛) < 𝑆𝑆 < (𝐹𝑛))))
10652, 105mpd 15 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝐹𝑛) < 𝑆𝑆 < (𝐹𝑛)))
10728, 74lttri2d 10214 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝐹𝑛) ≠ 𝑆 ↔ ((𝐹𝑛) < 𝑆𝑆 < (𝐹𝑛))))
108106, 107mpbird 247 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ≠ 𝑆)
109108neneqd 2828 . . . 4 ((𝜑𝑛 ∈ ℕ) → ¬ (𝐹𝑛) = 𝑆)
110109nrexdv 3030 . . 3 (𝜑 → ¬ ∃𝑛 ∈ ℕ (𝐹𝑛) = 𝑆)
111 risset 3091 . . . 4 (𝑆 ∈ ran 𝐹 ↔ ∃𝑧 ∈ ran 𝐹 𝑧 = 𝑆)
112 ffn 6083 . . . . 5 (𝐹:ℕ⟶ℝ → 𝐹 Fn ℕ)
113 eqeq1 2655 . . . . . 6 (𝑧 = (𝐹𝑛) → (𝑧 = 𝑆 ↔ (𝐹𝑛) = 𝑆))
114113rexrn 6401 . . . . 5 (𝐹 Fn ℕ → (∃𝑧 ∈ ran 𝐹 𝑧 = 𝑆 ↔ ∃𝑛 ∈ ℕ (𝐹𝑛) = 𝑆))
1152, 112, 1143syl 18 . . . 4 (𝜑 → (∃𝑧 ∈ ran 𝐹 𝑧 = 𝑆 ↔ ∃𝑛 ∈ ℕ (𝐹𝑛) = 𝑆))
116111, 115syl5bb 272 . . 3 (𝜑 → (𝑆 ∈ ran 𝐹 ↔ ∃𝑛 ∈ ℕ (𝐹𝑛) = 𝑆))
117110, 116mtbird 314 . 2 (𝜑 → ¬ 𝑆 ∈ ran 𝐹)
11817, 117eldifd 3618 1 (𝜑𝑆 ∈ (ℝ ∖ ran 𝐹))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  ⦋csb 3566   ∖ cdif 3604   ∪ cun 3605   ⊆ wss 3607  ∅c0 3948  ifcif 4119  {csn 4210  ⟨cop 4216   class class class wbr 4685   × cxp 5141  ran crn 5144   ∘ ccom 5147   Fn wfn 5921  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ↦ cmpt2 6692  1st c1st 7208  2nd c2nd 7209  supcsup 8387  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   < clt 10112   ≤ cle 10113   − cmin 10304   / cdiv 10722  ℕcn 11058  2c2 11108  ℕ0cn0 11330  seqcseq 12841 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-sup 8389  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-seq 12842 This theorem is referenced by:  ruclem13  15015
 Copyright terms: Public domain W3C validator