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

Theorem ivthlem2 24045
 Description: Lemma for ivth 24047. Show that the supremum of 𝑆 cannot be less than 𝑈. If it was, continuity of 𝐹 implies that there are points just above the supremum that are also less than 𝑈, a contradiction. (Contributed by Mario Carneiro, 17-Jun-2014.)
Hypotheses
Ref Expression
ivth.1 (𝜑𝐴 ∈ ℝ)
ivth.2 (𝜑𝐵 ∈ ℝ)
ivth.3 (𝜑𝑈 ∈ ℝ)
ivth.4 (𝜑𝐴 < 𝐵)
ivth.5 (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
ivth.7 (𝜑𝐹 ∈ (𝐷cn→ℂ))
ivth.8 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)
ivth.9 (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))
ivth.10 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑥) ≤ 𝑈}
ivth.11 𝐶 = sup(𝑆, ℝ, < )
Assertion
Ref Expression
ivthlem2 (𝜑 → ¬ (𝐹𝐶) < 𝑈)
Distinct variable groups:   𝑥,𝐵   𝑥,𝐷   𝑥,𝐹   𝜑,𝑥   𝑥,𝐴   𝑥,𝐶   𝑥,𝑆   𝑥,𝑈

Proof of Theorem ivthlem2
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ivth.7 . . . . 5 (𝜑𝐹 ∈ (𝐷cn→ℂ))
21adantr 483 . . . 4 ((𝜑 ∧ (𝐹𝐶) < 𝑈) → 𝐹 ∈ (𝐷cn→ℂ))
3 ivth.5 . . . . . 6 (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
4 ivth.11 . . . . . . . 8 𝐶 = sup(𝑆, ℝ, < )
5 ivth.10 . . . . . . . . . . 11 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑥) ≤ 𝑈}
65ssrab3 4055 . . . . . . . . . 10 𝑆 ⊆ (𝐴[,]𝐵)
7 ivth.1 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
8 ivth.2 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℝ)
9 iccssre 12810 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
107, 8, 9syl2anc 586 . . . . . . . . . 10 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
116, 10sstrid 3976 . . . . . . . . 9 (𝜑𝑆 ⊆ ℝ)
12 ivth.3 . . . . . . . . . . . 12 (𝜑𝑈 ∈ ℝ)
13 ivth.4 . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
14 ivth.8 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)
15 ivth.9 . . . . . . . . . . . 12 (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))
167, 8, 12, 13, 3, 1, 14, 15, 5ivthlem1 24044 . . . . . . . . . . 11 (𝜑 → (𝐴𝑆 ∧ ∀𝑧𝑆 𝑧𝐵))
1716simpld 497 . . . . . . . . . 10 (𝜑𝐴𝑆)
1817ne0d 4299 . . . . . . . . 9 (𝜑𝑆 ≠ ∅)
1916simprd 498 . . . . . . . . . 10 (𝜑 → ∀𝑧𝑆 𝑧𝐵)
20 brralrspcev 5117 . . . . . . . . . 10 ((𝐵 ∈ ℝ ∧ ∀𝑧𝑆 𝑧𝐵) → ∃𝑥 ∈ ℝ ∀𝑧𝑆 𝑧𝑥)
218, 19, 20syl2anc 586 . . . . . . . . 9 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧𝑆 𝑧𝑥)
2211, 18, 21suprcld 11596 . . . . . . . 8 (𝜑 → sup(𝑆, ℝ, < ) ∈ ℝ)
234, 22eqeltrid 2915 . . . . . . 7 (𝜑𝐶 ∈ ℝ)
2411, 18, 21, 17suprubd 11595 . . . . . . . 8 (𝜑𝐴 ≤ sup(𝑆, ℝ, < ))
2524, 4breqtrrdi 5099 . . . . . . 7 (𝜑𝐴𝐶)
2611, 18, 213jca 1123 . . . . . . . . . 10 (𝜑 → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧𝑆 𝑧𝑥))
27 suprleub 11599 . . . . . . . . . 10 (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧𝑆 𝑧𝑥) ∧ 𝐵 ∈ ℝ) → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧𝑆 𝑧𝐵))
2826, 8, 27syl2anc 586 . . . . . . . . 9 (𝜑 → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧𝑆 𝑧𝐵))
2919, 28mpbird 259 . . . . . . . 8 (𝜑 → sup(𝑆, ℝ, < ) ≤ 𝐵)
304, 29eqbrtrid 5092 . . . . . . 7 (𝜑𝐶𝐵)
31 elicc2 12793 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵)))
327, 8, 31syl2anc 586 . . . . . . 7 (𝜑 → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵)))
3323, 25, 30, 32mpbir3and 1337 . . . . . 6 (𝜑𝐶 ∈ (𝐴[,]𝐵))
343, 33sseldd 3966 . . . . 5 (𝜑𝐶𝐷)
3534adantr 483 . . . 4 ((𝜑 ∧ (𝐹𝐶) < 𝑈) → 𝐶𝐷)
36 fveq2 6663 . . . . . . . 8 (𝑥 = 𝐶 → (𝐹𝑥) = (𝐹𝐶))
3736eleq1d 2895 . . . . . . 7 (𝑥 = 𝐶 → ((𝐹𝑥) ∈ ℝ ↔ (𝐹𝐶) ∈ ℝ))
3814ralrimiva 3180 . . . . . . 7 (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹𝑥) ∈ ℝ)
3937, 38, 33rspcdva 3623 . . . . . 6 (𝜑 → (𝐹𝐶) ∈ ℝ)
40 difrp 12419 . . . . . 6 (((𝐹𝐶) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹𝐶) < 𝑈 ↔ (𝑈 − (𝐹𝐶)) ∈ ℝ+))
4139, 12, 40syl2anc 586 . . . . 5 (𝜑 → ((𝐹𝐶) < 𝑈 ↔ (𝑈 − (𝐹𝐶)) ∈ ℝ+))
4241biimpa 479 . . . 4 ((𝜑 ∧ (𝐹𝐶) < 𝑈) → (𝑈 − (𝐹𝐶)) ∈ ℝ+)
43 cncfi 23494 . . . 4 ((𝐹 ∈ (𝐷cn→ℂ) ∧ 𝐶𝐷 ∧ (𝑈 − (𝐹𝐶)) ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑦𝐷 ((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))))
442, 35, 42, 43syl3anc 1366 . . 3 ((𝜑 ∧ (𝐹𝐶) < 𝑈) → ∃𝑧 ∈ ℝ+𝑦𝐷 ((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))))
45 ssralv 4031 . . . . . . 7 ((𝐴[,]𝐵) ⊆ 𝐷 → (∀𝑦𝐷 ((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶)))))
463, 45syl 17 . . . . . 6 (𝜑 → (∀𝑦𝐷 ((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶)))))
4746ad2antrr 724 . . . . 5 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (∀𝑦𝐷 ((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶)))))
488ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐵 ∈ ℝ)
4923ad2antrr 724 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐶 ∈ ℝ)
50 rphalfcl 12408 . . . . . . . . . . . 12 (𝑧 ∈ ℝ+ → (𝑧 / 2) ∈ ℝ+)
5150adantl 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (𝑧 / 2) ∈ ℝ+)
5251rpred 12423 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (𝑧 / 2) ∈ ℝ)
5349, 52readdcld 10662 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (𝐶 + (𝑧 / 2)) ∈ ℝ)
5448, 53ifcld 4510 . . . . . . . 8 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ)
557ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐴 ∈ ℝ)
5625ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐴𝐶)
5715simprd 498 . . . . . . . . . . . . . . 15 (𝜑𝑈 < (𝐹𝐵))
58 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
5958eleq1d 2895 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐵 → ((𝐹𝑥) ∈ ℝ ↔ (𝐹𝐵) ∈ ℝ))
607rexrd 10683 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ ℝ*)
618rexrd 10683 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ ℝ*)
627, 8, 13ltled 10780 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴𝐵)
63 ubicc2 12845 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
6460, 61, 62, 63syl3anc 1366 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ (𝐴[,]𝐵))
6559, 38, 64rspcdva 3623 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹𝐵) ∈ ℝ)
66 lttr 10709 . . . . . . . . . . . . . . . 16 (((𝐹𝐶) ∈ ℝ ∧ 𝑈 ∈ ℝ ∧ (𝐹𝐵) ∈ ℝ) → (((𝐹𝐶) < 𝑈𝑈 < (𝐹𝐵)) → (𝐹𝐶) < (𝐹𝐵)))
6739, 12, 65, 66syl3anc 1366 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐹𝐶) < 𝑈𝑈 < (𝐹𝐵)) → (𝐹𝐶) < (𝐹𝐵)))
6857, 67mpan2d 692 . . . . . . . . . . . . . 14 (𝜑 → ((𝐹𝐶) < 𝑈 → (𝐹𝐶) < (𝐹𝐵)))
6968imp 409 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐹𝐶) < 𝑈) → (𝐹𝐶) < (𝐹𝐵))
7069adantr 483 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (𝐹𝐶) < (𝐹𝐵))
7139ltnrd 10766 . . . . . . . . . . . . . . . . 17 (𝜑 → ¬ (𝐹𝐶) < (𝐹𝐶))
72 fveq2 6663 . . . . . . . . . . . . . . . . . . 19 (𝐵 = 𝐶 → (𝐹𝐵) = (𝐹𝐶))
7372breq2d 5069 . . . . . . . . . . . . . . . . . 18 (𝐵 = 𝐶 → ((𝐹𝐶) < (𝐹𝐵) ↔ (𝐹𝐶) < (𝐹𝐶)))
7473notbid 320 . . . . . . . . . . . . . . . . 17 (𝐵 = 𝐶 → (¬ (𝐹𝐶) < (𝐹𝐵) ↔ ¬ (𝐹𝐶) < (𝐹𝐶)))
7571, 74syl5ibrcom 249 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 = 𝐶 → ¬ (𝐹𝐶) < (𝐹𝐵)))
7675necon2ad 3029 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐹𝐶) < (𝐹𝐵) → 𝐵𝐶))
7776, 30jctild 528 . . . . . . . . . . . . . 14 (𝜑 → ((𝐹𝐶) < (𝐹𝐵) → (𝐶𝐵𝐵𝐶)))
7823, 8ltlend 10777 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 < 𝐵 ↔ (𝐶𝐵𝐵𝐶)))
7977, 78sylibrd 261 . . . . . . . . . . . . 13 (𝜑 → ((𝐹𝐶) < (𝐹𝐵) → 𝐶 < 𝐵))
8079ad2antrr 724 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → ((𝐹𝐶) < (𝐹𝐵) → 𝐶 < 𝐵))
8170, 80mpd 15 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐶 < 𝐵)
8249, 51ltaddrpd 12456 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐶 < (𝐶 + (𝑧 / 2)))
83 breq2 5061 . . . . . . . . . . . 12 (𝐵 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < 𝐵𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))))
84 breq2 5061 . . . . . . . . . . . 12 ((𝐶 + (𝑧 / 2)) = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < (𝐶 + (𝑧 / 2)) ↔ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))))
8583, 84ifboth 4503 . . . . . . . . . . 11 ((𝐶 < 𝐵𝐶 < (𝐶 + (𝑧 / 2))) → 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
8681, 82, 85syl2anc 586 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
8749, 54, 86ltled 10780 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐶 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
8855, 49, 54, 56, 87letrd 10789 . . . . . . . 8 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
89 min1 12574 . . . . . . . . 9 ((𝐵 ∈ ℝ ∧ (𝐶 + (𝑧 / 2)) ∈ ℝ) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)
9048, 53, 89syl2anc 586 . . . . . . . 8 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)
91 elicc2 12793 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)))
927, 8, 91syl2anc 586 . . . . . . . . 9 (𝜑 → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)))
9392ad2antrr 724 . . . . . . . 8 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)))
9454, 88, 90, 93mpbir3and 1337 . . . . . . 7 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵))
9549, 54, 87abssubge0d 14783 . . . . . . . 8 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) = (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶))
96 rpre 12389 . . . . . . . . . . . 12 (𝑧 ∈ ℝ+𝑧 ∈ ℝ)
9796adantl 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝑧 ∈ ℝ)
9849, 97readdcld 10662 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (𝐶 + 𝑧) ∈ ℝ)
99 min2 12575 . . . . . . . . . . 11 ((𝐵 ∈ ℝ ∧ (𝐶 + (𝑧 / 2)) ∈ ℝ) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ (𝐶 + (𝑧 / 2)))
10048, 53, 99syl2anc 586 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ (𝐶 + (𝑧 / 2)))
101 rphalflt 12410 . . . . . . . . . . . 12 (𝑧 ∈ ℝ+ → (𝑧 / 2) < 𝑧)
102101adantl 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (𝑧 / 2) < 𝑧)
10352, 97, 49, 102ltadd2dd 10791 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (𝐶 + (𝑧 / 2)) < (𝐶 + 𝑧))
10454, 53, 98, 100, 103lelttrd 10790 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) < (𝐶 + 𝑧))
10554, 49, 97ltsubadd2d 11230 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → ((if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶) < 𝑧 ↔ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) < (𝐶 + 𝑧)))
106104, 105mpbird 259 . . . . . . . 8 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶) < 𝑧)
10795, 106eqbrtrd 5079 . . . . . . 7 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧)
108 fvoveq1 7171 . . . . . . . . . 10 (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (abs‘(𝑦𝐶)) = (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)))
109108breq1d 5067 . . . . . . . . 9 (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → ((abs‘(𝑦𝐶)) < 𝑧 ↔ (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧))
110 breq2 5061 . . . . . . . . 9 (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < 𝑦𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))))
111109, 110anbi12d 632 . . . . . . . 8 (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (((abs‘(𝑦𝐶)) < 𝑧𝐶 < 𝑦) ↔ ((abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))))
112111rspcev 3621 . . . . . . 7 ((if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ∧ ((abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦𝐶)) < 𝑧𝐶 < 𝑦))
11394, 107, 86, 112syl12anc 834 . . . . . 6 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦𝐶)) < 𝑧𝐶 < 𝑦))
114 r19.29 3252 . . . . . . 7 ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦𝐶)) < 𝑧𝐶 < 𝑦)) → ∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))) ∧ ((abs‘(𝑦𝐶)) < 𝑧𝐶 < 𝑦)))
115 pm3.45 623 . . . . . . . . . 10 (((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))) → (((abs‘(𝑦𝐶)) < 𝑧𝐶 < 𝑦) → ((abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶)) ∧ 𝐶 < 𝑦)))
116115imp 409 . . . . . . . . 9 ((((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))) ∧ ((abs‘(𝑦𝐶)) < 𝑧𝐶 < 𝑦)) → ((abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶)) ∧ 𝐶 < 𝑦))
117 simprr 771 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝐶 < 𝑦)
118 fveq2 6663 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
119118eleq1d 2895 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((𝐹𝑥) ∈ ℝ ↔ (𝐹𝑦) ∈ ℝ))
120 simplll 773 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝜑)
121120, 38syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹𝑥) ∈ ℝ)
122 simprl 769 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑦 ∈ (𝐴[,]𝐵))
123119, 121, 122rspcdva 3623 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹𝑦) ∈ ℝ)
124120, 39syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹𝐶) ∈ ℝ)
125120, 12syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑈 ∈ ℝ)
126125, 124resubcld 11060 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑈 − (𝐹𝐶)) ∈ ℝ)
127123, 124, 126absdifltd 14785 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶)) ↔ (((𝐹𝐶) − (𝑈 − (𝐹𝐶))) < (𝐹𝑦) ∧ (𝐹𝑦) < ((𝐹𝐶) + (𝑈 − (𝐹𝐶))))))
128 ltle 10721 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑦) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹𝑦) < 𝑈 → (𝐹𝑦) ≤ 𝑈))
129123, 125, 128syl2anc 586 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹𝑦) < 𝑈 → (𝐹𝑦) ≤ 𝑈))
130124recnd 10661 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹𝐶) ∈ ℂ)
131125recnd 10661 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑈 ∈ ℂ)
132130, 131pncan3d 10992 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹𝐶) + (𝑈 − (𝐹𝐶))) = 𝑈)
133132breq2d 5069 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹𝑦) < ((𝐹𝐶) + (𝑈 − (𝐹𝐶))) ↔ (𝐹𝑦) < 𝑈))
134118breq1d 5067 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → ((𝐹𝑥) ≤ 𝑈 ↔ (𝐹𝑦) ≤ 𝑈))
135134, 5elrab2 3681 . . . . . . . . . . . . . . . . . . 19 (𝑦𝑆 ↔ (𝑦 ∈ (𝐴[,]𝐵) ∧ (𝐹𝑦) ≤ 𝑈))
136135baib 538 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (𝐴[,]𝐵) → (𝑦𝑆 ↔ (𝐹𝑦) ≤ 𝑈))
137136ad2antrl 726 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦𝑆 ↔ (𝐹𝑦) ≤ 𝑈))
138129, 133, 1373imtr4d 296 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹𝑦) < ((𝐹𝐶) + (𝑈 − (𝐹𝐶))) → 𝑦𝑆))
139 suprub 11594 . . . . . . . . . . . . . . . . . . . 20 (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧𝑆 𝑧𝑥) ∧ 𝑦𝑆) → 𝑦 ≤ sup(𝑆, ℝ, < ))
140139, 4breqtrrdi 5099 . . . . . . . . . . . . . . . . . . 19 (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧𝑆 𝑧𝑥) ∧ 𝑦𝑆) → 𝑦𝐶)
141140ex 415 . . . . . . . . . . . . . . . . . 18 ((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧𝑆 𝑧𝑥) → (𝑦𝑆𝑦𝐶))
142120, 26, 1413syl 18 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦𝑆𝑦𝐶))
143120, 10syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐴[,]𝐵) ⊆ ℝ)
144143, 122sseldd 3966 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑦 ∈ ℝ)
145120, 23syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝐶 ∈ ℝ)
146144, 145lenltd 10778 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦𝐶 ↔ ¬ 𝐶 < 𝑦))
147142, 146sylibd 241 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦𝑆 → ¬ 𝐶 < 𝑦))
148138, 147syld 47 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹𝑦) < ((𝐹𝐶) + (𝑈 − (𝐹𝐶))) → ¬ 𝐶 < 𝑦))
149148adantld 493 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((((𝐹𝐶) − (𝑈 − (𝐹𝐶))) < (𝐹𝑦) ∧ (𝐹𝑦) < ((𝐹𝐶) + (𝑈 − (𝐹𝐶)))) → ¬ 𝐶 < 𝑦))
150127, 149sylbid 242 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶)) → ¬ 𝐶 < 𝑦))
151117, 150mt2d 138 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ¬ (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶)))
152151pm2.21d 121 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶)) → ¬ (𝐹𝐶) < 𝑈))
153152expr 459 . . . . . . . . . 10 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐶 < 𝑦 → ((abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶)) → ¬ (𝐹𝐶) < 𝑈)))
154153impcomd 414 . . . . . . . . 9 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶)) ∧ 𝐶 < 𝑦) → ¬ (𝐹𝐶) < 𝑈))
155116, 154syl5 34 . . . . . . . 8 ((((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))) ∧ ((abs‘(𝑦𝐶)) < 𝑧𝐶 < 𝑦)) → ¬ (𝐹𝐶) < 𝑈))
156155rexlimdva 3282 . . . . . . 7 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))) ∧ ((abs‘(𝑦𝐶)) < 𝑧𝐶 < 𝑦)) → ¬ (𝐹𝐶) < 𝑈))
157114, 156syl5 34 . . . . . 6 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦𝐶)) < 𝑧𝐶 < 𝑦)) → ¬ (𝐹𝐶) < 𝑈))
158113, 157mpan2d 692 . . . . 5 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))) → ¬ (𝐹𝐶) < 𝑈))
15947, 158syld 47 . . . 4 (((𝜑 ∧ (𝐹𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (∀𝑦𝐷 ((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))) → ¬ (𝐹𝐶) < 𝑈))
160159rexlimdva 3282 . . 3 ((𝜑 ∧ (𝐹𝐶) < 𝑈) → (∃𝑧 ∈ ℝ+𝑦𝐷 ((abs‘(𝑦𝐶)) < 𝑧 → (abs‘((𝐹𝑦) − (𝐹𝐶))) < (𝑈 − (𝐹𝐶))) → ¬ (𝐹𝐶) < 𝑈))
16144, 160mpd 15 . 2 ((𝜑 ∧ (𝐹𝐶) < 𝑈) → ¬ (𝐹𝐶) < 𝑈)
162161pm2.01da 797 1 (𝜑 → ¬ (𝐹𝐶) < 𝑈)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1082   = wceq 1531   ∈ wcel 2108   ≠ wne 3014  ∀wral 3136  ∃wrex 3137  {crab 3140   ⊆ wss 3934  ∅c0 4289  ifcif 4465   class class class wbr 5057  ‘cfv 6348  (class class class)co 7148  supcsup 8896  ℂcc 10527  ℝcr 10528   + caddc 10532  ℝ*cxr 10666   < clt 10667   ≤ cle 10668   − cmin 10862   / cdiv 11289  2c2 11684  ℝ+crp 12381  [,]cicc 12733  abscabs 14585  –cn→ccncf 23476 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-er 8281  df-map 8400  df-en 8502  df-dom 8503  df-sdom 8504  df-sup 8898  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-n0 11890  df-z 11974  df-uz 12236  df-rp 12382  df-icc 12737  df-seq 13362  df-exp 13422  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-cncf 23478 This theorem is referenced by:  ivthlem3  24046
 Copyright terms: Public domain W3C validator