metakunt29 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > metakunt29		Structured version Visualization version GIF version

Theorem metakunt29 42214

Description: Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)

**Hypotheses**
Ref	Expression
metakunt29.1	⊢ (𝜑 → 𝑀 ∈ ℕ)
metakunt29.2	⊢ (𝜑 → 𝐼 ∈ ℕ)
metakunt29.3	⊢ (𝜑 → 𝐼 ≤ 𝑀)
metakunt29.4	⊢ (𝜑 → 𝑋 ∈ (1...𝑀))
metakunt29.5	⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))
metakunt29.6	⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))
metakunt29.7	⊢ (𝜑 → ¬ 𝑋 = 𝐼)
metakunt29.8	⊢ (𝜑 → 𝑋 < 𝐼)
metakunt29.9	⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))
metakunt29.10	⊢ 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)

**Assertion**
Ref	Expression
metakunt29	⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))

Distinct variable groups: 𝑦,𝐻 𝑦,𝐼 𝑧,𝐼 𝑥,𝑀 𝑦,𝑀 𝑧,𝑀 𝑥,𝑋 𝑦,𝑋 𝑧,𝑋 𝜑,𝑥 𝜑,𝑦 𝜑,𝑧 Allowed substitution hints: 𝐴(𝑥,𝑦,𝑧) 𝐵(𝑥,𝑦,𝑧) 𝐶(𝑥,𝑦,𝑧) 𝐻(𝑥,𝑧) 𝐼(𝑥)

**Proof of Theorem metakunt29**
Step	Hyp	Ref	Expression
1		metakunt29.1	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
2		metakunt29.2	. . . 4 ⊢ (𝜑 → 𝐼 ∈ ℕ)
3		metakunt29.3	. . . 4 ⊢ (𝜑 → 𝐼 ≤ 𝑀)
4		metakunt29.4	. . . 4 ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))
5		metakunt29.5	. . . 4 ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))
6		metakunt29.6	. . . 4 ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))
7		metakunt29.7	. . . 4 ⊢ (𝜑 → ¬ 𝑋 = 𝐼)
8		metakunt29.8	. . . 4 ⊢ (𝜑 → 𝑋 < 𝐼)
9	1, 2, 3, 4, 5, 6, 7, 8	metakunt27 42212	. . 3 ⊢ (𝜑 → (𝐵‘(𝐴‘𝑋)) = (𝑋 + (𝑀 − 𝐼)))
10	9	fveq2d 6910	. 2 ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = (𝐶‘(𝑋 + (𝑀 − 𝐼))))
11		metakunt29.9	. . . 4 ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))
12	11	a1i 11	. . 3 ⊢ (𝜑 → 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))))
13		elfznn 13589	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ)
14	4, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ℕ)
15		nnre 12270	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℕ → 𝑋 ∈ ℝ)
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
17	1	nnred 12278	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ)
18	2	nnred 12278	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℝ)
19	17, 18	resubcld 11688	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℝ)
20	16, 19	readdcld 11287	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℝ)
21	16	recnd 11286	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ℂ)
22	17	recnd 11286	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℂ)
23	18	recnd 11286	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℂ)
24	21, 22, 23	addsub12d 11640	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) = (𝑀 + (𝑋 − 𝐼)))
25	22, 23, 21	subsub2d 11646	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝐼 − 𝑋)) = (𝑀 + (𝑋 − 𝐼)))
26	18, 16	resubcld 11688	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼 − 𝑋) ∈ ℝ)
27	16, 18	posdifd 11847	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 < 𝐼 ↔ 0 < (𝐼 − 𝑋)))
28	8, 27	mpbid 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < (𝐼 − 𝑋))
29	26, 28	elrpd 13071	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼 − 𝑋) ∈ ℝ⁺)
30	17, 29	ltsubrpd 13106	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝐼 − 𝑋)) < 𝑀)
31	25, 30	eqbrtrrd 5171	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 + (𝑋 − 𝐼)) < 𝑀)
32	24, 31	eqbrtrd 5169	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) < 𝑀)
33	20, 32	ltned 11394	. . . . . . . 8 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀)
34	33	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀)
35		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
36	35	neeq1d 2997	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → (𝑦 ≠ 𝑀 ↔ (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀))
37	34, 36	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → 𝑦 ≠ 𝑀)
38	37	neneqd 2942	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → ¬ 𝑦 = 𝑀)
39	38	iffalsed 4541	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))
40		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
41	18	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ∈ ℝ)
42	16	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑋 ∈ ℝ)
43	17	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑀 ∈ ℝ)
44	43, 41	resubcld 11688	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑀 − 𝐼) ∈ ℝ)
45	42, 44	readdcld 11287	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) ∈ ℝ)
46	41, 45	lenltd 11404	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) ↔ ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
47	40, 46	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼)
48	47	3adant2 1130	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼)
49		simp2 1136	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
50	49	breq1d 5157	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 < 𝐼 ↔ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
51	50	notbid 318	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (¬ 𝑦 < 𝐼 ↔ ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
52	48, 51	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ 𝑦 < 𝐼)
53	52	iffalsed 4541	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = (𝑦 + 1))
54	49	oveq1d 7445	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 + 1) = ((𝑋 + (𝑀 − 𝐼)) + 1))
55	53, 54	eqtrd 2774	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 1))
56		simp3 1137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
57	56	iftrued 4538	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 1)
58	57	eqcomd 2740	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 1 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
59		metakunt29.10	. . . . . . . . 9 ⊢ 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)
60	58, 59	eqtr4di 2792	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 1 = 𝐻)
61	60	oveq2d 7446	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ((𝑋 + (𝑀 − 𝐼)) + 1) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
62	55, 61	eqtrd 2774	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
63	62	3expa 1117	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
64	20, 18	ltnled 11405	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) < 𝐼 ↔ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))))
65	64	biimprd 248	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) → (𝑋 + (𝑀 − 𝐼)) < 𝐼))
66	65	imp 406	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) < 𝐼)
67	66	3adant2 1130	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) < 𝐼)
68		simp2 1136	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
69	68	breq1d 5157	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 < 𝐼 ↔ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
70	67, 69	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 < 𝐼)
71	70	iftrued 4538	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = 𝑦)
72	21	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝑋 ∈ ℂ)
73	22	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝑀 ∈ ℂ)
74	23	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝐼 ∈ ℂ)
75	73, 74	subcld 11617	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑀 − 𝐼) ∈ ℂ)
76	72, 75	addcld 11277	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) ∈ ℂ)
77	76	addridd 11458	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ((𝑋 + (𝑀 − 𝐼)) + 0) = (𝑋 + (𝑀 − 𝐼)))
78	77	eqcomd 2740	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 0))
79	64	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
80	79	iffalsed 4541	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 0)
81	80	eqcomd 2740	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 0 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
82	59	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
83	82	eqcomd 2740	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 𝐻)
84	81, 83	eqtrd 2774	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 0 = 𝐻)
85	84	oveq2d 7446	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ((𝑋 + (𝑀 − 𝐼)) + 0) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
86	78, 85	eqtrd 2774	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
87	86	ex 412	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) < 𝐼 → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)))
88	65, 87	syld 47	. . . . . . . . . 10 ⊢ (𝜑 → (¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)))
89	88	imp 406	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
90	89	3adant2 1130	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
91	68, 90	eqtrd 2774	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
92	71, 91	eqtrd 2774	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
93	92	3expa 1117	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
94	63, 93	pm2.61dan 813	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
95	39, 94	eqtrd 2774	. . 3 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
96		1zzd 12645	. . . 4 ⊢ (𝜑 → 1 ∈ ℤ)
97	1	nnzd 12637	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℤ)
98	14	nnzd 12637	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℤ)
99	2	nnzd 12637	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
100	97, 99	zsubcld 12724	. . . . 5 ⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℤ)
101	98, 100	zaddcld 12723	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ)
102		1p0e1 12387	. . . . 5 ⊢ (1 + 0) = 1
103		1red 11259	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
104		0red 11261	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
105	14	nnge1d 12311	. . . . . 6 ⊢ (𝜑 → 1 ≤ 𝑋)
106	17, 18	subge0d 11850	. . . . . . 7 ⊢ (𝜑 → (0 ≤ (𝑀 − 𝐼) ↔ 𝐼 ≤ 𝑀))
107	3, 106	mpbird 257	. . . . . 6 ⊢ (𝜑 → 0 ≤ (𝑀 − 𝐼))
108	103, 104, 16, 19, 105, 107	le2addd 11879	. . . . 5 ⊢ (𝜑 → (1 + 0) ≤ (𝑋 + (𝑀 − 𝐼)))
109	102, 108	eqbrtrrid 5183	. . . 4 ⊢ (𝜑 → 1 ≤ (𝑋 + (𝑀 − 𝐼)))
110	20, 17, 32	ltled 11406	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ≤ 𝑀)
111	96, 97, 101, 109, 110	elfzd 13551	. . 3 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ (1...𝑀))
112	111	elfzelzd 13561	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ)
113		0zd 12622	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℤ)
114	96, 113	ifcld 4576	. . . . 5 ⊢ (𝜑 → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ)
115	59	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
116	115	eleq1d 2823	. . . . 5 ⊢ (𝜑 → (𝐻 ∈ ℤ ↔ if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ))
117	114, 116	mpbird 257	. . . 4 ⊢ (𝜑 → 𝐻 ∈ ℤ)
118	112, 117	zaddcld 12723	. . 3 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) + 𝐻) ∈ ℤ)
119	12, 95, 111, 118	fvmptd 7022	. 2 ⊢ (𝜑 → (𝐶‘(𝑋 + (𝑀 − 𝐼))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
120	10, 119	eqtrd 2774	1 ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1536 ∈ wcel 2105 ≠ wne 2937 ifcif 4530 class class class wbr 5147 ↦ cmpt 5230 ‘cfv 6562 (class class class)co 7430 ℂcc 11150 ℝcr 11151 0cc0 11152 1c1 11153 + caddc 11155 < clt 11292 ≤ cle 11293 − cmin 11489 ℕcn 12263 ℤcz 12610 ...cfz 13543

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 ax-cnex 11208 ax-resscn 11209 ax-1cn 11210 ax-icn 11211 ax-addcl 11212 ax-addrcl 11213 ax-mulcl 11214 ax-mulrcl 11215 ax-mulcom 11216 ax-addass 11217 ax-mulass 11218 ax-distr 11219 ax-i2m1 11220 ax-1ne0 11221 ax-1rid 11222 ax-rnegex 11223 ax-rrecex 11224 ax-cnre 11225 ax-pre-lttri 11226 ax-pre-lttrn 11227 ax-pre-ltadd 11228 ax-pre-mulgt0 11229

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-pss 3982 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-iun 4997 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5640 df-we 5642 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-pred 6322 df-ord 6388 df-on 6389 df-lim 6390 df-suc 6391 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-om 7887 df-1st 8012 df-2nd 8013 df-frecs 8304 df-wrecs 8335 df-recs 8409 df-rdg 8448 df-er 8743 df-en 8984 df-dom 8985 df-sdom 8986 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 df-sub 11491 df-neg 11492 df-nn 12264 df-n0 12524 df-z 12611 df-uz 12876 df-rp 13032 df-fz 13544

This theorem is referenced by: metakunt31 42216

W3C validator