dedekindicclemlu - Intuitionistic Logic Explorer

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

Theorem dedekindicclemlu 13363

Description: Lemma for dedekindicc 13366. 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 13362	. 2 ⊢ (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)))
13		simpr 109	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝑞 ∈ 𝐿)
14	3	ad3antrrr 489	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝐿 ⊆ (𝐴[,]𝐵))
15	14, 13	sseldd 3148	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝑞 ∈ (𝐴[,]𝐵))
16		rsp 2517	. . . . . . . . . . 11 ⊢ (∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟) → (𝑞 ∈ (𝐴[,]𝐵) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)))
17	7, 16	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (𝑞 ∈ (𝐴[,]𝐵) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)))
18	17	ad3antrrr 489	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → (𝑞 ∈ (𝐴[,]𝐵) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)))
19	15, 18	mpd 13	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
20	13, 19	mpbid 146	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)
21		iccssre 9901	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
22	1, 2, 21	syl2anc 409	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
23	22	ad4antr 491	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → (𝐴[,]𝐵) ⊆ ℝ)
24	15	adantr 274	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ (𝐴[,]𝐵))
25	23, 24	sseldd 3148	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ ℝ)
26	3	ad4antr 491	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝐿 ⊆ (𝐴[,]𝐵))
27		simprl 526	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ 𝐿)
28	26, 27	sseldd 3148	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ (𝐴[,]𝐵))
29	23, 28	sseldd 3148	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ ℝ)
30		simp-4r 537	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑥 ∈ (𝐴[,]𝐵))
31	23, 30	sseldd 3148	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑥 ∈ ℝ)
32		simprr 527	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 < 𝑟)
33		breq2 3991	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (𝑥 < 𝑦 ↔ 𝑥 < 𝑟))
34	33	notbid 662	. . . . . . . . . 10 ⊢ (𝑦 = 𝑟 → (¬ 𝑥 < 𝑦 ↔ ¬ 𝑥 < 𝑟))
35		simprl 526	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦)
36	35	ad2antrr 485	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → ∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦)
37	34, 36, 27	rspcdva 2839	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → ¬ 𝑥 < 𝑟)
38	29, 31, 37	nltled 8029	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ≤ 𝑥)
39	25, 29, 31, 32, 38	ltletrd 8331	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 < 𝑥)
40	20, 39	rexlimddv 2592	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝑞 < 𝑥)
41	40	ralrimiva 2543	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑞 ∈ 𝐿 𝑞 < 𝑥)
42		simpr 109	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑟 ∈ 𝑈)
43		simplll 528	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝜑)
44	4	ad3antrrr 489	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑈 ⊆ (𝐴[,]𝐵))
45	44, 42	sseldd 3148	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑟 ∈ (𝐴[,]𝐵))
46		rsp 2517	. . . . . . . . . 10 ⊢ (∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟) → (𝑟 ∈ (𝐴[,]𝐵) → (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟)))
47	8, 46	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝑟 ∈ (𝐴[,]𝐵) → (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟)))
48	43, 45, 47	sylc 62	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
49	42, 48	mpbid 146	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → ∃𝑞 ∈ 𝑈 𝑞 < 𝑟)
50	22	ad4antr 491	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → (𝐴[,]𝐵) ⊆ ℝ)
51		simp-4r 537	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 ∈ (𝐴[,]𝐵))
52	50, 51	sseldd 3148	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 ∈ ℝ)
53	4	ad4antr 491	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑈 ⊆ (𝐴[,]𝐵))
54		simprl 526	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ 𝑈)
55	53, 54	sseldd 3148	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ (𝐴[,]𝐵))
56	50, 55	sseldd 3148	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ ℝ)
57	45	adantr 274	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ (𝐴[,]𝐵))
58	50, 57	sseldd 3148	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ ℝ)
59	54	adantr 274	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ 𝑈)
60	43	ad2antrr 485	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝜑)
61		simpr 109	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 < 𝑥)
62		breq1 3990	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑞 → (𝑦 < 𝑥 ↔ 𝑞 < 𝑥))
63		breq1 3990	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑞 → (𝑦 < 𝑧 ↔ 𝑞 < 𝑧))
64	63	rexbidv 2471	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑞 → (∃𝑧 ∈ 𝐿 𝑦 < 𝑧 ↔ ∃𝑧 ∈ 𝐿 𝑞 < 𝑧))
65	62, 64	imbi12d 233	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑞 → ((𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧) ↔ (𝑞 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑞 < 𝑧)))
66		simprr 527	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))
67	66	ad3antrrr 489	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))
68	55	adantr 274	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ (𝐴[,]𝐵))
69	65, 67, 68	rspcdva 2839	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → (𝑞 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑞 < 𝑧))
70	61, 69	mpd 13	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∃𝑧 ∈ 𝐿 𝑞 < 𝑧)
71		breq2 3991	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑟 → (𝑞 < 𝑧 ↔ 𝑞 < 𝑟))
72	71	cbvrexv 2697	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ 𝐿 𝑞 < 𝑧 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)
73	70, 72	sylib 121	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)
74	60, 68, 17	sylc 62	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
75	73, 74	mpbird 166	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ 𝐿)
76		disj 3462	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∩ 𝑈) = ∅ ↔ ∀𝑞 ∈ 𝐿 ¬ 𝑞 ∈ 𝑈)
77	9, 76	sylib 121	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑞 ∈ 𝐿 ¬ 𝑞 ∈ 𝑈)
78	77	r19.21bi 2558	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐿) → ¬ 𝑞 ∈ 𝑈)
79	60, 75, 78	syl2anc 409	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ¬ 𝑞 ∈ 𝑈)
80	59, 79	pm2.65da 656	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → ¬ 𝑞 < 𝑥)
81	52, 56, 80	nltled 8029	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 ≤ 𝑞)
82		simprr 527	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 < 𝑟)
83	52, 56, 58, 81, 82	lelttrd 8033	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 < 𝑟)
84	49, 83	rexlimddv 2592	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑥 < 𝑟)
85	84	ralrimiva 2543	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)
86	41, 85	jca 304	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))
87	86	ex 114	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)) → (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)))
88	87	reximdva 2572	. 2 ⊢ (𝜑 → (∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)) → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)))
89	12, 88	mpd 13	1 ⊢ (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 703 = wceq 1348 ∈ wcel 2141 ∀wral 2448 ∃wrex 2449 ∩ cin 3120 ⊆ wss 3121 ∅c0 3414 class class class wbr 3987 (class class class)co 5851 ℝcr 7762 < clt 7943 [,]cicc 9837

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4102 ax-sep 4105 ax-nul 4113 ax-pow 4158 ax-pr 4192 ax-un 4416 ax-setind 4519 ax-iinf 4570 ax-cnex 7854 ax-resscn 7855 ax-1cn 7856 ax-1re 7857 ax-icn 7858 ax-addcl 7859 ax-addrcl 7860 ax-mulcl 7861 ax-mulrcl 7862 ax-addcom 7863 ax-mulcom 7864 ax-addass 7865 ax-mulass 7866 ax-distr 7867 ax-i2m1 7868 ax-0lt1 7869 ax-1rid 7870 ax-0id 7871 ax-rnegex 7872 ax-precex 7873 ax-cnre 7874 ax-pre-ltirr 7875 ax-pre-ltwlin 7876 ax-pre-lttrn 7877 ax-pre-apti 7878 ax-pre-ltadd 7879 ax-pre-mulgt0 7880 ax-pre-mulext 7881 ax-arch 7882 ax-caucvg 7883 ax-pre-suploc 7884

This theorem depends on definitions: df-bi 116 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rmo 2456 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3526 df-pw 3566 df-sn 3587 df-pr 3588 df-op 3590 df-uni 3795 df-int 3830 df-iun 3873 df-br 3988 df-opab 4049 df-mpt 4050 df-tr 4086 df-id 4276 df-po 4279 df-iso 4280 df-iord 4349 df-on 4351 df-ilim 4352 df-suc 4354 df-iom 4573 df-xp 4615 df-rel 4616 df-cnv 4617 df-co 4618 df-dm 4619 df-rn 4620 df-res 4621 df-ima 4622 df-iota 5158 df-fun 5198 df-fn 5199 df-f 5200 df-f1 5201 df-fo 5202 df-f1o 5203 df-fv 5204 df-isom 5205 df-riota 5807 df-ov 5854 df-oprab 5855 df-mpo 5856 df-1st 6117 df-2nd 6118 df-recs 6282 df-frec 6368 df-sup 6958 df-inf 6959 df-pnf 7945 df-mnf 7946 df-xr 7947 df-ltxr 7948 df-le 7949 df-sub 8081 df-neg 8082 df-reap 8483 df-ap 8490 df-div 8579 df-inn 8868 df-2 8926 df-3 8927 df-4 8928 df-n0 9125 df-z 9202 df-uz 9477 df-rp 9600 df-icc 9841 df-seqfrec 10391 df-exp 10465 df-cj 10795 df-re 10796 df-im 10797 df-rsqrt 10951 df-abs 10952

This theorem is referenced by: dedekindicclemicc 13365

W3C validator