dedekindicclemlu - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > dedekindicclemlu		GIF version

Theorem dedekindicclemlu 15424

Description: Lemma for dedekindicc 15427. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.)

**Hypotheses**
Ref	Expression
dedekindicc.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
dedekindicc.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
dedekindicc.lss	⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))
dedekindicc.uss	⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))
dedekindicc.lm	⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)
dedekindicc.um	⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)
dedekindicc.lr	⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
dedekindicc.ur	⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
dedekindicc.disj	⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)
dedekindicc.loc	⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))
dedekindicc.ab	⊢ (𝜑 → 𝐴 < 𝐵)

**Assertion**
Ref	Expression
dedekindicclemlu	⊢ (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))

Distinct variable groups: 𝐴,𝑞,𝑟,𝑥 𝐵,𝑞,𝑟,𝑥 𝐿,𝑞,𝑟,𝑥 𝑈,𝑞,𝑟 𝜑,𝑞,𝑟,𝑥 Allowed substitution hint: 𝑈(𝑥)

Proof of Theorem dedekindicclemlu Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dedekindicc.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		dedekindicc.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		dedekindicc.lss	. . 3 ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))
4		dedekindicc.uss	. . 3 ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))
5		dedekindicc.lm	. . 3 ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)
6		dedekindicc.um	. . 3 ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)
7		dedekindicc.lr	. . 3 ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
8		dedekindicc.ur	. . 3 ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
9		dedekindicc.disj	. . 3 ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)
10		dedekindicc.loc	. . 3 ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))
11		dedekindicc.ab	. . 3 ⊢ (𝜑 → 𝐴 < 𝐵)
12	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11	dedekindicclemlub 15423	. 2 ⊢ (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)))
13		simpr 110	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝑞 ∈ 𝐿)
14	3	ad3antrrr 492	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝐿 ⊆ (𝐴[,]𝐵))
15	14, 13	sseldd 3229	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝑞 ∈ (𝐴[,]𝐵))
16		rsp 2580	. . . . . . . . . . 11 ⊢ (∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟) → (𝑞 ∈ (𝐴[,]𝐵) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)))
17	7, 16	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (𝑞 ∈ (𝐴[,]𝐵) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)))
18	17	ad3antrrr 492	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → (𝑞 ∈ (𝐴[,]𝐵) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)))
19	15, 18	mpd 13	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
20	13, 19	mpbid 147	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)
21		iccssre 10234	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
22	1, 2, 21	syl2anc 411	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
23	22	ad4antr 494	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → (𝐴[,]𝐵) ⊆ ℝ)
24	15	adantr 276	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ (𝐴[,]𝐵))
25	23, 24	sseldd 3229	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ ℝ)
26	3	ad4antr 494	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝐿 ⊆ (𝐴[,]𝐵))
27		simprl 531	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ 𝐿)
28	26, 27	sseldd 3229	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ (𝐴[,]𝐵))
29	23, 28	sseldd 3229	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ ℝ)
30		simp-4r 544	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑥 ∈ (𝐴[,]𝐵))
31	23, 30	sseldd 3229	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑥 ∈ ℝ)
32		simprr 533	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 < 𝑟)
33		breq2 4097	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (𝑥 < 𝑦 ↔ 𝑥 < 𝑟))
34	33	notbid 673	. . . . . . . . . 10 ⊢ (𝑦 = 𝑟 → (¬ 𝑥 < 𝑦 ↔ ¬ 𝑥 < 𝑟))
35		simprl 531	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦)
36	35	ad2antrr 488	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → ∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦)
37	34, 36, 27	rspcdva 2916	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → ¬ 𝑥 < 𝑟)
38	29, 31, 37	nltled 8342	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ≤ 𝑥)
39	25, 29, 31, 32, 38	ltletrd 8645	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 < 𝑥)
40	20, 39	rexlimddv 2656	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝑞 < 𝑥)
41	40	ralrimiva 2606	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑞 ∈ 𝐿 𝑞 < 𝑥)
42		simpr 110	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑟 ∈ 𝑈)
43		simplll 535	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝜑)
44	4	ad3antrrr 492	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑈 ⊆ (𝐴[,]𝐵))
45	44, 42	sseldd 3229	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑟 ∈ (𝐴[,]𝐵))
46		rsp 2580	. . . . . . . . . 10 ⊢ (∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟) → (𝑟 ∈ (𝐴[,]𝐵) → (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟)))
47	8, 46	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝑟 ∈ (𝐴[,]𝐵) → (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟)))
48	43, 45, 47	sylc 62	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
49	42, 48	mpbid 147	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → ∃𝑞 ∈ 𝑈 𝑞 < 𝑟)
50	22	ad4antr 494	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → (𝐴[,]𝐵) ⊆ ℝ)
51		simp-4r 544	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 ∈ (𝐴[,]𝐵))
52	50, 51	sseldd 3229	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 ∈ ℝ)
53	4	ad4antr 494	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑈 ⊆ (𝐴[,]𝐵))
54		simprl 531	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ 𝑈)
55	53, 54	sseldd 3229	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ (𝐴[,]𝐵))
56	50, 55	sseldd 3229	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ ℝ)
57	45	adantr 276	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ (𝐴[,]𝐵))
58	50, 57	sseldd 3229	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ ℝ)
59	54	adantr 276	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ 𝑈)
60	43	ad2antrr 488	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝜑)
61		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 < 𝑥)
62		breq1 4096	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑞 → (𝑦 < 𝑥 ↔ 𝑞 < 𝑥))
63		breq1 4096	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑞 → (𝑦 < 𝑧 ↔ 𝑞 < 𝑧))
64	63	rexbidv 2534	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑞 → (∃𝑧 ∈ 𝐿 𝑦 < 𝑧 ↔ ∃𝑧 ∈ 𝐿 𝑞 < 𝑧))
65	62, 64	imbi12d 234	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑞 → ((𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧) ↔ (𝑞 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑞 < 𝑧)))
66		simprr 533	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))
67	66	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))
68	55	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ (𝐴[,]𝐵))
69	65, 67, 68	rspcdva 2916	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → (𝑞 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑞 < 𝑧))
70	61, 69	mpd 13	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∃𝑧 ∈ 𝐿 𝑞 < 𝑧)
71		breq2 4097	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑟 → (𝑞 < 𝑧 ↔ 𝑞 < 𝑟))
72	71	cbvrexv 2769	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ 𝐿 𝑞 < 𝑧 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)
73	70, 72	sylib 122	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)
74	60, 68, 17	sylc 62	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
75	73, 74	mpbird 167	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ 𝐿)
76		disj 3545	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∩ 𝑈) = ∅ ↔ ∀𝑞 ∈ 𝐿 ¬ 𝑞 ∈ 𝑈)
77	9, 76	sylib 122	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑞 ∈ 𝐿 ¬ 𝑞 ∈ 𝑈)
78	77	r19.21bi 2621	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐿) → ¬ 𝑞 ∈ 𝑈)
79	60, 75, 78	syl2anc 411	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ¬ 𝑞 ∈ 𝑈)
80	59, 79	pm2.65da 667	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → ¬ 𝑞 < 𝑥)
81	52, 56, 80	nltled 8342	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 ≤ 𝑞)
82		simprr 533	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 < 𝑟)
83	52, 56, 58, 81, 82	lelttrd 8346	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 < 𝑟)
84	49, 83	rexlimddv 2656	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑥 < 𝑟)
85	84	ralrimiva 2606	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)
86	41, 85	jca 306	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))
87	86	ex 115	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)) → (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)))
88	87	reximdva 2635	. 2 ⊢ (𝜑 → (∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)) → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)))
89	12, 88	mpd 13	1 ⊢ (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 716 = wceq 1398 ∈ wcel 2202 ∀wral 2511 ∃wrex 2512 ∩ cin 3200 ⊆ wss 3201 ∅c0 3496 class class class wbr 4093 (class class class)co 6028 ℝcr 8074 < clt 8256 [,]cicc 10170

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4209 ax-sep 4212 ax-nul 4220 ax-pow 4270 ax-pr 4305 ax-un 4536 ax-setind 4641 ax-iinf 4692 ax-cnex 8166 ax-resscn 8167 ax-1cn 8168 ax-1re 8169 ax-icn 8170 ax-addcl 8171 ax-addrcl 8172 ax-mulcl 8173 ax-mulrcl 8174 ax-addcom 8175 ax-mulcom 8176 ax-addass 8177 ax-mulass 8178 ax-distr 8179 ax-i2m1 8180 ax-0lt1 8181 ax-1rid 8182 ax-0id 8183 ax-rnegex 8184 ax-precex 8185 ax-cnre 8186 ax-pre-ltirr 8187 ax-pre-ltwlin 8188 ax-pre-lttrn 8189 ax-pre-apti 8190 ax-pre-ltadd 8191 ax-pre-mulgt0 8192 ax-pre-mulext 8193 ax-arch 8194 ax-caucvg 8195 ax-pre-suploc 8196

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ne 2404 df-nel 2499 df-ral 2516 df-rex 2517 df-reu 2518 df-rmo 2519 df-rab 2520 df-v 2805 df-sbc 3033 df-csb 3129 df-dif 3203 df-un 3205 df-in 3207 df-ss 3214 df-nul 3497 df-if 3608 df-pw 3658 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-int 3934 df-iun 3977 df-br 4094 df-opab 4156 df-mpt 4157 df-tr 4193 df-id 4396 df-po 4399 df-iso 4400 df-iord 4469 df-on 4471 df-ilim 4472 df-suc 4474 df-iom 4695 df-xp 4737 df-rel 4738 df-cnv 4739 df-co 4740 df-dm 4741 df-rn 4742 df-res 4743 df-ima 4744 df-iota 5293 df-fun 5335 df-fn 5336 df-f 5337 df-f1 5338 df-fo 5339 df-f1o 5340 df-fv 5341 df-isom 5342 df-riota 5981 df-ov 6031 df-oprab 6032 df-mpo 6033 df-1st 6312 df-2nd 6313 df-recs 6514 df-frec 6600 df-sup 7226 df-inf 7227 df-pnf 8258 df-mnf 8259 df-xr 8260 df-ltxr 8261 df-le 8262 df-sub 8394 df-neg 8395 df-reap 8797 df-ap 8804 df-div 8895 df-inn 9186 df-2 9244 df-3 9245 df-4 9246 df-n0 9445 df-z 9524 df-uz 9800 df-rp 9933 df-icc 10174 df-seqfrec 10756 df-exp 10847 df-cj 11465 df-re 11466 df-im 11467 df-rsqrt 11621 df-abs 11622

This theorem is referenced by: dedekindicclemicc 15426

W3C validator